yukawa_SM_ratio_adjacent
plain-language theorem explainer
The ratio of Yukawa couplings for the same sector and charge but adjacent rungs on the phi-ladder equals exactly phi. Model builders deriving standard-model fermion masses from Recognition Science would cite this to confirm parameter-free scaling. The proof is a direct algebraic reduction that applies the phi-scaling lemma for Yukawas, invokes positivity to justify the division, and simplifies the resulting expression.
Claim. Let $s$ be any sector, $n,Z$ integers, and $v>0$. Then the ratio of the Yukawa coupling at rung $n+1$ to the coupling at rung $n$ equals the golden ratio: $y(s,n+1,Z,v)/y(s,n,Z,v)=phi$, where each Yukawa is obtained from the Recognition Science mass law via $y=sqrt(2)m/v$.
background
The Higgs-Yukawa Bridge module defines the Yukawa coupling for any fermion as the ratio of its Recognition Science mass (from Masses.MassLaw.predict_mass) to the electroweak scale $v$, using the standard-model extraction convention $y_f=sqrt(2)m_f/v$. The phi-ladder supplies the mass values, so the Yukawa inherits the same rung structure and scaling. Upstream results establish the underlying phi-forcing (T6) and the spectral emergence of three generations with 24 chiral fermions from the cube combinatorics (SpectralEmergence.of).
proof idea
The proof applies the phi-scaling lemma yukawa_SM_phi_scaling to replace the numerator by phi times the denominator. It then calls yukawa_SM_pos to obtain strict positivity of the denominator, converts that to non-zero via ne_of_gt, rewrites the ratio, and finishes with field_simp.
why it matters
This result confirms that Yukawa couplings scale exactly by phi between adjacent rungs, so generation jumps are phi to the power of the rung difference. It directly supports the module claim that no Yukawa is fit independently and feeds the HiggsYukawaBridgeCert construction. The scaling traces to the self-similar fixed point phi forced in the foundation chain (T6) and preserves the eight-tick octave structure. It touches the open rung-map derivation from cube combinatorics noted in the module status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.