ResidualPair
plain-language theorem explainer
A residual pair is the ordered pair of sub-leading rung corrections for generation steps 1→2 and 2→3. It is the carrier type for exact PDG residuals, predicted residuals, and lepton/quark anchors throughout the Item 8 closure module. Anyone fitting or falsifying the unified sub-leading mass formula cites it. The declaration is a plain two-field structure with extensionality; no proof content.
Claim. A residual pair is an ordered pair $(r_{12}, r_{23}) \in \mathbb{R}^2$ of sub-leading rung corrections associated to the generation steps $1 \to 2$ and $2 \to 3$ in the $\varphi$-ladder mass formula.
background
Item 8 of the Recognition verification program concerns sub-leading corrections to sector masses beyond the leading $\varphi$-ladder term (yardstick times $\varphi$ to a rung offset). After the leading power is fixed, each charged-fermion sector leaves two residual rung shifts: one for the first-to-second generation step and one for the second-to-third.
This module builds the smallest precise theorem framework that would close that open quark correction and make the all-sector generalization falsifiable. Residuals are compared against a sign-split ratio family whose outputs must match observed pairs sector by sector.
The structure simply packages those two real corrections. Downstream definitions such as downExact and the lepton anchor fill the fields from PDG mass ratios versus $\varphi^{\mathrm{SDGT}}$ steps; prediction maps fill them from coefficient data and a residual signature (sign class, step sizes, coupling).
proof idea
Definition only: a structure with two ℝ fields (gen12, gen23) and the @[ext] attribute so equality of pairs reduces to equality of components. No tactics, no lemmas, no proof body.
why it matters
Every Item 8 closure statement is typed over residual pairs. The target proposition item8ClosureTarget asks for unique ratio-family coefficients that reproduce given up- and down-quark residual pairs. Consistency theorems (consistency_of_ratioFamily, consistency_necessary) force the cross-product identity $r_{12}s_{12}+r_{23}s_{23}=0$ on any pair the sign-split family can hit; PDG data violate that rigidity, which motivates the refined $\eta$-family.
Anchors (anchorUpExact, anchorDownExact, downExact, lepton-anchored targets) are concrete residual pairs used as in-sample fits or out-of-sample predictions once global coefficients freeze. Closing Item 8 means fixing both quark pairs inside one closed family so later lepton, genetic, and $\theta$ instantiations become genuine tests rather than refits. The type is the shared interface for that program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.