pith. machine review for the scientific record. sign in
def

theta12_degrees

definition
show as:
view math explainer →
module
IndisputableMonolith.StandardModel.PMNSMatrix
domain
StandardModel
line
44 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.StandardModel.PMNSMatrix on GitHub at line 44.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  41/-! ## Observed PMNS Parameters -/
  42
  43/-- The solar mixing angle θ₁₂ ≈ 33.44° (sin²θ₁₂ ≈ 0.307). -/
  44noncomputable def theta12_degrees : ℝ := 33.44
  45noncomputable def sin2_theta12_observed : ℝ := 0.307
  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. -/