upExact
plain-language theorem explainer
Packages the exact up-quark sub-leading residual pair (generation 1→2 and 2→3 rung corrections) extracted from PDG mass ratios against the φ-ladder SDGT step. Approximate values are about +0.25 and −0.79 rungs. Cited by every Item 8 closure and all-sector test that freezes global ratio-family coefficients on quark data. The body is a two-field structure instance wiring named residual constants.
Claim. Define the exact up-quark residual pair as the ordered pair of real sub-leading rung corrections $(\delta_{12}^{\mathrm{up}}, \delta_{23}^{\mathrm{up}})$ obtained by comparing PDG up-sector mass ratios to the pure $\varphi^{\mathrm{SDGT}}$ step. Numerically $\delta_{12}^{\mathrm{up}} \approx +0.25$ and $\delta_{23}^{\mathrm{up}} \approx -0.79$ rungs.
background
Item 8 concerns sub-leading corrections to quark masses on the Recognition Science $\varphi$-ladder. The leading mass formula places each species on a rung; residual pairs record the two generation-step corrections (1→2 and 2→3) left after the pure SDGT step is subtracted from PDG mass ratios.
A residual pair is the two-component real structure $(\mathrm{gen}{12}, \mathrm{gen}{23})$. The module builds the smallest precise target that would close Item 8: fit both up and down residual pairs inside one closed coefficient family, freeze the globals, and turn lepton (and later) sectors into out-of-sample tests.
Couplings in the specialized targets use $\kappa = \alpha_s = 2/17$. Sign-split and refined (log-asymmetry) families are the candidate predictors; this definition supplies the up-sector data those predictors must match.
proof idea
Not a proof: a noncomputable structure instance. It fills the two fields of a residual pair with the named constants for the up-quark generation-12 and generation-23 residuals (PDG versus $\varphi^{\mathrm{SDGT}}$). No lemmas or tactics are invoked.
why it matters
This is the up-sector data anchor for Item 8 closure. Downstream, item8ClosureTarget and its specialized form ask for unique ratio-family coefficients reproducing both this pair and the down-quark pair at $\kappa=\alpha_s$. The refined closure and refined all-sector test do the same with three coefficients (including universal $\eta$) against four or six equations.
All-sector and sign-class tests reuse the same object so that coefficients frozen on quarks must also hit lepton residuals under the lepton signature—an out-of-sample falsification path. Closing Item 8 would lock the global family and convert later lepton, genetic, and $\theta$ instantiations into genuine predictions rather than fits. The mass ladder and $\varphi$-rung structure from the forcing chain are the ambient setting; this definition does not itself invoke T5–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.