Encyclopedia Holography Holography Gibbs Casini Bound Bekenstein Bound From Gibbs Reference

ARTICLE 4 claims 4 theorems

Holography Gibbs Casini Bound Bekenstein Bound From Gibbs Reference

A machine-checked theorem shows that a simple inequality from information theory, applied to a thermal reference state, yields the Bekenstein entropy bound for every state in a finite model.

Verify this page

The assembled bound

The Bekenstein bound is a physics conjecture that the entropy of any physical system fits inside a sphere of radius R and energy E cannot exceed 2πER. In the Recognition Science framework, this bound is not taken as an axiom. Its library of formal theorems derives it from a much older and simpler fact: the Gibbs inequality, which says that the entropy of a probability distribution is at most its cross-entropy against any other positive reference distribution.

The Gibbs inequality itself is unconditional mathematics, proved in the library from the tangent-line bound log x ≤ x − 1. For any probability vector p and any positive reference q with total weight at most 1, the entropy S(p) is at most the cross-entropy ⟨K_q⟩_p, where K_q i = −log(q i) is the modular Hamiltonian. This is the finite, discrete form of Casini's relative-entropy argument, which resolves the Bekenstein bound in continuum quantum field theory.

What the declaration bekenstein_bound_from_gibbs_reference adds is the assembly. If the reference state q is a Gibbs state at inverse temperature β over record energies En, so q i = exp(−β·En i), then its modular Hamiltonian prices each record linearly: K_q i = β·En i. If the delivered state p has mean energy at most E, and if β equals the euclidean period 2π/κ with κ = 1/R, then the Gibbs inequality becomes S(p) ≤ 2πER. The 2π comes from the deficit-free period, the inequality from Gibbs, and the conclusion holds for every delivered state p, not just the thermal one.

In Recognition Science, this is the labeled framework turn. The framework models a physical boundary as a finite seam alphabet of records, and the reference state as the period-β closure state. The declaration proves that, given these named model premises, the Bekenstein bound is a consequence, not a postulate. The library also exhibits a concrete two-record example that satisfies every hypothesis and saturates the bound, showing the inequality is not vacuous.

What the declaration does not claim is just as important. The Gibbs reference form is a model premise, not a theorem; deriving it from deeper structure remains open. The surface gravity normalization κ = 1/R is likewise a premise. And the finite seam alphabet is the ledger's discreteness; the continuum version of Casini's argument is out of scope. The theorem is conditional on these named premises, and the framework says so plainly.

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
THEOREM bekenstein_bound_nonvacuous · IndisputableMonolith/Holography/GibbsCasiniBound.lean
bekenstein_bound_nonvacuous · IndisputableMonolith/Holography/GibbsCasiniBound.lean:252 
/-- End-to-end non-vacuity witness: a concrete two-record seam (uniform delivered
state, matching Gibbs reference at `κ = 1`, `R = 1`, `β = 2π`, record energies
`log 2 / 2π`) satisfies every hypothesis of the assembly and SATURATES the bound:
`S = log 2 = 2πER`. -/
theorem bekenstein_bound_nonvacuous :
    KeystoneFactorThree.TotalEntropyBekensteinBound
      (shannonEntropy (fun _ : Fin 2 => (1 : ℝ) / 2))
      (Real.log 2 / (2 * Real.pi)) 1 := by
  refine bekenstein_bound_from_gibbs_reference
    (fun _ => (1 : ℝ) / 2) (fun _ => (1 : ℝ) / 2)
    (fun _ => Real.log 2 / (2 * Real.pi))
    (2 * Real.pi) 1 (Real.log 2 / (2 * Real.pi)) 1
    (fun _ => by norm_num) ?_ ?_ ?_ ?_ one_pos ?_ ?_
  · rw [Fin.sum_univ_two]; norm_num
  · intro i
    have hval : 2 * Real.pi * (Real.log 2 / (2 * Real.pi)) = Real.log 2 := by
      have h2pi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
      field_simp
    show (1 : ℝ) / 2 = Real.exp (-(2 * Real.pi * (Real.log 2 / (2 * Real.pi))))
    rw [hval, Real.exp_neg, Real.exp_log (by norm_num : (0 : ℝ) < 2), one_div]
  · rw [Fin.sum_univ_two]; norm_num
  · show (1 : ℝ) = 1 / 1
    norm_num
  · show (2 : ℝ) * Real.pi = DeficitFreePeriod.euclideanPeriod 1
    unfold DeficitFreePeriod.euclideanPeriod
    norm_num
  · exact le_of_eq (by rw [Fin.sum_univ_two]; ring)

What this page does not claim

The Gibbs reference form is not derived; it is a model premise. The surface gravity normalization κ = 1/R is not derived. The continuum version of Casini's argument is not claimed.

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