theorem
proved
lambda_pos
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.RGTransport on GitHub at line 95.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
92def lambda : ℝ := Real.log phi
93
94/-- λ is positive. -/
95theorem lambda_pos : lambda > 0 := by
96 have h : 1 < phi := one_lt_phi
97 exact Real.log_pos h
98
99/-! ## Canonical one-loop beta/gamma kernels (Level-B groundwork) -/
100
101/-- One-loop QCD beta coefficient in the convention `beta0 = 11 - 2*nf/3`. -/
102def beta0QCD (nf : ℕ) : ℚ := (11 : ℚ) - (2 : ℚ) * nf / 3
103
104/-- Real-valued view of `beta0QCD`. -/
105def beta0QCDReal (nf : ℕ) : ℝ := (beta0QCD nf : ℝ)
106
107/-- One-loop QCD running for `alpha_s`:
108`d alpha_s / d ln mu = -(beta0/(2*pi)) * alpha_s^2`. -/
109noncomputable def betaQCD1L (nf : ℕ) (alphaS : ℝ) : ℝ :=
110 -((beta0QCDReal nf) / (2 * Real.pi)) * alphaS ^ 2
111
112/-- One-loop QED running with an effective charge-weight factor.
113This keeps the kernel explicit while allowing policy-level charge sums. -/
114noncomputable def betaQED1L (chargeWeight : ℝ) (alpha : ℝ) : ℝ :=
115 (chargeWeight / (3 * Real.pi)) * alpha ^ 2
116
117/-- Minimal one-loop mass anomalous-dimension scaffold for QCD.
118The exact scheme-dependent higher-loop expression is left to Level-B extensions. -/
119noncomputable def gammaMassQCD1L (alphaS : ℝ) : ℝ :=
120 (2 / Real.pi) * alphaS
121
122/-- Minimal one-loop mass anomalous-dimension scaffold for QED. -/
123noncomputable def gammaMassQED1L (chargeSq : ℝ) (alpha : ℝ) : ℝ :=
124 (3 * chargeSq / (4 * Real.pi)) * alpha
125