NormalizationHypothesis
plain-language theorem explainer
NormalizationHypothesis encodes the equality linking the recognition scale to the Higgs mass and electroweak vev. Collider physicists matching RS cost geometry to the Standard Model Lagrangian would cite this relation when extracting the quadratic term from the potential expansion. The declaration is introduced as a direct definitional equality that remains open for closure against the phi-ladder yardstick.
Claim. The normalization hypothesis asserts that for recognition scale $Λ$, electroweak scale $v$, and Higgs mass $m_H$, one has $Λ^4 = m_H^2 v^2$.
background
The module defines the recognition-cost potential as $V_{RS} Λ v h := Λ^4 · J(exp(h/v))$ with $J(x) = ½(x + x^{-1}) - 1$, which expands to the quadratic coefficient $Λ^4/(2v^2)$ and quartic coefficient $Λ^4/(24v^4)$. These are matched to the SM form ½ m_H² h² + (λ_SM/4) h⁴, yielding the dictionary m_H² = Λ⁴/v² and λ_SM = (1/6) Λ⁴/v⁴. The dimensionless coordinate is ε = h/v with v supplied by the recognition substrate.
proof idea
The declaration is a definition that directly encodes the equality Λ⁴ = m_H² v² as a Prop.
why it matters
This supplies the defining normalization map required by HiggsEFTBridgeCert and is invoked in mass_term_matches_SM together with quartic_coupling_from_normalization. It fills the open collider-normalisation step flagged in the module documentation and connects to J-uniqueness (T5) and the phi fixed point (T6) in the forcing chain. The hypothesis remains conditional on fixing Λ from the phi-ladder yardstick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.