anchorUpGen12Residual
plain-language theorem explainer
Defines the generation-1–2 residual for the up-quark sector at the RS anchor scale: the φ-ladder excess of the transported charm-to-up mass ratio beyond the integer rung step 13. Downstream residual-pair packaging and Item 8 closure use this number as the gen12 coordinate. It is a one-line composition of the rung-residual map with the RG-transported charm and up masses.
Claim. The generation-1–2 anchor residual for the up sector is $\log_\varphi\!\bigl(m_c(\mu_*)/m_u(\mu_*)\bigr) - 13$, where $m_c(\mu_*)$ and $m_u(\mu_*)$ are the charm and up masses RG-transported to the Recognition Science anchor scale $\mu_*$, and $\varphi$ is the golden ratio.
background
Item 8 of the Recognition Science verification program concerns sub-leading quark mass corrections on the φ-ladder. Masses sit at integer rungs with a residual correction measured in rung units. The module builds the smallest precise theorem framework that would close that item and make the all-sector generalization falsifiable.
The rung residual of a positive ratio $r$ against an integer step $n$ is $\log_\varphi(r) - n$. It isolates the non-integer part of the mass ratio once the leading ladder step is subtracted. Here the ratio is formed from charm and up masses after LO transport through the piecewise $\alpha_s$ running to the common anchor scale $\mu_*$ (charm from its threshold; up from the 2 GeV reference).
The integer 13 is the nominal gen12 rung gap between charm and up on the φ-ladder under the current LO scaffold. Shell evaluation of the resulting residual pair is quoted in the doc-comment as approximately $(0.02,+0.57)$ for the up sector.
proof idea
Pure definitional abbreviation: apply the rung-residual map to the ratio of the already-defined anchor-scale charm mass over the anchor-scale up mass, with fixed integer step 13. No proof obligations beyond the noncomputable real arithmetic of Real.log and the upstream transport definitions.
why it matters
Feeds anchorUpExact, which packages this value as the gen12 field of the up-sector ResidualPair (paired with the corresponding gen23 residual). Those residual pairs are the data inputs to the refined-family solvability and uniqueness theorems in this module (refinedFamily_neg_solvable, refined_neg_sector_closure, and siblings), which aim to close Item 8: a unique sub-leading correction $(c,\eta)$ matching each sector's residuals.
In the broader RS picture the mass formula is yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$; this residual is precisely the measured gap beyond the integer rung, so it is the empirical handle on the open quark sub-leading term. The module already proves structural rigidity and $\exists!$ for refined coefficients once residuals are supplied; this definition supplies one of those residual coordinates from PDG-transported masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.