Encyclopedia Holography Holography Gibbs Uniqueness Bekenstein Bound From Equilibrium

ARTICLE 4 claims 4 theorems

Holography Gibbs Uniqueness Bekenstein Bound From Equilibrium

A machine-checked proof shows that the exponential form of a thermal state, long assumed, is actually forced by a variational principle.

Verify this page

The bound from equilibrium

The Bekenstein bound is a physical conjecture limiting the entropy S of any system of energy E and size R to S ≤ 2πER. In the Recognition Science framework, this bound is not taken as an axiom. The declaration bekenstein_bound_from_equilibrium establishes it as a conditional theorem, derived from a strictly weaker premise than the one used in earlier work.

The older approach simply assumed the reference state had the exponential, Gibbs form q_i = exp(−β·En_i). That is a strong premise: it asserts the answer. The new theorem replaces it with a variational premise. It assumes the reference state minimizes a free-energy functional β⟨En⟩ − S, a condition called equilibrium reference. From this weaker assumption, the framework's machine-checked library of formal theorems derives the Gibbs form as a consequence, not an input.

The proof has three unconditional parts. First, equality in the Gibbs inequality S(p) = ⟨K_q⟩_p holds if and only if p = q. Second, the free energy F(p) = β⟨En⟩_p − S(p) obeys F(p) ≥ −log Z, with equality only at the normalized Gibbs state. Third, any state that minimizes free energy must be the Gibbs state, record by record. These are proved in the library with no special axioms.

The assembled bound then follows: if the equilibrium reference minimizes free energy, the partition function satisfies Z ≤ 1, and the horizon rate is κ = 1/R, then every delivered state obeys S(p) ≤ 2πER. The conclusion is identical to the earlier form, but the premise ledger has moved. The exponential form is no longer posited; it is derived.

The remaining physical burden is explicit. The theorem does not explain why the seam closure state minimizes free energy at the deficit-free period β = 2π/κ. That stationarity statement is a separate, open target. The theorem also carries the condition Z ≤ 1, meaning records are expensive: every β·En_i ≥ 0 suffices. These are the conditions under which the bound holds, not hidden assumptions.

THEOREM bekenstein_bound_from_equilibrium · IndisputableMonolith/Holography/GibbsUniqueness.lean
bekenstein_bound_from_equilibrium · IndisputableMonolith/Holography/GibbsUniqueness.lean:355 
/-- **CONDITIONAL Bekenstein bound for ALL states, from the equilibrium premise.**
Identical conclusion to `GibbsCasiniBound.bekenstein_bound_from_gibbs_reference`
(`S(p) ≤ 2πER` for every delivered record distribution), but the reference-state
premise is downgraded from the exponential FORM to the variational statement
`EquilibriumReference` (the reference minimizes `β⟨En⟩ − S` at the deficit-free
period). The chain: equilibrium forces the Gibbs form (THEOREM), the Gibbs inequality
prices the delivered state against it (THEOREM), `Z ≤ 1` converts the free-energy
offset into slack (premise), and the deficit-free period supplies `β = 2πR`
(THEOREM given `HorizonRate`). -/
theorem bekenstein_bound_from_equilibrium {n : ℕ}
    (p q En : Fin n → ℝ) (beta kappa E R : ℝ)
    (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i = 1)
    (heq : EquilibriumReference q beta En)
    (hZ : partitionFunction beta En ≤ 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 hn : 0 < n := by
    rcases Nat.eq_zero_or_pos n with rfl | hn
    · exact absurd heq.2.1 (by simp)
    · exact hn
  have hZpos := partitionFunction_pos hn beta En
  have hlogZ : Real.log (partitionFunction beta En) ≤ 0 :=
    Real.log_nonpos (le_of_lt hZpos) hZ
  have hgibbs := gibbs_inequality p (gibbsState beta En) hp
    (gibbsState_pos hn beta En) hp1 (le_of_eq (gibbsState_normalized hn beta En))
  have hcross := crossEntropy_gibbsState hn p beta En hp1
  -- κ = 1/R with κ > 0 forces R > 0, hence β = 2πR ≥ 0.
  have hR' : kappa = 1 / R := hR
  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
  have hmean : beta * (∑ i, p i * En i) ≤ beta * E :=
    mul_le_mul_of_nonneg_left hE hbeta_nonneg
  show shannonEntropy p ≤ 2 * Real.pi * E * R
  calc shannonEntropy p
      ≤ crossEntropy p (gibbsState beta En) := hgibbs
    _ = beta * (∑ i, p i * En i) + Real.log (partitionFunction beta En) := hcross
    _ ≤ beta * E := by linarith
    _ = 2 * Real.pi * E * R := by rw [hbetaR]; ring
THEOREM equilibrium_forces_gibbs_form · IndisputableMonolith/Holography/GibbsUniqueness.lean
equilibrium_forces_gibbs_form · IndisputableMonolith/Holography/GibbsUniqueness.lean:340 
/-- **The exponential form is forced.** Any free-energy-minimizing reference IS the
normalized Gibbs state, record by record. The form assumption in `GibbsReference` is
hereby a theorem downstream of the variational premise. -/
theorem equilibrium_forces_gibbs_form {n : ℕ} {q : Fin n → ℝ} {beta : ℝ}
    {En : Fin n → ℝ} (h : EquilibriumReference q beta En) :
    q = gibbsState beta En := by
  obtain ⟨hq0, hq1, hF⟩ := h
  have hn : 0 < n := by
    rcases Nat.eq_zero_or_pos n with rfl | hn
    · exact absurd hq1 (by simp)
    · exact hn
  exact (free_energy_eq_iff hn q beta En hq0 hq1).mp hF
THEOREM gibbs_inequality_eq_iff · IndisputableMonolith/Holography/GibbsUniqueness.lean
gibbs_inequality_eq_iff · IndisputableMonolith/Holography/GibbsUniqueness.lean:142 
/-- **Equality in the Gibbs inequality holds iff the states coincide.** For a probability
vector `p` and a positive subnormalized reference `q`: `S(p) = ⟨K_q⟩_p ↔ p = q`.
Equality forces normalization of `q` along the way (a strictly subnormalized reference
always has positive slack). -/
theorem gibbs_inequality_eq_iff {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 ↔ p = q := by
  constructor
  · intro heq
    -- The summed log-ratio vanishes at equality.
    have hcrossE : crossEntropy p q = -(∑ i, p i * Real.log (q i)) := by
      simp only [crossEntropy, modularHamiltonian]
      simp [mul_neg]
    have hshannon : shannonEntropy p = -(∑ i, p i * Real.log (p i)) := rfl
    have hzero : ∑ i, p i * (Real.log (q i) - Real.log (p i)) = 0 := by
      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 hA : (∑ i, p i * Real.log (q i)) = -crossEntropy p q := by
        rw [hcrossE]; ring
      have hB : (∑ i, p i * Real.log (p i)) = -shannonEntropy p := by
        rw [hshannon]; ring
      rw [hexpand, hA, hB, heq]
      ring
    -- The per-record slack terms are nonnegative and sum to ∑q − 1 ≤ 0, hence all vanish.
    have htnonneg : ∀ i ∈ Finset.univ,
        0 ≤ (q i - p i) - p i * (Real.log (q i) - Real.log (p i)) :=
      fun i _ => sub_nonneg.mpr (per_gap_le (hp i) (hq i))
    have htsum : ∑ i, ((q i - p i) - p i * (Real.log (q i) - Real.log (p i)))
        = (∑ i, q i) - 1 := by
      rw [Finset.sum_sub_distrib, Finset.sum_sub_distrib, hp1, hzero]
      ring
    have hsum_nonneg : (0 : ℝ) ≤ (∑ i, q i) - 1 := by
      rw [← htsum]
      exact Finset.sum_nonneg htnonneg
    have hall : ∀ i ∈ Finset.univ,
        (q i - p i) - p i * (Real.log (q i) - Real.log (p i)) = 0 := by
      rw [← Finset.sum_eq_zero_iff_of_nonneg htnonneg, htsum]
      linarith
    funext i
    have hi := hall i (Finset.mem_univ i)
    exact per_gap_eq (hp i) (hq i) (by linarith)
  · rintro rfl
    simp only [shannonEntropy, crossEntropy, modularHamiltonian]
    simp [mul_neg]
THEOREM free_energy_bound · free_energy_eq_iff · IndisputableMonolith/Holography/GibbsUniqueness.lean
free_energy_bound · IndisputableMonolith/Holography/GibbsUniqueness.lean:281 
/-- **Free-energy lower bound.** Every record distribution obeys `F(p) ≥ −log Z`. -/
theorem free_energy_bound {n : ℕ} (hn : 0 < n) (p : Fin n → ℝ)
    (beta : ℝ) (En : Fin n → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i = 1) :
    -Real.log (partitionFunction beta En) ≤ freeEnergyFunctional beta En p := by
  have hgibbs := gibbs_inequality p (gibbsState beta En) hp
    (gibbsState_pos hn beta En) hp1 (le_of_eq (gibbsState_normalized hn beta En))
  have hcross := crossEntropy_gibbsState hn p beta En hp1
  unfold freeEnergyFunctional
  linarith
free_energy_eq_iff · IndisputableMonolith/Holography/GibbsUniqueness.lean:292 
/-- **Uniqueness of the minimizer.** `F(p) = −log Z` iff `p` IS the Gibbs state. -/
theorem free_energy_eq_iff {n : ℕ} (hn : 0 < n) (p : Fin n → ℝ)
    (beta : ℝ) (En : Fin n → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i = 1) :
    freeEnergyFunctional beta En p = -Real.log (partitionFunction beta En)
      ↔ p = gibbsState beta En := by
  have hcross := crossEntropy_gibbsState hn p beta En hp1
  have hiff := gibbs_inequality_eq_iff p (gibbsState beta En) hp
    (gibbsState_pos hn beta En) hp1 (le_of_eq (gibbsState_normalized hn beta En))
  constructor
  · intro hF
    apply hiff.mp
    unfold freeEnergyFunctional at hF
    linarith
  · intro hpg
    have hS := hiff.mpr hpg
    unfold freeEnergyFunctional
    linarith

What this page does not claim

The theorem does not prove that the equilibrium reference condition holds for any physical system. The theorem does not derive the value of the inverse temperature β from first principles. The theorem does not establish the Bekenstein bound unconditionally.

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/GibbsUniqueness.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