Under diagonal ±1 parities the adjoint of SU(n) furnishes no chiral state

Orbifold parities P₅, P₅' act diagonally on the indices of the fundamental. A component of a bulk multiplet survives in the multiplet of parities (η, η') iff P₅ P₅' = η η', and then carries 4D chirality −η P₅ (Komori–Maru, eqs. (37)–(40)). The component (i, j̄) of n ⊗ n̄ carries the parity p i * (p j)⁻¹; for its conjugate (j, ī) this is p j * (p i)⁻¹. When every p i squares to 1 the two coincide, so (i, j̄) and (j, ī) survive together, with the same chirality and opposite charges: the surviving spectrum of the adjoint is vector-like.

The hypothesis p i * p i = 1 is exactly what is used: in a general commutative group the conjugate index carries the inverse parity and the swap no longer preserves it. For the ℤ₂ parities of the model (ℤˣ-valued) it holds automatically (Int.units_mul_self).

The counts of the paper are checked by decide on its data P₅ = diag(+,+,+,+,+,−,−), P₅' = diag(+,+,+,−,−,−,+), with the hypercharge and the extra U(1) per index (in units of 1/2). Off the Cartan (42 components, as in the paper's script), a 48^(+,+) has 18 survivors and a 48^(+,−) has 24, all paired; the complex controls 28 = Sym² 7 and 84 = Sym³ 7 leave 10 and 34 unpaired states at (+,+). "Paired" means: another survivor of the same chirality with opposite (Y, extra).

Main results

• adjParity_swap: with parities squaring to 1, (i, j̄) and (j, ī) have the same parity.
• survives_swap, chirality_swap, charge_swap: the swap preserves survival and chirality and negates every additive charge.
• adjoint_vectorLike: every off-diagonal survivor of the adjoint has a distinct partner of the same chirality and opposite charges, for any n, any ℤˣ parities and any (η, η').
• adjoint_survivors_pp, adjoint_survivors_pm: 18 and 24 survivors on the paper's data; adjoint_unpaired_pp, adjoint_unpaired_pm: none unpaired (derived from adjoint_vectorLike).
• sym2_survivors, sym2_unpaired, sym3_survivors, sym3_unpaired: the controls, 16 survivors with 10 unpaired, and 44 survivors with 34 unpaired.

References

• C. Marín, Proton Decay in SU(7) Grand Gauge-Higgs Unification: An Obstruction, Its Minimal Escapes, and the One Row of Their Table 1 That Can Pay for Them (Part VI), Zenodo, doi:10.5281/zenodo.22033303, Proposition (a real representation under diagonal ±1 parities furnishes no chiral generation).
• Y. Komori, N. Maru, SU(7) grand gauge-Higgs unification, arXiv:2503.04090, eqs. (37)–(41).

def GaugeHiggsUnification.SU7RealPairing.adjParity {G : Type u_1} [CommGroup G] {n : ℕ} (p : Fin n → G) (i j : Fin n) : G

The parity of the component (i, j̄) of n ⊗ n̄: the conjugate index carries the inverse.

Equations

• GaugeHiggsUnification.SU7RealPairing.adjParity p i j = p i * (p j)⁻¹

theorem GaugeHiggsUnification.SU7RealPairing.adjParity_swap {G : Type u_1} [CommGroup G] {n : ℕ} (p : Fin n → G) (hp : ∀ (i : Fin n), p i * p i = 1) (i j : Fin n) : adjParity p j i = adjParity p i j

With parities squaring to 1, the conjugate component (j, ī) has the parity of (i, j̄).

def GaugeHiggsUnification.SU7RealPairing.Survives {n : ℕ} (p5 p5' : Fin n → ℤˣ) (η η' : ℤˣ) (i j : Fin n) : Prop

The component (i, j̄) survives in the multiplet of parities (η, η') iff P₅ P₅' = η η'.

Equations

• GaugeHiggsUnification.SU7RealPairing.Survives p5 p5' η η' i j = (GaugeHiggsUnification.SU7RealPairing.adjParity p5 i j * GaugeHiggsUnification.SU7RealPairing.adjParity p5' i j = η * η')

def GaugeHiggsUnification.SU7RealPairing.chirality {n : ℕ} (p5 : Fin n → ℤˣ) (η : ℤˣ) (i j : Fin n) : ℤˣ

The 4D chirality −η P₅ of the component (i, j̄).

Equations

• GaugeHiggsUnification.SU7RealPairing.chirality p5 η i j = -(η * GaugeHiggsUnification.SU7RealPairing.adjParity p5 i j)

def GaugeHiggsUnification.SU7RealPairing.charge {n : ℕ} {A : Type u_1} [AddCommGroup A] (Q : Fin n → A) (i j : Fin n) : A

The additive charge Q i − Q j of the component (i, j̄).

Equations

• GaugeHiggsUnification.SU7RealPairing.charge Q i j = Q i - Q j

theorem GaugeHiggsUnification.SU7RealPairing.survives_swap {n : ℕ} (p5 p5' : Fin n → ℤˣ) (η η' : ℤˣ) (i j : Fin n) : Survives p5 p5' η η' j i ↔ Survives p5 p5' η η' i j

theorem GaugeHiggsUnification.SU7RealPairing.chirality_swap {n : ℕ} (p5 : Fin n → ℤˣ) (η : ℤˣ) (i j : Fin n) : chirality p5 η j i = chirality p5 η i j

theorem GaugeHiggsUnification.SU7RealPairing.charge_swap {n : ℕ} {A : Type u_1} [AddCommGroup A] (Q : Fin n → A) (i j : Fin n) : charge Q j i = -charge Q i j

theorem GaugeHiggsUnification.SU7RealPairing.adjoint_vectorLike {n : ℕ} {A : Type u_1} {B : Type u_2} [AddCommGroup A] [AddCommGroup B] (p5 p5' : Fin n → ℤˣ) (η η' : ℤˣ) (Y : Fin n → A) (E : Fin n → B) (i j : Fin n) (hij : i ≠ j) (hs : Survives p5 p5' η η' i j) : (j, i) ≠ (i, j) ∧ Survives p5 p5' η η' j i ∧ chirality p5 η j i = chirality p5 η i j ∧ charge Y j i = -charge Y i j ∧ charge E j i = -charge E i j

The adjoint is vector-like. Every off-diagonal survivor (i, j̄) has a distinct partner (j, ī) that survives, with the same chirality and opposite values of any two additive charges.

The paper's data

def GaugeHiggsUnification.SU7RealPairing.P5 : Fin 7 → ℤˣ

P₅ = diag(+,+,+,+,+,−,−).

Equations

• GaugeHiggsUnification.SU7RealPairing.P5 = ![1, 1, 1, 1, 1, -1, -1]

def GaugeHiggsUnification.SU7RealPairing.P5' : Fin 7 → ℤˣ

P₅' = diag(+,+,+,−,−,−,+).

Equations

• GaugeHiggsUnification.SU7RealPairing.P5' = ![1, 1, 1, -1, -1, -1, 1]

def GaugeHiggsUnification.SU7RealPairing.Y2 : Fin 7 → ℤ

Twice the hypercharge per index: Y = (0,0,0,½,½,−1,0).

Equations

• GaugeHiggsUnification.SU7RealPairing.Y2 = ![0, 0, 0, 1, 1, -2, 0]

def GaugeHiggsUnification.SU7RealPairing.E2 : Fin 7 → ℤ

Twice the extra U(1) charge per index: extra = (0,0,0,0,0,½,−½).

Equations

• GaugeHiggsUnification.SU7RealPairing.E2 = ![0, 0, 0, 0, 0, 1, -1]

structure GaugeHiggsUnification.SU7RealPairing.QN : Type

The quantum numbers of a component: P₅, P₅', 2Y, 2·extra.

• p5 : ℤˣ

  The parity P₅.

• p5' : ℤˣ

  The parity P₅'.

• y : ℤ

  Twice the hypercharge.

• e : ℤ

  Twice the extra charge.

def GaugeHiggsUnification.SU7RealPairing.survivors {α : Type u_1} (comps : Finset α) (qn : α → QN) (η η' : ℤˣ) : Finset α

Survivors of a list of components in the multiplet of parities (η, η').

Equations

• GaugeHiggsUnification.SU7RealPairing.survivors comps qn η η' = {c ∈ comps | (qn c).p5 * (qn c).p5' = η * η'}

def GaugeHiggsUnification.SU7RealPairing.Paired {α : Type u_1} (S : Finset α) (qn : α → QN) (η : ℤˣ) (c : α) : Prop

A survivor is paired if another survivor has the same chirality and opposite (Y, extra).

Equations

• GaugeHiggsUnification.SU7RealPairing.Paired S qn η c = ∃ d ∈ S, d ≠ c ∧ -(η * (qn d).p5) = -(η * (qn c).p5) ∧ (qn d).y = -(qn c).y ∧ (qn d).e = -(qn c).e

@[instance_reducible]

instance GaugeHiggsUnification.SU7RealPairing.instDecidablePredPairedOfDecidableEq {α : Type u_1} [DecidableEq α] (S : Finset α) (qn : α → QN) (η : ℤˣ) : DecidablePred (Paired S qn η)

Equations

• GaugeHiggsUnification.SU7RealPairing.instDecidablePredPairedOfDecidableEq S qn η x✝ = id inferInstance

def GaugeHiggsUnification.SU7RealPairing.unpaired {α : Type u_1} [DecidableEq α] (comps : Finset α) (qn : α → QN) (η η' : ℤˣ) : ℕ

The number of unpaired (chiral) survivors.

Equations

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

def GaugeHiggsUnification.SU7RealPairing.adjComps : Finset (Fin 7 × Fin 7)

The off-diagonal components (i, j̄), i ≠ j, of the adjoint (the Cartan left aside).

Equations

• GaugeHiggsUnification.SU7RealPairing.adjComps = {c : Fin 7 × Fin 7 | c.1 ≠ c.2}

def GaugeHiggsUnification.SU7RealPairing.qnAdj (c : Fin 7 × Fin 7) : QN

Quantum numbers of (i, j̄).

Equations

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

def GaugeHiggsUnification.SU7RealPairing.sym2Comps : Finset (Fin 7 × Fin 7)

The components i ≤ j of Sym² 7.

Equations

• GaugeHiggsUnification.SU7RealPairing.sym2Comps = {c : Fin 7 × Fin 7 | c.1 ≤ c.2}

def GaugeHiggsUnification.SU7RealPairing.qnSym2 (c : Fin 7 × Fin 7) : QN

Quantum numbers of a component of Sym² 7.

Equations

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

def GaugeHiggsUnification.SU7RealPairing.sym3Comps : Finset (Fin 7 × Fin 7 × Fin 7)

The components i ≤ j ≤ k of Sym³ 7.

Equations

• GaugeHiggsUnification.SU7RealPairing.sym3Comps = {c : Fin 7 × Fin 7 × Fin 7 | c.1 ≤ c.2.1 ∧ c.2.1 ≤ c.2.2}

def GaugeHiggsUnification.SU7RealPairing.qnSym3 (c : Fin 7 × Fin 7 × Fin 7) : QN

Quantum numbers of a component of Sym³ 7.

Equations

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

theorem GaugeHiggsUnification.SU7RealPairing.adjComps_card : adjComps.card = 42

theorem GaugeHiggsUnification.SU7RealPairing.sym2Comps_card : sym2Comps.card = 28

theorem GaugeHiggsUnification.SU7RealPairing.sym3Comps_card : sym3Comps.card = 84

theorem GaugeHiggsUnification.SU7RealPairing.adjoint_survivors_pp : (survivors adjComps qnAdj 1 1).card = 18

theorem GaugeHiggsUnification.SU7RealPairing.adjoint_survivors_pm : (survivors adjComps qnAdj 1 (-1)).card = 24

theorem GaugeHiggsUnification.SU7RealPairing.adjoint_unpaired_eq_zero (η η' : ℤˣ) : unpaired adjComps qnAdj η η' = 0

On the paper's data, no off-diagonal survivor of the adjoint is unpaired, at any (η, η'); derived from adjoint_vectorLike, not by enumeration.

theorem GaugeHiggsUnification.SU7RealPairing.adjoint_unpaired_pp : unpaired adjComps qnAdj 1 1 = 0

theorem GaugeHiggsUnification.SU7RealPairing.adjoint_unpaired_pm : unpaired adjComps qnAdj 1 (-1) = 0

theorem GaugeHiggsUnification.SU7RealPairing.sym2_survivors : (survivors sym2Comps qnSym2 1 1).card = 16

Control: Sym² 7 at (+,+) has 16 survivors.

theorem GaugeHiggsUnification.SU7RealPairing.sym2_unpaired : unpaired sym2Comps qnSym2 1 1 = 10

Control: Sym² 7 at (+,+) leaves 10 unpaired (chiral) states.

theorem GaugeHiggsUnification.SU7RealPairing.sym3_survivors : (survivors sym3Comps qnSym3 1 1).card = 44

Control: Sym³ 7 at (+,+) has 44 survivors.

theorem GaugeHiggsUnification.SU7RealPairing.sym3_unpaired : unpaired sym3Comps qnSym3 1 1 = 34

Control: Sym³ 7 at (+,+) leaves 34 unpaired (chiral) states.