Encyclopedia Holography Holography Gibbs Casini Bound Modular Hamiltonian Of Gibbs Reference

ARTICLE 4 claims 4 theorems

Holography Gibbs Casini Bound Modular Hamiltonian Of Gibbs Reference

A machine-checked theorem shows that when a reference state takes the Gibbs form, its modular Hamiltonian prices each record linearly by energy, a step toward a general entropy bound.

Verify this page

Pricing records by energy

In statistical physics, the Gibbs state is the probability distribution that maximizes entropy under a fixed average energy, taking the form q(i) = exp(−β·En(i)) for a temperature parameter β. Its modular Hamiltonian, defined as K(i) = −log q(i), measures how surprising each outcome i is relative to that reference. For a Gibbs state, this quantity simplifies dramatically: K(i) = β·En(i). The machine-checked theorem modularHamiltonian_of_gibbsReference in the framework's library establishes exactly this linear pricing relation, with no measure theory and no operator algebra, because it works on a finite set of records.

The result is a definitional identity, not a physical assumption. Given the definition of a Gibbs reference and the definition of a modular Hamiltonian, the logarithm and exponential cancel to leave β times the energy. The proof is a short chain of rewrites in the machine-checked library of formal theorems. Positivity of the reference state follows automatically from the exponential form, a separate theorem named gibbsReference_pos. Together these facts mean that for any Gibbs-form reference, the modular Hamiltonian assigns each record a price proportional to its energy, with β as the conversion factor.

This linear pricing is the hinge for a larger claim. The framework's library proves the Gibbs inequality, which states that for any probability distribution p and any positive subnormalized reference q, the Shannon entropy S(p) is at most the cross entropy ⟨K_q⟩_p. When the reference is Gibbs-form, the cross entropy becomes β times the mean energy, so the inequality reads S(p) ≤ β·⟨En⟩_p. This is the finite, discrete version of Casini's resolution of the Bekenstein bound, and it holds for every delivered state p, not just the thermal one.

The assembled Bekenstein bound, bekenstein_bound_from_gibbs_reference, upgrades this to S(p) ≤ 2πER for all states, but only under named premises. The reference must be Gibbs-form, the reference must be subnormalized, the horizon rate must satisfy κ = 1/R, and β must equal the euclidean period 2π/κ. The 2π comes from the deficit-free period theorem, and the inequality from Gibbs. What the declaration does not claim is that the reference state is in fact thermal: deriving the Gibbs form from the deficit-free-period and KMS structure remains open work, tracked as the B2/B3 physics. The continuum, type-III algebra version of Casini's argument is also out of scope.

What this establishes is a clean separation: the entropy bound for all states reduces to the thermality of the reference, never of the delivered state. A concrete two-record example saturates the bound with S = log 2 = 2πER, showing the inequality is sharp and not vacuous. The reader can now see that the entire burden of the physical Bekenstein bound in this framework rests on one open question: why the reference seam state should be Gibbs at the deficit-free period.

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 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 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 form of the reference state is not derived here; it is a named model premise. The continuum version of Casini's bound for type-III algebras is not claimed. The horizon rate κ = 1/R is not derived; it remains a normalization premise.

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