yukawa_SM_pos_of_hypothesis
plain-language theorem explainer
The theorem shows that the Standard Model Yukawa coupling extracted from the RS mass formula remains positive once the normalization hypothesis equates it to the SM value. Researchers modeling fermion masses on the phi-ladder would cite this to confirm consistency with electroweak data. The proof is a direct reduction that unfolds the equality hypothesis and applies the upstream positivity lemma for the RS Yukawa under positive v.
Claim. If the normalization hypothesis holds, so that the RS-derived Yukawa equals the SM value $y_{SM}$ for a given sector, rung, and charge parameter $Z$, and if the electroweak scale satisfies $v > 0$, then $y_{SM} > 0$.
background
The Higgs-Yukawa bridge module defines the fermion Yukawa as $y_f = √2 m_f / v$, where $m_f$ comes from the RS mass law on the phi-ladder. The normalization hypothesis states that this expression coincides with the SM-extracted Yukawa when the same electroweak scale $v$ is used; it is the fermion counterpart of the corresponding hypothesis in the Higgs EFT bridge. The module preserves phi-rung scaling, so that a rung increase multiplies the Yukawa by phi.
proof idea
The proof unfolds the normalization hypothesis to replace $y_{SM}$ by the RS Yukawa expression, invokes the upstream lemma yukawa_SM_pos that establishes positivity of that expression when $v > 0$, and rewrites to obtain the desired inequality.
why it matters
This result supplies the positivity claim under the normalization hypothesis inside the Higgs-Yukawa bridge, directly supporting the master bridge certificate. It reinforces the framework claim that Yukawas are not fitted independently but derived from rung position on the phi-ladder. It leaves open the separate task of mapping each SM species to its rung via cube combinatorics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.