GRM_theta12
plain-language theorem explainer
GRM_theta12 supplies the golden-ratio-based value for sin²θ₁₂ in the PMNS neutrino mixing matrix as 1/(2 + φ). Neutrino physicists testing RS-derived mixing would cite it to compare φ-quantized predictions against data. It is a direct definition with no proof steps.
Claim. The golden ratio mixing hypothesis predicts $sin^2 θ_{12} = (2 + φ)^{-1}$ where φ denotes the golden ratio.
background
The module derives the PMNS neutrino mixing matrix from RS by positing that the three mixing angles are φ-quantized. Neutrino flavor states (ν_e, ν_μ, ν_τ) relate to mass eigenstates (ν_1, ν_2, ν_3) via the unitary PMNS matrix, with large angles unlike the small CKM angles. GRM_theta12 implements Hypothesis 5 by fixing the solar angle parameter to the reciprocal of 2 plus φ.
proof idea
This is a one-line definition that directly assigns 1 divided by 2 plus phi. No lemmas or tactics are applied.
why it matters
The definition fills Hypothesis 5 inside the module's target derivation of PMNS angles from φ-geometry, as referenced in the planned PRD paper. It sits within the broader RS program that quantizes mixing via the phi-ladder and self-similar fixed point, addressing the large PMNS angles while leaving the ~10% discrepancy with data as an open refinement question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.