charm_threshold
plain-language theorem explainer
The charm_threshold definition supplies the SM flavor threshold data for the charm quark in the RS-derived renormalization group equations. It sets the threshold scale at 1.27 GeV with the active flavor count stepping from 3 to 4. QCD phenomenologists would cite this when computing the running of alpha_s across the charm mass in the phi-ladder beta function. The definition is a direct structure instantiation with positivity and step conditions discharged by norm_num.
Claim. The charm flavor threshold is the structure with scale $1.27$, $n_f$ below equal to 3, $n_f$ above equal to 4, satisfying $0 < 1.27$ and $n_f$ below $+1 = n_f$ above.
background
In the RS renormalization group framework the beta function for the strong coupling is obtained from the derivative of the coupling along the phi-ladder. Flavor thresholds mark the points at which a new quark mass is crossed and the number of active flavors in the beta-function coefficient increases by one. The FlavorThreshold structure packages the threshold scale together with the flavor counts below and above it, plus the two hypotheses that the scale is positive and that the flavor count steps by exactly one.
proof idea
The declaration directly constructs the FlavorThreshold structure by assigning the numerical scale 1.27 together with n_f_below = 3 and n_f_above = 4. The two hypotheses 0 < scale and n_f_below + 1 = n_f_above are discharged by the norm_num tactic.
why it matters
This supplies one of the quark mass thresholds required to integrate the running of alpha_s through the full SM flavor content. It feeds the alpha_s_running and rs_alpha_s_perturbative constructions that ultimately anchor the strong coupling at the Z mass. Within the Recognition Science chain it realizes the step-wise change in the beta-function coefficient at each phi-ladder rung corresponding to a new flavor, consistent with the eight-tick octave and the forced D=3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.