bottom_threshold
plain-language theorem explainer
bottom_threshold supplies the concrete flavor threshold data at the bottom quark mass scale of 4.18 GeV, with four active flavors below and five above. QCD phenomenologists computing the running of the strong coupling would cite this definition when crossing the b-quark threshold in the beta function. The definition is a direct record constructor whose two proof obligations are discharged by norm_num.
Claim. The bottom quark flavor threshold is the structure with scale $4.18$, $n_{f,below}=4$, $n_{f,above}=5$, satisfying $0<4.18$ and $4+1=5$.
background
FlavorThreshold is the structure that packages SM flavor threshold data: a positive real scale together with the integer counts of active flavors immediately below and above that scale, plus the two obvious proofs that the scale is positive and that the flavor counts differ by one. The module obtains the beta function as the ladder derivative of the coupling with respect to the Recognition Science phi-ladder and shows that asymptotic freedom holds for $n_f$ up to 16. The upstream scale definition in LargeScaleStructureFromRS supplies noncomputable powers of phi, but the present definition inserts the empirical numerical value 4.18 GeV for the bottom threshold.
proof idea
The definition is a one-line record constructor that sets scale to 4.18, n_f_below to 4, n_f_above to 5 and closes the two field proofs with norm_num.
why it matters
This definition supplies the numerical threshold needed to step the beta function when the strong coupling is evolved across the bottom quark mass inside the RS renormalization framework. It feeds the running-coupling formulas and the asymptotic-freedom criterion that follow from the phi-ladder derivative of the coupling. The construction is consistent with the T5 J-uniqueness and T7 eight-tick octave that fix the discrete ladder on which the beta function is defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.