deltaCP_pmns_range
plain-language theorem explainer
The theorem establishes that the torsion-corrected CP-violating phase in the PMNS neutrino mixing matrix lies strictly between π and 2π, matching the observed central value near 197°. Neutrino oscillation analysts and model builders comparing Recognition Science to T2K, NOvA, and DUNE data would cite the bound. The proof is a direct constructor that imports the left inequality from the third-quadrant predecessor and closes the right inequality with linear arithmetic on π positivity.
Claim. The torsion-corrected CP-violating phase δ_CP in the PMNS matrix satisfies π < δ_CP < 2π.
background
The module derives the PMNS neutrino mixing matrix from φ-quantized angles under Recognition Science, where flavor states relate to mass eigenstates via large mixing angles θ12 ≈ 34°, θ23 ≈ 45° (maximal), and θ13 ≈ 8.6°. The CP phase δ_CP arises from torsion corrections in the phase-lift construction on the circle. Upstream, the third-quadrant result supplies the concrete lower bound π together with an upper-bound fragment that the present theorem tightens to 2π.
proof idea
Constructor splits the conjunction. The left conjunct is discharged by exact application of the first projection of the third-quadrant theorem. The right conjunct binds the second projection and invokes linarith with the positivity of π.
why it matters
The result is invoked directly by the PMNS scorecard theorem that checks the phase lies in the open experimental band. It completes the SM-014 derivation of PMNS angles from golden-ratio geometry and supplies the range constraint consistent with ≈1.094π. In the broader framework it supports the claim that neutrino mixing follows from self-similar fixed-point structure rather than free parameters, feeding into tests that involve the eight-tick octave and phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.