IndisputableMonolith.Verification.QuarkForwardPipeline

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.Anchor
   4import IndisputableMonolith.Masses.MassLaw
   5import IndisputableMonolith.Masses.ZMapForcing
   6import IndisputableMonolith.Verification.QuarkCoordinateUnification
   7
   8/-!
   9# Unified Quark Forward Pipeline (No PDG-Targeting)
  10
  11This module implements a SINGLE forward-prediction pipeline for all six quark
  12masses using Convention A exclusively: sector yardsticks from cube geometry,
  13integer rungs from generation torsion, and gap(Z) from the charge-band map.
  14
  15## Key Property: NO PDG INPUT
  16
  17Every quark mass prediction is computed from:
  18- Counting-layer integers (V=8, E=12, F=6, E_p=11, W=17, A=1)
  19- The golden ratio φ (from T5/T6)
  20- The fine-structure constant α (from the same counting layer)
  21- Nothing else.
  22
  23No measured quark mass enters any formula. The predictions are genuine
  24forward predictions, not fits.
  25
  26## Output: Dimensionless Mass Ratios
  27
  28Rather than computing absolute masses (which require a calibration seam),
  29we compute dimensionless ratios m_quark / m_electron at the anchor μ*.
  30These ratios are seam-free and directly testable.
  31
  32## The Forward Pipeline
  33
  341. Sector yardstick: A_s = 2^{B_pow(s)} × E_coh × φ^{r₀(s)}
  352. Integer rung: r_i = baseline + τ_gen (generation torsion)
  363. Band correction: gap(Z_i) = log_φ(1 + Z_i/φ)
  374. Predicted mass: m_i(μ*) = A_s × φ^{r_i - 8 + gap(Z_i)}
  385. Dimensionless ratio: m_i / m_e = [A_s × φ^{r_i - 8 + gap(Z_i)}] /
  39                                     [A_lepton × φ^{r_e - 8 + gap(Z_e)}]
  40-/
  41
  42namespace IndisputableMonolith
  43namespace Verification
  44namespace QuarkForwardPipeline
  45
  46open Constants
  47open Masses.Anchor
  48open Masses.Integers
  49open Masses.ChargeIndex
  50open Masses.MassLaw
  51open Masses.ZMapForcing
  52open Verification.QuarkCoordinateUnification
  53
  54noncomputable section
  55
  56/-! ## Forward Predictions: All Six Quarks -/
  57
  58/-- Up quark mass at anchor μ*. -/
  59def m_up : ℝ := predict_mass .UpQuark (r_up "u") (Z .UpQuark (2/3))
  60/-- Charm quark mass at anchor μ*. -/
  61def m_charm : ℝ := predict_mass .UpQuark (r_up "c") (Z .UpQuark (2/3))
  62/-- Top quark mass at anchor μ*. -/
  63def m_top : ℝ := predict_mass .UpQuark (r_up "t") (Z .UpQuark (2/3))
  64/-- Down quark mass at anchor μ*. -/
  65def m_down : ℝ := predict_mass .DownQuark (r_down "d") (Z .DownQuark (-1/3))
  66/-- Strange quark mass at anchor μ*. -/
  67def m_strange : ℝ := predict_mass .DownQuark (r_down "s") (Z .DownQuark (-1/3))
  68/-- Bottom quark mass at anchor μ*. -/
  69def m_bottom : ℝ := predict_mass .DownQuark (r_down "b") (Z .DownQuark (-1/3))
  70
  71/-- Electron mass at anchor μ* (for ratios). -/
  72def m_electron : ℝ := predict_mass .Lepton (r_lepton "e") (Z .Lepton (-1))
  73
  74/-- Sector yardsticks are strictly positive. -/
  75theorem yardstick_pos (s : Sector) : 0 < yardstick s := by
  76  unfold yardstick Masses.Anchor.E_coh
  77  apply mul_pos
  78  · apply mul_pos
  79    · exact zpow_pos (by norm_num) (B_pow s)
  80    · exact zpow_pos phi_pos (-5 : ℤ)
  81  · exact zpow_pos phi_pos (r0 s)
  82
  83/-! ## All masses are positive (trivial from predict_mass_pos). -/
  84
  85theorem m_up_pos : 0 < m_up := predict_mass_pos _ _ _
  86theorem m_charm_pos : 0 < m_charm := predict_mass_pos _ _ _
  87theorem m_top_pos : 0 < m_top := predict_mass_pos _ _ _
  88theorem m_down_pos : 0 < m_down := predict_mass_pos _ _ _
  89theorem m_strange_pos : 0 < m_strange := predict_mass_pos _ _ _
  90theorem m_bottom_pos : 0 < m_bottom := predict_mass_pos _ _ _
  91theorem m_electron_pos : 0 < m_electron := predict_mass_pos _ _ _
  92
  93/-! ## Seam-Free Mass Ratios: Equal-Z Families -/
  94
  95/-- Within equal-Z families, the mass ratio equals φ^{Δr} where Δr is the
  96    rung difference. This is an algebraic consequence of the mass law:
  97    when sector and Z are equal, yardstick and gap cancel in the ratio.
  98    Lean proof: the general theorem mass_rung_scaling in MassLaw.lean
  99    establishes m(r+1)/m(r) = φ. Applied 11 times gives m(15)/m(4) = φ^11. -/
 100theorem charm_to_up_ratio_structural :
 101    ∀ (s : Sector) (r₁ r₂ : ℤ) (Z_val : ℤ),
 102    predict_mass s r₂ Z_val / predict_mass s r₁ Z_val =
 103    phi ^ ((r₂ : ℝ) - (r₁ : ℝ)) := by
 104  intro s r₁ r₂ Z_val
 105  unfold predict_mass
 106  set gap := gap_correction Z_val
 107  set Y := yardstick s
 108  have hY : 0 < Y := by
 109    simp only [Y, yardstick, Masses.Anchor.E_coh]
 110    apply mul_pos; apply mul_pos
 111    · exact zpow_pos (by norm_num) (B_pow s)
 112    · exact zpow_pos phi_pos (-5 : ℤ)
 113    · exact zpow_pos phi_pos (r0 s)
 114  have hYne : Y ≠ 0 := ne_of_gt hY
 115  -- Step 1: cancel Y from numerator and denominator
 116  have hp₁ : 0 < phi ^ ((r₁ : ℝ) - 8 + gap) := Real.rpow_pos_of_pos phi_pos _
 117  rw [show Y * phi ^ ((r₂ : ℝ) - 8 + gap) = Y * phi ^ ((r₂ : ℝ) - 8 + gap) from rfl]
 118  rw [show Y * phi ^ ((r₁ : ℝ) - 8 + gap) = Y * phi ^ ((r₁ : ℝ) - 8 + gap) from rfl]
 119  rw [mul_div_mul_left _ _ hYne]
 120  -- Step 2: φ^a / φ^b = φ^(a-b)
 121  rw [div_eq_iff (ne_of_gt hp₁)]
 122  rw [← Real.rpow_add phi_pos]
 123  congr 1
 124  ring
 125
 126/-- Corollary: charm/up = φ^11 (rung difference 15 − 4 = 11). -/
 127theorem charm_to_up_eq_phi11 :
 128    m_charm / m_up = phi ^ (11 : ℝ) := by
 129  have := charm_to_up_ratio_structural .UpQuark (r_up "u") (r_up "c") (Z .UpQuark (2/3))
 130  simp only [m_charm, m_up] at this ⊢
 131  rw [this]
 132  congr 1
 133  simp only [r_up, tau, Masses.Anchor.E_passive,
 134    Constants.AlphaDerivation.passive_field_edges,
 135    Constants.AlphaDerivation.cube_edges,
 136    Constants.AlphaDerivation.active_edges_per_tick,
 137    Constants.AlphaDerivation.D]
 138  push_cast; norm_num
 139
 140/-- Corollary: bottom/strange = φ^6 (rung difference 21 − 15 = 6). -/
 141theorem bottom_to_strange_eq_phi6 :
 142    m_bottom / m_strange = phi ^ (6 : ℝ) := by
 143  have := charm_to_up_ratio_structural .DownQuark (r_down "s") (r_down "b") (Z .DownQuark (-1/3))
 144  simp only [m_bottom, m_strange] at this ⊢
 145  rw [this]
 146  congr 1
 147  simp only [r_down, tau, Masses.Anchor.W,
 148    Constants.AlphaDerivation.wallpaper_groups,
 149    Masses.Anchor.E_passive,
 150    Constants.AlphaDerivation.passive_field_edges,
 151    Constants.AlphaDerivation.cube_edges,
 152    Constants.AlphaDerivation.active_edges_per_tick,
 153    Constants.AlphaDerivation.D]
 154  push_cast; norm_num
 155
 156/-! ## The Integer Rungs (No PDG Input) -/
 157
 158/-- Verify: all rung values are derived from baselines + torsion, nothing else. -/
 159theorem quark_rungs_from_torsion :
 160    r_up "u" = 4 ∧ r_up "c" = 15 ∧ r_up "t" = 21 ∧
 161    r_down "d" = 4 ∧ r_down "s" = 15 ∧ r_down "b" = 21 := by
 162  simp only [r_up, r_down, tau, Masses.Anchor.E_passive, Masses.Anchor.W,
 163    Constants.AlphaDerivation.passive_field_edges,
 164    Constants.AlphaDerivation.cube_edges,
 165    Constants.AlphaDerivation.active_edges_per_tick,
 166    Constants.AlphaDerivation.D,
 167    Constants.AlphaDerivation.wallpaper_groups]
 168  norm_num
 169
 170/-- Verify: all Z-values are derived from the charge-band map, nothing else. -/
 171theorem quark_Z_from_charges :
 172    Z .UpQuark (2/3) = 276 ∧ Z .DownQuark (-1/3) = 24 := by
 173  simp only [Z]
 174  norm_num
 175
 176/-- Verify: the lepton Z-value for comparison. -/
 177theorem lepton_Z_from_charge :
 178    Z .Lepton (-1) = 1332 := by
 179  simp only [Z]
 180  norm_num
 181
 182/-! ## Convention-B Coordinates Are Derived from Convention-A Pipeline -/
 183
 184/-- Residue coordinate of any species relative to the electron anchor mass. -/
 185def residue_from_pipeline (s : Sector) (r : ℤ) (Z_val : ℤ) : ℝ :=
 186  residueFromCore (yardstick s) m_electron r (gap_correction Z_val)
 187
 188/-- Core (Convention A) prediction equals residue form (Convention B coordinates)
 189    with electron reference mass. -/
 190theorem pipeline_equals_residue_form (s : Sector) (r : ℤ) (Z_val : ℤ) :
 191    predict_mass s r Z_val = residueMass m_electron (residue_from_pipeline s r Z_val) := by
 192  unfold predict_mass residue_from_pipeline
 193  exact core_eq_residue_of_positive (yardstick_pos s) m_electron_pos
 194
 195/-- A single canonical forward pipeline generates all six quarks; the quarter/residue
 196    convention is derived as a coordinate representation from that same pipeline. -/
 197theorem all_quark_predictions_have_derived_residue_coordinates :
 198    ∃ R_u R_c R_t R_d R_s R_b : ℝ,
 199      m_up = residueMass m_electron R_u ∧
 200      m_charm = residueMass m_electron R_c ∧
 201      m_top = residueMass m_electron R_t ∧
 202      m_down = residueMass m_electron R_d ∧
 203      m_strange = residueMass m_electron R_s ∧
 204      m_bottom = residueMass m_electron R_b := by
 205  refine ⟨residue_from_pipeline .UpQuark (r_up "u") (Z .UpQuark (2/3)),
 206    residue_from_pipeline .UpQuark (r_up "c") (Z .UpQuark (2/3)),
 207    residue_from_pipeline .UpQuark (r_up "t") (Z .UpQuark (2/3)),
 208    residue_from_pipeline .DownQuark (r_down "d") (Z .DownQuark (-1/3)),
 209    residue_from_pipeline .DownQuark (r_down "s") (Z .DownQuark (-1/3)),
 210    residue_from_pipeline .DownQuark (r_down "b") (Z .DownQuark (-1/3)), ?_⟩
 211  repeat' constructor
 212  · simpa [m_up] using pipeline_equals_residue_form .UpQuark (r_up "u") (Z .UpQuark (2/3))
 213  · simpa [m_charm] using pipeline_equals_residue_form .UpQuark (r_up "c") (Z .UpQuark (2/3))
 214  · simpa [m_top] using pipeline_equals_residue_form .UpQuark (r_up "t") (Z .UpQuark (2/3))
 215  · simpa [m_down] using pipeline_equals_residue_form .DownQuark (r_down "d") (Z .DownQuark (-1/3))
 216  · simpa [m_strange] using pipeline_equals_residue_form .DownQuark (r_down "s") (Z .DownQuark (-1/3))
 217  · simpa [m_bottom] using pipeline_equals_residue_form .DownQuark (r_down "b") (Z .DownQuark (-1/3)
 218    )
 219
 220/-! ## The Yardstick Inputs (No PDG Input) -/
 221
 222/-- Up-quark yardstick components. -/
 223theorem up_yardstick_components :
 224    B_pow .UpQuark = -1 ∧ r0 .UpQuark = 35 := by
 225  exact ⟨B_pow_UpQuark_eq, r0_UpQuark_eq⟩
 226
 227/-- Down-quark yardstick components. -/
 228theorem down_yardstick_components :
 229    B_pow .DownQuark = 23 ∧ r0 .DownQuark = -5 := by
 230  exact ⟨B_pow_DownQuark_eq, r0_DownQuark_eq⟩
 231
 232/-! ## Non-Circularity Certificate -/
 233
 234/-- The forward pipeline is non-circular: no PDG quark mass enters any formula.
 235    This is a DESIGN ASSERTION verified by inspection of the definition chain:
 236    predict_mass → yardstick → B_pow/r0 → counting-layer integers
 237    predict_mass → gap_correction → Z → charge-band map
 238    predict_mass → rung → baseline + torsion → counting-layer integers -/
 239structure QuarkNonCircularity where
 240  /-- Yardsticks come from cube geometry (no mass input) -/
 241  yardsticks_geometric : B_pow .UpQuark = -1 ∧ r0 .UpQuark = 35 ∧
 242                         B_pow .DownQuark = 23 ∧ r0 .DownQuark = -5
 243  /-- Rungs come from generation torsion (no mass input) -/
 244  rungs_from_torsion : r_up "u" = 4 ∧ r_up "c" = 15 ∧ r_up "t" = 21 ∧
 245                       r_down "d" = 4 ∧ r_down "s" = 15 ∧ r_down "b" = 21
 246  /-- Z-values come from charges (no mass input) -/
 247  Z_from_charges : Z .UpQuark (2/3) = 276 ∧ Z .DownQuark (-1/3) = 24
 248
 249/-- The non-circularity certificate is satisfied. -/
 250def non_circular : QuarkNonCircularity where
 251  yardsticks_geometric := ⟨B_pow_UpQuark_eq, r0_UpQuark_eq,
 252                            B_pow_DownQuark_eq, r0_DownQuark_eq⟩
 253  rungs_from_torsion := quark_rungs_from_torsion
 254  Z_from_charges := quark_Z_from_charges
 255
 256/-! ## Summary: What This Module Proves
 257
 2581. ALL SIX quark masses are computed by a SINGLE forward formula:
 259   m_i(μ*) = yardstick(sector) × φ^{r_i − 8 + gap(Z_i)}
 260
 2612. Every input is derived from counting-layer integers:
 262   - B_pow, r0: cube geometry (proved in Anchor.lean)
 263   - r_i: baseline + torsion (proved above)
 264   - Z_i: charge-band map (proved above)
 265
 2663. NO PDG quark mass appears anywhere in the forward direction.
 267
 2684. Equal-Z mass ratios are pure φ-powers (generation torsion only).
 269
 270## What This Module Does NOT Prove
 271
 272- That the predicted masses MATCH PDG values.
 273  (That requires SM RG transport from μ* to PDG conventions,
 274   which is bookkeeping in Paper IV, not part of the forward pipeline.)
 275
 276- That Convention B (quarter-ladder) is equivalent.
 277  (That is proved in QuarkCoordinateUnification.lean at the formula level.)
 278
 279## Status
 280
 281This module resolves the "quark dual-coordinate" problem by demonstrating
 282that Convention A provides a complete, non-circular forward pipeline for
 283all six quarks. Convention B is a derived consequence (via the coordinate
 284transform in QuarkCoordinateUnification.lean), not a separate theory.
 285-/
 286
 287end
 288
 289end QuarkForwardPipeline
 290end Verification
 291end IndisputableMonolith
 292