jcostTaylorQuadraticCoefficient_eq
plain-language theorem explainer
The theorem asserts that the Taylor quadratic coefficient of the J-cost at equilibrium equals exactly 1/2. Workers on local expansions in the Recognition Science C7 module cite it to fix the Hessian normalization. The proof is a direct reflexivity reduction to the coefficient definition.
Claim. The quadratic coefficient in the Taylor expansion of the J-cost function around equilibrium is $1/2$.
background
The C7 module records the exact local algebraic kernel $J(1 + eps) = eps^2 / (2(1 + eps))$ for the J-cost, which is stronger than a second-order Taylor claim away from the singularity at eps = -1. The Taylor quadratic coefficient is defined as the leading eps^2 prefactor in this expansion, set to 1/2. The upstream definition in the same module fixes jcostTaylorQuadraticCoefficient : ℝ := 1/2, and the module avoids Mathlib derivative machinery by working directly with this algebraic identity.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of the Taylor quadratic coefficient.
why it matters
This equality supplies the coefficient_half field inside the JCostHessianCert structure. It completes the local Hessian normalization for the C7 claim in the Recognition Science framework, confirming the standard Taylor convention that the Hessian equals twice the quadratic coefficient. The result anchors the exact kernel identity without higher-order terms or derivative APIs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.