Information Information Is Ledger Shannon Entropy Equals Expected Jcost

The entropy identity

Shannon entropy, introduced by Claude Shannon in 1948, measures the average surprise of a random event. For a set of outcomes with probabilities p₁, p₂, ..., pₙ, it is computed as -Σ pᵢ log pᵢ. A coin that always lands heads has entropy zero; a fair coin has entropy log 2. The quantity appears throughout information theory, thermodynamics, and machine learning, wherever one needs a single number for how much uncertainty a distribution contains.

The Recognition Science framework models physical facts as recognition events, each carrying a positive ratio x, and assigns each event a cost J(x) = (x + 1/x)/2 - 1. The cost is zero exactly when x = 1, positive otherwise, and symmetric under x → 1/x. The framework's machine-checked library of formal theorems proves that for any finite probability distribution, the Shannon entropy equals the average of these costs: shannon_entropy_equals_expected_jcost. The identity is a theorem in the library's InformationIsLedger module, derived from the definitions of entropy and cost.

This identity is not a numerical coincidence. It says the classical measure of information content and the framework's measure of recognition cost are the same function, up to the choice of logarithm base. The framework's interpretation is that information is not an abstract quantity but a property of a physical ledger of events; the entropy of a distribution is the expected cost of recognizing which event occurred. The theorem also yields classical facts: the uniform distribution has maximum entropy log n, and a deterministic distribution has entropy zero.

The identity does not claim that Shannon entropy is the only measure of information, nor that the framework's cost function is the only possible one. It does not assert that physical information is always stored in discrete events, nor that the ledger model applies to all forms of information. What it establishes is a precise, proved correspondence between two mathematical objects: the entropy of a probability distribution and the average recognition cost over the same distribution.

/-- **THEOREM IC-001.9**: Shannon entropy equals expected J-cost.
    H(X) = Σ p_i · J(p_i) = expected information cost.
    This proves our information measure is consistent with Shannon's. -/
theorem shannon_entropy_equals_expected_jcost {n : ℕ} (d : ShannonEntropy.ProbDist n) :
    ShannonEntropy.shannonEntropy d = ShannonEntropy.totalJCost d :=
  ShannonEntropy.shannon_equals_jcost d

/-- **THEOREM IC-001.12**: Maximum entropy occurs for the uniform distribution.
    Uniform = maximum uncertainty = maximum information cost. -/
theorem uniform_has_max_entropy (n : ℕ) (hn : n > 0) :
    ShannonEntropy.shannonEntropy (ShannonEntropy.uniform n hn) = Real.log n :=
  ShannonEntropy.max_entropy_uniform n hn

/-- **THEOREM IC-001.11**: The deterministic distribution (one outcome certain) has zero entropy.
    Perfect knowledge = zero information cost = balanced ledger. -/
theorem deterministic_has_zero_entropy {n : ℕ} (d : ShannonEntropy.ProbDist n) (i : Fin n)
    (hdet : d.probs i = 1) (hother : ∀ j ≠ i, d.probs j = 0) :
    ShannonEntropy.shannonEntropy d = 0 :=
  ShannonEntropy.zero_entropy_deterministic d i hdet hother

What this page does not claim

This does not claim that Shannon entropy is the only valid measure of information. This does not claim that all physical information is stored in discrete recognition events. This does not claim that the framework's cost function is the unique possible cost function, only that it satisfies the framework's axioms.

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/InformationIsLedger.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: