IndisputableMonolith.Masses.ZMapForcing

   1import Mathlib
   2import IndisputableMonolith.Masses.Anchor
   3import IndisputableMonolith.Verification.ZMapTopologicalDerivation
   4
   5/-!
   6# Masses Z-Map Forcing Bridge
   7
   8This module upstreams the partial O2/O3 closure into the canonical mass-layer
   9namespace.
  10
  11It packages two concrete facts:
  121. Integerization scale closure (in the currently adopted parity-constrained class):
  13   `k = 6` is the smallest positive even scale that integerizes SM charges.
  142. The canonical anchor charge map evaluates to the expected family values:
  15   `Z_lepton = 1332`, `Z_up = 276`, `Z_down = 24`.
  16
  17This is not full first-principles closure yet, but it makes the current forcing
  18progress directly consumable from `Masses.*`.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Masses
  23namespace ZMapForcing
  24
  25open Anchor
  26open Verification.ZMapTopologicalDerivation
  27
  28/-- `k = 6` is the smallest positive even integerization scale for SM charges. -/
  29theorem smallest_positive_even_integerization_scale :
  30    integerizes_all 6 ∧
  31      (∀ k : ℕ, 0 < k → Even k → integerizes_all k → 6 ≤ k) :=
  32  six_smallest_positive_even_integerizer
  33
  34/-- Canonical color offset from 3-cube edge-direction count. -/
  35theorem canonical_color_offset : edge_direction_count = 4 :=
  36  edge_direction_eq_four
  37
  38/-- Canonical mass-layer charge map values for the three charged families. -/
  39theorem anchor_charge_map_values :
  40    ChargeIndex.Z Sector.Lepton (-1) = 1332 ∧
  41    ChargeIndex.Z Sector.UpQuark (2 / 3) = 276 ∧
  42    ChargeIndex.Z Sector.DownQuark (-1 / 3) = 24 := by
  43  native_decide
  44
  45/-- Mass-layer bridge: if a topology-compatible family
  46    (`Z_lepton = aQ̃² + bQ̃⁴`, `Z_quark = c + aQ̃² + bQ̃⁴`) matches the canonical
  47    anchor outputs, then `(a,b,c)` are forced to `(1,1,4)`. -/
  48theorem canonical_tuple_forced_from_anchor_outputs
  49    {a b c : ℤ}
  50    (hlep : Z_lepton a b = ChargeIndex.Z Sector.Lepton (-1))
  51    (hup : Z_up_with_offset c a b = ChargeIndex.Z Sector.UpQuark (2 / 3))
  52    (hdown : Z_down_with_offset c a b = ChargeIndex.Z Sector.DownQuark (-1 / 3)) :
  53    a = 1 ∧ b = 1 ∧ c = 4 := by
  54  rcases anchor_charge_map_values with ⟨hℓv, huv, hdv⟩
  55  have hlep' : Z_lepton a b = 1332 := by
  56    calc
  57      Z_lepton a b = ChargeIndex.Z Sector.Lepton (-1) := hlep
  58      _ = 1332 := hℓv
  59  have hup' : Z_up_with_offset c a b = 276 := by
  60    calc
  61      Z_up_with_offset c a b = ChargeIndex.Z Sector.UpQuark (2 / 3) := hup
  62      _ = 276 := huv
  63  have hdown' : Z_down_with_offset c a b = 24 := by
  64    calc
  65      Z_down_with_offset c a b = ChargeIndex.Z Sector.DownQuark (-1 / 3) := hdown
  66      _ = 24 := hdv
  67  exact full_anchor_tuple_forces_coefficients_and_offset hlep' hup' hdown'
  68
  69/-- Topology-only selection-rule bridge:
  70if a topology-compatible complete polynomial family is ordered and satisfies the
  71minimal complete coefficient budget, then the coefficients are forced to
  72`(a,b) = (1,1)`. -/
  73theorem complete_ordered_min_budget_forces_unit_coeffs
  74    {a b : ℤ}
  75    (ha : a ≥ 1)
  76    (hb : b ≥ 1)
  77    (hord : ordered_hierarchy a b)
  78    (hmin : a + b = 2) :
  79    a = 1 ∧ b = 1 :=
  80  Verification.ZMapTopologicalDerivation.complete_ordered_min_budget_forces_unit_coeffs
  81    ha hb hord hmin
  82
  83/-- Upstreamed minimizer-form selection rule bridge for O2':
  84any complete ordered minimizer in the topology family is forced to `(a,b)=(1,1)`. -/
  85theorem complete_ordered_minimizer_forces_unit_coeffs
  86    {a b : ℤ}
  87    (hmin : complete_ordered_minimizer a b) :
  88    a = 1 ∧ b = 1 :=
  89  Verification.ZMapTopologicalDerivation.complete_ordered_minimizer_forces_unit_coeffs hmin
  90
  91/-- Upstreamed joint first-principles Z-map tuple forcing:
  92if `(k, a, b, c)` satisfies smallest-positive-even integerization + minimal-complete-ordered
  93coefficients + edge-direction color offset, then `(k, a, b, c) = (6, 1, 1, 4)`. -/
  94theorem zmap_canonical_tuple_forced_from_first_principles
  95    {k : ℕ} {a b c : ℤ}
  96    (hk_pos : 0 < k) (hk_even : Even k)
  97    (hint : integerizes_all k)
  98    (hmin_k : ∀ k' : ℕ, 0 < k' → Even k' → integerizes_all k' → k ≤ k')
  99    (hminab : complete_ordered_minimizer a b)
 100    (hc : c = (edge_direction_count : ℤ)) :
 101    k = 6 ∧ a = 1 ∧ b = 1 ∧ c = 4 :=
 102  Verification.ZMapTopologicalDerivation.zmap_canonical_tuple_forced_from_first_principles
 103    hk_pos hk_even hint hmin_k hminab hc
 104
 105/-- Upstreamed converse: canonical `(6, 1, 1, 4)` satisfies all first-principles
 106characterization conditions. -/
 107theorem zmap_canonical_tuple_satisfies_first_principles :
 108    integerizes_all 6 ∧
 109    (∀ k' : ℕ, 0 < k' → Even k' → integerizes_all k' → 6 ≤ k') ∧
 110    complete_ordered_minimizer 1 1 ∧
 111    (4 : ℤ) = (edge_direction_count : ℤ) :=
 112  Verification.ZMapTopologicalDerivation.zmap_canonical_tuple_satisfies_first_principles
 113
 114/-- Upstreamed bundled first-principles tuple predicate for the Z-map lane. -/
 115def first_principles_zmap_tuple (k : ℕ) (a b c : ℤ) : Prop :=
 116  Verification.ZMapTopologicalDerivation.first_principles_zmap_tuple k a b c
 117
 118/-- Upstreamed iff characterization:
 119`(k, a, b, c)` is canonical iff it satisfies the bundled first-principles
 120tuple constraints. -/
 121theorem canonical_tuple_iff_first_principles (k : ℕ) (a b c : ℤ) :
 122    first_principles_zmap_tuple k a b c ↔ (k = 6 ∧ a = 1 ∧ b = 1 ∧ c = 4) :=
 123  Verification.ZMapTopologicalDerivation.canonical_tuple_iff_first_principles k a b c
 124
 125end ZMapForcing
 126end Masses
 127end IndisputableMonolith
 128