thresholdsFromBottom
plain-language theorem explainer
Singleton list of SM flavor thresholds crossed when running the bottom mass up to the RS anchor: only the top threshold (n_f: 5→6 at 172.69 GeV). Downstream mass-transport at the anchor cites it. The body is a one-element list literal of the existing top threshold record.
Claim. The list of Standard Model flavor thresholds between the bottom pole mass and the RS anchor scale $\mu^*$ consists of the single top-quark threshold: scale $172.69$, with $n_f$ stepping from $5$ below to $6$ above.
background
Module Item8ClosureTarget builds the smallest precise theorem layer that would close the open quark sub-leading correction (Item 8) and make the all-sector generalization falsifiable. Proved pieces already include ratio-family consistency, closed-form $\eta$ identities, and unique solvability of the refined family on each sign sector.
A FlavorThreshold packages one SM flavor crossing: a positive energy scale together with the active flavor counts $n_f$ immediately below and above, forced to differ by one. The top threshold is the concrete record at $172.69$ GeV with $n_f:5\to 6$.
Mass transport to the RS anchor $\mu^*$ must step through every threshold between the starting pole mass and the anchor; for the bottom quark that path only crosses the top.
proof idea
Definition by list literal. The body is the singleton [top_threshold]; no lemmas or tactics are involved. The threshold record itself already carries positivity and the $n_f$ step proofs via norm_num.
why it matters
Feeds bottomMassAtAnchor, which runs the PDG bottom mass through the piecewise $\alpha_s$ RG flow from the bottom threshold scale to the RS anchor, inserting this threshold list and $n_f=5$ as the starting flavor count. That transported mass is the numerical input the Item 8 refined-family closure needs when matching sub-leading quark residuals at a common scale.
In the broader RS ladder picture, masses sit on the $\varphi$-ladder with sector gaps; Item 8 is the remaining obstruction to a unified sub-leading formula across quark sectors. Packaging the threshold path as an explicit list keeps the transport call site auditable and swap-ready if further thresholds are later required.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.