Jcost_one_plus_eps_quadratic
plain-language theorem explainer
The lemma establishes that J(1 + ε) expands as ε²/2 plus a cubic remainder c ε³ with |c| ≤ 2 whenever |ε| ≤ 1/2. Physicists deriving quadratic Hamiltonians from recognition cost cite this to justify the leading energy term ½ Σ ε_i². The proof rewrites J via its squared form, isolates the explicit cubic coefficient, and bounds it from the strain hypothesis using elementary inequalities.
Claim. For every 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
Jcost is defined by J(x) = (x + x^{-1})/2 - 1. An algebraically equivalent form is J(x) = (x - 1)²/(2x), obtained by clearing the denominator. The present lemma sits in the small-strain Taylor expansion section of the Cost module and supplies the local quadratic approximation near the ground state x = 1. It depends on the squared-expression lemma Jcost_eq_sq, which converts the hyperbolic definition into a rational function amenable to direct expansion.
proof idea
The proof invokes Jcost_eq_sq to replace Jcost(1 + ε) by ε²/(2(1 + ε)). It then rewrites the right-hand side as ε²/2 + c ε³ by setting c = -1/(2(1 + ε)) and verifying the identity with field_simp and ring. The coefficient bound follows from 1 + ε ≥ 1/2, which implies 1/(2(1 + ε)) ≤ 1 and therefore |c| ≤ 1 ≤ 2; the final step applies le_trans.
why it matters
This supplies the quadratic approximation that underpins Hamiltonian emergence from the recognition operator. It is invoked directly by quadratic_emergence (HamiltonianEmergence), jcost_unit_curvature (JCostGeometry), perturbation_cost_quadratic (StillnessGenerative), and hamiltonian_approximation_bound (UltramassiveBH). The result realizes the small-strain regime in which the leading energy is ½ Σ ε_i², consistent with the phi-ladder and eight-tick octave; the cubic correction quantifies the R̂-specific deviation missed by standard quadratic Hamiltonians.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Golden-ratio exponent fixes a gravity kernel, then meets 147 galaxies
"Proposition 1 (Reciprocal closure cost): J(x) = ½(x + x⁻¹) − 1, and near equilibrium x = 1+ε, J(1+ε) = ½ε² + O(ε³)"