structure definition def or abbrev

`WeakCouplingCert`

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

formal statement (Lean)

  95structure WeakCouplingCert where
  96  alpha_from_cube : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed))
  97  sin2_from_phi : sin2_theta_W_rs = (3 - Constants.phi) / 6
  98  alpha_W_def : alpha_W = alpha / sin2_theta_W_rs
  99  alpha_W_positive : 0 < alpha_W
 100  alpha_W_exceeds_alpha : alpha < alpha_W
 101

used by (1)

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

weak_coupling_cert in IndisputableMonolith.StandardModel.WeakCoupling decl_use

depends on (12)

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
alphaInv in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
f_gap in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
f_gap in IndisputableMonolith.Constants.GapWeight decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
sin2_theta_W_rs in IndisputableMonolith.Masses.ElectroweakMasses decl_use
f_gap in IndisputableMonolith.Pipelines decl_use
alpha_W in IndisputableMonolith.QFT.RunningCouplings decl_use
alpha_W in IndisputableMonolith.StandardModel.WeakCoupling decl_use