row_deltaCP_pmns_in_open_band
plain-language theorem explainer
The declaration certifies that the torsion-corrected PMNS CP-violating phase lies strictly between π and 2π radians, placing it in the third quadrant near the observed 197°. Neutrino physicists checking RS predictions against PDG or NuFIT data would cite this band to confirm quadrant consistency for the full PMNS scorecard. The proof is a direct one-line wrapper invoking the upstream deltaCP_pmns_range theorem.
Claim. $π < δ_{CP}^{PMNS,torsion} < 2π$, where $δ_{CP}^{PMNS,torsion} = π + (6/11)·(π/4)$ is the torsion correction to the PMNS Dirac CP phase.
background
The PMNSScoreCard module assembles a scorecard for full PMNS mixing in Phase 2 of the particle spectrum. It packages predicted sin²θ₁₂, sin²θ₁₃, sin²θ₂₃, Jarlskog invariant, and the δ_CP quadrant band, drawing values from MixingDerivation and PMNSMatrix while targeting PDG-like centers (sin²θ₁₂ ≈ 0.307, sin²θ₁₃ ≈ 0.0220, δ_CP ≈ 197°). The local falsifier is any NuFIT update that shifts a center outside the RS absolute-error certificates without compensating changes in α or φ-bounds.
proof idea
This is a one-line wrapper that applies the deltaCP_pmns_range theorem from the PMNSMatrix module.
why it matters
The result supplies the δ_CP open-band check required by the PMNS scorecard certificate. It is invoked inside pmnsScoreCardCert_holds to construct the full Nonempty PMNSScoreCardCert record. Module documentation classifies the angle matches and δ_CP band as PARTIAL_THEOREM, noting scheme dependence of sin²θ_W and PMNS parameters as a named residual. It realizes the PMNS quadrant prediction arising from the torsion correction in the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.