Encyclopedia Holography Holography Gibbs Casini Bound

ARTICLE 4 claims 3 theorems 1 model

Holography Gibbs Casini Bound

A classical inequality about information and probability, proved in full generality, supplies the missing half of a famous entropy bound.

Verify this page

The Gibbs form of the bound

The Gibbs inequality is a classical result in information theory: for any two probability distributions over a finite set of outcomes, the Shannon entropy of one distribution never exceeds its cross-entropy against the other. In symbols, S(p) ≤ Σ pᵢ log(1/qᵢ). The inequality is unconditional, a theorem of pure mathematics. It says that you cannot pack more surprise into a message than the reference distribution you compare it against budgets for.

In the Recognition Science framework, this inequality is the engine behind a bound on entropy. The framework models reality as a discrete ledger, a finite record of recognition events on a seam alphabet. A state is a probability distribution over those records. The framework's library proves the Gibbs inequality from a single tangent-line fact, log x ≤ x − 1, summed over the finite alphabet. No measure theory, no operator algebra: finite sums suffice. The library also proves that if the reference distribution is a Gibbs state, one of the form qᵢ = exp(−β·Eᵢ), then its modular Hamiltonian prices each record linearly at β times its energy.

In Recognition Science, the module assembles these pieces into a Bekenstein bound for all states. Given that the reference is a Gibbs state, that its total weight is at most one, that the horizon rate κ equals 1/R, that β = 2π/κ, and that the delivered state's mean energy is within budget, the conclusion follows: S(p) ≤ 2πER. The 2π comes from the deficit-free period, a theorem; the inequality comes from Gibbs. The bound holds for every delivered state, not just the thermal one. The delivered state itself is never assumed to be thermal.

The framework's library proves this assembly as a theorem, but the premises carry named MODEL tags. The Gibbs form of the reference state is a premise, not a derivation. That the seam reference is thermal at the deficit-free period remains open work. The finite seam alphabet is the ledger's discreteness; the continuum version of Casini's argument is out of scope. The Gibbs inequality itself is unconditional, axiom-clean mathematics. The assembly is conditional on its named premises.

What this changes: the bound is no longer a bare postulate in the framework's capstone. It is a consequence of sharper named premises, with the 2π supplied by the period and the inequality by Gibbs. The remaining open question is exactly the thermality of the reference state, never of the delivered state.

THEOREM gibbs_inequality · IndisputableMonolith/Holography/GibbsCasiniBound.lean
gibbs_inequality · IndisputableMonolith/Holography/GibbsCasiniBound.lean:100 
/-- **Gibbs inequality.** For a probability vector `p` and a positive reference `q`
with `∑ q ≤ 1` (subnormalized allowed): `S(p) ≤ ⟨K_q⟩_p`. This is relative-entropy
positivity, the finite form of Casini's bound. The entire proof reduces to the
tangent-line bound `log x ≤ x − 1` applied per record at `x = q i / p i`. -/
theorem gibbs_inequality {n : ℕ} (p q : Fin n → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 < q i)
    (hp1 : ∑ i, p i = 1) (hq1 : ∑ i, q i ≤ 1) :
    shannonEntropy p ≤ crossEntropy p q := by
  -- Per-record tangent bound: p·(log q − log p) ≤ q − p.
  have key : ∀ i : Fin n, p i * (Real.log (q i) - Real.log (p i)) ≤ q i - p i := by
    intro i
    rcases eq_or_lt_of_le (hp i) with h0 | hpi
    · rw [← h0]
      simpa using (hq i).le
    · have hdiv : 0 < q i / p i := div_pos (hq i) hpi
      have hlog : Real.log (q i / p i) ≤ q i / p i - 1 :=
        Real.log_le_sub_one_of_pos hdiv
      have hlogdiv : Real.log (q i / p i) = Real.log (q i) - Real.log (p i) :=
        Real.log_div (ne_of_gt (hq i)) (ne_of_gt hpi)
      have hmul : p i * Real.log (q i / p i) ≤ p i * (q i / p i - 1) :=
        mul_le_mul_of_nonneg_left hlog hpi.le
      have hpne : p i ≠ 0 := ne_of_gt hpi
      have hpq : p i * (q i / p i) = q i := by
        field_simp
      have hcancel : p i * (q i / p i - 1) = q i - p i := by
        calc p i * (q i / p i - 1) = p i * (q i / p i) - p i := by ring
          _ = q i - p i := by rw [hpq]
      calc p i * (Real.log (q i) - Real.log (p i))
          = p i * Real.log (q i / p i) := by rw [hlogdiv]
        _ ≤ p i * (q i / p i - 1) := hmul
        _ = q i - p i := hcancel
  -- Sum the per-record bounds; the mass difference is ≤ 0.
  have hsum : ∑ i, p i * (Real.log (q i) - Real.log (p i)) ≤ ∑ i, (q i - p i) :=
    Finset.sum_le_sum fun i _ => key i
  have hmass : ∑ i, (q i - p i) ≤ 0 := by
    rw [Finset.sum_sub_distrib, hp1]
    linarith
  have hexpand : ∑ i, p i * (Real.log (q i) - Real.log (p i))
      = (∑ i, p i * Real.log (q i)) - ∑ i, p i * Real.log (p i) := by
    rw [← Finset.sum_sub_distrib]
    exact Finset.sum_congr rfl fun i _ => by ring
  have hdiff : (∑ i, p i * Real.log (q i)) - (∑ i, p i * Real.log (p i)) ≤ 0 := by
    rw [← hexpand]
    linarith
  simp only [shannonEntropy, crossEntropy, modularHamiltonian]
  have hneg : (∑ i, p i * -Real.log (q i)) = -(∑ i, p i * Real.log (q i)) := by
    simp [mul_neg]
  rw [hneg]
  linarith
THEOREM modularHamiltonian_of_gibbsReference · IndisputableMonolith/Holography/GibbsCasiniBound.lean
modularHamiltonian_of_gibbsReference · IndisputableMonolith/Holography/GibbsCasiniBound.lean:178 
/-- Modular pricing: the modular Hamiltonian of a period-`β` Gibbs reference prices
each record at `β` times its energy, `K_q i = β·En i`. -/
theorem modularHamiltonian_of_gibbsReference {n : ℕ} {q : Fin n → ℝ} {beta : ℝ}
    {En : Fin n → ℝ} (h : GibbsReference q beta En) (i : Fin n) :
    modularHamiltonian q i = beta * En i := by
  unfold modularHamiltonian
  rw [h i, Real.log_exp, neg_neg]
THEOREM bekenstein_bound_from_gibbs_reference · IndisputableMonolith/Holography/GibbsCasiniBound.lean
bekenstein_bound_from_gibbs_reference · IndisputableMonolith/Holography/GibbsCasiniBound.lean:188 
/-- **CONDITIONAL Bekenstein bound for ALL states.** Given the named premises
(`GibbsReference`: the seam reference is the period-β closure state;
`∑ q ≤ 1`: subnormalized reference; `HorizonRate`: `κ = 1/R` with `κ > 0`;
`β = 2π/κ` from the deficit-free period; `⟨En⟩_p ≤ E`: the delivered mean record
energy is within the seam budget), EVERY delivered record distribution `p` obeys
`S(p) ≤ 2πER`, i.e. `KeystoneFactorThree.TotalEntropyBekensteinBound`. The 2π comes
from `euclideanPeriod_isLeast`; the inequality from `gibbs_inequality`; nothing here
assumes the delivered state is thermal. -/
theorem bekenstein_bound_from_gibbs_reference {n : ℕ}
    (p q En : Fin n → ℝ) (beta kappa E R : ℝ)
    (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i = 1)
    (href : GibbsReference q beta En)
    (hq1 : ∑ i, q i ≤ 1)
    (hR : DeficitFreePeriod.HorizonRate kappa R) (hkappa : 0 < kappa)
    (hbeta : beta = DeficitFreePeriod.euclideanPeriod kappa)
    (hE : ∑ i, p i * En i ≤ E) :
    KeystoneFactorThree.TotalEntropyBekensteinBound (shannonEntropy p) E R := by
  have hq : ∀ i, 0 < q i := fun i => gibbsReference_pos href i
  have hgibbs := gibbs_inequality p q hp hq hp1 hq1
  have hR' : kappa = 1 / R := hR
  -- Cross entropy = β · mean record energy.
  have hcross : crossEntropy p q = beta * ∑ i, p i * En i := by
    simp only [crossEntropy]
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [modularHamiltonian_of_gibbsReference href i]
    ring
  -- κ = 1/R with κ > 0 forces R > 0, hence β = 2πR ≥ 0.
  have hRpos : 0 < R := by
    rcases lt_trichotomy R 0 with hneg | hzero | hpos
    · exfalso
      have h1 : 1 / R < 0 := div_neg_of_pos_of_neg one_pos hneg
      rw [hR'] at hkappa
      linarith
    · exfalso
      rw [hzero, div_zero] at hR'
      rw [hR'] at hkappa
      exact lt_irrefl 0 hkappa
    · exact hpos
  have hbetaR : beta = 2 * Real.pi * R := by
    rw [hbeta]
    simp only [DeficitFreePeriod.euclideanPeriod]
    rw [hR']
    field_simp
  have hbeta_nonneg : 0 ≤ beta := by
    rw [hbetaR]
    positivity
  show shannonEntropy p ≤ 2 * Real.pi * E * R
  calc shannonEntropy p ≤ crossEntropy p q := hgibbs
    _ = beta * ∑ i, p i * En i := hcross
    _ ≤ beta * E := mul_le_mul_of_nonneg_left hE hbeta_nonneg
    _ = 2 * Real.pi * E * R := by rw [hbetaR]; ring
MODEL GibbsReference · IndisputableMonolith/Holography/GibbsCasiniBound.lean
GibbsReference · IndisputableMonolith/Holography/GibbsCasiniBound.lean:165 
/-- Named MODEL premise (reference closure state): the seam reference is the
period-`β` Gibbs state over the record energies, `q i = exp(−β·En i)`. Deriving this
form (thermality of the REFERENCE at the deficit-free period) is the open B2/B3
physics; it is consumed here as a typed premise, never proved. -/
def GibbsReference {n : ℕ} (q : Fin n → ℝ) (beta : ℝ) (En : Fin n → ℝ) : Prop :=
  ∀ i, q i = Real.exp (-(beta * En i))

What this page does not claim

The Gibbs form of the reference state is derived, not assumed. The continuum type-III algebra version of Casini's argument is proved here. The delivered state is assumed to be thermal.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND