The x₆ parity of SU(7) gauge components separates colour

In the SU(7) gauge-Higgs unification model of Komori–Maru the parity acting in x₆ is P₆ = diag(+,+,+,−,−,−,−): the first three indices of the fundamental are the colour triplet. A gauge component along E_ij carries the product P₆(i) P₆(j). This file proves the arithmetic half of the theorem "colour lives on the small circle": P₆(i) P₆(j) = −1 iff exactly one of i, j is a colour index, and there are exactly 24 such components. The other half (the P₆-odd components expand in sin (m x₆ / R₆), m ≥ 1) is a reading of the mode expansions of Komori–Maru and is not formalized.

Main results

• colourParity_neg_iff: P₆ i * P₆ j = −1 ↔ (IsColour i ↔ ¬ IsColour j).
• colourChanging_card: exactly 24 ordered index pairs (i, j) have P₆ i * P₆ j = −1.
• colourChanging_parity_neg: no colour-changing component has P₆ = +1.

References

• C. Marín, An Upper Bound on the Compactification Scale of SU(7) Grand Gauge-Higgs Unification, and the Dijet Angular Distribution That Tests It (Part VII), Zenodo, doi:10.5281/zenodo.22087252, eq. (colourparity) and Theorem (colour lives on the small circle).
• Y. Komori, N. Maru, SU(7) grand gauge-Higgs unification, arXiv:2503.04090, eq. (11).

def GaugeHiggsUnification.SU7ColourParity.IsColour (i : Fin 7) : Prop

The colour block: the first three indices of the fundamental 7.

Equations

• GaugeHiggsUnification.SU7ColourParity.IsColour i = (↑i < 3)

@[instance_reducible]

instance GaugeHiggsUnification.SU7ColourParity.instDecidablePredFinOfNatNatIsColour : DecidablePred IsColour

Equations

• GaugeHiggsUnification.SU7ColourParity.instDecidablePredFinOfNatNatIsColour i = { decide := (↑i).succ.ble 3, reflects_decide := ⋯ }

def GaugeHiggsUnification.SU7ColourParity.P6 (i : Fin 7) : ℤ

The x₆ parity P₆ = diag(+,+,+,−,−,−,−) on the indices of the fundamental.

Equations

• GaugeHiggsUnification.SU7ColourParity.P6 i = if GaugeHiggsUnification.SU7ColourParity.IsColour i then 1 else -1

theorem GaugeHiggsUnification.SU7ColourParity.colourParity_neg_iff (i j : Fin 7) : P6 i * P6 j = -1 ↔ (IsColour i ↔ ¬IsColour j)

P₆(i) P₆(j) = −1 exactly when one and only one index is a colour index.

theorem GaugeHiggsUnification.SU7ColourParity.colourChanging_card : {p : Fin 7 × Fin 7 | P6 p.1 * P6 p.2 = -1}.card = 24

There are exactly 24 gauge components E_ij with P₆(i) P₆(j) = −1.

theorem GaugeHiggsUnification.SU7ColourParity.colourChanging_parity_neg (i j : Fin 7) (h : IsColour i ↔ ¬IsColour j) : P6 i * P6 j = -1

No colour-changing component carries P₆ = +1.