upGen12Residual
plain-language theorem explainer
Defines the up-sector generation-1–2 residual as the φ-ladder rung residual of the PDG charm-to-up mass ratio against integer step 13. Anyone assembling the exact up-quark residual pair or the mixed-scheme η fit cites this constant. It is a one-line specialization of the rung-residual formula to fixed PDG inputs.
Claim. The up-sector generation-1–2 residual is $\log_\varphi(m_c^{\mathrm{PDG}}/m_u^{\mathrm{PDG}})-13$, with $m_c^{\mathrm{PDG}}=1270$ and $m_u^{\mathrm{PDG}}=2.16$ (MeV-scale PDG values as used in the module).
background
Item 8 Closure Target builds the smallest precise theorem layer that would close the open quark sub-leading mass correction and make the all-sector generalization falsifiable. Residuals are measured in φ-ladder rung units: the rung residual of a positive mass ratio against a natural step is $\log_\varphi(\mathrm{ratio})-\mathrm{step}$, i.e. $\ln(\mathrm{ratio})/\ln\varphi$ minus the integer step.
PDG anchors used here are the module constants $m_u=2.16$ and $m_c=1270$. The integer 13 is the SDGT generation-1–2 step against which the charm/up ratio is compared. The same pattern defines the companion gen-2–3 residual; together they form the exact up residual pair fed to the refined-family and η-from-data constructions.
proof idea
Pure definition, not a proof. Instantiates the rung-residual formula on the fixed ratio $\mathrm{pdg_charm}/\mathrm{pdg_up}$ and step 13. No tactics, lemmas, or algebraic reduction beyond that specialization.
why it matters
Supplies the gen12 coordinate of the exact up-quark residual pair (approximate value $\approx +0.25$ rungs) and is the first argument to the mixed-scheme up-quark η extractor (reported $\eta\approx -2.72$, inflated by the $t/c$ pole vs $\overline{\mathrm{MS}}$ comparison). Those objects sit inside the Item 8 closure stack: solvability and uniqueness of refined-family coefficients $(c,\eta)$ for each sign sector, and the path toward a falsifiable all-sector sub-leading mass formula on the φ-ladder. Without a concrete gen12 residual, the up-sector $\exists!$ closure and the η identities have no numerical input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.