thresholdsFromCharm
plain-language theorem explainer
Lists the SM flavor thresholds that sit above the charm scale: bottom at 4.18 GeV (n_f: 4→5) and top at 172.69 GeV (n_f: 5→6). Anyone transporting a charm mass from its pole to the RS anchor cites this list as the intermediate crossing schedule. The body is a two-element list literal of the existing threshold records.
Claim. The ordered list of Standard Model flavor thresholds above the charm scale consists of the bottom threshold (scale $4.18$, $n_f$ stepping $4\to 5$) and the top threshold (scale $172.69$, $n_f$ stepping $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. Mass transport between a PDG pole and the RS anchor must cross heavy-flavor thresholds where the active flavor count $n_f$ jumps.
A flavor threshold is a record with positive scale, integer $n_f$ below and above, and the step identity $n_f^{\mathrm{below}}+1=n_f^{\mathrm{above}}$. The bottom threshold is fixed at scale $4.18$ with $n_f:4\to 5$; the top threshold at $172.69$ with $n_f:5\to 6$. Both come from the running-couplings module and carry positivity and step proofs by norm_num.
For charm, the only thresholds between the charm pole and a high RS anchor are bottom and top; charm itself is the starting scale, not an intermediate crossing.
proof idea
Definitional list literal. No proof obligations: the two upstream threshold definitions already discharge positivity and the $n_f$ step. The body is simply the ordered pair [bottom_threshold, top_threshold].
why it matters
Feeds charmMassAtAnchor, which runs transport_mass_through from the PDG charm pole to the RS anchor under the piecewise $\alpha_s$ schedule, using this list as the intermediate threshold itinerary and starting $n_f=4$. Without an explicit above-charm schedule, the RG mass transport used in Item 8 residual comparisons is not pinned down.
In the broader Recognition framework this is bookkeeping infrastructure for the quark-sector sub-leading correction (Item 8), not a forcing-chain step. It does not touch T5–T8, the RCL, or the $\phi$-ladder mass formula directly; it only makes the running input to those mass comparisons concrete and auditable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.