row_anchor_strange_down_ratio_rpow
plain-language theorem explainer
The ratio of Recognition Science anchor masses for the strange quark to the down quark equals phi to the power eleven. Researchers verifying within-family ratios on the phi-ladder for equal-Z fermions would cite this when assembling the absolute bridge scorecard. The proof rewrites the exponential ratio form, converts via the positive-base definition of real exponentiation, and applies ring normalization.
Claim. The ratio of the anchor mass for the strange quark to the anchor mass for the down quark equals $phi^{11}$, where the anchor mass of fermion $f$ is $M_0 exp(((rung(f)-8 + gap(Z(f))) log phi))$.
background
The Quark Absolute Bridge Score Card module deepens the existing QuarkScoreCard by confirming within-family ratios for the down sector via the equal-Z anchor bridge. The anchor mass is the native expression $M_0 * exp(((rung f - 8 + gap(ZOf f)) * log phi))$, distinct from the MeV-displaying sector yardstick. Upstream, the exponential form first shows the ratio equals exp(11 * log phi) by proving ZOf strange equals ZOf down and the rung difference is exactly 11.
proof idea
The proof applies the exponential strange-down ratio, rewrites using the definition of real power for positive base, then normalizes the resulting expression with ring tactics.
why it matters
This supplies the strange-down field to the QuarkAbsoluteBridgeScoreCardCert_holds theorem that collects ratio agreements for scorecard certification. It advances the Phase 0 absolute bridge rows for down-sector quarks on the phi-ladder, consistent with the self-similar fixed point and forcing chain landmarks, while the module notes the absolute MeV mapping remains a residual open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.