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)
73theorem sin2_pos : 0 < sin2_theta_W_rs := sin2_theta_positive
proof body
Term-mode proof.
74
75/-- sin²θ_W < 1/2 (the weak mixing is mild). -/
depends on (6)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
sin2_theta_positive
in IndisputableMonolith.Masses.ElectroweakMasses
decl_use
-
sin2_theta_W_rs
in IndisputableMonolith.Masses.ElectroweakMasses
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use