anchorUpExact
plain-language theorem explainer
Packages the two anchor-scale up-sector rung residuals (charm/up at step 13, top/charm at step 11) into a single residual pair. Cited by the lepton-anchored Item 8 falsification targets that demand the refined family predict these numbers. Pure structure assembly: no proof content.
Claim. Define the exact anchor-scale up residual pair by $r_{12}^{\mathrm{up}} = R\!\left(m_c^{\mathrm{anc}}/m_u^{\mathrm{anc}},\,13\right)$ and $r_{23}^{\mathrm{up}} = R\!\left(m_t^{\mathrm{anc}}/m_c^{\mathrm{anc}},\,11\right)$, where $R$ is the rung residual of a mass ratio at the stated ladder step.
background
Item 8 concerns sub-leading corrections on the $\varphi$-ladder mass formula beyond the leading rung count. Residuals live in generation steps $1\to 2$ and $2\to 3$; a ResidualPair is just that ordered pair of real corrections.
Anchor-scale masses are PDG values transported to a common scale. The up-sector generators are the charm/up ratio at rung step 13 and the top/charm ratio at step 11. Under the present LO scaffold those evaluate near $(0.02,+0.57)$ in rung units.
The module builds the smallest theorem framework that would close Item 8 and make an all-sector generalization falsifiable, via refined coefficient families $(c,\eta)$ and lepton-anchored prediction tests.
proof idea
Definition only: construct a ResidualPair by assigning gen12 to anchorUpGen12Residual and gen23 to anchorUpGen23Residual. No tactics, no lemmas, no computation beyond the two upstream residual defs.
why it matters
Supplies the concrete up-sector target that lepton-anchored closure must hit. Downstream, leptonAnchoredAnchorTest requires the refined up prediction at $\kappa_{\mathrm{lep}}$ to equal this pair, and that the down sector induce a single consistent $c_{\mathrm{Pos}}$. The broader leptonAnchoredTarget quantifies over refined coefficients that fit leptons and simultaneously predict both anchor residual pairs.
In the RS mass ladder (yardstick $\cdot,\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), these residuals are the sub-leading data Item 8 must absorb. Packaging them as one pair keeps the falsification proposition tidy and sector-symmetric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.