predicted_deltaCP
plain-language theorem explainer
The definition supplies the RS-predicted value for the CP-violating phase δ_CP in the neutrino mixing matrix as π plus a φ-dependent correction term. Neutrino phenomenologists and RS model builders would cite this when comparing the golden-ratio-derived angle to experimental bounds on δ_CP. The expression is introduced directly as a noncomputable real constant without further reduction.
Claim. $δ_{CP} = π + (φ - 1) π / 10$, where φ is the golden ratio.
background
Recognition Science derives neutrino mixing angles from the golden ratio φ that emerges as the self-similar fixed point in the J-uniqueness theorem. The PMNS matrix relates neutrino flavor eigenstates to mass eigenstates through three large mixing angles and one CP-violating phase δ_CP. In this module the angles are φ-quantized, with the phase receiving the explicit correction (φ - 1)π/10 on top of the base value π.
proof idea
This declaration is a direct definition that states the predicted phase explicitly in terms of the imported constant phi and the mathematical constant π. No lemmas or tactics are applied; the body is the closed-form expression Real.pi + (phi - 1) * Real.pi / 10.
why it matters
The definition provides the concrete target checked by the downstream theorem deltaCP_prediction_matches, which confirms the value lies in (π, 2π). It completes the CP-phase component of the PMNS-from-φ-Angles program in SM-014, connecting the Recognition Science forcing chain (T5 J-uniqueness, T6 φ fixed point) to observable neutrino CP violation near 191°. The construction leaves open whether the small correction term arises from a deeper symmetry in the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.