jcost_quartic_error
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit quartic approximation polynomial.
- Does not restrict ε to small values; the bound holds for all real ε.
- Does not incorporate the dimensionful scales Λ or v into the error estimate.
- Does not address renormalization or higher-dimensional operators.
- Does not connect to the full Standard-Model gauge sector or collider observables.
formal statement (Lean)
142theorem jcost_quartic_error (ε : ℝ) :
143 |Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24| ≤ Real.exp |ε| * |ε| ^ 6 := by
proof body
Tactic-mode proof.
144 have h := cosh_quartic_error ε
145 have hcosh : Jcost (Real.exp ε) = Real.cosh ε - 1 := Cost.Jcost_exp_cosh ε
146 -- |Jcost(exp ε) - ε²/2 - ε⁴/24| = |cosh ε - 1 - ε²/2 - ε⁴/24|
147 have hrewrite :
148 Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24
149 = Real.cosh ε - 1 - ε ^ 2 / 2 - ε ^ 4 / 24 := by
150 rw [hcosh]
151 rw [hrewrite]
152 exact h
153
154/-- The error in approximating `V_RS` by its quartic Taylor polynomial is
155 bounded uniformly on `|h| ≤ v / 2`. -/