Information Shannon Entropy

Information as a cost

Shannon entropy, written H = -Σ p_i log(p_i), quantifies the average surprise or information content of a random variable. It is the fundamental limit of lossless data compression: no uniquely decodable code can have an average length shorter than H. It also measures uncertainty, with the maximum value log(n) achieved by the uniform distribution over n outcomes, and a deterministic event carrying zero entropy. Claude Shannon introduced the formula in 1948, and it now underpins thermodynamics, quantum information, and coding theory.

In Recognition Science, the framework models information as a recognition cost, a discrete ledger of the effort required to distinguish one outcome from another. The core cost function J(x) = (x + 1/x)/2 - 1 measures this effort, and when applied to probability ratios, the framework proves that the total expected cost equals Shannon entropy. The theorem shannon_equals_jcost establishes this identity for any finite probability distribution, meaning the classical measure of information is exactly the average recognition effort in this account.

The framework's library, a machine-checked collection of formal theorems, also proves the standard properties: entropy is nonnegative, uniform distributions maximize it, and deterministic outcomes give zero. It defines surprisal as -log(p), the information content of a single outcome, and shows entropy is the expected surprisal. The module includes falsifiers, such as the impossibility of compressing below entropy, and connects to thermodynamic entropy through Boltzmann's constant.

What this establishes in plain language: the familiar formula for information is not an arbitrary definition but a forced consequence of how recognition costs compound. The framework derives Shannon entropy from a single cost function, rather than postulating it. It also provides a unified view: the same cost structure that forces physical constants in the framework also yields the measure of information.

The payoff is a bridge between information theory and the framework's broader claims. If recognition costs are fundamental, then entropy is not just a mathematical convenience but a physical quantity tied to the effort of observation. The module makes precise that connection, proving the identity and its classical properties within a single formal system.

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

/-- Information content (surprisal) of an outcome.
    I(x) = -log(p(x)) = "how surprising is this outcome?" -/
noncomputable def surprisal (p : ℝ) (hp : p > 0) : ℝ := -Real.log p

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

What this page does not claim

The module does not prove Shannon's source coding theorem; it only states it as a comment. The framework does not derive the fine-structure constant or other specific physical constants from this entropy result. The identity holds for finite probability distributions, not necessarily for continuous or infinite cases.

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: