bottomMassAtAnchor
plain-language theorem explainer
Defines the bottom-quark mass evolved from the PDG pole value at the bottom threshold up to the RS anchor scale μ* ≈ 182.2 GeV. Anyone comparing generation-23 down-sector mass ratios at the common RS anchor cites this number. It is a direct application of multi-segment RG mass transport through the listed flavor thresholds with piecewise one-loop α_s.
Claim. Let $m_b^{\mathrm{PDG}} = 4180\,\mathrm{MeV}$ be the PDG bottom mass, $\alpha_s^{\mathrm{pw}}$ the piecewise one-loop strong coupling stitched across heavy-quark thresholds, $\mu_b = 4.18\,\mathrm{GeV}$ the bottom threshold, and $\mu^* = 182.201\,\mathrm{GeV}$ the RS anchor. Then $m_b(\mu^*)$ is the mass obtained by transporting $m_b^{\mathrm{PDG}}$ from $\mu_b$ to $\mu^*$ through the bottom-sector threshold list, starting with $n_f = 5$.
background
Item 8 of the Recognition Science verification program asks for a unified sub-leading correction to the phi-ladder mass formula in the quark sector. Residuals are compared at a single common scale, the RS anchor $\mu^* = 182.201,\mathrm{GeV}$, the stationarity point of the RG flow. Raw PDG masses sit at flavor thresholds, so each must be run to $\mu^*$ before ratios enter the residual signature.
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 using a supplied $\alpha_s(\mu)$. The piecewise coupling $\alpha_s^{\mathrm{pw}}$ stitches one-loop running across top, bottom, and charm thresholds. The bottom threshold is fixed at $4.18,\mathrm{GeV}$ with $n_f$ jumping from 4 to 5; the PDG bottom mass is $4180,\mathrm{MeV}$.
proof idea
Pure definition: one call to multi-segment mass transport. Arguments are the PDG bottom mass, the piecewise $\alpha_s$, start scale equal to the bottom threshold, end scale equal to the RS anchor, the bottom-sector threshold list, and initial flavor count $n_f = 5$. No lemmas or tactics; the value is whatever the transport function returns.
why it matters
Feeds the generation-23 down-sector residual at the anchor: the ratio of this bottom mass to the corresponding strange mass at $\mu^*$, passed to the rung-residual map at rung 8. That residual is part of the Item 8 closure target, which aims to make the all-sector sub-leading mass formula falsifiable. Without a common-scale bottom mass, the down-sector gen23 residual cannot be formed, and the refined-family uniqueness results in this module have nothing to match against PDG data. Ties to the RS mass ladder (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}}$) by supplying the RG-corrected input that the residual measures against the pure ladder prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.