partitionFunction
plain-language theorem explainer
PartitionFunction sums the J-cost Boltzmann factors across a finite set of positive ratios at positive temperature. Thermodynamic derivations in the Recognition Science framework cite it when converting J-cost constraints into standard partition functions. The definition reduces to a direct sum over the per-ratio Boltzmann weights supplied by jcostBoltzmann.
Claim. For positive ratios $r_1, dots, r_n > 0$ and temperature $T > 0$, the partition function is $Z = sum_{i=1}^n w(r_i, T)$, where $w(r, T)$ is the Boltzmann weight obtained from the J-cost of ratio $r$ at temperature $T$.
background
The J-Cost to Thermodynamics Bridge module links Recognition Science's J-cost functional $J(x) = (x + x^{-1})/2 - 1$ to thermodynamic distributions. Temperature $T$ serves as the Lagrange multiplier enforcing the J-cost constraint. The module states that the Boltzmann factor emerges as the distribution minimizing average J-cost subject to constraints. Upstream, the standard partition function in BoltzmannDistribution is the sum of factors exp(-β E_i). This version substitutes the J-cost evaluated on the supplied ratios.
proof idea
The definition is a one-line wrapper. It applies Finset.univ.sum to the function that calls jcostBoltzmann on each ratio, using the positivity hypotheses to satisfy the preconditions of jcostBoltzmann.
why it matters
This supplies the partition function required by downstream definitions of average energy, entropy, and free energy in BoltzmannDistribution. It fills the bridge step that converts J-cost minimization into the standard thermodynamic potentials. The construction supports the link from J-uniqueness through the eight-tick structure to spin-statistics and Fermi/Bose distributions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.