def definition def or abbrev

`alpha_W`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  48noncomputable def alpha_W : ℝ := 1/30

proof body

Definition body.

  49
  50/-! ## The Beta Function -/
  51
  52/-- The beta function describes how a coupling changes with scale:
  53    β(g) = μ dg/dμ. For QED β > 0; for QCD β < 0 (asymptotic freedom). -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

alpha_W in IndisputableMonolith.StandardModel.WeakCoupling decl_use
alpha_W_expanded in IndisputableMonolith.StandardModel.WeakCoupling decl_use
alpha_W_gt_alpha in IndisputableMonolith.StandardModel.WeakCoupling decl_use
alpha_W_gt_two_alpha in IndisputableMonolith.StandardModel.WeakCoupling decl_use
alpha_W_pos in IndisputableMonolith.StandardModel.WeakCoupling decl_use
WeakCouplingCert in IndisputableMonolith.StandardModel.WeakCoupling decl_use

depends on (5)

Lean names referenced from this declaration's body.

scale in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
beta in IndisputableMonolith.Relativity.ILG.PPN decl_use
alpha_W in IndisputableMonolith.StandardModel.WeakCoupling decl_use
beta in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use