`lambda`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.RGTransport
domain: Physics
line: 92 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.RGTransport on GitHub at line 92.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  89/-! ## RG Transport Integral -/
  90
  91/-- The λ-normalization constant: `λ = ln(φ)`. -/
  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. -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.