Jcost_small_strain_bound
plain-language theorem explainer
Recognition Science employs the J-cost to quantify deviation from the unit fixed point. This lemma supplies the uniform error bound |J(1 + ε) - ε²/2| ≤ ε²/10 whenever |ε| ≤ 1/10, enabling quadratic approximations in effective actions and Hamiltonians. It is invoked in the QuadraticLimit module for Taylor expansions, in StillnessGenerative for perturbation bounds, and in UltramassiveBH for small-strain validity checks. The proof reduces the difference via the squared-ratio identity, isolates the cubic remainder, and applies denominator bounds 1/
Claim. For real ε with |ε| ≤ 1/10, |J(1 + ε) - ε²/2| ≤ ε²/10, where J(x) := (x + x^{-1})/2 - 1.
background
J-cost is the Recognition Science functional J(x) = (x + x^{-1})/2 - 1 that vanishes at the self-similar fixed point x = 1 and measures scale deviation. The sibling lemma Jcost_eq_sq rewrites it exactly as (x - 1)²/(2x) for x ≠ 0. This result lives in the Cost domain and supplies the concrete error control needed to justify quadratic truncation near the minimum. It depends on the arithmetic lemmas add_assoc and add_comm together with the primitive distinction axioms that underwrite the real-number field operations.
proof idea
Tactic proof begins by calling Jcost_eq_sq to obtain Jcost(1 + ε) = ε²/(2(1 + ε)). The exact difference is then simplified by field_simp and ring to -ε³/(2(1 + ε)). Absolute value yields |ε|³/(2(1 + ε)). From |ε| ≤ 1/10 the proof derives 1/(1 + ε) ≤ 10/9, hence 1/(2(1 + ε)) ≤ 5/9. Multiplying through by |ε| produces the factor 1/18, so the cubic term is ≤ ε²/18. The final comparison 1/18 ≤ 1/10 closes the bound.
why it matters
The bound is the direct parent of Jcost_taylor_quadratic, which rebrands it for the quadratic action limit, and of small_strain_hamiltonian_valid, which uses it to certify Ĥ ≈ R̂ for ultramassive black holes. It also feeds perturbation_cost_small_bound in the generative stillness setting. Within the framework it quantifies the regime where the quadratic term dominates before cubic corrections appear, consistent with the J-uniqueness fixed point and the small-strain window prior to the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.