Pith. sign in
module module high

IndisputableMonolith.StandardModel.HiggsYukawaBridge

show as:
view Lean formalization →

Defines the Standard-Model Yukawa extraction y_f = √2 m_f / v from φ-ladder masses. Supplies positivity, φ-scaling, and v-independence lemmas, plus a normalization hypothesis and a bridge certificate. Cited by Higgs EFT low-energy and observable-skeleton modules. Mostly definitional with short algebraic proofs from the mass law.

claimFor each fermion $f$ with $\phi$-ladder mass $m_f = \mathrm{predict\_mass}(\mathrm{sector}, r, Z)$, the SM Yukawa is $y_f = \sqrt{2}\, m_f / v$. The module records $y_f > 0$, $\phi$-power scaling of $y_f$, adjacent-rung ratios independent of the Higgs vev $v$, and a certificate packaging these facts under an optional normalization hypothesis.

background

Recognition Science places every stable particle on a $\phi$-ladder rung. The master mass law (Masses.MassLaw) writes $m$ as a sector yardstick times $\phi$ to a power fixed by rung and atomic number gap; Anchor centralises the parameter-free constants used in that formula. Constants supplies the RS time quantum and related units.

In the Standard Model the fermion mass is $m_f = y_f v / \sqrt{2}$, so inverting gives the extraction convention $y_f = \sqrt{2}, m_f / v$. This module takes $m_f$ from the $\phi$-ladder predictor and treats $v$ as an external electroweak scale, thereby translating RS masses into SM Yukawa couplings without introducing new free parameters beyond the ladder data.

The local setting is the Model layer: no claim of experimental agreement is made here; the goal is a clean bridge from ladder masses to Yukawa numbers usable by Higgs EFT and collider-observable skeletons.

proof idea

Definitional core: yukawa_SM is the literal map $(\mathrm{sector},r,Z,v)\mapsto \sqrt{2},\mathrm{predict_mass}/v$. Positivity follows from positivity of the mass law and $v>0$. Scaling lemmas are algebraic rewrites of the $\phi$-power in the mass formula, so ratios of adjacent Yukawas cancel $v$ and the overall yardstick. The normalization hypothesis is a Prop interface; a short lemma derives positivity from it when assumed. The bridge certificate is an inhabited structure bundling the main lemmas for downstream import.

why it matters in Recognition Science

Feeds the Higgs EFT low-energy limit master certificate, which chains RS cost geometry through an effective scalar coordinate to a canonical Higgs EFT, and the Higgs observable skeleton that parametrises partial widths, branching ratios, and signal-strength modifiers. Without a uniform Yukawa extraction, those modules cannot attach ladder masses to SM-like couplings. The construction sits downstream of the mass law and Anchor constants; it does not itself force $\phi$ or the eight-tick structure (those live in the T5–T7 forcing chain). It closes the Model-layer gap between $\phi$-ladder masses and the Yukawa inputs expected by Higgs phenomenology modules.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)