Encyclopedia Holography Holography Gibbs Casini Bound Gibbs Casini Cert Holds

ARTICLE 3 claims 2 theorems 1 model

Holography Gibbs Casini Bound Gibbs Casini Cert Holds

A machine-checked certificate proves that entropy never exceeds a certain kind of average, a finite and exact version of a famous physics bound.

Verify this page

The certificate

The Gibbs inequality is a classical result in information theory and statistical mechanics: for any probability distribution p and any positive reference distribution q, the entropy of p is at most the cross-entropy of p against q. In symbols, S(p) ≤ Σ p(i) log(1/q(i)). The inequality says that using the wrong distribution q costs you at least the entropy you would have paid with the right one. It is the mathematical core of many derivations in physics, because relative entropy, the gap between the two sides, is never negative.

The Recognition Science framework's machine-checked library of formal theorems contains a certificate named gibbsCasiniCert_holds. The certificate states, in full generality, that the Gibbs inequality holds for every finite set of possible records, every probability vector p, and every positive reference vector q whose entries sum to at most one. The proof is unconditional and axiom-clean: it reduces to the tangent-line bound log x ≤ x − 1 applied to each record individually, summed over the finite alphabet. No measure theory, no operator algebra, and no framework-specific axioms are needed; finite sums suffice. The certificate is a theorem, not a model or a hypothesis.

In Recognition Science, this certificate is the mathematical half of a larger claim about ledgers, discrete records of events. The framework models a horizon as a finite seam alphabet of records, and it aims to prove a Bekenstein-type bound: the entropy of any state is at most 2π times its energy times the horizon radius. The certificate supplies the inequality S(p) ≤ Σ p(i) β E(i) when the reference is a Gibbs state q(i) = exp(−β E(i)), because then the modular Hamiltonian prices each record linearly at β times its energy. The 2π factor comes from a separate theorem about the deficit-free period, and the assembly yields the bound for every delivered state, not just the thermal one.

What the certificate does not claim is just as important. It does not prove that the reference state is thermal; that is a named model premise, the GibbsReference hypothesis, which the framework consumes as an assumption and does not derive. It does not prove the surface-gravity normalization κ = 1/R, another named premise. And it does not address the continuum, type-III algebra version of Casini's argument; the certificate lives entirely in the finite setting. The Gibbs inequality itself is unconditional mathematics, but the assembled Bekenstein bound inherits the weakest link: it is conditional on those model premises. The certificate is a real proof, and its scope is exactly what its hypotheses name.

THEOREM gibbsCasiniCert_holds · gibbs_inequality · IndisputableMonolith/Holography/GibbsCasiniBound.lean
gibbsCasiniCert_holds · IndisputableMonolith/Holography/GibbsCasiniBound.lean:287 
theorem gibbsCasiniCert_holds : gibbsCasiniCert :=
  fun _ p q hp hq hp1 hq1 => gibbs_inequality p q hp hq hp1 hq1
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
MODEL 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 certificate does not prove that any reference state is thermal; GibbsReference is a model premise, not a theorem. The certificate does not derive the surface-gravity normalization κ = 1/R. The certificate does not 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