row_anchor_strange_down_ratio_exp
plain-language theorem explainer
The theorem proves the anchor mass ratio between strange and down quarks equals exp(11 log phi). Recognition Science mass modelers cite it to confirm the within-family down-sector ratio on the phi ladder. The tactic proof applies the general anchor_ratio lemma after deciding equal ZOf values and simplifying the rung difference to exactly 11.
Claim. $m_s / m_d = e^{11 ln phi}$ where $m_f$ denotes the Recognition Science anchor mass for fermion $f$, given by $M_0 exp(((rung(f) - 8 + gap(ZOf(f))) ln phi))$.
background
The QuarkAbsoluteBridgeScoreCard module develops absolute bridges for quark masses, deepening the earlier QuarkScoreCard by showing agreement on within-family ratios under equal Z. The anchor mass for fermion f is massAtAnchor(f) := M0 * exp(((rung f : R) - 8 + gap(ZOf f)) * log phi), with rung values taken from RSBridge.Anchor: rung(s) = 15 and rung(d) = 4. The upstream anchor_ratio theorem states that when ZOf f = ZOf g the ratio massAtAnchor f / massAtAnchor g equals exp(((rung f - rung g) * log phi)).
proof idea
The proof decides ZOf .s = ZOf .d by reflexivity. It invokes anchor_ratio .s .d with this equality. A separate simp and norm_num block establishes that rung .s - rung .d equals 11. The final simpa substitutes the difference into the ratio expression from anchor_ratio.
why it matters
This supplies the exponential form of the strange-to-down ratio, which the downstream row_anchor_strange_down_ratio_rpow rewrites as phi^11. It fills a Phase 0 row in the quark absolute bridge, consistent with the phi-ladder mass formula and the eight-tick octave. The module records that the full SI-display bridge remains partial pending calibration of the 10^6 divisor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.