sin2_theta23_observed

formal source

  46
  47/-- The atmospheric mixing angle θ₂₃ ≈ 49° (sin²θ₂₃ ≈ 0.545). -/
  48noncomputable def theta23_degrees : ℝ := 49.0
  49noncomputable def sin2_theta23_observed : ℝ := 0.545
  50
  51/-- The reactor mixing angle θ₁₃ ≈ 8.57° (sin²θ₁₃ ≈ 0.0220). -/
  52noncomputable def theta13_degrees : ℝ := 8.57
  53noncomputable def sin2_theta13_observed : ℝ := 0.0220
  54
  55/-- The CP-violating phase δ_CP ≈ 197° (normal ordering). -/
  56noncomputable def deltaCP_degrees : ℝ := 197
  57
  58/-! ## The PMNS Matrix Structure -/
  59
  60/-- The PMNS matrix in standard parametrization:
  61
  62U = ⎛ c₁₂c₁₃         s₁₂c₁₃         s₁₃e^{-iδ} ⎞
  63    ⎜ -s₁₂c₂₃-c₁₂s₂₃s₁₃e^{iδ}  c₁₂c₂₃-s₁₂s₂₃s₁₃e^{iδ}  s₂₃c₁₃ ⎟
  64    ⎝ s₁₂s₂₃-c₁₂c₂₃s₁₃e^{iδ}  -c₁₂s₂₃-s₁₂c₂₃s₁₃e^{iδ}  c₂₃c₁₃ ⎠
  65
  66where c_ij = cos θ_ij and s_ij = sin θ_ij
  67-/
  68structure PMNSParameters where
  69  theta12 : ℝ  -- Solar angle
  70  theta23 : ℝ  -- Atmospheric angle
  71  theta13 : ℝ  -- Reactor angle
  72  deltaCP : ℝ  -- CP phase
  73
  74/-- The best-fit PMNS parameters. -/
  75noncomputable def bestFitPMNS : PMNSParameters := {
  76  theta12 := theta12_degrees * Real.pi / 180,
  77  theta23 := theta23_degrees * Real.pi / 180,
  78  theta13 := theta13_degrees * Real.pi / 180,
  79  deltaCP := deltaCP_degrees * Real.pi / 180