upGen23Residual
plain-language theorem explainer
Defines the generation-2–3 residual for the up sector as the φ-ladder excess of the PDG top-to-charm mass ratio over eleven rungs. Anyone fitting Item-8 sub-leading quark corrections cites this number as the gen23 coordinate of the up residual pair. The body is a one-line specialization of the rung-residual formula to those PDG masses and step.
Claim. The up-sector generation-2–3 residual is $\log_\varphi(m_t^{\mathrm{PDG}}/m_c^{\mathrm{PDG}}) - 11$, with $m_t^{\mathrm{PDG}}=172690$ and $m_c^{\mathrm{PDG}}=1270$ (MeV-scale PDG inputs as used in the module).
background
Item 8 concerns the sub-leading correction to quark masses on the Recognition Science φ-ladder. Masses sit near integer rungs; the residual is the non-integer leftover after subtracting the integer step from the φ-log of an observed ratio.
The rung residual of a positive ratio $r$ at step $n$ is $\log_\varphi r - n = \ln r/\ln\varphi - n$. It measures how many fractional rungs the data sit off the pure power $\varphi^n$. Here the ratio is the PDG top over charm masses, and the integer step is 11 (the SDGT gen23 step for the up sector).
This module builds the smallest precise target that would close Item 8: residual pairs, sign-split and refined families, and unique $(c,\eta)$ fits per sector. The up gen23 residual is one coordinate of that data vector.
proof idea
Pure definitional specialization: apply the rung-residual map to the quotient of the module’s PDG top and charm constants with integer step 11. No proof obligations; the value is the real number $\ln(m_t/m_c)/\ln\varphi - 11$.
why it matters
Feeds the exact up residual pair (gen12 and gen23 coordinates from PDG ratios versus φ-steps) and the mixed-scheme up-quark η extractor, which reports η ≈ −2.72 and notes inflation from the pole versus MS-bar t/c comparison. Those objects sit inside the Item-8 closure stack: consistency of the ratio family, η-from-data identities, refined-family solvability and uniqueness, and full ∃! sector closure for negative sign class.
In the broader RS picture this is the gen23 leg of the up-sector mass formula on the φ-ladder (yardstick · φ^{rung−8+gap(Z)}), isolating the sub-leading correction the forcing chain does not fix. Closing Item 8 makes the all-sector generalization falsifiable against PDG ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.