universalSensitivity_eq
plain-language theorem explainer
The universal sensitivity constant is fixed at one half as the quadratic coefficient in the J-cost expansion around equilibrium. Researchers citing the C25 convexity universality or the C7 meta-claim reference this equality to anchor the leading-order cost of small deviations. The proof is a one-line reflexivity that follows immediately from the definition of the constant.
Claim. The universal sensitivity constant equals $1/2$, which is the second-order coefficient such that the leading-order J-cost of a small deviation $ε = r - 1$ is $ε^2/2$.
background
The module C25 treats J-cost convexity on $(0, ∞)$ with a minimum of zero at ratio $r = 1$. The explicit identity $J(r) = (r-1)^2/(2r)$ yields the local quadratic $J(r) ≈ (r-1)^2/2$ near equilibrium, fixing the sensitivity coefficient at $1/2$. Upstream results define the cost of any recognition event as its J-cost and introduce universalSensitivity directly as the constant $1/2$ to encode the meta-claim referenced in C7.
proof idea
The proof is a one-line term proof that applies reflexivity to the definition of universalSensitivity.
why it matters
This equality supplies the sensitivity_constant field inside jConvexityUniversalityCert, completing the structural claim for C25. It anchors the second-order coefficient at equilibrium that is referenced in C7 and fixes the leading-order cost scale for small deviations in RS equilibria.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.