partition_pos
plain-language theorem explainer
The partition function summing J-cost Boltzmann factors over a finite nonempty collection of positive ratios at positive temperature is strictly positive. Thermodynamic derivations in Recognition Science cite this to guarantee normalizable probabilities and well-defined free energies. The proof unfolds the sum definition and applies Finset.sum_pos using the positivity of each Boltzmann term plus the nonempty index set.
Claim. Let $Z = Z(r_1, r_2, ..., r_n, T)$ denote the partition function $Z = sum_{i=1}^n exp(-J(r_i)/T)$ where each ratio $r_i > 0$, temperature $T > 0$, and $n > 0$. Then $Z > 0$.
background
The J-Cost to Thermodynamics Bridge module formalizes how Recognition Science's J-cost functional $J(x) = 1/2(x + 1/x) - 1$ generates thermodynamic distributions. The partition function aggregates Boltzmann weights derived from J-cost ratios, with $T$ serving as the Lagrange multiplier enforcing the cost constraint. This setting connects J-cost minimization to free-energy minimization and links eight-tick phases to spin-statistics distributions.
proof idea
The term proof unfolds partitionFunction to expose a Finset sum, then applies Finset.sum_pos. The positivity subgoal for each summand is discharged by jcost_boltzmann_pos using the ratio positivity and $T > 0$ hypotheses. The nonempty subgoal follows from the $n > 0$ hypothesis via simp on Finset.univ_nonempty_iff.
why it matters
This supplies the partition_pos field inside HelmholtzRealCert, which certifies the identity $F = E - TS$ for the Helmholtz free energy. It completes a required step for the module's main theorems on Boltzmann weights minimizing expected J-cost. The result supports the framework's derivation of thermodynamic laws from the forcing chain and ledger balance without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.