partition_function_pos
plain-language theorem explainer
The partition function Z for a RecognitionSystem on any finite nonempty state space is strictly positive. Researchers extending zero-temperature J-minimization to finite Recognition Temperature would cite this to guarantee that the Gibbs measure is a well-defined probability distribution. The proof is a one-line wrapper that unfolds the sum and applies Finset.sum_pos using positivity of each Gibbs weight together with the nonempty universe.
Claim. Let $T_R > 0$ be the recognition temperature of a system and let $X : Ω → ℝ$ assign a real cost to each state in a finite nonempty set $Ω$. The partition function $Z = ∑_{ω ∈ Ω} exp(-J(X(ω))/T_R)$ satisfies $Z > 0$.
background
Recognition Thermodynamics extends the deterministic J-cost minimization of Recognition Science to finite temperature $T_R > 0$. The RecognitionSystem structure carries a positive temperature parameter $T_R$ whose inverse beta = 1/$T_R$ appears in the Gibbs weight exp(-J(x)/$T_R$). The partition function is defined as the sum of these weights over the finite state space, serving as the normalizing constant for the Gibbs measure $p(ω) ∝ exp(-J(X(ω))/T_R)$. Upstream results establish that J(x) = (x + 1/x)/2 - 1 is strictly convex with unique minimum at x = 1, and that individual Gibbs weights are positive.
proof idea
The proof unfolds the definition of partition_function to a Finset sum over the universe, then applies Finset.sum_pos. The first hypothesis supplies the positivity of each term via the sibling lemma gibbs_weight_pos sys (X ω); the second hypothesis uses the nonempty universe to ensure the sum is taken over at least one element.
why it matters
This positivity result is invoked directly by the downstream theorems gibbs_measure_nonneg, gibbs_measure_pos, gibbs_measure_sum_one, gibbs_log_form, and free_energy_nonpos. It completes the finite-temperature extension of the Recognition framework, ensuring the Gibbs measure is a valid probability distribution and that free energy F = -T ln Z is nonpositive. The construction aligns with the phi-ladder discretization and the eight-tick octave that supplies the fundamental time unit in the broader T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.