log_at_MZ
plain-language theorem explainer
At the Z boson mass scale the logarithm in the one-loop running formula for the strong coupling vanishes. Particle physicists modeling QCD evolution or Recognition Science derivations of α_s would cite this identity. The proof is a one-line term reduction that rewrites the argument as one and applies the logarithm of unity.
Claim. $log((M_Z^2 / M_Z^2)) = 0$, where $M_Z$ denotes the Z-boson mass in GeV.
background
The module treats the running of the strong coupling α_s within Recognition Science. It employs the one-loop beta function with b₀ = (11N_c - 2N_f)/(12π) > 0, yielding asymptotic freedom for N_f < 17. The constant M_Z_GeV is fixed at 91.1876 GeV as the reference scale where α_s equals 2/17.
proof idea
The term proof first rewrites the ratio M_Z_GeV² / M_Z_GeV² using self-division, justified by positivity after unfolding the definition. It then applies the fact that the logarithm of one is zero.
why it matters
This identity supplies the reference point for the running α_s formula in the Recognition Science treatment of the strong force. It anchors the one-loop evolution from the Z scale down to nuclear energies, consistent with the asymptotic freedom built into the beta function. No parent theorems are listed yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.