low_temp_selection
plain-language theorem explainer
Researchers modeling low-temperature selection in Recognition Science thermodynamics cite the strict positivity of J-cost away from the ground state at x=1. This supplies the prerequisite that excited states carry positive cost, enabling dominance of the ground state in the Boltzmann limit. The proof is a direct term reduction that rewrites J-cost via its squared algebraic form and verifies the resulting fraction is positive.
Claim. For every real number $x > 0$ with $x ≠ 1$, the J-cost satisfies $J(x) > 0$, where $J(x) = (x-1)^2/(2x)$.
background
The J-cost arises from the Recognition Composition Law and equals $(x + x^{-1})/2 - 1$, which is algebraically identical to the squared ratio $(x-1)^2/(2x)$ for $x ≠ 0$. This module builds the bridge from J-cost to Boltzmann statistical mechanics for RecognitionSystems, supplying Gibbs weights, partition functions, and free energies with $x=1$ as the zero-cost ground state. The upstream lemma Jcost_eq_sq supplies the squared expression used throughout the module.
proof idea
The term proof invokes the lemma Jcost_eq_sq to replace Jcost x by $(x-1)^2/(2x)$. It then applies div_pos, using sq_pos_iff to obtain positivity of the numerator from $x ≠ 1$ and mul_pos (with norm_num) to obtain positivity of the denominator from $x > 0$.
why it matters
This result is invoked by ground_state_dominates to prove the Gibbs weight at $x=1$ strictly exceeds the weight at any other $x$, and it is packaged into the JCostBoltzmannCert that collects all bridge theorems. It realizes the low-temperature selection step in the J-Cost Boltzmann bridge, aligning with T5 J-uniqueness in the forcing chain where the fixed point at unity has zero cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.