universalSensitivity
The universal sensitivity constant is defined as exactly 1/2, supplying the quadratic coefficient in the J-cost expansion at equilibrium. Cross-domain analysts cite it when certifying the Hessian scale for all Recognition Science equilibria under C7. The declaration is introduced by direct assignment with no computation or lemmas required.
claimThe second-order coefficient in the expansion of the J-cost function near its minimum at unity equals $1/2$.
background
The module establishes that the J-cost satisfies the identity J(r) = (r - 1)^2 / (2 r) for r > 0. This expression is nonnegative, vanishes at r = 1, and expands locally to (r - 1)^2 / 2 because the factor 1/(2r) approaches 1/2. The universal sensitivity constant therefore records the precise leading-order scale for small symmetric deviations from equilibrium.
proof idea
The declaration is a direct definition that assigns the literal value 1/2. No lemmas, tactics, or reductions are applied.
why it matters in Recognition Science
The constant is referenced in the C7 meta-claim and appears as the sensitivity_constant field inside the JConvexityUniversalityCert structure. It is invoked by the leading_order theorem to equate sensitivity times delta squared with delta squared over 2, and by the reflexivity equality theorem. In the Recognition framework it supplies the universal quadratic scale that closes the local analysis of J-cost convexity begun in the Cost module.
scope and limits
- Does not derive the coefficient from the full J-cost identity.
- Does not address terms beyond the quadratic order.
- Does not specify the range of validity for the approximation.
- Does not link to the forcing chain steps T5-T8.
Lean usage
theorem leading_order (δ : ℝ) : universalSensitivity * δ^2 = δ^2 / 2 := by unfold universalSensitivity; ringformal statement (Lean)
67noncomputable def universalSensitivity : ℝ := 1 / 2
proof body
Definition body.
68