Particle Spectrum from State Functions

Derives the complete SM particle spectrum from StateFunctions:

1. Particle counts from structural integers + channel weights
2. Forbidden particles from Fζ kernel structure
3. Quantum number constraints from mode structure

Fermion generations

3 flavors from the 3 active SY sub-operators (Diff5, Diff3, Diff2).

@[reducible, inline]

abbrev FUST.ParticleSpectrum.fermionFlavorCount : ℕ

Equations

• FUST.ParticleSpectrum.fermionFlavorCount = 3

Spin degeneracy from AF channel

SU(2) fundamental rep dimension = 2.

@[reducible, inline]

abbrev FUST.ParticleSpectrum.spinDegeneracy : ℕ

Equations

• FUST.ParticleSpectrum.spinDegeneracy = 2

Lepton count: 2 per flavor (particle + neutrino)

spinDegeneracy = 2 from AF channel gives the isospin doublet.

@[reducible, inline]

abbrev FUST.ParticleSpectrum.leptonCount : ℕ

Equations

• FUST.ParticleSpectrum.leptonCount = FUST.ParticleSpectrum.spinDegeneracy * FUST.ParticleSpectrum.fermionFlavorCount

theorem FUST.ParticleSpectrum.leptonCount_eq : leptonCount = 6

Quark count: 2 × flavors × colors

Each flavor has up-type + down-type. Color triplet from colorRank.

@[reducible, inline]

abbrev FUST.ParticleSpectrum.quarkCount : ℕ

Equations

• FUST.ParticleSpectrum.quarkCount = FUST.ParticleSpectrum.spinDegeneracy * FUST.ParticleSpectrum.fermionFlavorCount * FUST.StateFunctions.colorRank

theorem FUST.ParticleSpectrum.quarkCount_eq : quarkCount = 18

SM fermion count

@[reducible, inline]

abbrev FUST.ParticleSpectrum.smFermionCount : ℕ

Equations

• FUST.ParticleSpectrum.smFermionCount = FUST.ParticleSpectrum.leptonCount + FUST.ParticleSpectrum.quarkCount

theorem FUST.ParticleSpectrum.smFermionCount_eq : smFermionCount = 24

Boson counts from gauge structure

Photon: 1 (U(1) singlet = photonMultiplicity) W±, Z: colorRank (SU(2) adjoint dim) Gluons: gluonMultiplicity = colorRank² - 1 = 8 Higgs: 1

@[reducible, inline]

abbrev FUST.ParticleSpectrum.weakBosonCount : ℕ

Equations

• FUST.ParticleSpectrum.weakBosonCount = FUST.StateFunctions.colorRank

theorem FUST.ParticleSpectrum.weakBosonCount_eq : weakBosonCount = 3

@[reducible, inline]

abbrev FUST.ParticleSpectrum.smBosonCount : ℕ

Equations

• FUST.ParticleSpectrum.smBosonCount = FUST.StateFunctions.photonMultiplicity + FUST.ParticleSpectrum.weakBosonCount + FUST.StateFunctions.gluonMultiplicity + 1

theorem FUST.ParticleSpectrum.smBosonCount_eq : smBosonCount = 13

Total SM particle count

@[reducible, inline]

abbrev FUST.ParticleSpectrum.smParticleCount : ℕ

Equations

• FUST.ParticleSpectrum.smParticleCount = FUST.ParticleSpectrum.smFermionCount + FUST.ParticleSpectrum.smBosonCount

theorem FUST.ParticleSpectrum.smParticleCount_eq : smParticleCount = 37

SM count derivation chain

theorem FUST.ParticleSpectrum.smCount_derivation : fermionFlavorCount = 3 ∧ leptonCount = spinDegeneracy * fermionFlavorCount ∧ quarkCount = spinDegeneracy * fermionFlavorCount * StateFunctions.colorRank ∧ smFermionCount = leptonCount + quarkCount ∧ StateFunctions.gluonMultiplicity = StateFunctions.colorRank ^ 2 - 1 ∧ weakBosonCount = StateFunctions.colorRank ∧ smParticleCount = 37

Allowed charges: Q = n/3 where 3 = colorRank

Electric charge quantization follows from C(colorRank, 2) = 3.

@[reducible, inline]

abbrev FUST.ParticleSpectrum.chargeDenom : ℕ

Equations

• FUST.ParticleSpectrum.chargeDenom = FUST.StateFunctions.colorRank.choose FUST.StateFunctions.galoisOrder

theorem FUST.ParticleSpectrum.chargeDenom_eq : chargeDenom = 3

@[reducible, inline]

abbrev FUST.ParticleSpectrum.allowedChargeCount : ℕ

Equations

• FUST.ParticleSpectrum.allowedChargeCount = 2 * FUST.ParticleSpectrum.chargeDenom + 1

theorem FUST.ParticleSpectrum.allowedChargeCount_eq : allowedChargeCount = 7

@[reducible, inline]

abbrev FUST.ParticleSpectrum.allowedChargeNumerators : List ℤ

Equations

• FUST.ParticleSpectrum.allowedChargeNumerators = [-3, -2, -1, 0, 1, 2, 3]

theorem FUST.ParticleSpectrum.allowedChargeNumerators_length : allowedChargeNumerators.length = allowedChargeCount

theorem FUST.ParticleSpectrum.charge_one_fifth_forbidden (n : ℤ) : ↑n / 3 ≠ 1 / 5

Allowed spins from mode structure

Modes 0,1,2 give integer spin 0,1,2. Half-integer from spinDegeneracy doubling.

inductive FUST.ParticleSpectrum.Spin : Type

• zero : Spin
• half : Spin
• one : Spin
• two : Spin

instance FUST.ParticleSpectrum.instDecidableEqSpin : DecidableEq Spin

Equations

• FUST.ParticleSpectrum.instDecidableEqSpin x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FUST.ParticleSpectrum.instReprSpin.repr : Spin → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance FUST.ParticleSpectrum.instReprSpin : Repr Spin

Equations

• FUST.ParticleSpectrum.instReprSpin = { reprPrec := FUST.ParticleSpectrum.instReprSpin.repr }

@[reducible, inline]

abbrev FUST.ParticleSpectrum.allowedSpins : List Spin

Equations

• FUST.ParticleSpectrum.allowedSpins = [FUST.ParticleSpectrum.Spin.zero, FUST.ParticleSpectrum.Spin.half, FUST.ParticleSpectrum.Spin.one, FUST.ParticleSpectrum.Spin.two]

@[reducible, inline]

abbrev FUST.ParticleSpectrum.allowedSpinCount : ℕ

Equations

• FUST.ParticleSpectrum.allowedSpinCount = FUST.ParticleSpectrum.allowedSpins.length

theorem FUST.ParticleSpectrum.allowedSpinCount_eq : allowedSpinCount = 4

Kernel vs active mode disjointness

Quarks = kernel modes (0,2,3,4 mod 6), leptons = active modes (1,5 mod 6). A "colored lepton" would need both — the mod 6 classes are disjoint.

theorem FUST.ParticleSpectrum.kernel_active_disjoint (k : ℕ) : k % 6 = 0 ∨ k % 6 = 2 ∨ k % 6 = 3 ∨ k % 6 = 4 → k % 6 ≠ 1 ∧ k % 6 ≠ 5

Generation structure from pair counts

All mass exponents are sums of C(n,2) for structural integers. Generation exponents are sums of C(n,2) for structural integers.

theorem FUST.ParticleSpectrum.lepton_generation_exponents : StateFunctions.stencilWidth.choose StateFunctions.galoisOrder + StateFunctions.galoisOrder.choose StateFunctions.galoisOrder = 11 ∧ StateFunctions.kernelModeCount.choose StateFunctions.galoisOrder = 6 ∧ StateFunctions.stencilWidth.choose StateFunctions.galoisOrder + StateFunctions.galoisOrder.choose StateFunctions.galoisOrder + StateFunctions.kernelModeCount.choose StateFunctions.galoisOrder = 17

theorem FUST.ParticleSpectrum.proton_exponent : StateFunctions.stencilWidth.choose StateFunctions.galoisOrder + StateFunctions.colorRank.choose StateFunctions.galoisOrder + StateFunctions.galoisOrder.choose StateFunctions.galoisOrder = 14

theorem FUST.ParticleSpectrum.wBoson_exponent : StateFunctions.stencilWidth.choose StateFunctions.galoisOrder + StateFunctions.ζ₆Order.choose StateFunctions.galoisOrder = 25

theorem FUST.ParticleSpectrum.five_pair_counts : StateFunctions.galoisOrder.choose StateFunctions.galoisOrder = 1 ∧ StateFunctions.colorRank.choose StateFunctions.galoisOrder = 3 ∧ StateFunctions.kernelModeCount.choose StateFunctions.galoisOrder = 6 ∧ StateFunctions.stencilWidth.choose StateFunctions.galoisOrder = 10 ∧ StateFunctions.ζ₆Order.choose StateFunctions.galoisOrder = 15

Particle spectrum summary

theorem FUST.ParticleSpectrum.particle_spectrum_summary : smParticleCount = 37 ∧ fermionFlavorCount = 3 ∧ allowedSpinCount = 4 ∧ allowedChargeCount = 2 * chargeDenom + 1 ∧ chargeDenom = StateFunctions.colorRank.choose StateFunctions.galoisOrder ∧ StateFunctions.gluonMultiplicity = StateFunctions.colorRank ^ 2 - 1 ∧ weakBosonCount = StateFunctions.colorRank