jcost_quartic_error
plain-language theorem explainer
The quartic Taylor remainder for J(exp ε) satisfies |J(exp ε) − ε²/2 − ε⁴/24| ≤ exp(|ε|) |ε|⁶ for every real ε. Effective-field theorists matching recognition cost to the Higgs potential cite the bound to control O(h⁶) corrections in the effective potential. The proof is a short tactic sequence that rewrites via the upstream cosh identity and applies the sibling cosh_quartic_error lemma.
Claim. For any real number ε, |J(exp ε) − ε²/2 − ε⁴/24| ≤ exp(|ε|) · |ε|⁶, where J(x) = ½(x + x⁻¹) − 1.
background
The Higgs EFT Bridge module constructs the first link of the chain RS cost geometry → effective scalar coordinate → canonical Higgs EFT. The recognition-cost potential is V_RS Λ v h := Λ⁴ J(exp(h/v)), with J the reciprocal cost functional J(x) = ½(x + x⁻¹) − 1. The identity J(exp ε) = cosh ε − 1 is supplied by the upstream lemma Jcost_exp_cosh from the Cost module. This theorem supplies the precise remainder after the quadratic and quartic terms in the expansion around the vacuum.
proof idea
The tactic proof first applies Jcost_exp_cosh to replace Jcost(exp ε) by cosh ε − 1, rewrites the left-hand side of the target inequality to match the form handled by cosh_quartic_error, and concludes by exact application of that bound.
why it matters
The result is invoked directly by the downstream theorem V_RS_quartic_error, which bounds the approximation error of V_RS by its quartic truncation on |h| ≤ v/2. It thereby justifies the SM-to-RS dictionary m_H² = Λ⁴/v² and λ_SM = Λ⁴/(6 v⁴) given in the module documentation. Within the Recognition Science framework it completes the Taylor truncation step required by J-uniqueness (T5) and the self-similar fixed point (T6) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.