transport_mass_through
plain-language theorem explainer
The multi-segment mass transport function computes the evolved mass at the final scale by crossing a sequence of flavor thresholds and updating the active quark count at each step. QCD model builders working within the Recognition Science φ-ladder would invoke it to propagate reference masses consistently through the renormalization group flow. Implementation reduces to recursive application of the single-sector mass evolution formula on successive intervals.
Claim. The mass at scale $μ_{end}$ obtained from reference mass $m_{ref}$ at $μ_{start}$ by successive application of the leading-order QCD mass evolution formula across intervals delimited by the scales in a list of flavor thresholds, with the number of active flavors $n_f$ incremented by one at each threshold crossing.
background
In the RS renormalization group setup the coupling $α_s(μ)$ runs according to the β-function derived from the φ-ladder derivative. FlavorThreshold encodes the scale at which a new quark flavor becomes active, together with the step in $n_f$. The upstream running_mass computes the evolved mass within a fixed-$n_f$ sector via $m_{ref} · (α_{s,target} / α_{s,ref})^{γ_0/(2b_0)}$ where the exponent depends on $n_f$. The module establishes that asymptotic freedom holds for $n_f ≤ 16$ and anchors the RS scale at 182.201 GeV.
proof idea
The definition proceeds by pattern-matching on the list of thresholds. When the list is empty or the target scale lies before the next threshold, it applies running_mass directly with the initial $n_f$. Otherwise it evolves the mass up to the current threshold scale, then recurses on the remaining list with the updated $n_f$ supplied by the threshold record.
why it matters
This definition supplies the multi-threshold mass transport needed to connect low-scale reference masses to high-scale observables while respecting the stepwise change in active flavors forced by the RS φ-ladder. It sits inside the RunningCouplings module whose results on β-function sign and $α_s(M_Z) ≈ 0.1185$ rely on consistent mass evolution across sectors. No downstream uses are recorded yet, leaving open the question of its integration into full spectrum calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.