top_threshold
plain-language theorem explainer
The top_threshold definition supplies the SM flavor threshold data for the top quark at scale 172.69 GeV, switching active flavors from 5 to 6. Researchers computing the running of alpha_s across energy scales in the Recognition Science phi-ladder framework would cite this instance when crossing the top mass. It is a direct structure instantiation with norm_num discharging the positivity and increment conditions.
Claim. The top flavor threshold is the structure instance with scale $172.69$, $n_{f,below}=5$, $n_{f,above}=6$, satisfying $0<172.69$ and $n_{f,below}+1=n_{f,above}$.
background
The module treats renormalization group flow in Recognition Science via the phi-ladder, with the RS anchor scale as a stationarity point and the beta function sign fixed by the ladder derivative of the coupling. Flavor thresholds mark discrete changes in active quark flavors that alter the beta function coefficient. Upstream structures encode nuclear densities on phi-tiers and J-cost from primitive distinctions, supplying the discrete foundation that continuous RG evolution rests upon.
proof idea
The definition constructs the FlavorThreshold instance by direct field assignment of the numerical scale and flavor counts, then applies norm_num to discharge the positivity hypothesis and the flavor increment condition.
why it matters
This supplies the top quark threshold data required for multi-segment mass transport of couplings in the RS renormalization framework. It supports alpha_s evolution formulas by switching n_f at each crossing and connects to the phi-ladder derivative that determines the beta function sign, ensuring consistency with asymptotic freedom for n_f up to 16. The definition fills a concrete data point in the running couplings paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.