partition_function
The partition function Z sums Gibbs weights exp(-J(X(ω))/T_R) over every state ω in a finite discrete space Ω for a RecognitionSystem with positive temperature T_R. Thermodynamic derivations that extend J-cost minimization to finite Recognition Temperature cite this sum to obtain free energy and entropy. The definition is a direct summation of the already-defined gibbs_weight terms.
claim$Z = ∑_{ω ∈ Ω} exp(-J(X(ω))/T_R)$ where $T_R > 0$ is the recognition temperature of the system and $J$ denotes the J-cost function.
background
Recognition Thermodynamics extends the zero-temperature J-minimization of Recognition Science to finite Recognition Temperature T_R. The RecognitionSystem structure carries a single field T_R together with the proof that T_R > 0; its beta field is defined as the reciprocal 1/T_R. The Gibbs weight of a state with ratio x is exp(-Jcost(x)/T_R), which supplies the unnormalized probability in the sum that defines Z. This construction realizes the module's stated connection between J-cost as energy and the Born-rule weight as the Gibbs factor.
proof idea
One-line definition that sums the gibbs_weight sys (X ω) over the Fintype Ω.
why it matters in Recognition Science
The definition supplies the partition function required by free_energy_from_Z, gibbs_log_form, and the EntropyAncestorCertificate. It completes the bridge from the RS foundation (J as cost, phi-ladder discretization, eight-tick cycle) to finite-temperature statistical mechanics while preserving the T0-to-T8 forcing chain. Downstream results such as free_energy_monotone_status and lagrange_forces_gibbs rely on this Z to state monotonicity and uniqueness of the Gibbs measure.
scope and limits
- Does not define Z for continuous or infinite state spaces.
- Does not embed the phi-ladder rung or gap(Z) structure into the sum.
- Does not prove positivity or normalization of Z (those are separate theorems).
- Does not assume any specific functional form for the map X beyond real values.
formal statement (Lean)
79noncomputable def partition_function {Ω : Type*} [Fintype Ω]
80 (sys : RecognitionSystem) (X : Ω → ℝ) : ℝ :=
proof body
Definition body.
81 ∑ ω, gibbs_weight sys (X ω)
82
83/-- The partition function is positive. -/