Information Shannon Entropy Zero Entropy Deterministic

Zero entropy for a certain outcome

Shannon entropy, written H = -Σ p_i log(p_i), measures the uncertainty of a probability distribution. It is zero when there is no uncertainty at all: one outcome has probability 1 and every other outcome has probability 0. The machine-checked library of formal theorems in the Recognition Science framework contains a proof of exactly this fact, under the name zero_entropy_deterministic. The proof is a direct calculation from the definition of Shannon entropy: the term for the certain outcome contributes -1·log(1), which is 0, and every other term is multiplied by a zero probability, so the whole sum vanishes.

The same library also proves two neighboring facts. The entropy of any distribution is non-negative, and the uniform distribution, where every outcome has probability 1/n, has the maximum possible entropy, namely log(n). These three results together give the classical picture: entropy ranges from 0 for a deterministic outcome to log(n) for complete uniformity. The proof of zero_entropy_deterministic is a theorem in the library, meaning it is checked by the machine and requires no additional assumptions beyond the standard axioms of the underlying logic.

In Recognition Science, the framework models information cost through a function J(x) = ½(x + 1/x) - 1, and its library proves that Shannon entropy equals the total expected J-cost over a probability distribution. The zero-entropy theorem is the limiting case: when one outcome is certain, the expected recognition cost is also zero. This connection is a derivation within the framework, not an empirical claim about the world.

The declaration does not claim that any physical process actually achieves zero entropy, nor that the framework's cost function is the only way to derive Shannon entropy. It establishes a mathematical identity for a probability distribution with a certain outcome. The theorem's scope is exactly the definition: if one probability is 1 and the rest are 0, the entropy formula evaluates to 0. Nothing in the proof addresses whether such distributions occur in nature, only what the formula gives when they do.

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

What this page does not claim

No claim that zero entropy is physically achievable in any real system. No claim that the J-cost derivation is the unique or only way to obtain Shannon entropy. No claim that the theorem applies to continuous distributions; it is stated for finite probability distributions only.

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: