J_one
plain-language theorem explainer
The theorem establishes that the recognition cost J vanishes exactly at the identity ratio. Chemists and acousticians cite it to mark the zero-cost matched state in activation barriers and therapy thresholds. The proof is a one-line wrapper that unfolds the definition of J and normalizes the arithmetic.
Claim. $J(1) = 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The J-cost is the canonical recognition cost J(x) := ½(x + 1/x) - 1. This module supplies the six reusable clauses of the J-cost-on-ratio template used by every domain cert in the master chain. The upstream ActivationEnergy result records the identical identity for reactant minima via the same definition.
proof idea
One-line wrapper that unfolds the definition of J and normalizes the resulting arithmetic expression to zero.
why it matters
This supplies the matched_zero clause inside the CanonicalCert definition. It is invoked by eight downstream results including barrier_nonneg in ActivationEnergy, matched_at_safe in UltrasoundTherapyThresholdFromJCost, and the enzyme catalysis theorems. The clause anchors the minimum-cost point required by the Recognition Composition Law and the six-clause template.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.