Thermodynamics Partition Function

The partition function

The partition function is the central object of statistical mechanics. For a system with discrete energy levels E_i and degeneracies g_i at temperature T, it is defined as Z = Σ_i g_i exp(−E_i/k_BT), where k_B is the Boltzmann constant. Its power is that everything else follows from it: the free energy F = −k_BT ln Z, the average energy ⟨E⟩ = −∂ln Z/∂β (with β = 1/k_BT), and the entropy S = k_B(ln Z + β⟨E⟩). Ludwig Boltzmann introduced this weighting in the 1870s, and Josiah Willard Gibbs formalized the ensemble approach in 1902.

The partition function also explains why systems behave as they do. At low temperature, only the lowest energy states contribute, so Z is small and the system is ordered. As temperature rises, higher energy states become accessible, Z grows, and disorder increases. The two-level system is the simplest test: with energies 0 and ε, Z = 1 + exp(−ε/k_BT). At T → 0, Z → 1, meaning the system sits in its ground state; at high T, Z → 2, meaning both states are equally likely. The harmonic oscillator extends this to equally spaced levels, giving Z = exp(−ħω/2k_BT) / (1 − exp(−ħω/k_BT)).

In Recognition Science, the partition function emerges from a different starting point. The framework models a physical system as a ledger, a discrete record of recognition events. Each possible configuration of the ledger has a cost J, the forced cost of recognition. The framework then defines Z as the sum over all ledger configurations, weighted by exp(−J/k_BT), so that J plays the role of energy. This is a definitional choice, not a derived theorem, but it connects the framework's core cost function to the full machinery of statistical mechanics.

What the module actually proves is more limited. It shows that the partition function is always positive for any discrete system with at least one level and positive degeneracies. It proves that the two-level partition function is always greater than 1 for positive temperature, and equals exactly 2 when the energy gap is zero. These are small but real results. The larger claims, that quantum statistics follow from an eight-tick cycle and that the classical limit recovers Liouville's phase space measure, are stated as comments in the code, not proved. The module also includes a falsifier structure: if thermodynamics from Z fails, or if J-cost is not energy, or if the eight-tick cycle does not yield quantum statistics, the framework's account is falsified.

The practical upshot is that the framework has a working vocabulary for thermodynamics, not a completed theory. It defines the standard quantities, proves the basic positivity facts, and identifies exactly what would need to be proved for the framework's account to be complete. The classical limit and the connection to quantum statistics remain open targets, not achieved results.

/-- In Recognition Science, the partition function is a **sum over ledger states**.

    Each microscopic configuration corresponds to a ledger entry.
    The Boltzmann weight exp(-βE) comes from the J-cost:

    P(state) ∝ exp(-J_cost(state) / k_B T)

    The partition function normalizes these probabilities:
    Z = Σ_{ledger states} exp(-J_cost / k_B T) -/
theorem partition_from_ledger_sum :
    -- Z = sum over all ledger configurations
    -- Each configuration has a J-cost
    -- The weight is exp(-J_cost / k_B T)
    True := trivial

/-- **THEOREM**: Partition function is always positive. -/
theorem partition_function_positive (sys : DiscreteSystem) (T : ℝ) (hT : T > 0) :
    partitionFunction sys T hT > 0 := by
  unfold partitionFunction
  have hne : Nonempty (Fin sys.numLevels) := ⟨⟨0, sys.nonempty⟩⟩
  apply Finset.sum_pos
  · intro i _
    apply mul_pos
    · -- degeneracy ≥ 1 > 0
      have h := sys.deg_pos i
      exact Nat.cast_pos.mpr (Nat.lt_of_lt_of_le Nat.zero_lt_one h)
    · exact exp_pos _
  · exact @Finset.univ_nonempty (Fin sys.numLevels) _ hne

/-- Two-level partition function is always > 1. -/
theorem twoLevel_gt_one (epsilon : ℝ) (T : ℝ) (hT : T > 0) :
    twoLevelPartition epsilon T hT > 1 := by
  unfold twoLevelPartition
  have h : exp (-beta T hT * epsilon) > 0 := exp_pos _
  linarith

/-- At ε = 0, Z = 2 (two degenerate levels). -/
theorem twoLevel_at_zero (T : ℝ) (hT : T > 0) :
    twoLevelPartition 0 T hT = 2 := by
  unfold twoLevelPartition beta
  simp only [mul_zero, exp_zero]
  ring

What this page does not claim

The module does not prove that J-cost is energy, only that it is defined to play that role. The module does not prove the classical limit or quantum statistics; these are stated as comments, not theorems. The module does not derive the partition function from first principles; it defines it in terms of the ledger and J-cost.

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/PartitionFunction.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: