charmMassAtAnchor
plain-language theorem explainer
Defines the charm-quark mass after RG transport from the PDG charm threshold to the RS anchor μ* ≈ 182.2 GeV. Downstream residual constructions for up-sector gen12 and gen23 cite it as the common intermediate mass. The body is a direct application of multi-segment mass transport through the listed flavor thresholds with piecewise one-loop α_s and n_f = 4 at the start.
Claim. The charm mass at the RS anchor is the real number obtained by transporting the PDG charm mass $m_c^{\mathrm{PDG}} = 1270\,\mathrm{MeV}$ from the charm threshold scale $\mu_c = 1.27\,\mathrm{GeV}$ to the RS anchor $\mu^* = 182.201\,\mathrm{GeV}$, using the piecewise one-loop $\alpha_s$ and the charm-and-above threshold list, with initial active flavor count $n_f = 4$.
background
Item 8 Closure Target builds the smallest precise theorem layer that would close the open quark sub-leading correction and make the all-sector generalization falsifiable. Residuals at the RS anchor need masses evaluated at a common scale rather than at their native PDG thresholds.
The RS anchor $\mu^* = 182.201,\mathrm{GeV}$ is the stationarity point of the RG flow used throughout the running-couplings module. Multi-segment mass transport runs a reference mass from $\mu_{\mathrm{start}}$ to $\mu_{\mathrm{end}}$ through a list of flavor thresholds, switching $n_f$ at each crossing and evaluating $\alpha_s$ at the endpoints of each segment. Here $\alpha_s$ is the piecewise one-loop coupling stitched across top, bottom, and charm thresholds.
The PDG charm input is the fixed real $1270$ (MeV convention in this module). The charm threshold carries scale $1.27,\mathrm{GeV}$ with $n_f$ stepping $3\to 4$. Transport therefore starts above charm with $n_f=4$ and walks upward to $\mu^*$.
proof idea
Pure definitional wrapper: no proof obligations. The right-hand side is a single call to multi-segment mass transport with arguments (PDG charm mass, piecewise $\alpha_s$, charm-threshold scale, RS anchor scale, the charm-and-above threshold list, initial $n_f=4$). Evaluation is delegated entirely to that transport function and the stitched $\alpha_s$ pieces.
why it matters
Anchor-scale charm mass is the shared intermediate for up-sector residual ratios. anchorUpGen12Residual forms the rung residual of charm/up at step 13; anchorUpGen23Residual forms the residual of top/charm at step 11. Those residuals feed the refined-family solvability and uniqueness results that close Item 8 for each sign class.
In the broader RS picture this is bookkeeping, not a new forcing step: masses sit on the $\phi$-ladder with yardstick and rung corrections, but sub-leading quark corrections require a common RG scale before residual signatures can be compared to the structural identities (consistency of the ratio family, $\eta$ closed forms, $\exists!$ refined coefficients). Without transported charm, gen12 and gen23 up residuals are ill-defined at $\mu^*$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.