Holography Gibbs Uniqueness Cross Entropy Gibbs State

The cross-entropy identity

In probability and statistical physics, the cross-entropy between two distributions measures how surprised one is on average when using one distribution to predict events that actually follow the other. The Recognition Science declaration `crossEntropy_gibbsState` proves a precise identity for this quantity when the second distribution is the Gibbs state, the exponential form that describes a system in thermal equilibrium. The theorem states that for any probability distribution p over a finite set of states, the cross-entropy of p relative to the Gibbs state equals the average energy of p times the inverse temperature, plus the logarithm of the partition function. In symbols: H(p, q) = β·⟨E⟩_p + log Z, where q is the Gibbs state.

This identity is a workhorse of statistical mechanics. It connects the abstract information-theoretic notion of surprise to the concrete physical quantities of energy, temperature, and the partition function, which encodes how states are weighted at a given temperature. The theorem is unconditional and axiom-clean: it does not assume anything about how the Gibbs state arose, only that it has the standard exponential form. The proof follows from the definitions of cross-entropy, the Gibbs state, and the partition function, and the result holds for any finite system.

In the broader Recognition Science framework, this identity is a stepping stone. The framework's library of machine-checked theorems uses it to prove that any state which minimizes free energy must be the Gibbs state, and from there to derive a bound on the total entropy of a system. The cross-entropy identity itself, however, makes no claim about equilibrium, about why a system reaches the Gibbs state, or about the physical meaning of the inverse temperature. Those are separate, more substantive premises that the framework models explicitly.

What the theorem does not claim is as important as what it proves. It does not say that any real physical system is actually in the Gibbs state, nor does it explain why a system would evolve to that state. It does not assert that the inverse temperature β has any particular value, nor that the energies En are those of any specific physical system. The identity is a mathematical fact about a defined quantity; the physics enters only when one chooses to identify the Gibbs state with a real system's equilibrium state, a choice the framework marks as a model premise, not a theorem.

/-- Cross entropy against the normalized Gibbs state = β·⟨En⟩ + log Z. -/
theorem crossEntropy_gibbsState {n : ℕ} (hn : 0 < n) (p : Fin n → ℝ)
    (beta : ℝ) (En : Fin n → ℝ) (hp1 : ∑ i, p i = 1) :
    crossEntropy p (gibbsState beta En)
      = beta * (∑ i, p i * En i) + Real.log (partitionFunction beta En) := by
  have hZ := partitionFunction_pos hn beta En
  have hK : ∀ i, modularHamiltonian (gibbsState beta En) i
      = beta * En i + Real.log (partitionFunction beta En) := by
    intro i
    unfold modularHamiltonian gibbsState
    rw [Real.log_div (ne_of_gt (Real.exp_pos _)) (ne_of_gt hZ), Real.log_exp]
    ring
  unfold crossEntropy
  calc ∑ i, p i * modularHamiltonian (gibbsState beta En) i
      = ∑ i, (beta * (p i * En i)
          + p i * Real.log (partitionFunction beta En)) := by
        refine Finset.sum_congr rfl fun i _ => ?_
        rw [hK i]; ring
    _ = beta * (∑ i, p i * En i)
        + (∑ i, p i) * Real.log (partitionFunction beta En) := by
        rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul]
    _ = beta * (∑ i, p i * En i) + Real.log (partitionFunction beta En) := by
        rw [hp1, one_mul]

/-- Cross entropy against the normalized Gibbs state = β·⟨En⟩ + log Z. -/
theorem crossEntropy_gibbsState {n : ℕ} (hn : 0 < n) (p : Fin n → ℝ)
    (beta : ℝ) (En : Fin n → ℝ) (hp1 : ∑ i, p i = 1) :
    crossEntropy p (gibbsState beta En)
      = beta * (∑ i, p i * En i) + Real.log (partitionFunction beta En) := by
  have hZ := partitionFunction_pos hn beta En
  have hK : ∀ i, modularHamiltonian (gibbsState beta En) i
      = beta * En i + Real.log (partitionFunction beta En) := by
    intro i
    unfold modularHamiltonian gibbsState
    rw [Real.log_div (ne_of_gt (Real.exp_pos _)) (ne_of_gt hZ), Real.log_exp]
    ring
  unfold crossEntropy
  calc ∑ i, p i * modularHamiltonian (gibbsState beta En) i
      = ∑ i, (beta * (p i * En i)
          + p i * Real.log (partitionFunction beta En)) := by
        refine Finset.sum_congr rfl fun i _ => ?_
        rw [hK i]; ring
    _ = beta * (∑ i, p i * En i)
        + (∑ i, p i) * Real.log (partitionFunction beta En) := by
        rw [Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul]
    _ = beta * (∑ i, p i * En i) + Real.log (partitionFunction beta En) := by
        rw [hp1, one_mul]

What this page does not claim

The theorem does not assert that any real physical system is in the Gibbs state. The theorem does not explain why a system evolves to the Gibbs state. The theorem does not assign a specific value to the inverse temperature or to the energy levels.

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: