jConvexityUniversalityCert
plain-language theorem explainer
The J-cost convexity certificate assembles six properties of the recognition cost function into one structure: the exact squared representation, an upper bound for arguments at least one, vanishing at equilibrium, log symmetry, the universal sensitivity constant of one half, and the quadratic identity. Researchers working on equilibrium stability or cross-domain scaling in Recognition Science cite it to invoke the full convexity package at once. The definition is a direct construction that populates the structure fields from six supporting lemm
Claim. The certificate asserts that the J-cost function satisfies $J(r) = (r-1)^2/(2r)$ for all $r>0$, $J(r) ≤ (r-1)^2/2$ for $r ≥ 1$, $J(1)=0$, $J(r)=J(r^{-1})$ for $r>0$, the universal sensitivity equals $1/2$, and the identity $J(1+δ)·2(1+δ)=δ^2$ whenever $1+δ>0$.
background
In module C25 the J-cost is the recognition cost $J(r)=(r + r^{-1})/2 - 1$, nonnegative on the positive reals and minimized at $r=1$. The module proves its convexity and the local quadratic behavior that sets the universal sensitivity. The upstream structure JConvexityUniversalityCert is the container that collects these facts into a single object. The six component theorems each establish one field of that structure.
proof idea
The definition constructs an instance of JConvexityUniversalityCert by direct field assignment. It sets squared_form to the result of jcost_squared_form, upper_bound to jcost_upper_bound_at_geq_one, at_equilibrium to sensitivity_at_one, log_symmetry to jcost_log_symmetric, sensitivity_constant to universalSensitivity_eq, and quadratic_identity to jcost_quadratic_identity. No further reasoning or tactics are used.
why it matters
This certificate completes the C25 structural claim on J-cost convexity and supplies the Hessian computation referenced by the C7 universality certificate. It encodes the universal sensitivity constant of one half that governs leading-order deviations from equilibrium in all Recognition Science domains. The structure is intended for cross-domain scaling arguments, though no downstream uses are recorded yet. It directly implements the key identity $J(r)=(r-1)^2/(2r)$ and its immediate consequences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.