Information Shannon Entropy Entropy From Recognition Cost

The ledger of surprise

Shannon entropy is the standard measure of information in a message. For a set of possible outcomes with probabilities p₁, p₂, ..., pₙ, it is defined as H = −Σ pᵢ log(pᵢ). It quantifies uncertainty, the fundamental limit on lossless compression, and the capacity of a communication channel. A fair coin toss has entropy log(2), meaning it requires one bit to describe; a biased coin that always lands heads has entropy zero, meaning no information is conveyed.

The definition has a natural interpretation. Each outcome with probability p carries a surprisal of −log(p): the less likely the event, the more surprising it is. Entropy is the expected surprisal, the average surprise you should anticipate before observing the outcome. This view is standard information theory, and it leads directly to the famous properties: entropy is always non-negative, it is maximized by the uniform distribution where every outcome is equally likely, and it is zero for a deterministic outcome. Claude Shannon introduced this measure in his 1948 paper "A Mathematical Theory of Communication," which founded the field.

In Recognition Science, the framework models recognition as a ledger, a discrete record of events where each event has a forced cost. The framework's central cost function is J(x) = ½(x + 1/x) − 1, which measures the effort of recognizing a ratio x. Applied to probability ratios, this cost becomes exactly the surprisal: for a probability p, the recognition cost is −log(p). The framework's machine-checked library of formal theorems proves that Shannon entropy equals the total recognition cost over a probability distribution: shannon_equals_jcost. It also proves that this total cost is non-negative, that it is maximized by the uniform distribution, and that it is zero for a deterministic outcome. These are not new empirical discoveries; they are formal restatements of Shannon's own results in the framework's language.

What the declaration entropy_from_recognition_cost itself establishes is more modest. In the library, it is a theorem whose statement is simply True, with a comment noting that entropy equals expected recognition cost and that optimal code length approximates −log(p). It is a placeholder, a marker for a derivation that the framework intends to complete, not a proof that the derivation has been finished. The library does prove the equality shannon_equals_jcost, which is the substantive mathematical content. The placeholder theorem records the intended interpretation, not a new result.

The framework's contribution here is a reinterpretation, not a new law of physics. It says that the surprisal, a concept from information theory, can be seen as a recognition cost in its own ledger. This is a definitional choice that connects two fields, but it does not change what entropy is or how it behaves. The theorems in the library are consistent with Shannon's work; they do not extend it. The framework's hope is that this cost-based view will generalize, but that generalization remains a target, not an achievement.

/-- Shannon entropy: H = -Σ p_i log(p_i).
    We use natural logarithm; for bits, divide by log(2). -/
noncomputable def shannonEntropy {n : ℕ} (d : ProbDist n) : ℝ :=
  -(Finset.univ.sum fun i =>
    if d.probs i > 0 then d.probs i * Real.log (d.probs i)
    else 0)

/-- **THEOREM (Shannon = J-Cost)**: Shannon entropy equals total J-cost.
    This is the key connection! -/
theorem shannon_equals_jcost {n : ℕ} (d : ProbDist n) :
    shannonEntropy d = totalJCost d := by
  -- Both compute Σ p_i × (-log p_i), just with different notation
  -- shannonEntropy = -(Σ p*log(p)) and totalJCost = Σ p*(-log(p))
  -- These are equal since -(p*log(p)) = p*(-log(p))
  unfold shannonEntropy totalJCost probJCost
  -- Goal: -(Σ if p>0 then p*log(p) else 0) = Σ if p>0 then p*(-log(p)) else 0
  conv_lhs =>
    rw [← Finset.sum_neg_distrib]
  congr 1
  funext i
  by_cases hp : d.probs i > 0
  · simp only [hp, ↓reduceIte, dite_eq_ite, neg_mul, mul_neg, neg_neg]
  · simp only [hp, ↓reduceIte, dite_eq_ite, neg_zero]

/-- **THEOREM**: Entropy is non-negative. -/
theorem entropy_nonneg {n : ℕ} (d : ProbDist n) :
    shannonEntropy d ≥ 0 := by
  unfold shannonEntropy
  simp only [neg_nonneg]
  apply Finset.sum_nonpos
  intro i _
  by_cases h : d.probs i > 0
  · simp only [h, ↓reduceIte]
    have hp : d.probs i ≤ 1 := by
      have := d.normalized
      have hs := Finset.single_le_sum (fun j _ => d.nonneg j) (Finset.mem_univ i)
      simp at hs
      linarith
    have hlog : Real.log (d.probs i) ≤ 0 := Real.log_nonpos (le_of_lt h) hp
    -- p * log(p) ≤ 0 for 0 < p ≤ 1
    apply mul_nonpos_of_nonneg_of_nonpos (le_of_lt h) hlog
  · simp [h]

/-- **THEOREM**: Maximum entropy is log(n) for uniform distribution. -/
theorem max_entropy_uniform (n : ℕ) (hn : n > 0) :
    shannonEntropy (uniform n hn) = Real.log n := by
  -- H = -n × (1/n) × log(1/n) = -log(1/n) = log(n)
  unfold shannonEntropy uniform
  simp only
  have hn_pos : (0 : ℝ) < n := Nat.cast_pos.mpr hn
  have hn_ne : (n : ℝ) ≠ 0 := ne_of_gt hn_pos
  have h_prob_pos : (1 : ℝ) / n > 0 := by positivity
  simp only [h_prob_pos, ↓reduceIte, Finset.sum_const, Finset.card_fin, nsmul_eq_mul]
  -- Goal: -(n * (1/n * log(1/n))) = log(n)
  have h_log : Real.log (1 / n) = -Real.log n := by
    rw [Real.log_div (by norm_num : (1 : ℝ) ≠ 0) hn_ne, Real.log_one, zero_sub]
  rw [h_log]
  have h_simp : (n : ℝ) * (1 / n * -Real.log n) = -Real.log n := by
    field_simp
  rw [h_simp]
  ring

/-- **THEOREM**: Entropy is 0 for deterministic distribution. -/
theorem zero_entropy_deterministic {n : ℕ} (d : ProbDist n) (i : Fin n)
    (hdet : d.probs i = 1) (hother : ∀ j ≠ i, d.probs j = 0) :
    shannonEntropy d = 0 := by
  unfold shannonEntropy
  simp only [neg_eq_zero]
  apply Finset.sum_eq_zero
  intro j _
  by_cases heq : j = i
  · simp [heq, hdet, Real.log_one]
  · simp [hother j heq]

/-- In RS, Shannon entropy measures **recognition cost**:

    1. Each outcome has a recognition cost proportional to -log(p)
    2. Rare outcomes cost more to "recognize" (encode)
    3. Total expected cost is Σ p_i × (-log p_i) = entropy
    4. Optimal encoding minimizes expected recognition cost

    This explains why entropy is the fundamental limit! -/
theorem entropy_from_recognition_cost :
    -- Entropy = expected recognition cost
    -- Optimal code length ≈ -log(p) (Shannon coding theorem)
    True := trivial

What this page does not claim

The framework does not prove the source coding theorem; the declaration source_coding_theorem is also a placeholder with statement True. The framework does not derive the thermodynamic entropy connection; thermodynamic_entropy_connection is likewise a placeholder. The equality shannon_equals_jcost is a formal restatement of Shannon's definition, not a new physical law.

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