JConvexityUniversalityCert
plain-language theorem explainer
J-cost obeys the exact identity J(r) = (r-1)^2/(2r) for r>0 together with the bound J(r) <= (r-1)^2/2 for r>=1, vanishing at r=1, inversion symmetry, and the universal sensitivity constant 1/2. Cross-domain Recognition Science work cites the structure to anchor the Hessian at every equilibrium. The declaration is a structure that assembles six component lemmas already established for J-cost.
Claim. The J-cost function satisfies $J(r) = (r-1)^2/(2r)$ for every $r>0$, the inequality $J(r) <= (r-1)^2/2$ whenever $r >= 1$, $J(1)=0$, the symmetry $J(r)=J(r^{-1})$, the universal sensitivity constant equal to $1/2$, and the quadratic identity $J(1+delta) * 2(1+delta) = delta^2$ for all $delta$ with $1+delta>0$.
background
Recognition Science defines J-cost as the deviation measure arising from the forcing chain T0-T8. The module treats J-cost as a convex function on (0, infinity) whose minimum occurs at r=1 with value zero. The universal sensitivity constant is introduced as the second-order coefficient 1/2 at this minimum, the quantity referenced by the C7 universality certificate without prior explicit computation. The supplied upstream result states that this constant equals 1/2 and serves as the meta-claim for all RS equilibria.
proof idea
The declaration is a structure definition whose fields are populated directly by six prior lemmas on J-cost: the squared-form identity, the upper bound for r at least 1, the equilibrium value, log symmetry, the equality for the sensitivity constant, and the quadratic identity. No additional tactics or reductions are performed; the structure simply packages the already-proven statements.
why it matters
The structure supplies the C25 claim that J-cost is convex with the stated local quadratic form, thereby closing the Hessian computation left open in C7. It is consumed by the downstream jConvexityUniversalityCert definition that assembles the full certificate. The result fixes the universal sensitivity coefficient at 1/2 for every RS equilibrium and supports subsequent derivations that rely on the leading-order behavior near r=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.