Information Shannon Entropy Entropy Is Expected Surprisal

Entropy as expected surprisal

Shannon entropy, written H = -Σ p_i log(p_i), measures the average amount of surprise, or information, in a random outcome. If an event is certain (probability 1), it carries no surprise; if it is rare (probability near 0), it carries a great deal. The formula multiplies each outcome's surprisal, -log(p_i), by its probability p_i and sums the results. This is the standard definition from Claude Shannon's 1948 information theory, and it underlies data compression, cryptography, and channel capacity.

In the Recognition Science framework, the same quantity emerges from a different starting point. The framework models recognition as a ledger, a discrete record of events, where each event carries a forced cost. Its cost function J(x) = ½(x + 1/x) - 1 measures the effort of recognizing a ratio x. Applied to probabilities, the framework defines a per-outcome cost as -log(p), which is exactly the surprisal. Summing over all outcomes with their probabilities gives the total cost, and a theorem in the framework's machine-checked library of formal theorems shows that this total equals Shannon entropy.

The declaration entropy_is_expected_surprisal is a formal restatement of this identity. It establishes, for any finite probability distribution, that the Shannon entropy equals the expected value of the surprisal function. The proof is direct: it unfolds the definitions and shows both sides are the same sum of p times -log(p) for positive probabilities, with zero terms for zero probabilities. This is not a new physical law; it is a formal confirmation that the framework's cost-based definition reproduces the classical quantity exactly.

The framework also establishes standard consequences: entropy is always non-negative, a deterministic outcome has zero entropy, and the uniform distribution has maximum entropy, equal to log(n) for n outcomes. These match the classical properties of Shannon entropy. The framework labels the Shannon coding theorem and the thermodynamic connection as targets for future formalization, not as established results in this file.

What the declaration does not claim is more important than what it does. It does not derive entropy from first principles; it takes the standard definition and shows the framework's cost model agrees with it. It does not establish the source coding theorem, which states that optimal code length cannot beat entropy, nor does it establish the thermodynamic relation S = k_B × H. Those remain open in this file. The declaration is a bridge, not a foundation: it shows that a cost-based account of recognition lands on the same mathematical object as Shannon's information measure.

/-- **THEOREM**: Entropy is expected surprisal. -/
theorem entropy_is_expected_surprisal {n : ℕ} (d : ProbDist n) :
    shannonEntropy d = Finset.univ.sum fun i =>
      if h : d.probs i > 0 then d.probs i * surprisal (d.probs i) h
      else 0 := by
  -- H = E[I(X)] = Σ p_i × surprisal(p_i)
  -- This is just a restatement via the definitions
  rw [shannon_equals_jcost]
  unfold totalJCost probJCost surprisal
  -- Both are Σ if p>0 then p*(-log p) else 0
  rfl

/-- **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 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]

/-- **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

What this page does not claim

The declaration does not establish the source coding theorem or the thermodynamic relation S = k_B × H. It does not derive Shannon entropy from first principles; it shows agreement with the standard definition. The result does not establish that the framework's cost model is the unique source of information measures.

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: