row_pmns_theta23
plain-language theorem explainer
The RS mixing derivation predicts sin²θ₂₃ at 0.546 within 0.01 absolute error of the PDG center. Neutrino physicists would cite this row when comparing RS PMNS parameters to oscillation data. The proof is a direct one-line wrapper applying the upstream match theorem from MixingDerivation.
Claim. $|sin^2 θ_{23}^{pred} - 0.546| < 0.01$, where $sin^2 θ_{23}^{pred}$ denotes the RS atmospheric mixing prediction obtained as atmospheric weight plus radiative correction.
background
The PMNSScoreCard module tabulates RS predictions for the full PMNS mixing matrix against PDG/NuFIT centers, including sin²θ₁₂ ≈ 0.307, sin²θ₁₃ ≈ 0.0220, sin²θ₂₃ ≈ 0.546, and the δ_CP quadrant. The quantity sin²θ₂₃^pred is defined in MixingDerivation as the sum of atmospheric_weight and atmospheric_radiative_correction. The upstream theorem pmns_theta23_match states: 'The atmospheric angle sin²θ₂₃ matches observation (0.546) within 1%.' It evaluates the expression using alpha bounds from CKMGeometry, yielding approximately 0.5438.
proof idea
This declaration is a one-line wrapper that applies the theorem pmns_theta23_match from the MixingDerivation module.
why it matters
This row is assembled into the PMNSScoreCardCert constructed by pmnsScoreCardCert_holds, which certifies the complete set of PMNS predictions (θ12, θ13, θ23, Jarlskog, and δ_CP band). It supplies the atmospheric angle entry in the Phase 2 particle spectrum scorecard, using RS-native alpha bounds to close the match. The framework derives these angles from the phi-ladder and the alpha interval (137.030, 137.039). Scheme dependence of sin²θ_W remains a named residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.