deltaCP_pmns_leading_order_zero
plain-language theorem explainer
The leading-order Dirac CP phase in the PMNS neutrino mixing matrix vanishes identically under the Recognition Science φ-angle construction. Neutrino phenomenologists deriving large mixing angles from golden-ratio geometry cite this baseline result. The proof reduces to a direct algebraic cancellation of two identical multiples of π/4.
Claim. In the Recognition Science derivation of the PMNS matrix, the leading-order contribution to the CP-violating phase satisfies $0 = 2π/4 - 2π/4$.
background
The module derives the PMNS neutrino mixing matrix from φ-quantized angles, with large mixing angles θ₁₂ ≈ 34°, maximal θ₂₃ ≈ 45°, and θ₁₃ ≈ 8.6°. Neutrino flavor states relate to mass eigenstates via the PMNS matrix, and the framework treats mixing angles as arising from φ-ladder geometry rather than arbitrary parameters. The upstream result from PrimitiveDistinction supplies the structural axioms that reduce to four conditions plus definitional facts, while the correction factor from QuantumChannelCapacityFromPhi supplies the finite-N φ-ladder adjustment used in related channel-capacity estimates.
proof idea
The proof is a one-line wrapper that applies the ring tactic to the arithmetic identity.
why it matters
This result supplies the structural baseline vanishing of δ_CP in the PMNS construction, feeding the module's target of a PRD paper on neutrino mixing angles from golden-ratio geometry. It isolates the observed non-zero value (≈197°) as arising solely from torsion sub-corrections, consistent with the eight-tick octave and φ-ladder quantization in the broader Recognition Science chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.