topMassAtAnchor
plain-language theorem explainer
Defines the top-quark mass evaluated at the Recognition Science anchor scale by LO RG transport of the PDG top mass. Downstream residual constructions for up-type gen-2/3 cite this value as the numerator mass. The body is a direct call to the mass-transport helper with piecewise α_s, top-threshold start scale, empty intermediate threshold list, and six active flavors.
Claim. Let $m_t^{\mathrm{PDG}}$ be the PDG top mass. The top mass at the RS anchor is the real number obtained by transporting $m_t^{\mathrm{PDG}}$ under leading-order running of $\alpha_s$ (piecewise) from the top-threshold scale down to the RS anchor scale, with no intermediate thresholds and six active flavors.
background
Item 8 in the verification stack concerns sub-leading quark mass corrections on the φ-ladder. The module builds a minimal theorem framework so that those corrections become a falsifiable, all-sector formula rather than ad-hoc fits.
Masses enter residual comparisons only after they sit at a common scale. The RS anchor scale is that common reference; PDG inputs live at species thresholds (here the top threshold). Transport uses LO running of α_s via a piecewise coupling, matching the scaffold already used for other sector residuals.
Upstream scaffolding includes rung indexing on the φ-ladder, shell/capacity scales from periodic blocks, and species DOF tables (up/down as 12-DOF deconfined quarks). Those fix how transported masses later convert into rung residuals, not the transport step itself.
proof idea
Pure definition: one application of Physics.RG.transport_mass_through to the PDG top mass, the piecewise α_s runner, start scale top_threshold.scale, end scale rs_anchor_scale, empty intermediate-threshold list, and flavor count 6. No lemmas, no tactics.
why it matters
Feeds anchorUpGen23Residual, which forms the gen-2/3 up-type residual as the rung residual of the ratio (top mass at anchor)/(charm mass at anchor) against rung 11. That residual is part of the Item 8 closure target: matching predicted vs observed sub-leading corrections once LO transport puts all masses on the same scale.
In the broader RS picture, bare masses sit on the φ-ladder (yardstick · φ^(rung−8+gap(Z))). Anchor-scale transport is the bridge from PDG numbers into that ladder language so residual signatures (up/down/lepton families in this module) can be compared without scale mismatch. The module already proves structural rigidity and unique refined-family coefficients; this def supplies the numerical top endpoint those residual defs need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.