leptonAnchoredUpPrediction
plain-language theorem explainer
Given a lepton-sector scale parameter κ, this returns the predicted gen-12 and gen-23 sub-leading residuals for the up-quark sector after freezing the refined-family coefficients (c₋, η) on leptons. Citation target for anyone checking the lepton-anchored Item-8 out-of-sample test. One-line application of the refined predictor to the lepton-anchored coefficient pack and the up-quark signature.
Claim. For a real lepton scale $\kappa$, form the refined-family coefficient pack frozen on leptons at $\kappa$, evaluate it on the up-quark residual signature (with the strong coupling), and return the resulting residual pair $(r_{12}, r_{23})$ of generation $1\to 2$ and $2\to 3$ sub-leading corrections.
background
Item 8 concerns the unified sub-leading mass formula: after the leading $\phi$-ladder rung structure, each charged sector carries two residual corrections (generation steps $1\to 2$ and $2\to 3$). A ResidualPair is exactly that pair $(r_{12}, r_{23})$.
The refined family is the smallest coefficient model that can absorb the structural rigidity of the plain sign-split ratio family. Coefficients include a sign-split active $c$ and a shared $\eta$; uniqueness and solvability of $(c,\eta)$ per sector are already proved in this module.
Lepton anchoring freezes $(c_{-},\eta)$ from lepton data at a scale $\kappa$, then transports those coefficients to the quark sector. The up-quark signature packages the kinematic and coupling inputs (including $\alpha_s$) needed by the refined predictor. The local setting is the falsifiable closure target for all-sector generalization of Item 8.
proof idea
Definitional one-liner: call refinedPrediction on leptonAnchoredCoeffs kappaLepton and upQuarkSignature alphaStrong. No tactic proof; the body is pure composition of the lepton-frozen coefficient pack with the up-sector signature evaluator.
why it matters
Feeds the concrete lepton-anchored falsification target leptonAnchoredAnchorTest, whose first conjunct requires this prediction to equal the transported anchor up residuals (anchorUpExact), while the second demands a single consistent $c_{+}$ on the down sector.
In the Recognition mass ladder, leading masses sit on $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$; Item 8 is the sub-leading correction layer that must close before the all-sector formula is fully predictive. Lepton anchoring is the out-of-sample strategy: freeze on leptons, predict up, consistency-check down. This definition is the up-sector prediction half of that test, not a proved equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.