anchorDownGen12Residual
plain-language theorem explainer
Defines the generation-1–2 residual for the down sector at the RS mass anchor: the φ-ladder excess of the transported strange/down mass ratio above a six-rung step. Quark-sector Item-8 work cites it as the gen12 half of the down residual pair. It is a two-line composition of the rung residual with the RG-transported PDG masses.
Claim. Let $m_s^{\mathrm{anc}}$ and $m_d^{\mathrm{anc}}$ be the PDG strange and down masses transported to the RS anchor scale. The generation-1–2 down residual is $\log_\varphi(m_s^{\mathrm{anc}}/m_d^{\mathrm{anc}}) - 6$.
background
Item 8 concerns the sub-leading correction on the φ-mass ladder for quarks. The module builds a minimal theorem framework that would close that correction and make the all-sector generalization falsifiable. Residuals are measured in rung units: for a positive mass ratio $r$ and integer step $n$, the rung residual is $\log_\varphi r - n$, i.e. the excess (or deficit) of the observed ratio above a pure integer φ-power.
The two masses entering the ratio are not raw PDG values. Each is obtained by RG transport of the PDG mass through a piecewise $\alpha_s$ running from the 2 GeV quark reference scale to the RS anchor, with four active flavors and the module's threshold schedule. The integer step 6 is the nominal gen12 rung gap used for the down-sector signature.
This residual is the gen12 half of the down-sector residual pair at the anchor; its gen23 sibling uses the bottom/strange ratio with step 8.
proof idea
Pure definitional composition, not a proof. Evaluate the rung residual on the ratio of the two RG-transported anchor masses with step equal to 6: divide $\log(m_s^{\mathrm{anc}}/m_d^{\mathrm{anc}})$ by $\log\varphi$ and subtract 6. No lemmas are applied beyond the definitions of the residual and the two transported masses.
why it matters
Feeds the down-sector residual pair used as anchor data for Item 8. Downstream, anchorDownExact packages this value with the gen23 residual into a ResidualPair, and downAnchorCPosFromGen12 converts it into one of the two implied positive-sector amplitudes once lepton $\eta$ is frozen. Equality of those two amplitudes is the one-parameter down-sector consistency test under lepton anchoring.
In the broader RS picture this residual is the numerical sub-leading defect on the φ-ladder (mass formula yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Closing Item 8 means showing that a single refined-family coefficient pair $(c,\eta)$ absorbs such residuals across sectors; this constant is the concrete gen12 input for the down sector at the anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.