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)
119noncomputable def pmns_prob (dτ : ℤ) (total_weight : ℝ) : ℝ :=
proof body
Definition body.
120 pmns_weight dτ / total_weight
121
122/-- **CONJECTURE: PMNS angles from Rung Ratios**
123 The neutrino mixing angles are forced by the rung differences.
124 - θ₁₂: Solar angle, sin²θ₁₂ ≈ solar_weight - solar_radiative_correction.
125 - θ₂₃: Atmospheric angle, sin²θ₂₃ ≈ atmospheric_weight + atmospheric_radiative_correction.
126 - θ₁₃: Reactor angle, sin²θ₁₃ ≈ reactor_weight. -/
depends on (14)
Lean names referenced from this declaration's body.
-
rung
in IndisputableMonolith.Compat.Constants
decl_use
-
rung
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
rung
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
rung
in IndisputableMonolith.Masses.RSBridge.Anchor
decl_use
-
pmns_weight
in IndisputableMonolith.Physics.MixingDerivation
decl_use
-
atmospheric_radiative_correction
in IndisputableMonolith.Physics.MixingGeometry
decl_use
-
atmospheric_weight
in IndisputableMonolith.Physics.MixingGeometry
decl_use
-
reactor_weight
in IndisputableMonolith.Physics.MixingGeometry
decl_use
-
solar_radiative_correction
in IndisputableMonolith.Physics.MixingGeometry
decl_use
-
solar_weight
in IndisputableMonolith.Physics.MixingGeometry
decl_use
-
pmns_weight
in IndisputableMonolith.Physics.PMNS.Types
decl_use
-
rung
in IndisputableMonolith.RSBridge.Anchor
decl_use
-
Rung
in IndisputableMonolith.Support.RungFractions
decl_use