Jcost_one_plus_eps_quadratic
plain-language theorem explainer
The lemma establishes that for strains bounded by 1/2 the J-cost admits the expansion J(1+ε) = ε²/2 + c ε³ with |c| ≤ 2. Researchers deriving Hamiltonian emergence or unit curvature in J-cost geometry invoke it to justify the quadratic leading term. The proof rewrites Jcost via its squared-ratio identity, isolates the cubic coefficient by field simplification, and bounds the coefficient using the strain hypothesis together with elementary inequalities.
Claim. For any real number $ε$ satisfying $|ε| ≤ 1/2$, there exists a real number $c$ such that $J(1 + ε) = ε²/2 + c ε³$ and $|c| ≤ 2$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The J-cost is defined by $J(x) = (x + x^{-1})/2 - 1$. Its squared form states that $J(x) = (x-1)^2/(2x)$ for nonzero $x$. This lemma belongs to the Cost.JcostCore module, which assembles the elementary algebraic properties of J-cost used to measure deviations from unity throughout the recognition framework.
proof idea
The tactic proof first extracts bounds from the hypothesis on ε and proves 1+ε > 0. It applies the squared-form lemma to obtain Jcost(1+ε) = ε²/(2(1+ε)). Field simplification and ring tactics rearrange this into ε²/2 plus the cubic term whose coefficient is -1/(2(1+ε)). The absolute value of the coefficient is shown ≤1 by comparing the denominator against 2, which immediately yields the bound of 2.
why it matters
This supplies the controlled quadratic approximation required by downstream results on small-strain regimes. It is invoked directly by quadratic_emergence in HamiltonianEmergence, jcost_unit_curvature in JCostGeometry, perturbation_cost_quadratic in StillnessGenerative, and hamiltonian_approximation_bound in UltramassiveBH. In the framework it justifies the leading ½ Σ ε_i² energy term near the ground state, consistent with J-uniqueness and the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.