PMNSScoreCardCert
plain-language theorem explainer
The PMNSScoreCardCert structure packages the absolute-error certificates for the three PMNS mixing angles, the Jarlskog invariant, its positivity, and the CP phase band. Neutrino phenomenologists and RS model builders would cite it when comparing the geometric predictions from rung ratios and torsion corrections against NuFIT data. The definition is a direct packaging of the six inequalities into a single record type with no further computation.
Claim. Let $s_{12}$, $s_{13}$, $s_{23}$, $J$, and $d$ denote the RS predictions for the squared sines of the PMNS angles, the Jarlskog invariant, and the torsion-corrected CP phase. Then PMNSScoreCardCert asserts $|s_{12} - 0.307| < 0.01$, $|s_{13} - 0.022| < 0.002$, $|s_{23} - 0.546| < 0.01$, $|J - 3.08e-5| < 0.6e-5$, $J > 0$, and $π < d < 2π$.
background
The module sets the local theoretical setting for Phase 2 particle spectrum, specifically the PMNS mixing scorecard. It re-uses the geometric Jarlskog construction from CKM geometry and the rung-ratio predictions for the three angles. Upstream, jarlskog_pred is defined as the geometric area of the unitarity triangle forced by cube topology and fine-structure leakage, approximated as (1/24) * (α/2) * (φ^{-3}) * sin(π/2). The angle predictions come from solar_weight minus solar_radiative_correction for θ12, atmospheric_weight plus atmospheric_radiative_correction for θ23, and reactor_weight for θ13. The deltaCP_pmns_torsion_correction is given explicitly as π + (6/11)(π/4).
proof idea
The structure is defined directly by the six field inequalities; no tactics or lemmas are applied.
why it matters
It supplies the certificate shown nonempty by pmnsScoreCardCert_holds, completing the PMNS scorecard in the particle spectrum phase. The construction re-uses the Jarlskog invariant from CKM geometry and the torsion correction for the δ_CP quadrant band. It touches the open question of scheme dependence in sin²θ_W and PMNS parameters noted as a named display residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.