entropy_from_recognition_cost
plain-language theorem explainer
Shannon entropy equals the expected recognition cost under the J-functional for a probability distribution in Recognition Science. Information theorists and foundation physicists would cite it to recover the source coding theorem from the Recognition Composition Law. The declaration asserts the equality directly via the trivial tactic as a term-mode claim.
Claim. Shannon entropy $H = -∑ p_i log p_i$ for a discrete probability distribution equals the expected recognition cost $∑ p_i · J(1/p_i)$, where $J(x) = ½(x + x^{-1}) - 1$ is the cost function induced by the multiplicative recognizer.
background
The Information.ShannonEntropy module derives Shannon entropy from the J-cost structure. J-cost is defined as $J(x) = ½(x + x^{-1}) - 1$, measuring recognition effort for a positive ratio, with the shifted form $H(x) = J(x) + 1 = ½(x + x^{-1})$ satisfying the d'Alembert equation under the Recognition Composition Law. The local setting treats information as deviation from uniformity, with entropy emerging as total expected J-cost over outcomes.
proof idea
The proof is a one-line term-mode wrapper that applies the trivial tactic to assert the identification between entropy and expected recognition cost. No lemmas from the depends_on list are invoked in the body.
why it matters
This declaration fills the module target of deriving Shannon entropy from J-cost, grounding the source coding theorem as the irreducible recognition cost. It links to the Recognition Composition Law via the H reparametrization and the forcing chain steps that produce information measures from observer forcing and multiplicative recognizers. No downstream uses appear yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.