HiggsYukawaBridgeCert
plain-language theorem explainer
The HiggsYukawaBridgeCert structure certifies that Yukawa couplings obtained from the RS mass law are positive for positive electroweak scale v, scale exactly by phi under single-rung shifts and by phi to an integer power under multiple shifts, and that their ratios equal the corresponding mass ratios independently of v. A physicist assembling the Standard Model sector from the phi-ladder would cite this certificate when verifying that the Yukawa couplings inherit the required scaling without extra parameters. The construction is a direct one-s
Claim. Let $y(s,r,Z,v)$ denote the Yukawa coupling for fermion species $s$ at rung $r$ with parameter $Z$ and electroweak scale $v>0$. Then $y(s,r,Z,v)>0$, $y(s,r+1,Z,v)=phi·y(s,r,Z,v)$, $y(s,r+n,Z,v)=phi^n·y(s,r,Z,v)$ for $n∈ℤ$, and $y(s,r_1,Z,v)/y(s,r_2,Z,v)=predict_mass(s,r_1,Z)/predict_mass(s,r_2,Z)$.
background
The module defines the Yukawa coupling via the standard extraction $y_f=√2·m_f/v$ where the mass $m_f$ is supplied by the phi-ladder formula in Masses.MassLaw.predict_mass. The rung parameter places each fermion on the discrete self-similar ladder whose fixed point is the phi forced by T6 of the UnifiedForcingChain. Upstream lemmas on phi-forcing and ledger factorization already establish the multiplicative scaling that is inherited by the Yukawa function. The module states that generation jumps are therefore phi to the power of the rung difference rather than a fixed phi^1.
proof idea
The structure is a one-line wrapper that directly assigns the four component lemmas already proved in the same module: yukawa_pos is taken from yukawa_SM_pos, the single-step scaling from yukawa_SM_phi_scaling, the integer-power scaling from yukawa_SM_phi_pow_scaling, and the v-independent ratio from yukawa_SM_ratio_independent_of_v.
why it matters
This certificate supplies the Yukawa sector for the master HiggsEFTLowEnergyLimitCert that composes the full cost-geometry to SM-EFT bridge. It realizes the phi-rung scaling required by the T6 fixed-point and T7 eight-tick structure of the forcing chain. The open question it touches is the explicit derivation of the rung map for each SM fermion species from cube combinatorics, tracked under the OPEN_RUNG_MAP tag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.