JCostBoltzmannCert
plain-language theorem explainer
The JCostBoltzmannCert structure packages five properties of the Gibbs weight w(x) = exp(-J(x)/TR) for any recognition system: normalization at the ground state, global maximization at x=1, inversion symmetry, strict dominance of the ground state, and positivity of J away from 1. Statistical mechanicians or biologists working within Recognition Science cite it to justify low-temperature selection and free-energy bounds. It is realized as a bare structure definition that assembles five lemmas already established in the module.
Claim. Let $w(x) = e^{-J(x)/T_R}$ be the Gibbs weight for a recognition system with $T_R > 0$. The certificate asserts $w(1) = 1$, $w(x) ≤ w(1)$ for all $x > 0$, $w(x) = w(x^{-1})$ for all $x > 0$, $w(x) < w(1)$ whenever $x > 0$ and $x ≠ 1$, and $J(x) > 0$ whenever $x ≠ 1$.
background
The module supplies the J-cost Boltzmann bridge that links the Recognition Science J-cost function to classical statistical mechanics. A RecognitionSystem is a structure containing a single positive real parameter TR that sets the noise level; its beta is the inverse temperature. The upstream gibbs_weight definition supplies the explicit factor exp(-Jcost(x)/TR), which is always positive.
proof idea
The declaration is a structure definition with an empty proof body. It functions as a packaging record whose five fields are populated by the sibling lemmas weight_at_ground_state, weight_maximized_at_one, weight_symmetric, ground_state_dominates, and low_temp_selection.
why it matters
The certificate completes the biology-facing thermodynamic bridge by collecting the weight properties required for ground-state dominance and non-positive free energy. It is instantiated by the downstream jcostBoltzmannCert definition. In the larger framework it supplies the statistical-mechanics layer that connects J-uniqueness to the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.