Information Shannon Entropy Entropy Nonneg

Entropy is never negative

Shannon entropy, named for Claude Shannon's 1948 work, measures the average amount of surprise or information in a set of possible outcomes. For a probability distribution where outcome i occurs with probability p_i, the entropy is H = -Σ p_i log(p_i). It answers a practical question: how many bits, on average, do you need to describe which outcome happened? A coin flip has 1 bit of entropy; a sure thing has 0.

The entropy can never be negative. Each term -p log(p) is zero when p is 0 or 1, and positive for any probability strictly between them, because log(p) is negative for p less than 1. Summing these non-negative terms gives a non-negative total. This is a classical fact, known since Shannon's original work, and it is what the framework's entropy_nonneg theorem states: for any finite probability distribution, the Shannon entropy is greater than or equal to zero.

In Recognition Science, the framework models information through a recognition cost, a measure of how much effort it takes to distinguish an outcome from its alternatives. The framework's library, a machine-checked collection of formal theorems, defines Shannon entropy exactly as the classical formula above, then proves entropy_nonneg as a direct consequence of that definition. The proof is not a deep insight; it is a formal confirmation that the standard definition behaves as expected.

The theorem also connects to the framework's broader claim that information is a kind of deviation from uniformity. The uniform distribution, where every outcome is equally likely, has the maximum possible entropy, log(n) for n outcomes. Any other distribution is more predictable and has lower, but still non-negative, entropy. This matches the everyday intuition that a biased coin carries less information than a fair one.

What entropy_nonneg does not claim is more interesting than what it proves. It does not claim that the framework derives Shannon entropy from first principles; the definition is taken as given. It does not claim that entropy is always positive, only non-negative, and it says nothing about whether a particular distribution is realistic or optimal. The theorem is a small, solid brick in a larger structure, not the structure itself.

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

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

What this page does not claim

The framework derives Shannon entropy from first principles; it defines it directly. The theorem proves entropy is always positive, only that it is non-negative. The framework claims anything about the physical reality of information beyond its mathematical model.

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: