Encyclopedia Holography Holography Gibbs Casini Bound Gibbs Inequality

ARTICLE 4 claims 4 theorems

Holography Gibbs Casini Bound Gibbs Inequality

The Gibbs inequality says the entropy of a distribution never exceeds its cross-entropy against any reference. Recognition Science's machine-checked library proves it for finite alphabets and shows how it becomes a general bound on entropy.

Verify this page

The Gibbs inequality

The Gibbs inequality is a classical result in information theory and statistical mechanics. It says that for any probability distribution p and any positive reference distribution q, the cost of encoding p using q is at least the entropy of p. In symbols: S(p) ≤ ⟨K_q⟩_p, where K_q(i) = −log(q(i)). Equivalently, the relative entropy between p and q is never negative. This is a fundamental convexity property of the logarithm, and it underpins the second law of thermodynamics and much of statistical inference.

The inequality holds for any finite alphabet of outcomes. The proof is a one-line application of the tangent-line bound log(x) ≤ x − 1, summed over all outcomes. The reference q need not be normalized; it can be subnormalized (sum ≤ 1), which only strengthens the bound. This is the finite, discrete version of the bound that Casini used to prove the Bekenstein bound for all states in quantum field theory, not just thermal ones.

In Recognition Science, the machine-checked library of formal theorems proves this inequality unconditionally for finite distributions. The declaration gibbs_inequality states: for a probability vector p and a positive vector q with sum ≤ 1, the Shannon entropy of p is at most the cross-entropy of p against q. The proof is the per-record tangent bound summed over the finite alphabet. This is pure mathematics, with no physics assumptions and no measure theory; finite sums suffice.

The framework then assembles this inequality into a conditional Bekenstein bound. If the reference q is a Gibbs state at inverse temperature β, meaning q(i) = exp(−β·En(i)) for record energies En, then the modular Hamiltonian prices records linearly: K_q(i) = β·En(i). Given also a horizon rate κ = 1/R, the Euclidean period β = 2π/κ, and a mean energy budget ⟨En⟩_p ≤ E, the theorem concludes that the entropy of any delivered state p satisfies S(p) ≤ 2πER. This is the Bekenstein bound for all states, not just the thermal one.

What the Gibbs inequality itself does not claim is equally important. It does not claim that any physical reference state is actually Gibbs-form; that thermality of the reference is a separate MODEL premise, not a theorem. It does not claim the horizon rate κ = 1/R is derived; that remains a named premise. And it does not address the continuum, type-III algebra version of Casini's argument; the finite seam alphabet is the ledger's discreteness, and the continuum case is out of scope. The Gibbs inequality is unconditional mathematics; the assembled Bekenstein bound is conditional on those named physical premises.

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

What this page does not claim

The Gibbs inequality does not claim that any physical reference state is actually Gibbs-form; thermality of the reference remains a MODEL premise. The assembled Bekenstein bound does not claim the horizon rate κ = 1/R is derived; it is a named premise. The finite-alphabet result does not claim to cover the continuum, type-III algebra version of Casini's argument.

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