`twoLoopAlphaSCert_holds`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS
domain: Physics
line: 132 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS on GitHub at line 132.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 132theorem twoLoopAlphaSCert_holds : TwoLoopAlphaSCert :=
 133  { b0_at5_pos := b0_at_Nf5_pos
 134    b1_at5_pos := b1_at_Nf5_pos
 135    reduces_at_anchor := alpha_s_two_loop_at_anchor }
 136
 137end
 138
 139end IndisputableMonolith.Physics.QCDRGE.TwoLoopAlphaS

papers checked against this theorem

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