Holography Gibbs Casini Bound Shannon Entropy Uniform Two

A concrete entropy value

Shannon entropy measures the uncertainty of a probability distribution, in natural units called nats. For a system with two equally likely outcomes, each with probability 1/2, the entropy is the natural logarithm of 2, written log 2, which is about 0.693. This is a standard fact in information theory, and it is the specific content of the recognition framework's declaration shannonEntropy_uniform_two: a machine-checked theorem stating that the entropy of the uniform distribution on two records equals log 2.

The declaration is not a physical claim on its own. It is a non-vacuity exhibit, a proof that the entropy functional in the framework's ledger (a discrete record of events) is not identically zero. Before this theorem, one might worry that the framework's definition of entropy always produced zero, which would make any entropy-based bound trivial. This theorem shows that a concrete, two-record system has positive entropy, so the bound it feeds into is a real constraint.

The theorem lives inside a larger project that assembles a version of the Bekenstein bound, an inequality from gravitational physics linking entropy, energy, and size. The framework's library proves a Gibbs inequality, a finite form of a bound due to Casini, which states that the entropy of any state is at most its cross-entropy against a reference state. The uniform two-record value is used as a witness that the assembled bound can be saturated, meaning the inequality is sharp and not merely a loose upper limit.

In Recognition Science, the framework models physical states as distributions over a finite set of records, and this theorem is a small, fully proved step in that modeling. It establishes a concrete number, log 2, for the simplest nontrivial case. It does not claim that physical systems are actually two-state, nor that real black holes have entropy log 2. It does not derive the Bekenstein bound itself; that derivation requires additional modeling premises about the reference state and the horizon rate, which are named and left open.

/-- The uniform two-record distribution has entropy `log 2 > 0`: the entropy
functional is not identically zero, so the bound is a real constraint. -/
theorem shannonEntropy_uniform_two :
    shannonEntropy (fun _ : Fin 2 => (1 : ℝ) / 2) = Real.log 2 := by
  have hlog : Real.log ((1 : ℝ) / 2) = -Real.log 2 := by
    rw [one_div, Real.log_inv]
  simp only [shannonEntropy, Fin.sum_univ_two, hlog]
  ring

/-- The uniform two-record distribution has entropy `log 2 > 0`: the entropy
functional is not identically zero, so the bound is a real constraint. -/
theorem shannonEntropy_uniform_two :
    shannonEntropy (fun _ : Fin 2 => (1 : ℝ) / 2) = Real.log 2 := by
  have hlog : Real.log ((1 : ℝ) / 2) = -Real.log 2 := by
    rw [one_div, Real.log_inv]
  simp only [shannonEntropy, Fin.sum_univ_two, hlog]
  ring

What this page does not claim

This theorem does not claim that any physical system has exactly two states. It does not derive the Bekenstein bound; that requires additional modeling premises. It does not claim the entropy of a real black hole equals log 2.

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/Holography/GibbsCasiniBound.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: