row_anchor_bottom_strange_ratio_rpow
plain-language theorem explainer
The theorem establishes that the RS anchor mass ratio for bottom to strange quarks equals phi to the sixth power. Researchers checking phi-ladder consistency for down-type quarks in Recognition Science would cite it to confirm within-family ratio matches. The proof rewrites via the exponential ratio lemma, invokes the rpow definition, and finishes with algebraic normalization.
Claim. Let $M_f$ be the anchor mass of fermion $f$ given by $M_0$ times the exponential of $((rung(f)-8+gap(Z(f)))log phi)$. Then $M_b/M_s=phi^6$, where $b$ and $s$ label the bottom and strange quarks.
background
The Quark Absolute Bridge Score Card module deepens QuarkScoreCard by proving exact agreement on within-family ratios between the equal-Z anchor bridge and the structural mass formula. Anchor mass is defined as $M_0$ exp$(((rung f:ℝ)-8+gap(ZOf f))log phi)$, with phi the self-similar fixed point. Upstream, row_anchor_bottom_strange_ratio_exp derives the exponential form of the same ratio by using ZOf b = ZOf s together with the rung difference of 6 and the anchor_ratio lemma.
proof idea
The short tactic proof first rewrites the goal with row_anchor_bottom_strange_ratio_exp. It then applies Real.rpow_def_of_pos using phi_pos to convert the power into an exponential. Ring_nf completes the algebraic simplification.
why it matters
The result supplies the bottom_strange_anchor_ratio field inside quarkAbsoluteBridgeScoreCardCert_holds, the certificate collecting all structural-anchor agreements. It completes down-sector coverage for the absolute bridge, complementing up-type rows. In the Recognition framework it instantiates the phi-ladder mass formula for same-Z fermions with rung gap 6, consistent with the T6 fixed-point construction and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.