yukawa_SM_phi_pow_scaling
plain-language theorem explainer
The theorem states that the Yukawa coupling for a fermion scales exactly by phi to the power n when its rung on the phi-ladder increases by n. Researchers constructing fermion mass hierarchies inside Recognition Science would cite this to obtain generation ratios without independent fitting. The proof proceeds by induction on n, reducing each successor step to the single-step scaling lemma via integer casting and ring simplification.
Claim. For any sector $s$, integers $r$ and $Z$, natural number $n$, and $v>0$, the Yukawa coupling satisfies $y(s,r+n,Z,v)=phi^ncdot y(s,r,Z,v)$, where $y$ is the Standard Model Yukawa extracted via $sqrt{2} m_f/v$ and $m_f$ is supplied by the Recognition Science mass law on the phi-ladder.
background
The Higgs-Yukawa Bridge module expresses each fermion Yukawa as the ratio $y_f=sqrt{2}cdot m_f/v$, with the mass $m_f$ taken from the phi-ladder mass law. The phi-ladder places physical masses at discrete rungs scaled by the golden-ratio fixed point phi, so that rung increments produce exact multiplicative factors of phi. This theorem lifts the single-step scaling (already established for adjacent rungs) to arbitrary nonnegative integer steps. It draws on upstream arithmetic lemmas for integer addition and on the one-step Yukawa scaling result.
proof idea
Proof by induction on $n$. The zero case follows by direct simplification of the Yukawa definition. For the successor step, the single-step scaling lemma is applied to the intermediate rung, an integer cast is performed with push_cast and ring, the induction hypothesis is substituted, and the equation is closed by ring.
why it matters
The result supplies the power-scaling entry in the HiggsYukawaBridgeCert certificate that bundles positivity, scaling, and ratio independence for the RS-to-SM bridge. It realizes the phi self-similar fixed point (T6) inside the fermion sector and is compatible with the Recognition Composition Law. The module leaves open the explicit rung map for each Standard Model species, which is tracked separately under the OPEN_RUNG_MAP tag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.