higgsFermionCoupling
plain-language theorem explainer
The declaration supplies the standard Higgs-fermion coupling as the ratio of fermion mass to the vacuum expectation value. Model builders in the Recognition Science treatment of the Standard Model cite it when assembling interaction vertices after J-cost minimization fixes the VEV. The definition is a direct one-line assignment with no further reduction.
Claim. The Higgs-fermion coupling is given by $g_{Hff} = m_f / v$, where $m_f$ denotes the mass of the fermion and $v$ is the vacuum expectation value of the Higgs field.
background
The module derives electroweak symmetry breaking from the J-cost functional. The Higgs potential is identified with the J-cost, and the vacuum expectation value $v$ is the configuration that minimizes this cost, breaking SU(2)_L × U(1)_Y to U(1)_EM. The imported Cost and PhiForcing modules supply the J-cost definition and the phi-ladder structure that fixes the scale of $v$.
proof idea
This is a direct definition that encodes the textbook relation for the Yukawa coupling after the Higgs field acquires its vacuum expectation value.
why it matters
The definition supplies the fermion interaction term required by the Recognition Science account of electroweak symmetry breaking. It follows the module's identification of the Higgs potential with J-cost minimization and supports downstream mass and coupling calculations on the phi-ladder. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.