IndisputableMonolith.Masses.QuarkScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.Anchor
   4import IndisputableMonolith.Masses.Verification
   5import IndisputableMonolith.Masses.RSBridge.Anchor
   6
   7/-!
   8# Quark Score Card
   9
  10Phase 0 row P0-Q01..P0-Q06 of `planning/PHYSICAL_DERIVATION_PLAN.md`.
  11
  12This module is the canonical scorecard that records, in one place,
  13which quark-sector facts are theorem-grade and which remain open. It
  14does **not** introduce new physics. It only consolidates existing
  15proofs and tags the residuals honestly.
  16
  17## Status as of 2026-04-26
  18
  19- **THEOREM**: charm/up = `φ^11`, top/charm = `φ^6`, all quark mass
  20  predictions positive, top quark prediction in multi-GeV range.
  21- **THEOREM**: equal-Z fermions have anchor mass ratio that is a pure
  22  φ-power of the rung difference (`anchor_ratio` in `RSBridge`).
  23- **THEOREM**: u/c/t share `ZOf = 276`; d/s/b share `ZOf = 24`;
  24  e/μ/τ share `ZOf = 1332`.
  25- **OPEN**: absolute u/d/s/c/b/t mass match within PDG bands. The
  26  `rs_mass_MeV` formula in `Masses.Verification` does not include the
  27  `gap (ZOf f)` correction from `RSBridge.Anchor.massAtAnchor`. The
  28  bridge equivalence theorem is the missing piece.
  29
  30## Lean status: 0 sorry, 0 axiom
  31-/
  32
  33namespace IndisputableMonolith.Masses.QuarkScoreCard
  34
  35open Anchor RSBridge
  36
  37noncomputable section
  38
  39/-! ## Z-charge values per fermion
  40
  41Derived from `tildeQ` and the sector formula in `RSBridge.Anchor`.
  42For up-type quarks `q̃ = +4`, so `ZOf = 4 + 16 + 256 = 276`.
  43For down-type quarks `q̃ = -2`, so `ZOf = 4 + 4 + 16 = 24`.
  44For charged leptons `q̃ = -6`, so `ZOf = 36 + 1296 = 1332`.
  45-/
  46
  47theorem ZOf_up_quarks : ZOf .u = 276 ∧ ZOf .c = 276 ∧ ZOf .t = 276 := by
  48  refine ⟨?_, ?_, ?_⟩ <;> · decide
  49
  50theorem ZOf_down_quarks : ZOf .d = 24 ∧ ZOf .s = 24 ∧ ZOf .b = 24 := by
  51  refine ⟨?_, ?_, ?_⟩ <;> · decide
  52
  53theorem ZOf_charged_leptons : ZOf .e = 1332 ∧ ZOf .mu = 1332 ∧ ZOf .tau = 1332 := by
  54  refine ⟨?_, ?_, ?_⟩ <;> · decide
  55
  56/-! ## Equal-Z within a sector implies pure φ-power ratios -/
  57
  58theorem charm_up_equal_Z : ZOf .u = ZOf .c := by
  59  obtain ⟨hu, hc, _⟩ := ZOf_up_quarks
  60  rw [hu, hc]
  61
  62theorem top_up_equal_Z : ZOf .u = ZOf .t := by
  63  obtain ⟨hu, _, ht⟩ := ZOf_up_quarks
  64  rw [hu, ht]
  65
  66theorem strange_down_equal_Z : ZOf .d = ZOf .s := by
  67  obtain ⟨hd, hs, _⟩ := ZOf_down_quarks
  68  rw [hd, hs]
  69
  70theorem bottom_down_equal_Z : ZOf .d = ZOf .b := by
  71  obtain ⟨hd, _, hb⟩ := ZOf_down_quarks
  72  rw [hd, hb]
  73
  74/-! ## Generation rung spacing (proved directly from Integers definitions) -/
  75
  76open Integers in
  77theorem up_generation_spacing :
  78    r_up "c" - r_up "u" = 11 ∧ r_up "t" - r_up "u" = 17 := by
  79  decide
  80
  81open Integers in
  82theorem down_generation_spacing :
  83    r_down "s" - r_down "d" = 11 ∧ r_down "b" - r_down "d" = 17 := by
  84  decide
  85
  86/-! ## Structural ratios that already match PDG order of magnitude
  87
  88These are theorems in `Masses.Verification`. We re-export them under
  89explicit row IDs so the scorecard can be read at a glance.
  90-/
  91
  92/-- P0-Q structural row: m_c / m_u = φ^11 (proved). -/
  93theorem row_charm_up_ratio :
  94    Verification.charm_quark_pred / Verification.up_quark_pred =
  95      Constants.phi ^ (11 : ℕ) :=
  96  Verification.charm_up_ratio
  97
  98/-- P0-Q structural row: m_t / m_c = φ^6 (proved). -/
  99theorem row_top_charm_ratio :
 100    Verification.top_quark_pred / Verification.charm_quark_pred =
 101      Constants.phi ^ (6 : ℕ) :=
 102  Verification.top_charm_ratio
 103
 104/-- P0-Q06 structural row: top mass prediction lies in (10 GeV, 1 TeV). -/
 105theorem row_top_quark_in_band :
 106    (10000 : ℝ) < Verification.top_quark_pred ∧
 107      Verification.top_quark_pred < 1000000 :=
 108  Verification.top_quark_pred_order
 109
 110/-- All quark structural predictions are positive (proved). -/
 111theorem row_quark_preds_pos :
 112    0 < Verification.up_quark_pred ∧
 113      0 < Verification.charm_quark_pred ∧
 114        0 < Verification.top_quark_pred :=
 115  Verification.quark_preds_pos
 116
 117/-! ## Lepton mass match (already theorem-grade, re-exported for the audit)
 118
 119The lepton sector match is the strongest piece of the absolute-mass
 120scorecard, with bounds proved by interval arithmetic in
 121`Masses.Verification`.
 122-/
 123
 124/-- Electron mass within 0.3 percent of PDG. -/
 125theorem row_electron_pct :
 126    |Verification.rs_mass_MeV .Lepton 2 - Verification.m_e_exp| /
 127        Verification.m_e_exp < 0.003 :=
 128  Verification.electron_relative_error
 129
 130/-- Muon mass within 4 percent of PDG. -/
 131theorem row_muon_pct :
 132    |Verification.rs_mass_MeV .Lepton 13 - Verification.m_mu_exp| /
 133        Verification.m_mu_exp < 0.04 :=
 134  Verification.muon_relative_error
 135
 136/-- Tau mass within 3 percent of PDG. -/
 137theorem row_tau_pct :
 138    |Verification.rs_mass_MeV .Lepton 19 - Verification.m_tau_exp| /
 139        Verification.m_tau_exp < 0.03 :=
 140  Verification.tau_relative_error
 141
 142/-- Muon-electron PDG mass ratio matches `phi^11` within 4 percent. -/
 143theorem row_muon_electron_ratio_pct :
 144    |Constants.phi ^ (11 : ℕ) - Verification.ratio_mu_e_exp| /
 145        Verification.ratio_mu_e_exp < 0.04 :=
 146  Verification.muon_electron_ratio_error
 147
 148/-- Tau-electron PDG mass ratio matches `phi^17` within 3 percent. -/
 149theorem row_tau_electron_ratio_pct :
 150    |Constants.phi ^ (17 : ℕ) - Verification.ratio_tau_e_exp| /
 151        Verification.ratio_tau_e_exp < 0.03 :=
 152  Verification.tau_electron_ratio_error
 153
 154/-! ## The named open residual
 155
 156The `rs_mass_MeV` formula does not currently apply the gap correction
 157`gap (ZOf f)`. The closure target is the bridge equivalence connecting
 158the structural sector formula to the gap-corrected anchor formula.
 159
 160Once the bridge is proved, the absolute u/d/s/c/b/t mass intervals
 161become a numerical computation on the gap values:
 162
 163- `gap(276) ≈ 10.69` for up-type quarks,
 164- `gap(24)  ≈ 5.74`  for down-type quarks,
 165- `gap(1332) ≈ 13.95` for charged leptons.
 166-/
 167
 168/-- Named residual: the bridge between the structural `rs_mass_MeV`
 169    formula and the gap-corrected `massAtAnchor` formula on a chosen
 170    quark sector. A proof of this proposition would close the absolute
 171    quark-mass row of the scorecard. -/
 172def QuarkAbsoluteMassResidual : Prop :=
 173  ∀ (f : Fermion),
 174    sectorOf f = Sector.up →
 175    Verification.rs_mass_MeV Anchor.Sector.UpQuark (RSBridge.rung f)
 176      = M0 * Real.exp (((RSBridge.rung f : ℝ) - 8 + gap (ZOf f)) *
 177            Real.log Constants.phi)
 178
 179/-! ## ScoreCard certificate
 180
 181A single record bundling every theorem-grade row of this Phase 0
 182deliverable. -/
 183
 184structure QuarkScoreCardCert where
 185  ZOf_up : ZOf .u = 276 ∧ ZOf .c = 276 ∧ ZOf .t = 276
 186  ZOf_down : ZOf .d = 24 ∧ ZOf .s = 24 ∧ ZOf .b = 24
 187  ZOf_lep : ZOf .e = 1332 ∧ ZOf .mu = 1332 ∧ ZOf .tau = 1332
 188  charm_up_ratio_eq :
 189    Verification.charm_quark_pred / Verification.up_quark_pred =
 190      Constants.phi ^ (11 : ℕ)
 191  top_charm_ratio_eq :
 192    Verification.top_quark_pred / Verification.charm_quark_pred =
 193      Constants.phi ^ (6 : ℕ)
 194  top_in_band : (10000 : ℝ) < Verification.top_quark_pred ∧
 195      Verification.top_quark_pred < 1000000
 196  quark_preds_pos : 0 < Verification.up_quark_pred ∧
 197      0 < Verification.charm_quark_pred ∧ 0 < Verification.top_quark_pred
 198  electron_pct :
 199    |Verification.rs_mass_MeV .Lepton 2 - Verification.m_e_exp| /
 200        Verification.m_e_exp < 0.003
 201  muon_pct :
 202    |Verification.rs_mass_MeV .Lepton 13 - Verification.m_mu_exp| /
 203        Verification.m_mu_exp < 0.04
 204  tau_pct :
 205    |Verification.rs_mass_MeV .Lepton 19 - Verification.m_tau_exp| /
 206        Verification.m_tau_exp < 0.03
 207
 208theorem quarkScoreCardCert_holds : Nonempty QuarkScoreCardCert :=
 209  ⟨{ ZOf_up := ZOf_up_quarks
 210     ZOf_down := ZOf_down_quarks
 211     ZOf_lep := ZOf_charged_leptons
 212     charm_up_ratio_eq := row_charm_up_ratio
 213     top_charm_ratio_eq := row_top_charm_ratio
 214     top_in_band := row_top_quark_in_band
 215     quark_preds_pos := row_quark_preds_pos
 216     electron_pct := row_electron_pct
 217     muon_pct := row_muon_pct
 218     tau_pct := row_tau_pct }⟩
 219
 220/-! ## Falsifier
 221
 222If, in a deepening pass, any of the following is shown to fail, the
 223scorecard breaks and the entry must be retracted:
 224
 225- `m_c / m_u = φ^11` is not within 0.5 percent of `(1.27 GeV) / (2.16 MeV)`
 226  after the gap correction is applied.
 227- `m_t / m_c = φ^6` is not within 0.5 percent of
 228  `(172.69 GeV) / (1.27 GeV)` after the gap correction is applied.
 229- The bridge equivalence between `rs_mass_MeV` and `massAtAnchor`
 230  cannot be proved.
 231-/
 232
 233end
 234
 235end IndisputableMonolith.Masses.QuarkScoreCard
 236