No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
123structure TwoLoopAlphaSCert where
124 /-- One-loop coefficient is positive at N_f = 5. -/
125 b0_at5_pos : 0 < b0 5
126 /-- Two-loop coefficient is positive at N_f = 5. -/
127 b1_at5_pos : 0 < b1 5
128 /-- The running formula reduces to identity at the anchor scale. -/
129 reduces_at_anchor : ∀ (alpha_0 : ℝ) (N_f : ℕ) (mu_0_GeV : ℝ),
130 0 < mu_0_GeV → alpha_s_two_loop alpha_0 N_f mu_0_GeV mu_0_GeV = alpha_0
131
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (10)
Lean names referenced from this declaration's body.
-
scale
in IndisputableMonolith.Cosmology.LargeScaleStructureFromRS
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
alpha_s_two_loop
in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
decl_use
-
b0
in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
decl_use
-
b1
in IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use