jcost_boltzmann_max_at_unity
plain-language theorem explainer
The declaration proves that the J-cost Boltzmann weight equals 1 at the unity ratio for every positive temperature. Researchers connecting recognition cost to thermodynamic distributions would cite it to confirm the ground state carries maximum probability. The proof is a direct term-mode simplification that unfolds the weight definition and applies the fact that J-cost vanishes at unity.
Claim. For every real number $T > 0$, the Boltzmann weight derived from J-cost at ratio 1 equals 1.
background
The J-Cost to Thermodynamics Bridge module links the functional $J(x) = (x + x^{-1})/2 - 1$ to Boltzmann, Fermi-Dirac and Bose-Einstein distributions. Upstream lemma Jcost_unit0 records that $J(1) = 0$. The module treats temperature as the Lagrange multiplier that enforces the J-cost constraint while the eight-tick phase selects the statistics.
proof idea
Term-mode proof that unfolds jcostBoltzmann and simplifies with Jcost_unit0.
why it matters
It supplies one conjunct of the parent theorem jcost_thermo_fundamentals, which assembles the full J-cost thermodynamics: energy zero at unity, Boltzmann weight one at unity, and phase-dependent distributions. The result closes the step from J-uniqueness (T5) to equilibrium probabilities inside the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.