Encyclopedia Thermodynamics Thermodynamics Max Ent From Cost

ARTICLE 4 claims 4 theorems

Thermodynamics Max Ent From Cost

The Gibbs distribution, the workhorse of statistical mechanics, emerges from a single principle: minimize free energy, and maximum entropy follows as a theorem.

Verify this page

Maximum entropy from cost

The Gibbs distribution is the probability law that statistical physics assigns to a system in thermal equilibrium. For a system with states labeled ω, each carrying an energy X_ω, the Gibbs measure gives each state probability p_ω = exp(-X_ω / T) / Z, where T is temperature and Z is the partition function that normalizes the probabilities to sum to one. This distribution governs everything from ideal gases to magnetic spins, and its central role in physics is not an accident; it is the unique answer to a precise optimization problem.

The optimization problem has two classic faces. The first is free energy minimization: among all probability distributions over the states, the Gibbs distribution minimizes the free energy F(q) = ⟨X⟩_q - T·S(q), where ⟨X⟩_q is the expected energy and S(q) is the Shannon entropy. The second face is maximum entropy: among all distributions that share the same expected energy as the Gibbs distribution, the Gibbs distribution has the largest entropy. These two statements are not merely compatible; the framework proves they are the same statement seen from two angles.

The classical story has a long history. Ludwig Boltzmann's work in the 1870s connected entropy to the counting of microstates, and Josiah Willard Gibbs codified the distribution that bears his name in his 1902 book Elementary Principles in Statistical Mechanics. The modern derivation via maximum entropy was popularized by E.T. Jaynes in 1957, who framed statistical mechanics as an inference problem: choose the least biased distribution consistent with known constraints. The uniqueness of the Gibbs distribution as the maximum-entropy solution under an energy constraint is a key part of this view.

In Recognition Science, the same result is derived from a different starting point. The framework replaces the energy constraint with a recognition cost, a forced price the system pays for each state it occupies, and replaces the temperature with a recognition temperature T_R. The central theorem, proved in the machine-checked library of formal theorems, states that the Gibbs distribution minimizes the recognition free energy F_R(q) = ⟨X⟩_q - T_R·S(q). From this single minimization, the framework derives the maximum entropy result: any distribution with the same expected cost as the Gibbs distribution has entropy no greater than the Gibbs entropy.

The framework also proves a sharper identity. For any distribution q, the difference in free energy from the Gibbs distribution equals T_R times the Kullback-Leibler divergence between q and the Gibbs distribution: F_R(q) - F_R(Gibbs) = T_R · D_KL(q || Gibbs). Since the KL divergence is always non-negative and equals zero only when q equals the Gibbs distribution, this identity proves uniqueness: the Gibbs distribution is the unique minimizer of free energy, and therefore the unique maximum-entropy distribution under the cost constraint. The proof is fully formalized in the framework's library, with no gaps in the chain from the definition of free energy to the uniqueness theorem.

What this means in plain language is that the most important distribution in statistical mechanics does not need to be postulated. It follows from a single optimization principle once the framework defines what recognition costs and what entropy means. The framework's contribution is not a new physics but a new derivation: the Gibbs distribution is not an assumption but a theorem, and the maximum entropy principle is not a separate postulate but a consequence of free energy minimization.

THEOREM gibbs_minimizes_free_energy_basic · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean
gibbs_minimizes_free_energy_basic · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean:78 
/-- **THEOREM: Free Energy Minimization**
    The Gibbs distribution minimizes the Recognition Free Energy. -/
theorem gibbs_minimizes_free_energy_basic (p : ProbabilityDistribution Ω) :
    recognition_free_energy sys (gibbs_measure sys X) X ≤ recognition_free_energy sys p.p X := by
  have h := free_energy_kl_identity sys X p
  have hkl := kl_divergence_nonneg p.p (gibbs_measure sys X)
    p.nonneg
    (fun ω => gibbs_measure_pos sys X ω)
    p.sum_one
    (gibbs_measure_sum_one sys X)
  calc recognition_free_energy sys (gibbs_measure sys X) X
      = recognition_free_energy sys p.p X - sys.TR * kl_divergence p.p (gibbs_measure sys X) := by
        rw [← h]; ring
    _ ≤ recognition_free_energy sys p.p X := by
        have hTR := sys.TR_pos
        nlinarith
THEOREM max_ent_subject_to_cost · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean
max_ent_subject_to_cost · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean:95 
/-- **THEOREM: MaxEnt Subject to Cost**
    The Gibbs distribution has maximum entropy among all distributions with the same
    expected cost. -/
theorem max_ent_subject_to_cost (p : ProbabilityDistribution Ω)
    (h_cost : expected_cost p.p X = expected_cost (gibbs_measure sys X) X) :
    recognition_entropy p.p ≤ recognition_entropy (gibbs_measure sys X) := by
  have h_min := gibbs_minimizes_free_energy_basic sys X p
  unfold recognition_free_energy at h_min
  rw [h_cost] at h_min
  have hTR := sys.TR_pos
  -- expected_cost - TR * entropy_gibbs ≤ expected_cost - TR * entropy_p
  -- -TR * entropy_gibbs ≤ -TR * entropy_p
  -- TR * entropy_p ≤ TR * entropy_gibbs
  -- entropy_p ≤ entropy_gibbs
  nlinarith
THEOREM free_energy_kl_identity · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean
free_energy_kl_identity · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean:20 
/-- **THEOREM: The Free Energy - KL Divergence Identity**
    F_R(q) - F_R(Gibbs) = TR * D_KL(q || Gibbs)

    **Proof**: F_R(q) = ⟨X⟩_q - TR*S(q) = ∑ q_ω X_ω + TR ∑ q_ω log q_ω
    For Gibbs: p_ω = exp(-X_ω/TR)/Z, so log p_ω = -X_ω/TR - log Z
    D_KL(q||p) = ∑ q_ω log(q_ω/p_ω) = ∑ q_ω log q_ω + ∑ q_ω (X_ω/TR + log Z)
               = -S(q)/TR + ⟨X⟩_q/TR + log Z
    TR * D_KL = -TR*S(q) + ⟨X⟩_q + TR*log Z = F_R(q) - (-TR*log Z) = F_R(q) - F_R(Gibbs) -/
theorem free_energy_kl_identity (q : ProbabilityDistribution Ω) :
    recognition_free_energy sys q.p X - recognition_free_energy sys (gibbs_measure sys X) X =
    sys.TR * kl_divergence q.p (gibbs_measure sys X) := by
  -- Use the fact that F_R(Gibbs) = -TR * log(Z) from free_energy_identity
  have h_gibbs_FR := free_energy_identity sys X
  rw [h_gibbs_FR]
  unfold recognition_free_energy expected_cost recognition_entropy free_energy_from_Z

  -- F_R(q) = ∑ q J - TR * (-∑ q log q) = ∑ q J + TR ∑ q log q
  -- D_KL(q||p) = ∑ q log(q/p) where p = gibbs
  -- TR * D_KL = TR ∑ q log q - TR ∑ q log p
  -- log p_ω = log(exp(-J_ω/TR)/Z) = -J_ω/TR - log Z
  -- TR ∑ q log p = TR ∑ q (-J_ω/TR - log Z) = -∑ q J - TR log Z ∑ q = -∑ q J - TR log Z
  -- TR * D_KL = TR ∑ q log q + ∑ q J + TR log Z
  -- F_R(q) - F_R(Gibbs) = (∑ q J + TR ∑ q log q) - (-TR log Z) = ∑ q J + TR ∑ q log q + TR log Z
  -- These match! QED.

  unfold kl_divergence gibbs_measure partition_function
  simp only [gibbs_weight]
  set Z := ∑ ω, exp (-Jcost (X ω) / sys.TR) with hZ
  have hZ_pos : 0 < Z := by
    rw [hZ]; apply Finset.sum_pos (fun ω _ => exp_pos _) Finset.univ_nonempty
  have hq_sum := q.sum_one
  set S := ∑ ω : Ω, (if q.p ω > 0 then q.p ω * log (q.p ω) else 0)
  have lhs_simp :
    (∑ ω, q.p ω * Jcost (X ω) - sys.TR * -S) - -sys.TR * log Z =
    ∑ ω, q.p ω * Jcost (X ω) + sys.TR * S + sys.TR * log Z := by ring
  rw [lhs_simp]
  rw [show sys.TR * log Z = ∑ ω : Ω, sys.TR * log Z * q.p ω from
    by rw [← Finset.mul_sum, hq_sum, mul_one]]
  show ∑ ω, q.p ω * Jcost (X ω) + sys.TR * S + ∑ ω, sys.TR * log Z * q.p ω =
    sys.TR * ∑ ω, (if q.p ω > 0 ∧ exp (-Jcost (X ω) / sys.TR) / Z > 0
      then q.p ω * log (q.p ω / (exp (-Jcost (X ω) / sys.TR) / Z)) else 0)
  rw [show sys.TR * S = ∑ ω : Ω, sys.TR * (if q.p ω > 0 then q.p ω * log (q.p ω) else 0) from
    by rw [Finset.mul_sum]]
  rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib, Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro ω _
  have h_gibbs_pos : 0 < exp (-Jcost (X ω) / sys.TR) / Z := div_pos (exp_pos _) hZ_pos
  by_cases hq_pos : 0 < q.p ω
  · simp only [show q.p ω > 0 from hq_pos, show exp (-Jcost (X ω) / sys.TR) / Z > 0 from h_gibbs_pos,
               and_self, ite_true]
    rw [log_div (ne_of_gt hq_pos) (ne_of_gt h_gibbs_pos),
        log_div (exp_pos _).ne' hZ_pos.ne', log_exp]
    field_simp [sys.TR_pos.ne']
    ring
  · push_neg at hq_pos
    have hq_zero : q.p ω = 0 := le_antisymm hq_pos (q.nonneg ω)
    simp [hq_zero]
THEOREM gibbs_unique_minimizer · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean
gibbs_unique_minimizer · IndisputableMonolith/Thermodynamics/MaxEntFromCost.lean:192 
/-- The Gibbs distribution is the unique minimizer of free energy. -/
theorem gibbs_unique_minimizer (q : ProbabilityDistribution Ω)
    (h_eq : recognition_free_energy sys q.p X = recognition_free_energy sys (gibbs_measure sys X) X) :
    ∀ ω, q.p ω = gibbs_measure sys X ω := by
  have h := free_energy_kl_identity sys X q
  rw [h_eq, sub_self] at h
  have hTR := sys.TR_pos
  have hkl_zero : kl_divergence q.p (gibbs_measure sys X) = 0 := by
    rw [eq_comm] at h
    have := mul_eq_zero.mp h
    cases this with
    | inl hTR0 => linarith
    | inr hkl0 => exact hkl0
  apply (kl_divergence_zero_iff_eq q.p (gibbs_measure sys X) q.nonneg (fun ω => gibbs_measure_pos sys X ω) q.sum_one (gibbs_measure_sum_one sys X)).mp
  exact hkl_zero

What this page does not claim

The framework does not derive the value of the recognition temperature from first principles. The maximum entropy theorem does not apply to non-equilibrium distributions. The framework does not claim that physical energy is identical to recognition cost in all regimes.

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/Thermodynamics/MaxEntFromCost.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