Information Shannon Entropy3 From Jcost Shannon Entr3 Cert

The certificate's scope

Shannon entropy, in the classical information theory introduced by Claude Shannon in 1948, measures the average surprise of a random source. For a distribution with probabilities p_i, it is H = -sum p_i log p_i. The quantity is zero when one outcome is certain, and it reaches its maximum when all outcomes are equally likely. That maximum is the entropy a source can achieve, and the gap between a source's actual entropy and this maximum is a natural measure of redundancy.

The Recognition Science framework models this gap with a cost function. Its cost, a penalty assigned to a recognition event, is built from a proved function J(x) = (x + 1/x)/2 - 1. The framework's library, a machine-checked collection of formal theorems, defines a domain cost as J applied to a ratio of two positive numbers, m over e. The declaration ShannonEntr3Cert packages three facts about this cost: it is zero when the ratio equals one, it is never negative for positive inputs, and a threshold value phi - 3/2 is positive. The certificate is a structure that bundles these three properties, and the library shows such a certificate exists.

In plain terms, the certificate says that the cost function behaves sensibly: matching values costs nothing, and no positive ratio produces a negative penalty. The third fact, that phi - 3/2 is positive, is a numerical inequality about the golden ratio phi, roughly 1.618, minus 1.5. These are general facts about the cost function J, not facts about any particular information source.

In Recognition Science, the connection to Shannon entropy is a research note, not a proved result. The note observes that H = sum p_i * J(p_i / p_uniform), a formula that rewrites entropy using the cost function. The certificate itself does not establish this formula, because the definition of domainCost never references probability distributions. What would turn the certificate into a theorem about entropy is a separate definition of m and e in terms of a source's probabilities, which the module does not supply.

The certificate's value is therefore narrow but real: it shows that the cost function has the basic properties any sensible penalty should have, and it does so with machine-checked rigor. The step from these properties to Shannon entropy remains a target for future work, not an achievement of this declaration.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

This answer does not claim the certificate proves the Shannon entropy formula H = sum p_i * J(p_i / p_uniform). This answer does not claim the certificate establishes any property of a specific information source. This answer does not claim the cost function J is the only function satisfying the certificate's three properties.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/ShannonEntropy3FromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: