small_strain_hamiltonian_valid
plain-language theorem explainer
The declaration bounds the deviation of Jcost(1 + ε) from its quadratic approximation ε²/2 by at most ε²/10 whenever |ε| ≤ 1/10. Researchers modeling ultramassive black holes in Recognition Science cite it to delimit the regime where the effective Hamiltonian approximates the recognition operator. The proof is a one-line wrapper that applies the core Jcost small-strain bound lemma.
Claim. For every real ε with |ε| ≤ 1/10, |J(1 + ε) - ε²/2| ≤ ε²/10, where J is the J-cost function.
background
In Recognition Science the J-cost function J(x) = (x + x^{-1})/2 - 1 measures recognition cost for a scaling factor x. The small-strain regime concerns expansions around x = 1, where the quadratic term dominates and higher-order corrections remain controlled. This theorem sits inside the Ultramassive Black Holes module, whose setting formalizes black-hole interiors as maximal J-cost states rather than curvature singularities and derives the RS entropy S_BH = (ln φ) · A/(4ℓ₀²) together with the Hawking temperature in native units.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_small_strain_bound ε hε from the Cost.JcostCore module.
why it matters
The result supplies the Hamiltonian Approximation Bound stated in the module: Ĥ emerges from R̂ only inside the small-strain regime |ε| ≪ 1, rendering the Eddington limit an artifact of that approximation. It feeds the no-singularity theorem and the RS entropy formula already proved in the same file. The bound connects directly to the Recognition Science forcing chain at the level of the recognition operator and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.