predictedResiduals
plain-language theorem explainer
Maps a pair of global sign-split coefficients and a sector residual signature to the predicted generation 1→2 and 2→3 sub-leading corrections. Anyone stating Item 8 closure, consistency necessity, or all-sector out-of-sample tests cites this as the prediction map. The body is a one-line alias of the candidate ratio family.
Claim. Given global coefficients $(c_{-}, c_{+})$ of the sign-split ratio family and a residual signature $(\mathrm{sign}, s_{12}, s_{23}, \kappa)$, return the predicted residual pair $(r_{12}, r_{23})$ produced by that family on the signature.
background
Item 8 concerns the open quark sub-leading mass correction. This module builds the smallest precise target that would close it and make all-sector generalization falsifiable: one closed family of residual laws with two global coefficients, frozen on quarks, then tested out of sample on leptons.
A residual signature packages the sector structure needed for the law: a $B_{\mathrm{pow}}$ sign class, positive SDGT rung steps $s_{12}, s_{23}$ (cube-cell counts from the $Q_3$ decomposition), and a coupling $\kappa$. A residual pair is simply the two corrections $(r_{12}, r_{23})$ for generations $1\to 2$ and $2\to 3$. Ratio-family coefficients are the two globals $(c_{-}, c_{+})$ allowed by the smallest sign-split candidate.
The prediction map is the evaluation of that candidate family: coefficients plus signature yield the predicted pair. Downstream theorems treat equality of this prediction with exact or observed residuals as the matching condition.
proof idea
Definitional one-line wrapper. The body is exactly ratioFamily coeffs sig, so predictedResiduals is an alias that names the prediction interface used by closure and consistency statements. No separate algebraic work occurs here.
why it matters
This is the named prediction arrow for Item 8. The closure target asserts unique coefficients such that the map hits both exact up- and down-quark residual pairs. Consistency necessity rewrites a match through this definition and applies the structural identity of the ratio family, so a data pair that violates the cross-product law cannot be fit. The all-sector test freezes coefficients on quarks and demands the same map reproduce lepton residuals under the lepton signature $(11,6)$ and $\kappa_{\mathrm{lep}}$: a genuine out-of-sample check. Equal signatures give equal predictions (no extra knobs), which is required for those tests to be well-posed. In the RS mass picture this sits at the sub-leading layer on the $\varphi$-ladder, above the leading yardstick formula, and is the precise object that would close the quark correction item once exact residuals are supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.