FlavorThreshold
plain-language theorem explainer
FlavorThreshold records a single QCD flavor threshold as a positive real scale together with the integer flavor counts immediately below and above it. Running-coupling calculations cite the record when the beta-function coefficient must jump at a quark mass. The definition is a plain structure whose two constraints are discharged by norm_num in every concrete use.
Claim. A FlavorThreshold is a record consisting of a positive real number $scale > 0$, natural numbers $n_f^-$ and $n_f^+$ satisfying $n_f^- + 1 = n_f^+$.
background
The module derives the one-loop running of the strong coupling from the phi-ladder derivative of the coupling, with the RS anchor scale fixed at 182.201 GeV. Flavor thresholds mark the discrete jumps in the number of active quarks that alter the beta-function coefficient b0. The single upstream dependency supplies the auxiliary scale function scale(k) := phi^k used to place thresholds on the energy ladder.
proof idea
Structure definition; the four fields are introduced directly with no further computation or tactic steps.
why it matters
The record supplies the common type for the concrete instances bottom_threshold, charm_threshold and top_threshold. Those instances are passed to transport_mass_through, which evolves a reference mass across successive flavor steps while switching n_f at each crossing. The construction therefore realizes the stepwise change in active flavors required by the RS renormalization-group flow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.