row_anchor_bottom_strange_ratio_exp
plain-language theorem explainer
The theorem establishes that the ratio of anchor masses for the bottom and strange quarks equals exp(6 log phi). Researchers checking phi-ladder predictions for down-sector quarks against PDG data would cite this when confirming within-family consistency. The proof is a short tactic sequence that decides equal Z values, applies the general anchor ratio result, and reduces the rung difference to six.
Claim. $ m_b / m_s = e^{6 log phi} $, where $m_f$ denotes the native anchor mass $M_0 exp(((rung f - 8 + gap(ZOf f)) log phi))$ for fermion $f$, with rung assigning 21 to bottom and 15 to strange on the phi-ladder.
background
The Quark Absolute Bridge Score Card module deepens QuarkScoreCard by verifying equal-Z anchor bridges for within-family quark ratios. massAtAnchor(f) is defined as $M_0 exp(((rung f : R) - 8 + gap(ZOf f)) log phi)$, with rung a noncomputable map sending .b to 21 and .s to 15. The upstream anchor_ratio theorem states that if ZOf f = ZOf g then massAtAnchor f / massAtAnchor g equals exp(((rung f - rung g) log phi)). This setting treats the absolute MeV bridge as partial, with two distinct anchors still requiring SI calibration.
proof idea
The tactic proof first decides ZOf .b = ZOf .s. It then applies the anchor_ratio theorem to .b and .s under that equality. It next simplifies the rung difference to exactly 6 via simp and norm_num. The final simpa substitutes the difference into the ratio expression from anchor_ratio.
why it matters
This supplies the exponential form rewritten as phi^6 in the downstream row_anchor_bottom_strange_ratio_rpow. It fills Phase 0 rows P0-Q01..P0-Q06 from the physical derivation plan, confirming phi-ladder structure for down quarks. The result sits inside the Recognition framework's T5 J-uniqueness and T6 phi fixed point, while the absolute MeV bridge remains open pending display-sector calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.