jcost_ground_state
plain-language theorem explainer
J-cost vanishes if and only if its argument equals 1, for every positive real. Workers on thermodynamic selection in Recognition Science cite the result as the equilibrium condition that forces entropy non-decrease on closed ledgers. The proof splits the biconditional, derives a contradiction from positivity away from 1, and evaluates the unit case directly.
Claim. For every real number $x > 0$, the J-cost function satisfies $J(x) = 0$ if and only if $x = 1$.
background
J-cost is the recognition cost on the multiplicative group of positive reals, given explicitly by $J(x) = (x-1)^2/(2x)$. The ThermodynamicSelectionCert module encodes the pre-Big-Bang claim that the second law emerges as a selection principle: on a closed ledger, J-cost cannot decrease along any recognition path. Upstream lemmas establish strict positivity of J away from 1 and the evaluation J(1) = 0.
proof idea
The term proof constructs the two directions of the biconditional. The left-to-right direction assumes J(x) = 0 and x ≠ 1, then invokes the positivity lemma to reach a contradiction. The right-to-left direction substitutes x = 1 and applies the unit evaluation lemma.
why it matters
The theorem populates the ground_state field inside the ThermodynamicSelectionCert structure that certifies monotone recognition selection. It supplies the unique-minimum property required by the module's statement of the second-law selection principle. The parent certificate combines this fact with entropy-floor and divergence statements to close the thermodynamic argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.