anchorDownGen23Residual
plain-language theorem explainer
Defines the generation-2–3 rung residual for the down-quark sector at the RS anchor: the φ-ladder defect of the transported bottom-to-strange mass ratio against an eight-rung step. Mass-formula and Item-8 closure work cite it as the gen23 half of the down-sector residual pair. It is a one-line composition of the rung residual with the two anchor-scale masses.
Claim. The generation-2–3 down-sector residual at the Recognition Science anchor is $\log_\varphi(m_b^{\mathrm{anchor}}/m_s^{\mathrm{anchor}}) - 8$, where $m_b^{\mathrm{anchor}}$ and $m_s^{\mathrm{anchor}}$ are the PDG bottom and strange masses RG-transported to the RS anchor scale.
background
Item 8 concerns the sub-leading correction to the φ-ladder mass formula for quarks. Masses sit on a discrete φ-ladder; the leading prediction is an integer rung step, and the residual is the leftover in rung units.
The rung residual of a positive ratio against a natural step is $\log_\varphi(\mathrm{ratio}) - \mathrm{step}$, i.e. $\log(\mathrm{ratio})/\log\varphi$ minus the integer step. It measures how far the observed ratio sits from a pure ladder jump.
Here the ratio is bottom over strange, each mass first transported through the piecewise $\alpha_s$ running to the common RS anchor (bottom from its threshold with five active flavors; strange from the 2 GeV reference with four). The integer step is 8, the canonical gen-2–3 rung gap on the ladder.
proof idea
Pure definitional abbreviation: apply the rung-residual operator to the quotient of the two already-defined anchor masses with step equal to 8. No lemmas, no tactics; the value is that real number by construction.
why it matters
Feeds the down-sector residual pair used as the concrete anchor-scale falsification target for Item 8. That pair is the gen12/gen23 data against which the refined family (unique $(c,\eta)$ per sector) is fitted, and it supplies the gen23 input when solving for the positive-sector coefficient from the lepton-anchored $\eta$.
In the broader RS picture this is the sub-leading defect on the φ-ladder mass formula (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Closing Item 8 means showing the same refined-family coefficients that fit leptons predict these transported quark residuals; this constant is the gen23 half of that target for the down sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.