V_RS_quartic_error
V_RS_quartic_error supplies a uniform bound on the approximation error between the recognition cost potential and its quartic Taylor polynomial inside the disk |h| ≤ v/2. An effective field theorist matching the RS substrate to the Standard Model Higgs sector would cite the bound to control O(h^6) corrections in the effective potential. The argument rescales to the dimensionless variable ε = h/v, applies the pre-established quartic error lemma for Jcost, and factors out the positive prefactor |Λ|^4.
claimFor real numbers $Λ$, $v$, $h$ with $v > 0$ and $|h| ≤ v/2$, $|V_{RS}(Λ, v, h) - V_{RS,quartic}(Λ, v, h)| ≤ |Λ|^4 ⋅ exp(|h/v|) ⋅ |h/v|^6$, where $V_{RS}(Λ, v, h) = Λ^4 ⋅ Jcost(exp(h/v))$ and $V_{RS,quartic}$ retains only the quadratic and quartic terms in the Taylor expansion of $Jcost(exp ε)$ about ε = 0.
background
The Higgs EFT Bridge module defines the recognition cost potential as $V_{RS}(Λ, v, h) := Λ^4 ⋅ Jcost(exp(h/v))$, where the cost functional satisfies $Jcost(exp ε) = cosh ε - 1$. The quartic truncation $V_{RS,quartic}(Λ, v, h)$ is obtained by retaining only the ε²/2 + ε⁴/24 terms in the expansion of $Jcost(exp ε)$ about the vacuum. This bound justifies truncation of the effective potential when matching onto the Standard Model form ½ m_H² h² + (λ_SM/4) h⁴ + ⋯ inside the region containing the electroweak vacuum. The upstream result jcost_quartic_error provides the core remainder estimate |Jcost(exp ε) - ε²/2 - ε⁴/24| ≤ exp|ε| ⋅ |ε|^6 that is lifted to the dimensionful potential by the algebraic identity shown in the proof.
proof idea
The proof first establishes the auxiliary bound |ε| ≤ 1/2 where ε = h/v from the hypothesis |h| ≤ v/2 and v > 0. It then applies the lemma jcost_quartic_error to obtain the dimensionless remainder. Unfolding the definitions of V_RS and V_RS_quartic, a ring identity rewrites the difference as Λ^4 times the Jcost remainder. Taking absolute values, using |Λ^4| = |Λ|^4 and non-negativity of |Λ|^4, the core bound is multiplied through to yield the stated inequality.
why it matters in Recognition Science
The bound is invoked inside higgsEFTBridgeCert as the quartic_remainder component of the bridge certificate. It completes the first two arrows of the chain from RS cost geometry through the effective scalar coordinate to the canonical Higgs EFT, as described in the module documentation. Within the Recognition Science framework the result supplies the error control required to extract the forced quadratic and quartic coefficients that match onto the Standard Model mass and self-coupling terms, consistent with J-uniqueness in the forcing chain.
scope and limits
- Does not extend the bound beyond the disk |h| ≤ v/2.
- Does not fix the numerical value of the scale Λ.
- Does not derive the explicit values of the Higgs mass or quartic coupling.
- Does not address quantum corrections or renormalization.
formal statement (Lean)
156theorem V_RS_quartic_error (Λ v h : ℝ) (hv : 0 < v) (hbound : |h| ≤ v / 2) :
157 |V_RS Λ v h - V_RS_quartic Λ v h|
158 ≤ |Λ| ^ 4 * (Real.exp |h / v| * |h / v| ^ 6) := by
proof body
Tactic-mode proof.
159 have hε : |h / v| ≤ 1 / 2 := by
160 rw [abs_div, abs_of_pos hv]
161 rw [div_le_iff₀ hv]
162 linarith
163 have hcore := jcost_quartic_error (h / v)
164 -- |V_RS − V_RS_quartic| = |Λ|^4 · |J(exp ε) − ε²/2 − ε⁴/24|
165 unfold V_RS V_RS_quartic
166 set ε := h / v
167 have hL : Λ ^ 4 * Jcost (Real.exp ε) - Λ ^ 4 * (ε ^ 2 / 2 + ε ^ 4 / 24)
168 = Λ ^ 4 * (Jcost (Real.exp ε) - ε ^ 2 / 2 - ε ^ 4 / 24) := by ring
169 rw [hL, abs_mul]
170 have hΛ : |Λ ^ 4| = |Λ| ^ 4 := by rw [abs_pow]
171 rw [hΛ]
172 have hΛ4 : 0 ≤ |Λ| ^ 4 := by positivity
173 exact mul_le_mul_of_nonneg_left hcore hΛ4
174
175/-- The leading quadratic coefficient is forced: `Λ⁴ / (2 v²)`. -/