FlavorThreshold
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assign numerical values to scale or flavor counts.
- Does not derive the beta function or running formula.
- Does not relate the scale to the RS anchor or phi-ladder rungs.
- Does not compute the change in the coupling constant.
formal statement (Lean)
281structure FlavorThreshold where
282 scale : ℝ
283 n_f_below : ℕ
284 n_f_above : ℕ
285 h_pos : 0 < scale
286 h_step : n_f_below + 1 = n_f_above
287