cosh_quartic_error
plain-language theorem explainer
The declaration proves the quartic remainder bound |cosh ε − 1 − ε²/2 − ε⁴/24| ≤ exp|ε| ⋅ |ε|⁶ for every real ε. Effective field theorists matching the recognition cost potential to the Higgs Lagrangian cite it to control truncation errors when extracting quadratic and quartic coefficients. The proof averages the sixth-order exponential truncation bounds on exp ε and exp(−ε), then applies the triangle inequality together with algebraic cancellation.
Claim. For every real number $ε$, $|cosh ε - 1 - ε²/2 - ε⁴/24| ≤ exp(|ε|) ⋅ |ε|⁶$.
background
In the HiggsEFTBridge module the recognition-cost potential is V_RS(Λ, v, h) := Λ⁴ ⋅ J(exp(h/v)), where J(x) = (x + x^{-1})/2 − 1 is the reciprocal cost functional obeying the Recognition Composition Law. Substituting the exponential coordinate ε = h/v yields J(exp ε) = cosh ε − 1, so the vacuum expansion begins with the quadratic and quartic terms later matched to the Standard-Model parameters m_H² and λ_SM. The module documentation states that this supplies the first two arrows of the RS-to-SM dictionary.
proof idea
The proof introduces the auxiliary polynomial P(t) = 1 + t + t²/2 + t³/6 + t⁴/24 + t⁵/120. It invokes the upstream lemma exp_sub_trunc6_le on both ε and −ε to bound the respective remainders. A ring calculation shows that P(ε) + P(−ε) equals twice the quartic truncation of cosh. The error is rewritten as the average of the two exponential remainders; the triangle inequality followed by division by two yields the stated bound.
why it matters
This theorem supplies the error control required by the downstream jcost_quartic_error theorem, which translates the bound into J-cost language for the Higgs potential. It completes the Taylor-coefficient extraction step described in the module documentation, where the quadratic and quartic coefficients determine m_H² = Λ⁴/v² and λ_SM = Λ⁴/(6 v⁴). Within the Recognition Science framework it instantiates the J-uniqueness property (T5) that forces the cosh representation of the cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.