jcost_unit_curvature
plain-language theorem explainer
J-cost near the identity admits a quadratic approximation J(1+ε) = ε²/2 + c ε³ with |c|≤2 for |ε|≤1/2. Foundation paper F1 authors cite this when establishing unit curvature from the second derivative at x=1. The proof reduces directly to the pre-established quadratic expansion lemma for the J-cost function.
Claim. For any real ε with |ε| ≤ 1/2 there exists c ∈ ℝ such that J(1 + ε) = ε²/2 + c ε³ and |c| ≤ 2, where J(x) := ½(x + x⁻¹) − 1.
background
The module develops log-domain geometry for the reciprocal cost J(x) = ½(x + x⁻¹) − 1. At x = 1 the cost vanishes and the second derivative equals 1, which is the unit curvature. The identity event is defined to sit exactly at this minimum. The upstream lemma Jcost_one_plus_eps_quadratic supplies the explicit expansion J(1 + ε) = ε²/2 + c ε³ together with the uniform bound |c| ≤ 2 whenever |ε| ≤ 1/2.
proof idea
The proof is a one-line term wrapper that applies the lemma Jcost_one_plus_eps_quadratic directly to the given ε and bound hε.
why it matters
The declaration fills F1.1.6 of the foundation paper by confirming unit curvature at the J-cost minimum. It supports the subsequent cosh identity (F1.1.7) and the geometric-mean optimality results listed in the module. Within the Recognition framework this curvature anchors the phi-ladder construction and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.