Charge channels of SU(7) representations and the moment generators

Finite identities, checked by decide, for the six-dimensional SU(7) gauge-Higgs unification model. A weight records the Wilson-line charge q and two orbifold parities p, b; the 7, Sym² 7 = 28, End 7 = 48 + 1 and Sym³ 7 = 84 are built as lists of weights, and their charge channels give the gauge-sector coefficients and the moment generators (8D, 2A₄) of the eight bulk multiplets. This is conditional algebra; the Fourier and interval analysis of the potential is not formalized.

eight_generator_moments_eq_matter identifies the computed generators with the data OddEighths.matter, so the mod-6 law and the odd-eighths statement of OddEighths apply to them; they are not repeated here.

Main results

• symmetric2_dimension, symmetric3_dimension, adjoint_dimension: 28, 84, 48.
• symmetric2_coefficients, adjoint_coefficients, symmetric3_coefficients: the charge channels.
• printed_gauge_coefficients, background_gauge_coefficients: the gauge coefficients for 4 and 3 periodic degrees of freedom.
• seed_shift_d8, seed_shift_a4, seed_shift_w: in units of 1/4 the two seeds differ by 36 in 8D and 18 in A₄ (so Δ(8D) = 9, ΔA₄ = 9/2) and agree in W; seed_shift_preserves_law_combination: they agree in 8D − 2A₄.
• quartet_lower_weight_is_required: the SU(2) quartet has weights ±1 and ±3.
• eight_generator_moments, eight_generator_moments_eq_matter: the moments (8D, 2A₄) of the eight bulk multiplets.
• candidate_seed_even: with the candidate seed 8D is even for every content.

References

• Y. Komori, N. Maru, SU(7) grand gauge-Higgs unification, arXiv:2503.04090, eq. (68).

structure GaugeHiggsUnification.SU7WeightChannels.Weight : Type

A weight: Wilson-line charge q and the parities p, b.

• q : ℤ

  The Wilson-line charge.

• p : ℤ

  The first parity.

• b : ℤ

  The second parity.

@[instance_reducible]

instance GaugeHiggsUnification.SU7WeightChannels.instDecidableEqWeight : DecidableEq Weight

Equations

• GaugeHiggsUnification.SU7WeightChannels.instDecidableEqWeight = GaugeHiggsUnification.SU7WeightChannels.instDecidableEqWeight.decEq

def GaugeHiggsUnification.SU7WeightChannels.instDecidableEqWeight.decEq (x✝ x✝¹ : Weight) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance GaugeHiggsUnification.SU7WeightChannels.instReprWeight : Repr Weight

Equations

• GaugeHiggsUnification.SU7WeightChannels.instReprWeight = { reprPrec := GaugeHiggsUnification.SU7WeightChannels.instReprWeight.repr }

def GaugeHiggsUnification.SU7WeightChannels.instReprWeight.repr : Weight → ℕ → Std.Format

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.fundamental : List Weight

The weights of the fundamental 7.

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.tensor (a b : Weight) : Weight

The weight of a tensor product: charges add, parities multiply.

Equations

• GaugeHiggsUnification.SU7WeightChannels.tensor a b = { q := a.q + b.q, p := a.p * b.p, b := a.b * b.b }

def GaugeHiggsUnification.SU7WeightChannels.conjugate (a : Weight) : Weight

The conjugate weight.

Equations

• GaugeHiggsUnification.SU7WeightChannels.conjugate a = { q := -a.q, p := a.p, b := a.b }

@[instance_reducible]

instance GaugeHiggsUnification.SU7WeightChannels.instInhabitedWeight : Inhabited Weight

Equations

• GaugeHiggsUnification.SU7WeightChannels.instInhabitedWeight = { default := { q := 0, p := 1, b := 1 } }

def GaugeHiggsUnification.SU7WeightChannels.w (i : ℕ) : Weight

The i-th weight of the fundamental.

Equations

• GaugeHiggsUnification.SU7WeightChannels.w i = GaugeHiggsUnification.SU7WeightChannels.fundamental[i]!

def GaugeHiggsUnification.SU7WeightChannels.symmetric2 : List Weight

The weights of Sym² 7.

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.symmetric3 : List Weight

The weights of Sym³ 7.

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.endomorphisms : List Weight

The weights of End 7 (dimension 49). Removing its neutral singlet gives the adjoint; the singlet contributes to none of the nonzero-charge counts below.

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.channel (rep : List Weight) (q b : ℤ) : ℕ

The number of weights of charge q and parity b.

Equations

• GaugeHiggsUnification.SU7WeightChannels.channel rep q b = (List.filter (fun (a : GaugeHiggsUnification.SU7WeightChannels.Weight) => a.q == q && a.b == b) rep).length

def GaugeHiggsUnification.SU7WeightChannels.parityChannel (q p b : ℤ) : ℕ

The number of weights of End 7 of charge q and parities p, b.

Equations

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

theorem GaugeHiggsUnification.SU7WeightChannels.fundamental_dimension : fundamental.length = 7

The fundamental has dimension 7.

theorem GaugeHiggsUnification.SU7WeightChannels.symmetric2_dimension : symmetric2.length = 28

Sym² 7 has dimension 28.

theorem GaugeHiggsUnification.SU7WeightChannels.symmetric3_dimension : symmetric3.length = 84

Sym³ 7 has dimension 84.

theorem GaugeHiggsUnification.SU7WeightChannels.adjoint_dimension : endomorphisms.length - 1 = 48

The adjoint has dimension 48.

theorem GaugeHiggsUnification.SU7WeightChannels.fundamental_coefficients : channel fundamental 1 (-1) = 1 ∧ channel fundamental 1 1 = 0

The charge channels of the fundamental.

theorem GaugeHiggsUnification.SU7WeightChannels.symmetric2_coefficients : channel symmetric2 2 1 = 1 ∧ channel symmetric2 2 (-1) = 0 ∧ channel symmetric2 1 1 = 1 ∧ channel symmetric2 1 (-1) = 4

The charge channels of Sym² 7.

theorem GaugeHiggsUnification.SU7WeightChannels.adjoint_coefficients : channel endomorphisms 2 1 = 1 ∧ channel endomorphisms 2 (-1) = 0 ∧ channel endomorphisms 1 1 = 2 ∧ channel endomorphisms 1 (-1) = 8

The charge channels of the adjoint.

theorem GaugeHiggsUnification.SU7WeightChannels.symmetric3_coefficients : channel symmetric3 3 (-1) = 1 ∧ channel symmetric3 3 1 = 0 ∧ channel symmetric3 2 (-1) = 1 ∧ channel symmetric3 2 1 = 4 ∧ channel symmetric3 1 (-1) = 12 ∧ channel symmetric3 1 1 = 4

The charge channels of Sym³ 7.

theorem GaugeHiggsUnification.SU7WeightChannels.adjoint_parity_resolution : parityChannel 2 1 1 = 1 ∧ parityChannel 1 1 1 = 2 ∧ parityChannel 1 1 (-1) = 2 ∧ parityChannel 1 (-1) (-1) = 6 ∧ parityChannel 2 (-1) 1 = 0 ∧ parityChannel 1 (-1) 1 = 0

The adjoint channels resolved by both parities.

def GaugeHiggsUnification.SU7WeightChannels.gaugeFourM (periodicDof q b : ℤ) : ℤ

The gauge-sector coefficient of charge q and parity b, with periodicDof periodic degrees of freedom.

Equations

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

theorem GaugeHiggsUnification.SU7WeightChannels.printed_gauge_coefficients : gaugeFourM 4 2 1 = -4 ∧ gaugeFourM 4 1 1 = -8 ∧ gaugeFourM 4 1 (-1) = -14

The gauge coefficients with 4 periodic degrees of freedom (the printed seed).

theorem GaugeHiggsUnification.SU7WeightChannels.background_gauge_coefficients : gaugeFourM 3 2 1 = -3 ∧ gaugeFourM 3 1 1 = -6 ∧ gaugeFourM 3 1 (-1) = -12

The gauge coefficients with 3 periodic degrees of freedom (the candidate seed).

def GaugeHiggsUnification.SU7WeightChannels.d8Four (n : ℤ) : ℤ

Four times the gauge contribution to 8D.

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.a4Four (n : ℤ) : ℤ

Four times the gauge contribution to A₄.

Equations

• GaugeHiggsUnification.SU7WeightChannels.a4Four n = 16 * GaugeHiggsUnification.SU7WeightChannels.gaugeFourM n 2 1 + GaugeHiggsUnification.SU7WeightChannels.gaugeFourM n 1 1

def GaugeHiggsUnification.SU7WeightChannels.wFour (n : ℤ) : ℤ

Four times the gauge contribution to W.

Equations

• GaugeHiggsUnification.SU7WeightChannels.wFour n = -GaugeHiggsUnification.SU7WeightChannels.gaugeFourM n 1 1 + GaugeHiggsUnification.SU7WeightChannels.gaugeFourM n 1 (-1)

theorem GaugeHiggsUnification.SU7WeightChannels.seed_shift_d8 : d8Four 3 - d8Four 4 = 36

The seeds differ by 36 / 4 = 9 in 8D.

theorem GaugeHiggsUnification.SU7WeightChannels.seed_shift_a4 : a4Four 3 - a4Four 4 = 18

The seeds differ by 18 / 4 = 9/2 in A₄.

theorem GaugeHiggsUnification.SU7WeightChannels.seed_shift_w : wFour 3 = wFour 4

The seeds agree in W.

theorem GaugeHiggsUnification.SU7WeightChannels.seed_shift_preserves_law_combination : d8Four 3 - 2 * a4Four 3 = d8Four 4 - 2 * a4Four 4

The seeds agree in 8D − 2A₄.

def GaugeHiggsUnification.SU7WeightChannels.doublet : List Weight

The weights of the SU(2) doublet.

Equations

• GaugeHiggsUnification.SU7WeightChannels.doublet = [{ q := 1, p := -1, b := -1 }, { q := -1, p := -1, b := -1 }]

def GaugeHiggsUnification.SU7WeightChannels.quartet : List Weight

The weights of the SU(2) quartet Sym³ 2.

Equations

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

theorem GaugeHiggsUnification.SU7WeightChannels.quartet_lower_weight_is_required : channel quartet 1 (-1) = 1 ∧ channel quartet 3 (-1) = 1

The quartet has weights of charge 1 and 3, each once: its lower weight cannot be discarded.

theorem GaugeHiggsUnification.SU7WeightChannels.same_matter_preserves_d8_shift (matter : ℤ) : d8Four 3 + matter - (d8Four 4 + matter) = 36

The same matter content preserves the shift in 8D.

theorem GaugeHiggsUnification.SU7WeightChannels.same_matter_preserves_a4_shift (matter : ℤ) : a4Four 3 + matter - (a4Four 4 + matter) = 18

The same matter content preserves the shift in A₄.

theorem GaugeHiggsUnification.SU7WeightChannels.same_matter_preserves_w (matter : ℤ) : wFour 3 + matter = wFour 4 + matter

The same matter content preserves W.

theorem GaugeHiggsUnification.SU7WeightChannels.dirac_chirality_trace_cancels_parity (z : ℤ) : 2 * (1 + z) + 2 * (1 + z) + 2 * (1 - z) + 2 * (1 - z) = 8

The Dirac chirality trace cancels the parity.

def GaugeHiggsUnification.SU7WeightChannels.representationD8 (rep : List Weight) (eta : ℤ) : ℤ

The moment 8D of a representation with parity eta.

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.representation2A4 (rep : List Weight) (eta : ℤ) : ℤ

The moment 2A₄ of a representation with parity eta.

Equations

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

def GaugeHiggsUnification.SU7WeightChannels.representationMoments (rep : List Weight) (eta : ℤ) : ℤ × ℤ

The pair (8D, 2A₄).

Equations

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

theorem GaugeHiggsUnification.SU7WeightChannels.eight_generator_moments : [representationMoments fundamental 1, representationMoments fundamental (-1), representationMoments symmetric2 1, representationMoments symmetric2 (-1), representationMoments endomorphisms 1, representationMoments endomorphisms (-1), representationMoments symmetric3 1, representationMoments symmetric3 (-1)] = [(-6, 0), (8, 2), (16, 34), (2, 8), (0, 36), (28, 16), (10, 136), (80, 218)]

The moments (8D, 2A₄) of the eight bulk multiplets.

theorem GaugeHiggsUnification.SU7WeightChannels.eight_generator_moments_eq_matter : [representationMoments fundamental 1, representationMoments fundamental (-1), representationMoments symmetric2 1, representationMoments symmetric2 (-1), representationMoments endomorphisms 1, representationMoments endomorphisms (-1), representationMoments symmetric3 1, representationMoments symmetric3 (-1)] = List.map (fun (v : ℤ × ℤ × ℤ) => (v.2.1, v.1)) OddEighths.matter

The computed moments are the data OddEighths.matter (coordinates (2A₄, 8D, 2W)).

def GaugeHiggsUnification.SU7WeightChannels.bulkD8 (a b c d e f g h : ℤ) : ℤ

The moment 8D of a content with integer multiplicities.

Equations

• GaugeHiggsUnification.SU7WeightChannels.bulkD8 a b c d e f g h = -6 * a + 8 * b + 16 * c + 2 * d + 0 * e + 28 * f + 10 * g + 80 * h

theorem GaugeHiggsUnification.SU7WeightChannels.candidate_seed_even (a b c d e f g h : ℤ) : (-18 + bulkD8 a b c d e f g h) % 2 = 0

With the candidate seed (8D = −18), 8D is even for every content.