deltaCP_prediction_matches
plain-language theorem explainer
The theorem shows that the RS-predicted CP-violating phase for neutrinos satisfies π < δ_CP < 2π, placing the φ-derived value near 191° inside the interval that contains the observed 197°. Neutrino phenomenologists comparing golden-ratio mixing models to oscillation data would cite this bound. The proof unfolds the explicit expression for the predicted phase, invokes the elementary bounds 1 < φ < 2, and applies positivity and comparison lemmas for π to bound the correction term between 0 and π/10.
Claim. Let φ = (1 + √5)/2. Define the RS-predicted CP phase by δ_CP = π + (φ − 1)π/10. Then π < δ_CP < 2π.
background
The module derives the PMNS neutrino mixing matrix from Recognition Science by quantizing the three mixing angles in units of the golden ratio φ. Neutrino flavor states are related to mass eigenstates through large angles (θ12 ≈ 34°, θ23 ≈ 45°, θ13 ≈ 8.6°), with the CP phase δ_CP appearing in the standard parametrization of the unitary matrix. The local setting is the φ-angle construction for the PMNS parameters, where the maximal atmospheric angle and the solar angle are fixed by self-similar fixed-point properties of φ. Upstream lemmas supply the numerical bounds 1 < φ < 2 together with the definition of the fundamental tick (the RS time quantum τ0 = 1).
proof idea
The proof is a direct inequality argument. It unfolds the definition of the predicted phase and of φ, then obtains 0 < φ − 1 < 1 from one_lt_phi and phi_lt_two via linarith. Positivity of π yields that the correction term (φ − 1)π/10 is positive, so the sum exceeds π. The same bound φ − 1 < 1 together with division by 10 shows the correction is less than π/10; adding this to π produces a quantity strictly less than 11π/10, which is less than 2π.
why it matters
The result supplies a consistency check inside the φ-quantized PMNS construction (SM-014). It confirms that the golden-ratio prediction for the CP phase lies inside the physically allowed interval (π, 2π) that contains the measured value near 197°. The declaration therefore supports the broader claim that neutrino mixing angles arise from the same self-similar geometry that fixes the eight-tick octave and the spatial dimension D = 3 elsewhere in the framework. No downstream theorems are recorded, so the lemma functions as a standalone numerical sanity test for the PRD-proposed paper on golden-ratio neutrino geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.