low_Q_log_negative
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute the numerical value of α_s at any specific low scale.
- Does not incorporate two-loop or higher beta-function terms.
- Applies only to real positive Q; does not address complex scales.
- Relies on the fixed numerical value of M_Z_GeV without deriving it.
- Does not prove asymptotic freedom itself, only the sign of this logarithm.
formal statement (Lean)
60theorem low_Q_log_negative (Q : ℝ) (hQ : 0 < Q) (h : Q < M_Z_GeV) :
61 Real.log (Q ^ 2 / M_Z_GeV ^ 2) < 0 := by
proof body
Term-mode proof.
62 apply Real.log_neg
63 · apply div_pos (sq_pos_of_pos hQ)
64 exact sq_pos_of_pos (by unfold M_Z_GeV; norm_num)
65 · rw [div_lt_one (by unfold M_Z_GeV; positivity)]
66 nlinarith [sq_nonneg Q, sq_nonneg M_Z_GeV, sq_abs (Q - M_Z_GeV)]
67
68/-- At Q = M_Z the log vanishes so α_s = α_s(M_Z). -/