IndisputableMonolith.Physics.WZBosonRatioScoreCard

   1import Mathlib
   2import IndisputableMonolith.StandardModel.WZMassRatio
   3
   4/-!
   5# Phase 2 — P2-WZ: `m_W / m_Z` and `sin²θ_W` from the PDG mass pair
   6
   7**Inputs:** `WZMassRatio` uses `m_W = 80.377` GeV and `m_Z = 91.1876` GeV (PDG display).
   8
   9**Proved (numeric):** `m_W/m_Z ∈ (0.87,0.89)` and `sin²θ_W = 1 - (m_W/m_Z)² ∈ (0.22,0.23)` as
  10algebraic bounds from those definitions.
  11
  12**Falsifier (one sentence):** A PDG `m_W` or `m_Z` mass shift that drives `m_W/m_Z` out of
  13`(0.87,0.89)` refutes the stated interval certificate (trivially: update the input defs).
  14
  15**Status:** `PARTIAL_THEOREM` as a data-interface certificate; the RS-specific formula
  16`sin²θ_W = (3-φ)/6` is proved elsewhere (`Q3Representations` / `WeinbergAngleScoreCard`),
  17not in this file.
  18
  19**Lean: 0 sorry, 0 new axiom**
  20-/
  21
  22namespace IndisputableMonolith.Physics.WZBosonRatioScoreCard
  23
  24open IndisputableMonolith
  25open IndisputableMonolith.StandardModel.WZMassRatio
  26
  27noncomputable section
  28
  29theorem row_WZ_ratio_bracket : massRatio > 0.87 ∧ massRatio < 0.89 := mass_ratio_value
  30
  31theorem row_sin2_from_WZ_masses : sin2ThetaW > 0.22 ∧ sin2ThetaW < 0.23 := sin2_theta_w_value
  32
  33structure WZBosonRatioScoreCardCert where
  34  mass_ratio : massRatio > 0.87 ∧ massRatio < 0.89
  35  sin2 : sin2ThetaW > 0.22 ∧ sin2ThetaW < 0.23
  36
  37theorem wzBosonRatioScoreCardCert_holds : Nonempty WZBosonRatioScoreCardCert :=
  38  ⟨{ mass_ratio := row_WZ_ratio_bracket
  39     sin2 := row_sin2_from_WZ_masses }⟩
  40
  41end
  42
  43end IndisputableMonolith.Physics.WZBosonRatioScoreCard
  44