yukawa_SM
plain-language theorem explainer
The definition computes the Standard Model Yukawa coupling for a fermion as the square root of two times its phi-ladder mass prediction divided by the electroweak scale v. Particle physicists using Recognition Science mass assignments cite it to obtain all Yukawa values directly from rung and sector data without separate fitting. It is realized as a one-line definition that applies the canonical extraction formula to the output of the mass law.
Claim. For a fermion in sector $s$, rung $r$, and integer parameter $Z$, at electroweak scale $v$, the Yukawa coupling is $y = 2^{1/2} m(s,r,Z)/v$, where $m(s,r,Z)$ is the mass from the phi-ladder prediction.
background
The Higgs–Yukawa Bridge module translates Recognition Science masses into Standard Model Yukawa language via the extraction convention $y_f = 2^{1/2} m_f / v$. The mass $m_f$ is supplied by predict_mass from the MassLaw module, which implements the phi-ladder formula yardstick times phi raised to (rung plus gap minus 8). Sector is the inductive type with constructors Lepton, UpQuark, DownQuark, Electroweak; Z maps charge to an integer via the anchor relation. The rung parameter indexes position on the ladder, inheriting phi-scaling from upstream mass results.
proof idea
This is a one-line definition that applies the SM Yukawa extraction formula directly to predict_mass sector rung Z, multiplied by the square root of two and divided by v.
why it matters
This definition supplies the core mapping used by HiggsYukawaBridgeCert to certify positivity and phi-rung scaling of all Yukawas. It fills the module's role of ensuring no Yukawa is fit independently, with generation jumps given by phi to the power of rung difference. It connects to the phi-ladder mass formula and touches the open question of deriving explicit rung maps for each SM species from cube combinatorics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.