Information Shannon Entropy Shannon Equals Jcost

The equality

Shannon entropy, written H = -Σ p_i log(p_i), is the foundational measure of information in communication theory. It quantifies the average number of bits needed to describe outcomes of a random process, the uncertainty before an outcome is known, and the limit of lossless compression. Introduced by Claude Shannon in 1948, it is a classical object with a standard definition and a long list of proven properties, including nonnegativity and its maximum at the uniform distribution.

Within the Recognition Science framework, the declaration shannon_equals_jcost establishes that this classical entropy equals a quantity the framework calls total J-cost. The framework models recognition as a ledger: a discrete record of events where each event carries a forced cost. The total J-cost of a probability distribution is the sum over outcomes of the probability times a per-outcome cost, where that per-outcome cost is defined as -log(p). Since the classical Shannon entropy is defined as exactly that same sum, the theorem is a formal identity: the framework's cost model reproduces the standard information measure.

The theorem is proved in a machine-checked library of formal theorems. It does not derive Shannon entropy from the framework's cost function J(x) = ½(x + 1/x) - 1; the per-outcome cost in the definition is simply -log(p), not J(p). The declaration shows that the framework's total cost, as defined, coincides with Shannon entropy, not that Shannon entropy emerges from the framework's more distinctive cost function. The framework's own documentation describes a derivation from J-cost over probability ratios, but the formal statement itself does not contain that derivation.

What the theorem does not claim is equally specific. It does not claim that the framework's J-cost function is the source of Shannon entropy; the equality is a definitional match, not a derivation. It does not claim any new physical law or any empirical prediction about information. The theorem is a formal statement about two definitions within a particular formal system. The framework's broader ambitions, such as deriving thermodynamic entropy or black hole entropy from its principles, are not established by this declaration and remain targets, not results.

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

/-- The J-cost of a probability (relative to uniform).
    For p ∈ (0,1], this measures how "surprising" the probability is. -/
noncomputable def probJCost (p : ℝ) (hp : p > 0) (hp1 : p ≤ 1) : ℝ :=
  -Real.log p

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

What this page does not claim

The theorem does not derive Shannon entropy from the framework's J-cost function; it equates two definitions. The theorem does not establish any new physical law or empirical prediction about information. The framework's broader ambitions, such as deriving thermodynamic entropy, are not proved by this declaration.

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: