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)
44def alpha_W : ℝ := alpha / sin2_theta_W_rs
proof body
Definition body.
45
46/-- α_W expressed in terms of RS primitives:
47 α_W = (1/alphaInv) / ((3 − φ)/6) = 6 / (alphaInv · (3 − φ)) -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.
-
alpha_W
in IndisputableMonolith.QFT.RunningCouplings
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 (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
alpha
in IndisputableMonolith.Constants.Alpha
decl_use
-
alphaInv
in IndisputableMonolith.Constants.Alpha
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
sin2_theta_W_rs
in IndisputableMonolith.Masses.ElectroweakMasses
decl_use
-
alpha_W
in IndisputableMonolith.QFT.RunningCouplings
decl_use