Encyclopedia Holography Holography Gibbs Uniqueness Partition Function Term Le One

ARTICLE 3 claims 3 theorems

Holography Gibbs Uniqueness Partition Function Term Le One

A small inequality about the partition function, the sum that defines statistical mechanics, turns out to be the hinge for a much larger uniqueness result.

Verify this page

The partition function bound

The partition function is the workhorse of statistical mechanics. For a system with energy levels En i at inverse temperature beta, it is the sum Z = sum over i of exp(-beta * En i). Each term exp(-beta * En i) is a Boltzmann weight, the relative probability that the system occupies level i. The theorem partitionFunction_term_le_one states a simple fact: if every product beta * En i is nonnegative, then every Boltzmann weight is at most 1. Since exp(0) = 1 and exp decreases as its argument becomes more negative, this is immediate once beta * En i is nonnegative. The proof in the machine-checked library of formal theorems is a one-liner from the monotonicity of the exponential function.

The condition beta * En i >= 0 is the physically natural one. Inverse temperature beta is positive in ordinary thermodynamics, and energy levels are measured from a zero that makes them nonnegative. The bound then says no level can have a Boltzmann weight greater than 1, the weight of the zero-energy level. This is not a deep fact by itself; it is a warm-up lemma. Its role is to support the claim that the partition function itself is at most 1 under the same sign condition, which is the premise that makes the later entropy bound work. The theorem does not say that the partition function is bounded below by 1, nor that the Boltzmann weights sum to 1; that normalization is a separate, stronger condition enforced only for the Gibbs state.

In Recognition Science, the same lemma appears in a sharper context. The framework's library proves that a reference state which minimizes free energy at inverse temperature beta must be the Gibbs state, record by record. The exponential form of the Gibbs state is not assumed; it is derived from the variational principle. The bound Z <= 1, with partitionFunction_term_le_one as a supporting step, is carried explicitly into the assembled Bekenstein bound. What the lemma does not claim is any statement about the physical system itself: it is a theorem about real numbers and the exponential function, not about black holes or horizons. The physics enters through the separate premise that the reference state is an equilibrium state, which remains a named model assumption.

The practical upshot is a clean separation. The inequality partitionFunction_term_le_one is unconditional mathematics, true for any real beta and En satisfying the sign condition. The equilibrium identification, the claim that the seam reference state actually minimizes free energy at the deficit-free period, is a model premise. Readers who want to use the bound must supply that premise themselves. The lemma itself is a tool, not a physical law.

THEOREM partitionFunction_term_le_one · IndisputableMonolith/Holography/GibbsUniqueness.lean
partitionFunction_term_le_one · IndisputableMonolith/Holography/GibbsUniqueness.lean:201 
/-- Sufficient condition for the subnormalization premise `Z ≤ 1` used downstream:
if every record is priced nonnegatively (`0 ≤ β·En i`) and the alphabet is a single
record, or more generally if `∑ exp(−β·En i) ≤ 1`. For the common one-record-dominant
case: each term is `≤ 1`, so `Z ≤ n` always; `Z ≤ 1` is a genuine budget statement. -/
theorem partitionFunction_term_le_one {n : ℕ} (beta : ℝ) (En : Fin n → ℝ)
    (h : ∀ i, 0 ≤ beta * En i) (i : Fin n) :
    Real.exp (-(beta * En i)) ≤ 1 := by
  rw [Real.exp_le_one_iff]
  linarith [h i]
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 lemma does not claim that the partition function itself is at most 1 without the sign condition on beta * En i. The lemma does not claim that the Boltzmann weights sum to 1. The lemma does not assert that any physical system actually reaches the Gibbs state.

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