deltaCP_degrees
deltaCP_degrees supplies the numerical value 197 for the CP-violating phase δ_CP in the PMNS neutrino mixing matrix under normal ordering. Neutrino physicists constructing best-fit parameter sets for oscillation analyses would cite this constant. The definition is a direct real-number assignment with no lemmas or computation.
claimThe CP-violating phase in the standard parametrization of the PMNS matrix is fixed at $δ_{CP} = 197^∘$ for normal neutrino mass ordering.
background
The PMNS matrix relates neutrino flavor eigenstates (ν_e, ν_μ, ν_τ) to mass eigenstates (ν_1, ν_2, ν_3) via large mixing angles θ₁₂ ≈ 34°, θ₂₃ ≈ 45° (maximal), and θ₁₃ ≈ 8.6°. Recognition Science treats these angles as φ-quantized, with the maximal atmospheric angle pointing to an underlying symmetry distinct from the small-angle CKM matrix. The module sets the target of deriving the full PMNS structure from RS, citing the paper proposition on neutrino mixing angles from golden ratio geometry.
proof idea
The definition is a direct constant assignment of the real number 197. No upstream lemmas are invoked; the value serves as an empirical anchor passed downstream to bestFitPMNS.
why it matters in Recognition Science
This constant is consumed by bestFitPMNS to assemble the complete PMNS parameter record in radians. It supplies the experimental input slot in the SM-014 derivation of PMNS from φ-angles, where the large mixing pattern is contrasted with CKM and tied to the eight-tick octave and φ-ladder structure. The 197° value remains an empirical anchor rather than a first-principles prediction from J-cost or defectDist.
scope and limits
- Does not derive the numerical value from Recognition Science axioms or the RCL.
- Does not encode dependence on normal versus inverted mass ordering.
- Does not attach experimental uncertainty intervals.
- Does not compute the phase via CirclePhaseLift bounds or log-derivative estimates.
Lean usage
noncomputable def bestFitPMNS : PMNSParameters := { theta12 := theta12_degrees * Real.pi / 180, theta23 := theta23_degrees * Real.pi / 180, theta13 := theta13_degrees * Real.pi / 180, deltaCP := deltaCP_degrees * Real.pi / 180 }formal statement (Lean)
56noncomputable def deltaCP_degrees : ℝ := 197
proof body
Definition body.
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-/