anchorUpGen23Residual
plain-language theorem explainer
Defines the generation-2–3 residual for the up-type quark sector at the RS anchor: the φ-ladder excess of the top-to-charm mass ratio after subtracting eleven rungs. Downstream residual-pair constructions and Item 8 closure targets cite it as the gen23 coordinate of the up-sector data. The body is a one-line application of the rung-residual map to the RG-transported top/charm ratio.
Claim. The generation-2–3 up-sector residual at the Recognition anchor is $\log_\varphi(m_t^{\mathrm{anc}}/m_c^{\mathrm{anc}}) - 11$, where $m_t^{\mathrm{anc}}$ and $m_c^{\mathrm{anc}}$ are the top and charm pole masses transported by the LO running coupling to the RS anchor scale.
background
Item 8 of the Recognition verification stack concerns the sub-leading correction to quark mass ratios on the $\varphi$-ladder. Masses sit near integer rungs of $\varphi$, so the leading prediction is an integer step; the residual is the fractional excess in rung units.
The rung residual of a positive ratio $r$ against step $n$ is $\log_\varphi r - n = \log r/\log\varphi - n$. It measures how far the observed ratio sits from a pure $\varphi^n$ scaling. Here the ratio is top over charm after both masses have been RG-transported from their PDG thresholds to the common RS anchor scale (via the piecewise $\alpha_s$ running used elsewhere in the module).
The local module builds the smallest precise theorem framework that would close Item 8 and make the all-sector generalization falsifiable. Anchor-scale residuals for each charged sector supply the numerical data that the refined residual family and uniqueness theorems act on.
proof idea
Pure definitional wrapper. Evaluate the rung residual on the quotient of the two already-defined anchor masses topMassAtAnchor / charmMassAtAnchor with integer step $11$. No tactics, no lemmas beyond the three inlined definitions.
why it matters
Feeds anchorUpExact, which packages the up-sector gen12 and gen23 residuals into a ResidualPair. That pair is the concrete data object against which the refined-family solvability and uniqueness results of this module (and ultimately the Item 8 closure target) are checked.
In the broader RS picture the integer step $11$ is the leading $\varphi$-ladder gap between charm and top; the residual isolates the sub-leading correction that Item 8 must absorb. Closing that item is what makes the all-sector mass-ratio generalization falsifiable against PDG data. The definition itself is scaffolding input, not a proved claim: its numerical content inherits the LO RG transport assumptions of the upstream mass anchors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.