mass_ratio_rg_invariant
plain-language theorem explainer
Mass ratios of particles in the same sector remain unchanged when both are evolved under the same leading-order QCD renormalization group flow. Researchers studying quark mass running in the Standard Model would cite this invariance to preserve hierarchies across energy scales. The proof is a direct algebraic cancellation after substituting the explicit running mass formula.
Claim. Let $m_1, m_2$ be reference masses and let $r = (α_s^{target}/α_s^{ref})^{γ(n_f)}$ with $γ(n_f)$ the mass evolution exponent. If $r ≠ 0$, then $m_1 r / (m_2 r) = m_1/m_2$, where each evolved mass is defined by $m_i(α_s^{target}) = m_i · r$.
background
In the Recognition Science treatment of renormalization group flow the running mass at target coupling is defined as the reference mass multiplied by the coupling ratio raised to the power mass_evolution_exp(n_f). That exponent equals the mass anomalous dimension divided by twice the one-loop QCD coefficient b0_qcd(n_f). The module derives the beta function from the phi-ladder derivative and fixes the sign of asymptotic freedom for n_f ≤ 16.
proof idea
The term proof unfolds the running_mass definition on both sides, exposing the common multiplicative factor (α_s_target/α_s_ref) raised to mass_evolution_exp n_f. It then applies the algebraic identity mul_div_mul_right, justified by the hypothesis that this factor is nonzero, to cancel the common term and obtain the reference ratio.
why it matters
The result confirms that mass ratios are preserved under leading-order RG evolution, a basic consistency property required by the RS anchor scale and phi-ladder structure in RS_Renormalization_Running_Couplings.tex. It supports the module's key results on beta functions, running couplings, and asymptotic freedom. No downstream uses are recorded, but the invariance is a prerequisite for applying the phi-ladder mass formula across scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.