low_Q_log_negative
plain-language theorem explainer
The declaration shows that ln(Q²/M_Z²) is negative for any positive Q below the Z-boson mass. QCD phenomenologists would invoke it when verifying that the strong coupling grows toward infrared scales. The proof reduces to the standard criterion for a negative logarithm by establishing that the ratio inside is positive yet smaller than one.
Claim. Let $M_Z = 91.1876$ GeV denote the Z-boson mass. Then for every real number $Q$ satisfying $0 < Q < M_Z$, one has $ln(Q^2/M_Z^2) < 0$.
background
The module derives the one-loop running of the strong coupling α_s within Recognition Science. It sets α_s(M_Z) = 2/17 and employs the beta function b₀ = (11N_c - 2N_f)/(12π) with N_c = 3. The logarithm ln(Q²/M_Z²) appears in the explicit solution for α_s(Q). M_Z_GeV is defined as the numerical value 91.1876 GeV. The upstream definition supplies the reference scale at which the coupling is normalized.
proof idea
The proof applies the lemma Real.log_neg, which states that log x < 0 whenever 0 < x < 1. It first confirms positivity of the ratio Q²/M_Z² by positivity of squares, then shows the ratio is less than one by rewriting the inequality Q < M_Z and using nlinarith on the squared terms.
why it matters
This result supplies the sign needed for the infrared growth of α_s in the one-loop formula, consistent with asymptotic freedom. It supports the RS claim that α_s reaches order-one values near nuclear scales. The parent running formula alpha_s_running relies on this sign to guarantee the correct monotonicity below M_Z. No open questions are attached; the statement is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.