V_RS_quartic_error
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.