anchorDownExact
plain-language theorem explainer
Packages the down-quark sector's two generation-step sub-leading residuals at the anchor mass scale into a single residual pair. Downstream lepton-anchored Item 8 closure cites it as the out-of-sample target that a lepton-frozen refined family must hit for down-type quarks. The body is a pure structure constructor wiring two precomputed residual scalars.
Claim. The exact anchor-scale residual pair for the down-quark sector: the generation $1\to 2$ entry is the rung residual of the strange-to-down mass ratio at rung $6$, and the generation $2\to 3$ entry is the rung residual of the bottom-to-strange mass ratio at rung $8$.
background
Item 8 Closure Target builds the smallest precise theorem framework that would close the open quark sub-leading correction and make the all-sector generalization falsifiable. The basic data object is a residual pair: two real sub-leading rung corrections, one for the generation step $1\to 2$ and one for $2\to 3$.
The two scalars wired here are the down-sector anchor residuals. The $1\to 2$ residual is the rung residual of the strange-to-down mass ratio evaluated at rung $6$; the $2\to 3$ residual is the rung residual of the bottom-to-strange mass ratio at rung $8$. Together they form the exact down-quark residual pair at the anchor scale against which refined-family predictions are compared.
The module already proves structural rigidity of the plain sign-split family, closed-form $\eta$ identities that absorb consistency violations, and unique solvability of the refined family on each sign sector. This definition supplies one of the concrete quark targets those uniqueness results feed.
proof idea
Definition only: a ResidualPair structure literal. The gen12 field is set to the precomputed down-sector $1\to 2$ anchor residual, and gen23 to the precomputed down-sector $2\to 3$ anchor residual. No tactics, no lemmas, no computation beyond field assignment.
why it matters
Supplies the down-quark half of the out-of-sample target in the lepton-anchored closure proposition. That proposition asks for global refined coefficients that fit leptons at the lepton coupling and simultaneously predict both up- and down-quark residual pairs at the anchor scale. Without this packaged pair, the down-sector prediction clause has no concrete residual object to match.
In the Recognition mass ladder, sub-leading rung corrections sit on top of the leading $\phi$-power yardstick formula. Item 8 is the open quark correction that must be closed before the all-sector refined family is falsifiable against PDG data. This definition is bookkeeping, not a theorem, but it is the exact numerical target the refined-family uniqueness and solvability results are aimed at for the down sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.