universalSensitivity_eq
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the coefficient from an independent expansion.
- Does not compute J-cost at finite deviations.
- Does not address higher-order terms in the Taylor series.
- Does not incorporate specific values of phi or other RS constants.
formal statement (Lean)
69theorem universalSensitivity_eq : universalSensitivity = 1 / 2 := rfl
proof body
Term-mode proof.
70
71/-- The leading-order J-cost is sensitivity × δ². -/