Encyclopedia Holography Holography Gibbs Uniqueness

ARTICLE 3 claims 3 theorems

Holography Gibbs Uniqueness

In statistical physics, the Gibbs state is the unique distribution that minimizes free energy at a fixed temperature; a machine-checked library now proves the same forcing result without assuming the exponential form.

Verify this page

Gibbs uniqueness

The Gibbs distribution, also called the canonical ensemble, is the probability assignment qi = exp(−β·Ei)/Z over states i with energies Ei at inverse temperature β, where Z = Σi exp(−β·Ei) is the partition function. It is the standard answer to the question: what distribution describes a system in thermal equilibrium? The classical justification is the variational principle: among all normalized distributions p, the Gibbs state uniquely minimizes the free energy functional F(p) = β·⟨E⟩p − S(p), where S(p) is the Shannon entropy. This principle is a theorem of convex analysis, and it is the reason the exponential form appears throughout equilibrium statistical mechanics. The history runs from Boltzmann's 1877 counting argument through Gibbs's 1902 Elementary Principles to modern information-theoretic treatments.

The uniqueness has a sharper formulation. The Gibbs inequality states that the Shannon entropy of p is at most its cross-entropy against the reference q, with equality if and only if p = q. The proof upgrades the tangent bound log x ≤ x − 1 to the strict version log x < x − 1 for x ≠ 1, so every slack term in the summed bound must vanish record-by-record. A subnormalized reference, one whose probabilities sum to less than one, can never achieve equality; equality forces normalization as well. This equality condition is unconditional mathematics, proved in the machine-checked library of formal theorems.

In Recognition Science, the framework models reality as maintaining a discrete ledger, a record of recognition events, and the cost of recognition is forced by a proved functional equation. The holography program applies this to black hole thermodynamics, where the Bekenstein bound S(p) ≤ 2πER limits the entropy of any state in a region of size R with energy E. Earlier work assumed the reference state had the exponential Gibbs form as a premise. The module GibbsUniqueness.lean replaces that assumption with a strictly weaker one: the reference minimizes free energy. From this variational premise, the exponential form is no longer posited; it is derived as the unique solution. The theorem equilibrium_forces_gibbs_form states that any reference minimizing free energy at inverse temperature β is exactly the Gibbs state, record by record.

The assembled Bekenstein bound then follows from the weaker equilibrium premise instead of the form premise, with the partition-function condition Z ≤ 1 carried explicitly. The remaining physics burden is the KMS content: why the seam closure state at the deficit-free period β = 2π/κ is the free-energy minimizer. That is a stationarity statement, strictly weaker than the form assumption it replaces. The practical consequence: the exponential form in holography is not an input but an output of the variational problem, and the uniqueness is unconditional mathematics.

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

What this page does not claim

The exponential Gibbs form is not assumed; it is derived from the variational premise. The KMS stationarity of the seam closure state is not proved in this module; it remains the physics burden. The Bekenstein bound from equilibrium is conditional on the partition-function condition Z ≤ 1.

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