quartic_coupling_from_normalization
plain-language theorem explainer
The theorem shows that under the normalization hypothesis equating the recognition scale Λ to the Higgs mass and vev, the quartic coefficient extracted from the RS potential satisfies 4 λ_canonical(Λ, v) = m_H² / (6 v²). Particle physicists matching recognition-derived potentials to the Standard Model Higgs sector would cite this when fixing the quartic coupling. The proof is a direct algebraic reduction that substitutes the hypothesis into the canonical coefficient definition and simplifies via field operations.
Claim. Under the normalization hypothesis Λ⁴ = m_H² v² with v > 0, the quartic coefficient λ_canonical(Λ, v) extracted from the recognition-cost potential satisfies 4 λ_canonical(Λ, v) = m_H² / (6 v²).
background
The module maps recognition cost geometry to the Higgs effective field theory. The potential takes the form V_RS Λ v h := Λ⁴ · J(exp(h/v)) where J(x) = ½(x + x⁻¹) − 1. Taylor expansion around the vacuum produces the quadratic term Λ⁴/(2 v²) h² and the quartic term Λ⁴/(24 v⁴) h⁴. The normalization hypothesis is the defining relation Λ⁴ = m_H² v² that identifies the SM mass parameter and converts the quartic coefficient into λ_SM/4. Upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the underlying J-cost functional.
proof idea
The proof unfolds quartic_coefficient_canonical and NormalizationHypothesis. It records that v² and v⁴ are nonzero, rewrites the hypothesis, then applies field_simp and ring to obtain the identity.
why it matters
This supplies the quartic matching clause feeding the master bridge certificate higgsEFTBridgeCert. It closes the explicit link from RS cost geometry through the J-expansion to the canonical SM quartic coupling, as stated in the module documentation. The result leaves the determination of Λ from the phi-ladder yardstick as the remaining open collider-normalisation problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.