Information Shannon Entropy Thermodynamic Entropy Connection

The declared connection

Shannon entropy, introduced by Claude Shannon in 1948, quantifies the information content or uncertainty of a probability distribution. For a set of outcomes with probabilities p_i, it is H = -Σ p_i log(p_i), measured in bits when the logarithm is base 2. It answers a practical question: how many bits, on average, are needed to encode messages from a source? The uniform distribution, where all outcomes are equally likely, has the highest entropy; a deterministic outcome has zero entropy.

Thermodynamic entropy, by contrast, is a physical quantity from 19th-century thermodynamics. It measures the number of microscopic states consistent with a macroscopic system, or informally, the disorder or spread of energy. The two entropies were linked by Ludwig Boltzmann's formula S = k_B × log(W), where k_B is the Boltzmann constant (approximately 1.38 × 10⁻²³ J/K). This formula appears on Boltzmann's tombstone in Vienna.

The Recognition Science library contains a declaration named thermodynamic_entropy_connection. Its stated content is the equation S_thermo = k_B × S_shannon, for an appropriate interpretation. The declaration is a theorem in the machine-checked library, but the theorem's body is the trivial proposition True. In other words, the library asserts the connection as a statement of intent, not as a derived result. The library also defines boltzmannFactor as 1.38e-23 J/K, matching the accepted value of the Boltzmann constant.

What the library does prove, in the same file, is a separate and substantial result: Shannon entropy equals the total J-cost of a probability distribution. Here J-cost is the framework's concept of recognition effort, defined by J(x) = ½(x + 1/x) - 1. For a probability p, the per-outcome cost is -log(p), and the total cost is the expected value of that surprisal. The theorem shannon_equals_jcost states this equality for any finite probability distribution. This is a genuine mathematical identity, proved in the library.

In Recognition Science, this identity is the bridge: Shannon entropy is not a separate concept but a special case of recognition cost. The thermodynamic connection, however, is not derived from J-cost in the library. It is declared as a target, with a comment that it holds for an appropriate interpretation. The library's own list of potential falsifiers includes an entry that thermodynamic and information entropy agree, but that entry is a status report, not a proof.

What the declaration does not claim is equally important. It does not claim that thermodynamic entropy has been derived from first principles within the framework. It does not claim that the Boltzmann constant emerges from the framework's constants. It does not claim that the connection holds for all physical systems without qualification. The declaration is a placeholder for a future derivation, not a completed one.

theorem thermodynamic_entropy_connection :
    -- S_thermo = k_B × S_shannon (for appropriate interpretation)
    True := trivial

theorem thermodynamic_entropy_connection :
    -- S_thermo = k_B × S_shannon (for appropriate interpretation)
    True := trivial

/-- The connection between thermodynamic entropy and Shannon entropy.
    Boltzmann: S = k_B log(W) = k_B × H for uniform distribution. -/
noncomputable def boltzmannFactor : ℝ := 1.38e-23  -- J/K

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

What this page does not claim

The thermodynamic connection is not derived from J-cost; it is declared as a target. The Boltzmann constant is not derived; it is defined as a numerical value. The connection does not hold for all physical systems without an appropriate interpretation.

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: