IndisputableMonolith.Foundation.SMHyperchargeFromCube

   1import Mathlib
   2import IndisputableMonolith.Foundation.GaugeLieCompletionFromCube
   3
   4/-!
   5# Standard Model Hypercharge Layer from the Cube Completion
   6
   7This module continues `P0-S2-01` from
   8`planning/REALITY_DERIVATION_PUNCHLIST.md`.
   9
  10`GaugeLieCompletionFromCube` proves the compact gauge-factor skeleton:
  11
  12* `SU(3) x SU(2) x U(1)`
  13* recognition-axis counts `(3,2,1)`
  14* carrier counts `(8,3,1)`
  15
  16The next question is whether the Standard Model fermion multiplets and
  17hypercharges can be represented in the same cube-completion units.
  18
  19Here we use the canonical hypercharge denominator `6`, i.e. every
  20hypercharge is represented by the integer `Y6 = 6Y`.
  21
  22For one left-handed generation, including the sterile/right-handed neutrino
  23as the hypercharge-zero completion:
  24
  25* `Q_L`: multiplicity 6, `Y6 = 1`
  26* `u^c_L`: multiplicity 3, `Y6 = -4`
  27* `d^c_L`: multiplicity 3, `Y6 = 2`
  28* `L_L`: multiplicity 2, `Y6 = -3`
  29* `e^c_L`: multiplicity 1, `Y6 = 6`
  30* `nu^c_L`: multiplicity 1, `Y6 = 0`
  31
  32This gives `16` Weyl states per generation and exact cancellation of the
  33`SU(3)^2 U(1)`, `SU(2)^2 U(1)`, gravitational-`U(1)`, and `U(1)^3`
  34anomaly sums in integer arithmetic.
  35
  36This is still not a proof that these hypercharges are uniquely forced.
  37It is the exact anomaly-free SM hypercharge layer expressed in the cube
  38completion's `1/6` unit.
  39
  40Lean status: 0 sorry, 0 axiom.
  41-/
  42
  43namespace IndisputableMonolith.Foundation.SMHyperchargeFromCube
  44
  45open GaugeLieCompletionFromCube
  46
  47/-- One left-handed generation of SM Weyl multiplets. -/
  48inductive WeylMultiplet where
  49  | quarkDoublet
  50  | upConjugate
  51  | downConjugate
  52  | leptonDoublet
  53  | electronConjugate
  54  | neutrinoConjugate
  55  deriving DecidableEq, Repr, BEq, Fintype
  56
  57theorem weylMultiplet_count : Fintype.card WeylMultiplet = 6 := by
  58  decide
  59
  60/-- Number of Weyl states carried by each multiplet, including color and weak components. -/
  61def weylMultiplicity : WeylMultiplet -> ℕ
  62  | .quarkDoublet => 6
  63  | .upConjugate => 3
  64  | .downConjugate => 3
  65  | .leptonDoublet => 2
  66  | .electronConjugate => 1
  67  | .neutrinoConjugate => 1
  68
  69/-- Hypercharge in sixths: `Y6 = 6Y`. -/
  70def hypercharge6 : WeylMultiplet -> ℤ
  71  | .quarkDoublet => 1      -- Y =  1/6
  72  | .upConjugate => -4      -- Y = -2/3
  73  | .downConjugate => 2     -- Y =  1/3
  74  | .leptonDoublet => -3    -- Y = -1/2
  75  | .electronConjugate => 6 -- Y =  1
  76  | .neutrinoConjugate => 0 -- Y =  0
  77
  78/-- The Higgs doublet has `Y = 1/2`, i.e. `Y6 = 3`. -/
  79def higgsHypercharge6 : ℤ := 3
  80
  81theorem higgsHypercharge6_eq : higgsHypercharge6 = 3 := rfl
  82
  83/-- One generation has `6 + 3 + 3 + 2 + 1 + 1 = 16` Weyl states. -/
  84def generationWeylStateCount : ℕ :=
  85  weylMultiplicity .quarkDoublet +
  86  weylMultiplicity .upConjugate +
  87  weylMultiplicity .downConjugate +
  88  weylMultiplicity .leptonDoublet +
  89  weylMultiplicity .electronConjugate +
  90  weylMultiplicity .neutrinoConjugate
  91
  92theorem generationWeylStateCount_eq_16 : generationWeylStateCount = 16 := by
  93  native_decide
  94
  95/-- Three generations contain `48 = |B3|` Weyl states in this accounting. -/
  96def threeGenerationWeylStateCount : ℕ := 3 * generationWeylStateCount
  97
  98theorem threeGenerationWeylStateCount_eq_48 :
  99    threeGenerationWeylStateCount = Fintype.card (GaugeFromCube.SignedPerm 3) := by
 100  rw [GaugeFromCube.cube_aut_order]
 101  native_decide
 102
 103/-! ## Exact anomaly sums in `Y6 = 6Y` units -/
 104
 105/-- `SU(3)^2 U(1)` anomaly in sixth-units: `2Y_Q + Y_u^c + Y_d^c = 0`. -/
 106def su3SquaredU1Anomaly6 : ℤ :=
 107  2 * hypercharge6 .quarkDoublet +
 108  hypercharge6 .upConjugate +
 109  hypercharge6 .downConjugate
 110
 111theorem su3SquaredU1Anomaly6_eq_zero : su3SquaredU1Anomaly6 = 0 := by
 112  native_decide
 113
 114/-- `SU(2)^2 U(1)` anomaly: `3Y_Q + Y_L = 0`. -/
 115def su2SquaredU1Anomaly6 : ℤ :=
 116  3 * hypercharge6 .quarkDoublet +
 117  hypercharge6 .leptonDoublet
 118
 119theorem su2SquaredU1Anomaly6_eq_zero : su2SquaredU1Anomaly6 = 0 := by
 120  native_decide
 121
 122/-- Gravitational-`U(1)` anomaly, scaled by 6. -/
 123def gravitationalU1Anomaly6 : ℤ :=
 124  6 * hypercharge6 .quarkDoublet +
 125  3 * hypercharge6 .upConjugate +
 126  3 * hypercharge6 .downConjugate +
 127  2 * hypercharge6 .leptonDoublet +
 128  hypercharge6 .electronConjugate +
 129  hypercharge6 .neutrinoConjugate
 130
 131theorem gravitationalU1Anomaly6_eq_zero : gravitationalU1Anomaly6 = 0 := by
 132  native_decide
 133
 134/-- Cubic `U(1)^3` anomaly, scaled by `6^3`. -/
 135def cubicU1Anomaly6 : ℤ :=
 136  6 * (hypercharge6 .quarkDoublet)^3 +
 137  3 * (hypercharge6 .upConjugate)^3 +
 138  3 * (hypercharge6 .downConjugate)^3 +
 139  2 * (hypercharge6 .leptonDoublet)^3 +
 140  (hypercharge6 .electronConjugate)^3 +
 141  (hypercharge6 .neutrinoConjugate)^3
 142
 143theorem cubicU1Anomaly6_eq_zero : cubicU1Anomaly6 = 0 := by
 144  native_decide
 145
 146/-! ## Electric charges in sixth-units -/
 147
 148/-- Weak isospin third component in sixth-units: `T3_6 = 6T3 = ±3`. -/
 149inductive WeakComponent where
 150  | upper
 151  | lower
 152  deriving DecidableEq, Repr, BEq, Fintype
 153
 154def weakT3_6 : WeakComponent -> ℤ
 155  | .upper => 3
 156  | .lower => -3
 157
 158/-- Electric charge in sixth-units: `Q6 = 6Q = T3_6 + Y6`. -/
 159def electricCharge6 (m : WeylMultiplet) (c : WeakComponent) : ℤ :=
 160  weakT3_6 c + hypercharge6 m
 161
 162theorem quark_doublet_charges :
 163    electricCharge6 .quarkDoublet .upper = 4 ∧
 164    electricCharge6 .quarkDoublet .lower = -2 := by
 165  native_decide
 166
 167theorem lepton_doublet_charges :
 168    electricCharge6 .leptonDoublet .upper = 0 ∧
 169    electricCharge6 .leptonDoublet .lower = -6 := by
 170  native_decide
 171
 172structure SMHyperchargeCert where
 173  six_multiplets : Fintype.card WeylMultiplet = 6
 174  one_generation_16 : generationWeylStateCount = 16
 175  three_generations_b3 : threeGenerationWeylStateCount =
 176    Fintype.card (GaugeFromCube.SignedPerm 3)
 177  su3_anomaly_zero : su3SquaredU1Anomaly6 = 0
 178  su2_anomaly_zero : su2SquaredU1Anomaly6 = 0
 179  gravitational_anomaly_zero : gravitationalU1Anomaly6 = 0
 180  cubic_anomaly_zero : cubicU1Anomaly6 = 0
 181  quark_charges : electricCharge6 .quarkDoublet .upper = 4 ∧
 182    electricCharge6 .quarkDoublet .lower = -2
 183  lepton_charges : electricCharge6 .leptonDoublet .upper = 0 ∧
 184    electricCharge6 .leptonDoublet .lower = -6
 185  higgs_y6 : higgsHypercharge6 = 3
 186
 187def smHyperchargeCert : SMHyperchargeCert where
 188  six_multiplets := weylMultiplet_count
 189  one_generation_16 := generationWeylStateCount_eq_16
 190  three_generations_b3 := threeGenerationWeylStateCount_eq_48
 191  su3_anomaly_zero := su3SquaredU1Anomaly6_eq_zero
 192  su2_anomaly_zero := su2SquaredU1Anomaly6_eq_zero
 193  gravitational_anomaly_zero := gravitationalU1Anomaly6_eq_zero
 194  cubic_anomaly_zero := cubicU1Anomaly6_eq_zero
 195  quark_charges := quark_doublet_charges
 196  lepton_charges := lepton_doublet_charges
 197  higgs_y6 := higgsHypercharge6_eq
 198
 199end IndisputableMonolith.Foundation.SMHyperchargeFromCube
 200