leading_order
plain-language theorem explainer
The declaration proves that the universal sensitivity constant multiplies any real δ squared to recover exactly δ squared over 2. Researchers expanding J-cost to quadratic order near the equilibrium r equals 1 cite this identity when fixing the Hessian coefficient. The proof is a one-line wrapper that unfolds the constant definition and normalizes the resulting polynomial equality.
Claim. For any real number $δ$, the identity $½ δ² = δ² / 2$ holds, where the coefficient ½ is the second-order sensitivity of J-cost at the equilibrium point r = 1.
background
The J-Cost Convexity Universality module establishes that J(r) = (r - 1)² / (2r) for r > 0, which is nonnegative, vanishes at r = 1, and yields the local approximation J(r) ≈ (r - 1)² / 2. The universal sensitivity constant is defined as the second-order coefficient 1/2 at equilibrium; this is the meta-claim referenced in C7. Upstream results include the identity event in ObserverForcing, which sits at the J-cost minimum with zero cost, and the definition of universalSensitivity itself.
proof idea
The proof unfolds the definition of universalSensitivity (which equals 1/2) and applies the ring tactic to verify the polynomial identity.
why it matters
This algebraic identity supplies the explicit quadratic form for J-cost near r = 1, completing the local Hessian needed for the C7 universality certificate. It supports the module's structural claim that J-cost is convex with minimum at the identity state. The result aligns with the Recognition framework's use of J-cost convexity to derive universal sensitivity across equilibria.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.