Structural integers from ℤ[φ,ζ₆]

@[reducible, inline]

abbrev FUST.StateFunctions.ζ₆Order : ℕ

Equations

• FUST.StateFunctions.ζ₆Order = 6

@[reducible, inline]

abbrev FUST.StateFunctions.colorRank : ℕ

Equations

• FUST.StateFunctions.colorRank = 3

@[reducible, inline]

abbrev FUST.StateFunctions.kernelModeCount : ℕ

Equations

• FUST.StateFunctions.kernelModeCount = 4

@[reducible, inline]

abbrev FUST.StateFunctions.stencilWidth : ℕ

Equations

• FUST.StateFunctions.stencilWidth = 5

@[reducible, inline]

abbrev FUST.StateFunctions.galoisOrder : ℕ

Equations

• FUST.StateFunctions.galoisOrder = 2

Massless gauge boson (mode 0)

The most primitive state: constant function f(z) = 1. Fζ(1) = 0 gives zero eigenvalue → massless. Photon (U(1), 1 copy) and gluons (SU(3) adjoint, 8 copies) share this state; their distinction is channel multiplicity, not state function.

noncomputable def FUST.StateFunctions.masslessGaugeState : ℂ → ℂ

Equations

• FUST.StateFunctions.masslessGaugeState x✝ = 1

theorem FUST.StateFunctions.masslessGauge_kernel : TimeStructure.IsInKerFζ masslessGaugeState

@[reducible, inline]

abbrev FUST.StateFunctions.photonMultiplicity : ℕ

Equations

• FUST.StateFunctions.photonMultiplicity = 1

@[reducible, inline]

abbrev FUST.StateFunctions.gluonMultiplicity : ℕ

Equations

• FUST.StateFunctions.gluonMultiplicity = FUST.StateFunctions.colorRank ^ 2 - 1

Higgs mechanism: mode 0 → mode 1

timeEvolution preserves the Fζ kernel, so massless gauge bosons cannot acquire mass by φ-scaling alone. Mass requires coupling to the vacuum active mode z (mode 1): masslessGaugeState(z) · z = 1 · z = z.

theorem FUST.StateFunctions.masslessGauge_timeEvolution_kernel (k : ℕ) : TimeStructure.IsInKerFζ (TimeStructure.timeEvolution^[k] masslessGaugeState)

noncomputable def FUST.StateFunctions.electronState : ℂ → ℂ

The vacuum active mode: massless gauge coupled to z

Equations

• FUST.StateFunctions.electronState z = FUST.StateFunctions.masslessGaugeState z * z

theorem FUST.StateFunctions.electronState_eq : electronState = fun (z : ℂ) => z

Massive gauge bosons

W, Z, Higgs have mode 1 (active) with mass coefficients from structural integers. Each is electronState scaled by φ^k × rational correction.

@[reducible, inline]

abbrev FUST.StateFunctions.wBosonExponent : ℕ

W exponent: C(stencilWidth,2) + C(ζ₆Order,2) = 25

Equations

• FUST.StateFunctions.wBosonExponent = FUST.StateFunctions.stencilWidth.choose FUST.StateFunctions.galoisOrder + FUST.StateFunctions.ζ₆Order.choose FUST.StateFunctions.galoisOrder

@[reducible, inline]

abbrev FUST.StateFunctions.wBosonDegeneracy : ℕ

W degeneracy: C(ζ₆Order,2) = 15

Equations

• FUST.StateFunctions.wBosonDegeneracy = FUST.StateFunctions.ζ₆Order.choose FUST.StateFunctions.galoisOrder

@[reducible, inline]

abbrev FUST.StateFunctions.wBosonConstraint : ℕ

W constraint: C(ζ₆Order,2) + C(galoisOrder,2) = 16

Equations

• FUST.StateFunctions.wBosonConstraint = FUST.StateFunctions.ζ₆Order.choose FUST.StateFunctions.galoisOrder + FUST.StateFunctions.galoisOrder.choose FUST.StateFunctions.galoisOrder

noncomputable def FUST.StateFunctions.wBosonMassCoeff : ℝ

Equations

• FUST.StateFunctions.wBosonMassCoeff = FUST.φ ^ FUST.StateFunctions.wBosonExponent * (↑FUST.StateFunctions.wBosonDegeneracy / ↑FUST.StateFunctions.wBosonConstraint)

theorem FUST.StateFunctions.wBosonMassCoeff_eq : wBosonMassCoeff = φ ^ 25 * (15 / 16)

noncomputable def FUST.StateFunctions.wBosonState : ℂ → ℂ

W boson: electronState scaled by wBosonMassCoeff

Equations

• FUST.StateFunctions.wBosonState z = ↑FUST.StateFunctions.wBosonMassCoeff * FUST.StateFunctions.electronState z

theorem FUST.StateFunctions.Fζ_wBosonState (z : ℂ) : FζOperator.Fζ wBosonState z = ↑wBosonMassCoeff * FζOperator.Fζ electronState z

noncomputable def FUST.StateFunctions.higgsWFactor : ℝ

Higgs/W ratio: φ - 1/C(stencilWidth, galoisOrder) = φ - 1/10

Equations

• FUST.StateFunctions.higgsWFactor = FUST.φ - 1 / ↑(FUST.StateFunctions.stencilWidth.choose FUST.StateFunctions.galoisOrder)

theorem FUST.StateFunctions.higgsWFactor_eq : higgsWFactor = φ - 1 / 10

noncomputable def FUST.StateFunctions.higgsMassCoeff : ℝ

Higgs: W boson scaled by (φ - 1/10)

Equations

• FUST.StateFunctions.higgsMassCoeff = FUST.StateFunctions.wBosonMassCoeff * FUST.StateFunctions.higgsWFactor

noncomputable def FUST.StateFunctions.higgsState : ℂ → ℂ

Equations

• FUST.StateFunctions.higgsState z = ↑FUST.StateFunctions.higgsMassCoeff * FUST.StateFunctions.electronState z

theorem FUST.StateFunctions.higgsMassCoeff_pos : higgsMassCoeff > 0

noncomputable def FUST.StateFunctions.zBosonMassCoeff : ℝ

Z boson: W boson / cos θ_W where cos²θ_W = 3/4 from channel weights

Equations

• FUST.StateFunctions.zBosonMassCoeff = FUST.StateFunctions.wBosonMassCoeff / √(3 / 4)

noncomputable def FUST.StateFunctions.zBosonState : ℂ → ℂ

Equations

• FUST.StateFunctions.zBosonState z = ↑FUST.StateFunctions.zBosonMassCoeff * FUST.StateFunctions.electronState z

theorem FUST.StateFunctions.zBosonMassCoeff_gt_wBosonMassCoeff : zBosonMassCoeff > wBosonMassCoeff

noncomputable def FUST.StateFunctions.positronState : ℂ → ℂ

Equations

• FUST.StateFunctions.positronState z = z ^ 5

Electron is lightest: Diff5/Diff6 kernel at mode 1

Mode 1 is the unique active mode in ker(Diff5) ∩ ker(Diff6).

theorem FUST.StateFunctions.Diff5_kernel_at_mode1 : φ ^ 2 + φ - 4 + ψ + ψ ^ 2 = 0

theorem FUST.StateFunctions.Diff6_kernel_at_mode1 : φ ^ 3 - 3 * φ ^ 2 + φ - ψ + 3 * ψ ^ 2 - ψ ^ 3 = 0

theorem FUST.StateFunctions.Diff5_nonzero_at_mode5 : φ ^ 10 + φ ^ 5 - 4 + ψ ^ 5 + ψ ^ 10 > 0

Quarks: Fζ-kernel modes (confined)

noncomputable def FUST.StateFunctions.upQuarkState : ℂ → ℂ

Equations

• FUST.StateFunctions.upQuarkState z = z ^ 2

noncomputable def FUST.StateFunctions.downQuarkState : ℂ → ℂ

Equations

• FUST.StateFunctions.downQuarkState z = z ^ 3

noncomputable def FUST.StateFunctions.strangeQuarkState : ℂ → ℂ

Equations

• FUST.StateFunctions.strangeQuarkState z = z ^ 4

theorem FUST.StateFunctions.upQuark_confined : TimeStructure.IsInKerFζ upQuarkState

theorem FUST.StateFunctions.downQuark_confined : TimeStructure.IsInKerFζ downQuarkState

theorem FUST.StateFunctions.strangeQuark_confined : TimeStructure.IsInKerFζ strangeQuarkState

Neutrinos: seesaw-suppressed

Suppression factor 12/25 = afChannelWeight, exponent 2^5 = 32.

@[reducible, inline]

abbrev FUST.StateFunctions.seesawExponent : ℕ

Equations

• FUST.StateFunctions.seesawExponent = FUST.StateFunctions.galoisOrder ^ FUST.StateFunctions.stencilWidth

noncomputable def FUST.StateFunctions.afChannelWeight : ℝ

Equations

• FUST.StateFunctions.afChannelWeight = Complex.normSq FUST.DζOperator.AF_coeff / 5 ^ 2

theorem FUST.StateFunctions.afChannelWeight_eq : afChannelWeight = 12 / 25

noncomputable def FUST.StateFunctions.nu3State : ℂ → ℂ

Equations

• FUST.StateFunctions.nu3State z = ↑(FUST.StateFunctions.afChannelWeight * FUST.φ ^ (-↑FUST.StateFunctions.seesawExponent)) * z

theorem FUST.StateFunctions.nu3_coeff_pos : afChannelWeight * φ ^ (-↑seesawExponent) > 0

theorem FUST.StateFunctions.nu3_coeff_lt_one : afChannelWeight * φ ^ (-↑seesawExponent) < 1