NormalizationHypothesis
plain-language theorem explainer
The normalization hypothesis equates the recognition scale Λ to the fourth root of the product of Higgs mass squared and electroweak vev squared. Physicists constructing effective field theory bridges from recognition cost geometry to the Standard Model would cite this as the required matching condition between scales. The declaration is introduced as a direct algebraic equality with no derivation or lemmas.
Claim. The normalization hypothesis asserts that for recognition-cost scale Λ, electroweak vacuum expectation value v, and Higgs mass m_H, the equality Λ⁴ = m_H² v² holds.
background
The Higgs EFT Bridge module defines the recognition-cost potential as V_RS(Λ, v, h) := Λ⁴ · J(exp(h/v)), where J(x) = ½(x + x⁻¹) − 1 is the canonical reciprocal cost functional from the J-cost structure. Expansion around the vacuum yields the quadratic coefficient Λ⁴/(2 v²) and quartic coefficient Λ⁴/(24 v⁴). The hypothesis supplies the scale relation needed to match the Standard-Model form ½ m_H² h² + (λ_SM/4) h⁴. Upstream structures include J-cost minimization (convexity and 8-tick dynamics) from PhysicsComplexityStructure and the continuum identification from SimplicialLedger.ContinuumBridge.
proof idea
The declaration is a direct definition of the proposition as the algebraic equality Λ⁴ = m_H² v². No lemmas or tactics are applied; it functions as an interface hypothesis for conditional results in the module.
why it matters
This hypothesis supplies the defining normalisation map between the recognition-cost scale and the electroweak scale, closing the first two arrows of the RS cost geometry to canonical Higgs EFT chain. It is required by the master certificate HiggsEFTBridgeCert and by the theorems mass_term_matches_SM and quartic_coupling_from_normalization. The open collider-normalisation problem of fixing Λ(v) from the φ-ladder yardstick remains unresolved, as noted in the module documentation. It connects to J-uniqueness in the forcing chain and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.