yukawa_SM_ratio_independent_of_v
plain-language theorem explainer
The theorem shows that for any sector identifier, rungs, and charge, the ratio of Yukawa couplings equals the ratio of predicted masses from the mass law, with the electroweak scale v canceling exactly. Model builders examining fermion hierarchies or Yukawa textures in the Standard Model would cite it to confirm that ratios derive solely from the phi-ladder without extra v-tuning. The proof is a direct algebraic reduction: unfold the Yukawa definition, record positivity facts for sqrt(2), v, and the mass, then apply field_simp to cancel common
Claim. For sector identifier $S$, integers $r_1,r_2,Z$, and $v>0$, let $y(S,r,Z,v)$ denote the Yukawa coupling defined by $y=√2⋅m/v$ with $m$ the mass from the Recognition Science mass law. Then $y(S,r_1,Z,v)/y(S,r_2,Z,v)=m(S,r_1,Z)/m(S,r_2,Z)$.
background
The Higgs–Yukawa Bridge module translates the Standard Model extraction convention $y_f=√2 m_f/v$ into the Recognition Science setting, where each fermion mass $m_f$ is supplied by predict_mass on the phi-ladder. The Anchor.Sector inductive type labels Lepton, UpQuark, DownQuark, and Electroweak; the companion Z function converts charge to an integer anchor derived from cube geometry. Upstream, rung definitions in Compat.Constants and Engineering.AsteroidOreSpectroscopy locate positions on the ladder, while Generation abbrevs in SpectralEmergence and UniversalForcing.BiologyRealization encode the three-generation structure that matches cube dimension.
proof idea
Unfold yukawa_SM to expose the explicit √2⋅predict_mass/v form. Record four auxiliary facts: sqrt(2) positive and nonzero, v nonzero by hypothesis, and predict_mass at rung2 positive and nonzero. Apply field_simp to cancel the identical v factors in numerator and denominator.
why it matters
The result is one of the four fields assembled into higgsYukawaBridgeCert, which certifies the full bridge between the mass law and Standard Model Yukawa extraction. It guarantees that phi-power scaling under rung jumps survives the 1/v normalization, consistent with the Recognition Composition Law and the eight-tick octave. The module documentation flags the separate open task 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.