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)
48theorem alpha_W_expanded :
49 alpha_W = alpha / ((3 - Constants.phi) / 6) := rfl
proof body
Term-mode proof.
50
51/-! ## Part 2: Positivity and Bounds -/
52
depends on (5)
Lean names referenced from this declaration's body.
-
alpha
in IndisputableMonolith.Constants.Alpha
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
alpha_W
in IndisputableMonolith.QFT.RunningCouplings
decl_use
-
alpha_W
in IndisputableMonolith.StandardModel.WeakCoupling
decl_use