row_pmns_theta12
plain-language theorem explainer
The declaration certifies that the RS-predicted solar neutrino mixing angle satisfies |sin²θ₁₂^pred - 0.307| < 0.01. Neutrino model builders assembling PMNS scorecards cite this row when checking geometric predictions against oscillation data. The proof is a direct one-line wrapper invoking the upstream match theorem that bounds the difference using φ^{-2} and α.
Claim. $|sin^2 θ_{12}^{pred} - 0.307| < 0.01$, where $sin^2 θ_{12}^{pred}$ equals the solar weight minus the solar radiative correction derived from rung ratios.
background
The module assembles a Phase 2 scorecard for PMNS mixing angles, comparing RS predictions from rung differences against PDG centers (sin²θ₁₂ ≈ 0.307, sin²θ₁₃ ≈ 0.0220, sin²θ₂₃ ≈ 0.545). The definition sin2_theta12_pred is given as solar_weight - solar_radiative_correction, with the solar angle tied to rung ratios in the MixingDerivation module. Upstream, pmns_theta12_match states that the absolute difference from 0.307 stays below 0.01 once bounds on φ^{-2} and α are imposed, with the note that the proof requires those bounds.
proof idea
One-line wrapper that applies pmns_theta12_match from MixingDerivation.
why it matters
This row supplies the solar-angle entry inside PMNSScoreCardCert, which is assembled in pmnsScoreCardCert_holds to certify the full set of PMNS predictions. It completes the geometric mixing derivation step in the Phase 2 scorecard, linking rung-ratio forcing to observed neutrino angles. The framework places this inside the broader forcing chain that extracts mixing parameters from the phi-ladder without additional free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.