IndisputableMonolith.Masses.QuarkAbsoluteBridgeScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.QuarkScoreCard
   4
   5/-!
   6# Quark Absolute Bridge Score Card
   7
   8Phase 0 rows **P0-Q01..P0-Q06** in
   9`planning/PHYSICAL_DERIVATION_PLAN.md`.
  10
  11## Statement
  12
  13This module deepens the existing `QuarkScoreCard`: the equal-`Z`
  14anchor bridge and the structural `rs_mass_MeV` formula agree exactly on
  15the **within-family ratios** for `u/c/t`. This is theorem-grade.
  16
  17The absolute MeV bridge is still a **PARTIAL_THEOREM** / residual, not a
  18closed mass claim. The current definitions have two different anchors:
  19
  20* `Verification.rs_mass_MeV` is a sector yardstick in displayed MeV,
  21  including the `10^6` reporting divisor.
  22* `RSBridge.massAtAnchor` is a native anchor expression with the
  23  gap-corrected exponent `r - 8 + gap (ZOf f)` and no SI display divisor.
  24
  25## Measurement target
  26
  27PDG 2024 quark masses:
  28`m_u = 2.16 MeV`, `m_c = 1.27 GeV`, `m_t = 172.69 GeV`, with the
  29down-sector rows still awaiting the same absolute bridge.
  30
  31Falsifier: if the future SI/display bridge cannot map the native anchor
  32formula and the MeV sector formula into the same calibrated quantity, the
  33absolute quark-mass rows stay open.
  34
  35## Lean status: 0 sorry, 0 axiom
  36-/
  37
  38namespace IndisputableMonolith.Masses.QuarkAbsoluteBridgeScoreCard
  39
  40open Constants
  41open Verification
  42open QuarkScoreCard
  43open IndisputableMonolith.RSBridge
  44
  45noncomputable section
  46
  47/-! ## Re-exported row aliases -/
  48
  49/-- P0-Q bridge row: the structural charm/up ratio as a real-power φ law. -/
  50theorem row_structural_charm_up_ratio_rpow :
  51    charm_quark_pred / up_quark_pred = phi ^ (11 : ℝ) := by
  52  simpa [Real.rpow_natCast] using row_charm_up_ratio
  53
  54/-- P0-Q bridge row: the structural top/charm ratio as a real-power φ law. -/
  55theorem row_structural_top_charm_ratio_rpow :
  56    top_quark_pred / charm_quark_pred = phi ^ (6 : ℝ) := by
  57  simpa [Real.rpow_natCast] using row_top_charm_ratio
  58
  59/-! ## Anchor-side ratios -/
  60
  61theorem row_anchor_charm_up_ratio_exp :
  62    massAtAnchor .c / massAtAnchor .u =
  63      Real.exp ((11 : ℝ) * Real.log phi) := by
  64  have hZ : ZOf .c = ZOf .u := by decide
  65  have h := anchor_ratio .c .u hZ
  66  have hr : ((rung .c : ℝ) - rung .u) = (11 : ℝ) := by
  67    simp [rung]
  68    norm_num
  69  simpa [hr] using h
  70
  71theorem row_anchor_top_charm_ratio_exp :
  72    massAtAnchor .t / massAtAnchor .c =
  73      Real.exp ((6 : ℝ) * Real.log phi) := by
  74  have hZ : ZOf .t = ZOf .c := by decide
  75  have h := anchor_ratio .t .c hZ
  76  have hr : ((rung .t : ℝ) - rung .c) = (6 : ℝ) := by
  77    simp [rung]
  78    norm_num
  79  simpa [hr] using h
  80
  81theorem row_anchor_charm_up_ratio_rpow :
  82    massAtAnchor .c / massAtAnchor .u = phi ^ (11 : ℝ) := by
  83  rw [row_anchor_charm_up_ratio_exp]
  84  rw [Real.rpow_def_of_pos phi_pos]
  85  ring_nf
  86
  87theorem row_anchor_top_charm_ratio_rpow :
  88    massAtAnchor .t / massAtAnchor .c = phi ^ (6 : ℝ) := by
  89  rw [row_anchor_top_charm_ratio_exp]
  90  rw [Real.rpow_def_of_pos phi_pos]
  91  ring_nf
  92
  93theorem row_anchor_strange_down_ratio_exp :
  94    massAtAnchor .s / massAtAnchor .d =
  95      Real.exp ((11 : ℝ) * Real.log phi) := by
  96  have hZ : ZOf .s = ZOf .d := by decide
  97  have h := anchor_ratio .s .d hZ
  98  have hr : ((rung .s : ℝ) - rung .d) = (11 : ℝ) := by
  99    simp [rung]
 100    norm_num
 101  simpa [hr] using h
 102
 103theorem row_anchor_bottom_strange_ratio_exp :
 104    massAtAnchor .b / massAtAnchor .s =
 105      Real.exp ((6 : ℝ) * Real.log phi) := by
 106  have hZ : ZOf .b = ZOf .s := by decide
 107  have h := anchor_ratio .b .s hZ
 108  have hr : ((rung .b : ℝ) - rung .s) = (6 : ℝ) := by
 109    simp [rung]
 110    norm_num
 111  simpa [hr] using h
 112
 113theorem row_anchor_strange_down_ratio_rpow :
 114    massAtAnchor .s / massAtAnchor .d = phi ^ (11 : ℝ) := by
 115  rw [row_anchor_strange_down_ratio_exp]
 116  rw [Real.rpow_def_of_pos phi_pos]
 117  ring_nf
 118
 119theorem row_anchor_bottom_strange_ratio_rpow :
 120    massAtAnchor .b / massAtAnchor .s = phi ^ (6 : ℝ) := by
 121  rw [row_anchor_bottom_strange_ratio_exp]
 122  rw [Real.rpow_def_of_pos phi_pos]
 123  ring_nf
 124
 125/-! ## Structural/anchor ratio agreement -/
 126
 127theorem row_charm_up_structural_anchor_agree :
 128    charm_quark_pred / up_quark_pred =
 129      massAtAnchor .c / massAtAnchor .u := by
 130  rw [row_structural_charm_up_ratio_rpow, row_anchor_charm_up_ratio_rpow]
 131
 132theorem row_top_charm_structural_anchor_agree :
 133    top_quark_pred / charm_quark_pred =
 134      massAtAnchor .t / massAtAnchor .c := by
 135  rw [row_structural_top_charm_ratio_rpow, row_anchor_top_charm_ratio_rpow]
 136
 137/-! ## Absolute residual remains named and explicit -/
 138
 139/-- The absolute mass bridge is still the named residual from `QuarkScoreCard`. -/
 140def row_absolute_quark_bridge_residual : Prop :=
 141  QuarkAbsoluteMassResidual
 142
 143theorem row_absolute_quark_bridge_residual_is_named :
 144    row_absolute_quark_bridge_residual = QuarkAbsoluteMassResidual := rfl
 145
 146structure QuarkAbsoluteBridgeScoreCardCert where
 147  charm_up_ratio_agrees :
 148    charm_quark_pred / up_quark_pred =
 149      massAtAnchor .c / massAtAnchor .u
 150  top_charm_ratio_agrees :
 151    top_quark_pred / charm_quark_pred =
 152      massAtAnchor .t / massAtAnchor .c
 153  strange_down_anchor_ratio :
 154    massAtAnchor .s / massAtAnchor .d = phi ^ (11 : ℝ)
 155  bottom_strange_anchor_ratio :
 156    massAtAnchor .b / massAtAnchor .s = phi ^ (6 : ℝ)
 157  residual_named :
 158    row_absolute_quark_bridge_residual = QuarkAbsoluteMassResidual
 159
 160theorem quarkAbsoluteBridgeScoreCardCert_holds :
 161    Nonempty QuarkAbsoluteBridgeScoreCardCert :=
 162  ⟨{ charm_up_ratio_agrees := row_charm_up_structural_anchor_agree
 163     top_charm_ratio_agrees := row_top_charm_structural_anchor_agree
 164     strange_down_anchor_ratio := row_anchor_strange_down_ratio_rpow
 165     bottom_strange_anchor_ratio := row_anchor_bottom_strange_ratio_rpow
 166     residual_named := row_absolute_quark_bridge_residual_is_named }⟩
 167
 168end
 169
 170end IndisputableMonolith.Masses.QuarkAbsoluteBridgeScoreCard
 171