Holography Gibbs Uniqueness Gibbs Inequality Eq Iff

The equality condition

The Gibbs inequality is a classical fact about probability distributions: for two distributions p and q over the same finite set of outcomes, the entropy of p is at most the cross-entropy of p with respect to q. The inequality is strict unless the two distributions are identical. The Recognition Science library proves the exact equality condition as a theorem: recognition (a discrete record of events) equality holds if and only if p equals q, point for point. The proof upgrades the tangent bound log x ≤ x − 1 to its strict form log x < x − 1 for x ≠ 1, so every slack term in the summed bound must vanish record-by-record. A subnormalized reference, where the probabilities of q sum to less than 1, can never achieve equality; equality forces full normalization as well.

The theorem is unconditional, axiom-clean mathematics. It does not assume any physical model; it holds for any finite probability distributions satisfying the stated positivity and normalization conditions. The declaration is gibbs_inequality_eq_iff, and its statement is: shannonEntropy p = crossEntropy p q ↔ p = q, given that p has nonnegative entries summing to 1 and q has positive entries summing to at most 1. This is the sharpened form of the classical Gibbs inequality, with the equality case made explicit.

In Recognition Science, this equality condition is the load-bearing step for a larger result. The framework models a physical system as a finite set of recognition records, each with an energy. A reference distribution q is called an equilibrium if it minimizes the free energy functional β·⟨E⟩ − S at a given inverse temperature β. The library proves that any such minimizer is exactly the Gibbs state, the exponential distribution exp(−β·E_i)/Z, where Z is the partition function. The exponential form is not assumed; it is derived from the variational principle. The equality condition above is what makes the derivation work: the free-energy bound is tight only at the Gibbs state.

This result replaces a weaker premise. Earlier work simply posited that the reference has the exponential form. Now the framework posits only that the reference minimizes free energy, and the exponential form follows as a theorem. The remaining physical question, why the seam closure state should be the free-energy minimizer at the deficit-free period, is left open. The theorem does not claim that any actual physical system is in equilibrium; it says that if a distribution minimizes free energy, then it has the Gibbs form.

The practical consequence: in any finite system where the Gibbs inequality is tight, the two distributions are the same. This is a mathematical fact with no physical assumptions. It is the kind of result that lets a framework build from a variational principle to a specific distributional form without guessing the answer.

/-- **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]

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

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

What this page does not claim

The theorem does not claim that any actual physical system is in equilibrium. The theorem does not claim that the exponential form is assumed; it is derived. The theorem does not claim that the Gibbs inequality itself is new; only the equality condition is sharpened.

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: