Encyclopedia Holography Holography Gibbs Uniqueness Gibbs State Is Gibbs Reference

ARTICLE 3 claims 3 theorems

Holography Gibbs Uniqueness Gibbs State Is Gibbs Reference

The Gibbs state is the unique probability distribution that minimizes free energy, and its exponential form is a theorem, not an assumption.

Verify this page

The Gibbs state and its reference form

The Gibbs state is a probability distribution over the possible states of a physical system, named after Josiah Willard Gibbs. For a system with energy levels En at inverse temperature β, the Gibbs state assigns to each state i a probability proportional to exp(−β·Eni). This exponential form is the standard object of equilibrium statistical mechanics: it is the distribution that minimizes the free energy F(p) = β·⟨En⟩p − S(p), where S is the Shannon entropy.

The framework's library proves that this minimizer is unique. The theorem free_energy_eq_iff states that a distribution p achieves the minimum free energy, equal to −log Z where Z is the partition function, if and only if p equals the Gibbs state. The proof uses a strict version of the tangent bound log x ≤ x − 1, which is strict except at x = 1. Every slack term in the summed bound must therefore vanish record-by-record, forcing p to equal q. This is the equality condition for the Gibbs inequality: S(p) = ⟨Kq⟩p holds if and only if p = q.

In Recognition Science, the declaration gibbsState_is_gibbsReference establishes a specific technical fact: the Gibbs state, constructed from a given energy function and inverse temperature, is a reference state, meaning a probability distribution used as a baseline for comparison, in the framework's sense. The declaration shows that the Gibbs state satisfies the defining property of a Gibbs reference with respect to a shifted energy function. This is a theorem, proved in the machine-checked library of formal theorems, not an assumption. The exponential form of the Gibbs state is derived from the variational principle, not posited.

The framework's library replaces a weaker premise with a stronger theorem. Before, the reference state was assumed to have the exponential form. After, the premise is only that the reference minimizes free energy, and the exponential form follows as a theorem. This is the content of equilibrium_forces_gibbs_form: any reference state that minimizes free energy at inverse temperature β is the Gibbs state, record by record. The remaining physics burden is why the seam closure state is the free-energy minimizer at the deficit-free period, which is a stationarity statement, not a form assumption.

What the declaration does not claim is that the Gibbs state is the only possible reference state in general. It establishes that the Gibbs state is a Gibbs reference, not that every reference is a Gibbs state. The theorem gibbs_inequality_eq_iff does show that equality in the Gibbs inequality forces state identity, but this requires the reference to satisfy the conditions of the theorem. The declaration also does not claim that the exponential form is the only possible form for a reference state; it derives the form from the variational principle, but the variational principle itself is a premise.

THEOREM free_energy_eq_iff · equilibrium_forces_gibbs_form · IndisputableMonolith/Holography/GibbsUniqueness.lean
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
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 gibbsState_is_gibbsReference · IndisputableMonolith/Holography/GibbsUniqueness.lean
gibbsState_is_gibbsReference · IndisputableMonolith/Holography/GibbsUniqueness.lean:226 
/-- Bridge to the `GibbsCasiniBound.GibbsReference` interface: the normalized Gibbs
state satisfies the exponential-form premise with energies shifted by the free-energy
offset `log Z / β`. So everything proved downstream of `GibbsReference` applies to the
variationally derived state. -/
theorem gibbsState_is_gibbsReference {n : ℕ} (hn : 0 < n) {beta : ℝ}
    (hbeta : beta ≠ 0) (En : Fin n → ℝ) :
    GibbsReference (gibbsState beta En) beta
      (fun i => En i + Real.log (partitionFunction beta En) / beta) := by
  intro i
  have hZ := partitionFunction_pos hn beta En
  have harg : beta * (En i + Real.log (partitionFunction beta En) / beta)
      = beta * En i + Real.log (partitionFunction beta En) := by
    field_simp
  have hexplog : Real.exp (-(Real.log (partitionFunction beta En)))
      = (partitionFunction beta En)⁻¹ := by
    rw [Real.exp_neg, Real.exp_log hZ]
  show gibbsState beta En i
      = Real.exp (-(beta * (En i + Real.log (partitionFunction beta En) / beta)))
  rw [harg]
  show Real.exp (-(beta * En i)) / partitionFunction beta En
      = Real.exp (-(beta * En i + Real.log (partitionFunction beta En)))
  rw [neg_add, Real.exp_add, hexplog, div_eq_mul_inv]
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]

What this page does not claim

The declaration does not claim that every reference state is a Gibbs state. The declaration does not claim that the exponential form is the only possible form for a reference state. The declaration does not claim that the variational principle itself is derived from more basic principles.

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