YukawaNormalizationHypothesis
plain-language theorem explainer
The YukawaNormalizationHypothesis equates the Recognition Science Yukawa derived from the mass law to the Standard Model value extracted via y = √2 m_f / v, under the shared electroweak scale v. Model builders linking phi-ladder fermion masses to SM data would cite it to justify direct comparison of couplings. The declaration is a one-line definitional equality that downstream theorems unfold to transfer positivity and scaling properties.
Claim. The hypothesis holds when the RS Yukawa coupling for fermion sector $s$, rung $r$ and charge $Z$, computed as $y_{RS} = y_{SM}(s,r,Z,v)$ from the mass law at electroweak scale $v$, equals the supplied SM-extracted value $y_{SM}$.
background
The Higgs–Yukawa Bridge module defines the fermion Yukawa as $y_f = √2 m_f / v$, where $m_f$ comes from the phi-ladder mass law in Masses.MassLaw and $v$ is the electroweak vacuum expectation value. This construction preserves rung scaling: a unit increase in rung multiplies the Yukawa by φ. The module states that equating the RS Yukawa to the SM Lagrangian value is conditional on using the identical $v$ employed in the SM extraction $y_f = √2 m_f / v$, the fermion counterpart of the Higgs EFT normalization hypothesis.
proof idea
The declaration is a direct definitional equality: YukawaNormalizationHypothesis holds precisely when yukawa_SM sector rung Z v equals the parameter y_SM. Downstream results such as yukawa_SM_pos_of_hypothesis unfold the equality and invoke the positivity lemma yukawa_SM_pos under the assumption 0 < v.
why it matters
This hypothesis supplies the conditional identification step required for the Higgs–Yukawa Bridge theorems, feeding directly into yukawa_SM_pos_of_hypothesis. It implements the module's CONDITIONAL status for matching RS and SM Yukawas while leaving the rung map derivation open. The construction sits inside the phi-ladder mass formula and the eight-tick octave structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.