jcostBoltzmannCert
plain-language theorem explainer
jcostBoltzmannCert packages the five core properties of Gibbs weights under the J-cost function into one certificate structure for biological thermodynamics. A researcher modeling selection pressure in recognition systems would cite it to invoke normalization at the ground state, maximization, symmetry, strict dominance, and cost positivity together. The definition is a direct record construction that assigns each field to a prior lemma.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ be the J-cost. The certificate asserts that for any RecognitionSystem sys and $x > 0$, the Gibbs weight $w(x)$ satisfies $w(1) = 1$, $w(x) ≤ w(1)$, $w(x) = w(x^{-1})$, and $w(x) < w(1)$ whenever $x ≠ 1$; additionally $J(x) > 0$ for all $x ≠ 1$.
background
The J-Cost Boltzmann Bridge module connects the J-cost function to Boltzmann statistical mechanics for biology-facing results. It builds on RecognitionThermodynamics, which supplies gibbs_weight, partition_function, and free_energy. The module adds weight maximization at the ground state $x=1$, symmetry under $x ↔ 1/x$, monotonicity in J-cost, and temperature-dependent selection, all packaged in the JCostBoltzmannCert structure.
proof idea
This is a record definition that constructs an instance of JCostBoltzmannCert. It assigns weight_at_one to weight_at_ground_state, weight_max to weight_maximized_at_one, weight_sym to weight_symmetric, ground_dominates to ground_state_dominates, and cost_positive to low_temp_selection.
why it matters
The definition supplies the single interface for the thermodynamic bridge results derived from J-uniqueness and the recognition composition law. It collects the lemmas needed to model ground-state dominance as strong selection at low temperature in biological systems. No downstream uses are recorded yet, and it closes the packaging step without addressing open questions on high-temperature regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.