Jcost_small_strain_bound
plain-language theorem explainer
The lemma supplies a uniform cubic-error bound showing that J-cost stays within 10 percent of its quadratic approximation ε²/2 whenever the strain satisfies |ε| ≤ 1/10. It is invoked by Taylor expansions of action functionals and by small-strain Hamiltonian statements in gravitational models. The proof rewrites Jcost via its squared-ratio identity, isolates the exact cubic remainder -ε³/(2(1+ε)), and compares rational bounds derived from the strain hypothesis.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. For real $ε$ satisfying $|ε| ≤ 1/10$, $|J(1+ε) - ε²/2| ≤ ε²/10$.
background
The J-cost function is defined by Jcost(x) = (x + x^{-1})/2 - 1. The upstream lemma Jcost_eq_sq rewrites it as the squared ratio (x-1)²/(2x) for x ≠ 0. The present statement quantifies the deviation of this cost from its leading quadratic term near the minimum at unity. The local setting is the cost module of Recognition Science, where J-cost measures deviation from the self-similar fixed point and supplies the leading term in quadratic action limits.
proof idea
The tactic proof begins by extracting the absolute-value bounds from hε and proving positivity of 1+ε. It applies Jcost_eq_sq to obtain Jcost(1+ε) = ε²/(2(1+ε)). Algebraic simplification then yields the exact difference -ε³/(2(1+ε)). The absolute value becomes |ε|³/(2(1+ε)). From |ε| ≤ 1/10 one derives 1+ε ≥ 9/10, hence 1/(2(1+ε)) ≤ 5/9. Scaling the strain bound produces |ε|/(2(1+ε)) ≤ 1/18. Multiplication by |ε|² gives the cubic remainder ≤ |ε|²/18, which is finally compared with the target |ε|²/10.
why it matters
The result is called directly by Jcost_taylor_quadratic in Action.QuadraticLimit, by perturbation_cost_small_bound in StillnessGenerative, and by small_strain_hamiltonian_valid in Gravity.UltramassiveBH. It supplies the concrete error control that justifies replacing the full J-cost by its quadratic approximation in perturbation analyses and effective Hamiltonians. Within the Recognition framework it closes the local analytic step between the exact J-cost definition and the quadratic regime used for small deviations from the unit fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
One golden-ratio curve organizes four periodic-table trends at once
"Near ρ = 0, J_chem(ρ) ≈ ½(ln φ)² ρ² ≈ 0.116 ρ²; this small-step expansion is used in the noble-gas ratio derivation"