sensitivity_at_one
plain-language theorem explainer
J-cost vanishes exactly at the equilibrium ratio r=1. Cross-domain RS analyses cite this to anchor the minimum of the cost functional inside the convexity universality certificate. The proof is a direct term application of the upstream Jcost unit lemma.
Claim. $J(1)=0$, where $J(r)=((r-1)^2)/(2r)$ for $r>0$.
background
The module states that J-cost is convex on the positive reals with global minimum at r=1. The explicit identity is J(r) equals (r minus 1) squared over 2r, which is nonnegative everywhere and yields the universal leading-order sensitivity coefficient of one half near equilibrium. Upstream, the lemma Jcost_unit0 in the Cost module proves the same identity by simplification on the definition of Jcost, as recorded in its doc-comment: J(x) expressed as a squared ratio.
proof idea
The proof is a one-line term wrapper that applies the lemma Jcost_unit0 from the Cost module.
why it matters
This declaration supplies the at_equilibrium field inside the jConvexityUniversalityCert definition. It verifies the zero minimum required by the C25 structural claim for wave-64 cross-domain applications and supports the Recognition Science assertion that all equilibria share the same leading-order cost coefficient of one half. The result closes the local quadratic form referenced by the Hessian in the module without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.