thresholdsFromTwoGeV
plain-language theorem explainer
Fixed list of SM flavor thresholds crossed when running light-quark masses upward from the 2 GeV reference to the RS anchor. Anyone transporting PDG up/down/strange masses through the piecewise α_s ladder cites it. The body is a two-element list literal of the bottom and top thresholds.
Claim. The threshold list for upward mass transport from $2\,\mathrm{GeV}$ is the ordered pair of Standard Model flavor thresholds at the bottom and top quark poles: $m_b \approx 4.18\,\mathrm{GeV}$ ($n_f: 4\to 5$) and $m_t \approx 172.69\,\mathrm{GeV}$ ($n_f: 5\to 6$).
background
Item 8 Closure Target builds the smallest precise theorem layer that would close the open quark sub-leading mass correction and make the all-sector generalization falsifiable. Light-quark PDG masses sit at a $2,\mathrm{GeV}$ reference; RS comparisons need them at the recognition anchor $\mu^*$.
A flavor threshold records a heavy-quark pole scale together with the active-flavor counts just below and above it, with positivity and the unit step $n_f^{\mathrm{below}}+1=n_f^{\mathrm{above}}$. The bottom threshold is fixed at $4.18,\mathrm{GeV}$ ($4\to 5$ flavors); the top at $172.69,\mathrm{GeV}$ ($5\to 6$). Between thresholds the strong coupling runs with fixed $n_f$; each crossing updates the beta-function coefficients used by the mass-transport map.
proof idea
Pure definition: a two-element list literal packing the preexisting bottom and top flavor-threshold records. No proof obligations beyond the structure fields already discharged at those upstream definitions (norm_num for positivity and the $n_f$ step).
why it matters
Feeds the three light-quark anchor-mass definitions upMassAtAnchor, downMassAtAnchor, and strangeMassAtAnchor, each calling transport_mass_through from the $2,\mathrm{GeV}$ reference to the RS anchor with this threshold list and $n_f=4$ at the start. Those transported masses are the numerical inputs against which Item 8's refined residual family (unique $(c,\eta)$ per sign sector) is checked. Without a canonical threshold list the upward RG path is ambiguous, so the sub-leading correction item cannot be closed or falsified against PDG data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.