IndisputableMonolith.Physics.PMNSScoreCard

   1import Mathlib
   2import IndisputableMonolith.Physics.MixingDerivation
   3import IndisputableMonolith.StandardModel.PMNSMatrix
   4
   5/-!
   6# Phase 2 (Particle Spectrum) — P2-PMNS: PMNS mixing scorecard
   7
   8**Row:** full PMNS mixing (sin²θ₁₂, sin²θ₁₃, sin²θ₂₃), PMNS `δ_CP` quadrant band,
   9re-use **CKM-geometry** Jarlskog construction packaged with PDG-like targets.
  10
  11**Predicted (RS):** `sin2_theta*_pred` and `PMNSMatrix.deltaCP_pmns_torsion_correction`
  12from `MixingDerivation` / `PMNSMatrix`.
  13
  14**Observed (PDG / typical NuFIT center values):** sin²θ₁₂ ≈ 0.307, sin²θ₁₃ ≈ 0.0220,
  15sin²θ₂₃ ≈ 0.545–0.546, δ_CP ≈ 197° (quadrant check via radians in `(π,2π)`).
  16
  17**Falsifier (one sentence):** A NuFIT/PDG update that moves any sin²θ center outside
  18the stated RS absolute-error certificates with no compensating change in the RS inputs
  19(α, φ-bounds) falsifies the packaged matches.
  20
  21**Status:** The angle matches and δ_CP band are `PARTIAL_THEOREM` (proved intervals vs
  22centers); scheme dependence of sin²θ_W and PMNS parameters is a named display residual.
  23
  24**Lean: 0 sorry, 0 new axiom**
  25-/
  26
  27namespace IndisputableMonolith.Physics.PMNSScoreCard
  28
  29open IndisputableMonolith
  30open IndisputableMonolith.Physics.MixingDerivation
  31open IndisputableMonolith.StandardModel.PMNSMatrix
  32
  33noncomputable section
  34
  35/-! ## Row aliases re-exporting proved facts -/
  36
  37theorem row_pmns_theta12 :
  38    |sin2_theta12_pred - 0.307| < 0.01 := pmns_theta12_match
  39
  40theorem row_pmns_theta13 :
  41    |sin2_theta13_pred - 0.022| < 0.002 := pmns_theta13_match
  42
  43theorem row_pmns_theta23 :
  44    |sin2_theta23_pred - 0.546| < 0.01 := pmns_theta23_match
  45
  46theorem row_jarlskog :
  47    |jarlskog_pred - 3.08e-5| < 0.6e-5 := jarlskog_match
  48
  49theorem row_jarlskog_pos : 0 < jarlskog_pred := jarlskog_pos
  50
  51theorem row_deltaCP_pmns_in_open_band :
  52    Real.pi < deltaCP_pmns_torsion_correction ∧
  53      deltaCP_pmns_torsion_correction < 2 * Real.pi := deltaCP_pmns_range
  54
  55structure PMNSScoreCardCert where
  56  theta12 : |sin2_theta12_pred - 0.307| < 0.01
  57  theta13 : |sin2_theta13_pred - 0.022| < 0.002
  58  theta23 : |sin2_theta23_pred - 0.546| < 0.01
  59  jarlskog : |jarlskog_pred - 3.08e-5| < 0.6e-5
  60  j_pos : 0 < jarlskog_pred
  61  deltaCP_band :
  62    Real.pi < deltaCP_pmns_torsion_correction ∧
  63      deltaCP_pmns_torsion_correction < 2 * Real.pi
  64
  65theorem pmnsScoreCardCert_holds : Nonempty PMNSScoreCardCert :=
  66  ⟨{ theta12 := row_pmns_theta12
  67     theta13 := row_pmns_theta13
  68     theta23 := row_pmns_theta23
  69     jarlskog := row_jarlskog
  70     j_pos := row_jarlskog_pos
  71     deltaCP_band := row_deltaCP_pmns_in_open_band }⟩
  72
  73end
  74
  75end IndisputableMonolith.Physics.PMNSScoreCard
  76