yukawa_SM_phi_scaling
plain-language theorem explainer
The theorem establishes that the Yukawa coupling for any sector increases exactly by the factor phi when the rung index on the phi-ladder is incremented by one, holding for every positive electroweak scale v. Model builders embedding Standard Model fermion masses in a self-similar ladder structure would cite this result to relate couplings across generations without independent fits. The proof is a term-mode reduction that unfolds the Yukawa definition, invokes the mass rung scaling lemma, and finishes with field simplification after noting v ≠
Claim. Let $y(s,r,Z,v)$ denote the Yukawa coupling $y = 2^{1/2} m(s,r,Z)/v$ for sector $s$, rung $r$, atomic number $Z$, and electroweak vev $v>0$, where $m$ is the mass supplied by the phi-ladder prediction. Then $y(s,r+1,Z,v) = phi · y(s,r,Z,v)$.
background
In the Higgs–Yukawa Bridge module the Yukawa coupling of a fermion is defined as the ratio of its RS-derived mass to the electroweak scale: $y_f = 2^{1/2} m_f / v$, with $m_f$ taken directly from predict_mass in the Masses.MassLaw module. This construction ensures every Yukawa inherits the phi-ladder structure of the masses; no coupling is fitted independently. The phi-rung scaling property is therefore automatic once the mass scaling is known.
proof idea
The proof unfolds the definition of yukawa_SM, obtains the mass scaling predict_mass sector (rung+1) Z = phi · predict_mass sector rung Z from the mass_rung_scaling lemma, records v ≠ 0 from the positivity hypothesis, rewrites the expression, and applies field_simp to reach the desired equality.
why it matters
This theorem supplies the single-step phi scaling required by higgsYukawaBridgeCert, which packages positivity, phi-step, phi-power scaling, and v-independence into one certificate for the Higgs–Yukawa bridge. It realizes the rung-scaling step inside the Standard Model embedding of the Recognition Science mass law and supports the statement that generation jumps are phi^Δr. The result touches the open question of assigning explicit rungs to each SM species from cube combinatorics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.