pith. machine review for the scientific record. sign in
structure definition def or abbrev

BosonVerificationCert

show as:
view Lean formalization →

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)

  94structure BosonVerificationCert where
  95  weinberg_angle : (0.2302 : ℝ) < sin2_theta_W ∧ sin2_theta_W < 0.2304
  96  cos2_theta : (0.7696 : ℝ) < cos2_theta_W ∧ cos2_theta_W < 0.7698
  97  wz_ratio_from_phi : wz_mass_ratio_sq = cos2_theta_W
  98  sector_params : B_pow .Electroweak = 1 ∧ r0 .Electroweak = 55
  99

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.