The census of boundary-condition classes with a reflection-coset sector

Haba, Hosotani and Kawamura classify the boundary conditions of SU(N) gauge theory on S¹/ℤ₂ by the block sizes [p; q, r; s] of two commuting parity matrices P₀, P₁: p basis vectors with (P₀, P₁) = (+, +), q with (+, −), r with (−, +), s with (−, −), and p + q + r + s = N. Boundary conditions related by a gauge transformation that shifts the Wilson line are equivalent, and the equivalence is generated by the move [p; q, r; s] ~ [p−1; q+1, r+1; s−1]. The winding element U = P₀ P₁ has det U = (−1)^{q+r}, so the theory has a reflection-coset sector (where the boundary sign can act) exactly when q + r is odd. This file counts the classes that have one, for every N.

Main results

• label_move, rank_move, label_eqv, rank_eqv: the label (p+q, q+s) and N are invariant.
• eqv_of_label: two boundary conditions with the same N and the same label are joined by a chain of moves, so the label is a complete invariant; with witness_label the classes are the pairs (u, v) with u, v ≤ N, and card_classes recovers the count (N+1)².
• coset_parity: q + r and u + v + N have the same parity, so having a coset sector is a property of the class.
• card_cosetClasses: exactly ⌊(N+1)²/2⌋ of the (N+1)² classes have a coset sector.

References

• N. Haba, Y. Hosotani, Y. Kawamura, Classification and dynamics of equivalence classes in SU(N) gauge theory on the orbifold S¹/Z₂, arXiv:hep-ph/0309088.
• C. Marín, What the Higgs Potential Cannot See: Bulk Matter That Cannot Help Select a Boundary Condition (Part V), Zenodo, doi:10.5281/zenodo.21727094.

Boundary conditions, the move, and the label

structure GaugeHiggsUnification.CosetCensus.BC : Type

A boundary condition in HHK's block form [p; q, r; s].

• p : ℕ
• q : ℕ
• r : ℕ
• s : ℕ

@[instance_reducible]

instance GaugeHiggsUnification.CosetCensus.instDecidableEqBC : DecidableEq BC

Equations

• GaugeHiggsUnification.CosetCensus.instDecidableEqBC = GaugeHiggsUnification.CosetCensus.instDecidableEqBC.decEq

def GaugeHiggsUnification.CosetCensus.instDecidableEqBC.decEq (x✝ x✝¹ : BC) : Decidable (x✝ = x✝¹)

Equations

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

def GaugeHiggsUnification.CosetCensus.instReprBC.repr : BC → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GaugeHiggsUnification.CosetCensus.instReprBC : Repr BC

Equations

• GaugeHiggsUnification.CosetCensus.instReprBC = { reprPrec := GaugeHiggsUnification.CosetCensus.instReprBC.repr }

def GaugeHiggsUnification.CosetCensus.rank (x : BC) : ℕ

N: the rank of the gauge group, p + q + r + s.

Equations

• GaugeHiggsUnification.CosetCensus.rank x = x.p + x.q + x.r + x.s

def GaugeHiggsUnification.CosetCensus.label (x : BC) : ℕ × ℕ

The label (p+q, q+s) = (#(P₀ = +1), #(P₁ = -1)).

Equations

• GaugeHiggsUnification.CosetCensus.label x = (x.p + x.q, x.q + x.s)

def GaugeHiggsUnification.CosetCensus.hasCoset (x : BC) : Prop

Whether the class has a reflection-coset sector: det U = (-1)^(q+r) = -1.

Equations

• GaugeHiggsUnification.CosetCensus.hasCoset x = ((x.q + x.r) % 2 = 1)

@[instance_reducible]

instance GaugeHiggsUnification.CosetCensus.instDecidableHasCoset (x : BC) : Decidable (hasCoset x)

Equations

• GaugeHiggsUnification.CosetCensus.instDecidableHasCoset x = id inferInstance

inductive GaugeHiggsUnification.CosetCensus.Move : BC → BC → Prop

One class move, [p; q, r; s] → [p-1; q+1, r+1; s-1], stated without subtraction.

• intro (p q r s : ℕ) : Move { p := p + 1, q := q, r := r, s := s + 1 } { p := p, q := q + 1, r := r + 1, s := s }

def GaugeHiggsUnification.CosetCensus.Equivalent : BC → BC → Prop

Boundary conditions in the same equivalence class.

Equations

• GaugeHiggsUnification.CosetCensus.Equivalent = Relation.EqvGen GaugeHiggsUnification.CosetCensus.Move

theorem GaugeHiggsUnification.CosetCensus.rank_move {x y : BC} (h : Move x y) : rank x = rank y

theorem GaugeHiggsUnification.CosetCensus.label_move {x y : BC} (h : Move x y) : label x = label y

theorem GaugeHiggsUnification.CosetCensus.rank_eqv {x y : BC} (h : Equivalent x y) : rank x = rank y

theorem GaugeHiggsUnification.CosetCensus.label_eqv {x y : BC} (h : Equivalent x y) : label x = label y

The label is a complete invariant

The direction with content. If x and y have the same N and the same label, walk x towards y one move at a time. The step is legal because the label forces the room for it: if x.q < y.q then x.p = y.p + (y.q - x.q) ≥ 1 and x.s = y.s + (y.q - x.q) ≥ 1.

theorem GaugeHiggsUnification.CosetCensus.eqv_of_label {x y : BC} (hr : rank x = rank y) (hl : label x = label y) : Equivalent x y

The label is complete. Same N, same label ⟹ joined by moves.

theorem GaugeHiggsUnification.CosetCensus.label_le (x : BC) : (label x).1 ≤ rank x ∧ (label x).2 ≤ rank x

The label of a rank-N boundary condition lies in the (N+1) × (N+1) grid.

def GaugeHiggsUnification.CosetCensus.witness (N u v : ℕ) : BC

... and every point of the grid is a label: the explicit representative.

Equations

• GaugeHiggsUnification.CosetCensus.witness N u v = if u + v ≤ N then { p := u, q := 0, r := N - u - v, s := v } else { p := N - v, q := u + v - N, r := 0, s := N - u }

theorem GaugeHiggsUnification.CosetCensus.witness_rank {N u v : ℕ} (hu : u ≤ N) (hv : v ≤ N) : rank (witness N u v) = N

theorem GaugeHiggsUnification.CosetCensus.witness_label {N u v : ℕ} (hu : u ≤ N) (hv : v ≤ N) : label (witness N u v) = (u, v)

theorem GaugeHiggsUnification.CosetCensus.coset_parity (x : BC) : (x.q + x.r) % 2 = ((label x).1 + (label x).2 + rank x) % 2

hasCoset is a class function. q + r is not invariant under the move, but its parity is, and the parity is read off the label and N.

theorem GaugeHiggsUnification.CosetCensus.hasCoset_iff (x : BC) : hasCoset x ↔ ((label x).1 + (label x).2 + rank x) % 2 = 1

Counting the classes

def GaugeHiggsUnification.CosetCensus.classes (N : ℕ) : Finset (ℕ × ℕ)

The classes of rank N, as their labels: the (N+1) × (N+1) grid.

Equations

• GaugeHiggsUnification.CosetCensus.classes N = Finset.range (N + 1) ×ˢ Finset.range (N + 1)

def GaugeHiggsUnification.CosetCensus.cosetClasses (N : ℕ) : Finset (ℕ × ℕ)

The classes that admit a reflection-coset sector.

Equations

• GaugeHiggsUnification.CosetCensus.cosetClasses N = {c ∈ GaugeHiggsUnification.CosetCensus.classes N | (c.1 + c.2 + N) % 2 = 1}

theorem GaugeHiggsUnification.CosetCensus.card_classes (N : ℕ) : (classes N).card = (N + 1) ^ 2

HHK's count, recovered from the label.

theorem GaugeHiggsUnification.CosetCensus.label_mem_classes {x : BC} {N : ℕ} (h : rank x = N) : label x ∈ classes N

Every rank-N boundary condition has its label in the grid ...

theorem GaugeHiggsUnification.CosetCensus.exists_of_mem_classes {N : ℕ} {c : ℕ × ℕ} (h : c ∈ classes N) : ∃ (x : BC), rank x = N ∧ label x = c

... and every point of the grid comes from one. With eqv_of_label (same label ⟹ same class) this is the bijection: classes of rank N ↔ classes N.

theorem GaugeHiggsUnification.CosetCensus.card_mod_range (N j : ℕ) (hj : j < 2) : {v ∈ Finset.range (N + 1) | v % 2 = j}.card = (N + 2 - j) / 2

How many numbers below N+1 have a given residue mod 2.

theorem GaugeHiggsUnification.CosetCensus.card_mod_range_not (N j : ℕ) (hj : j < 2) : {v ∈ Finset.range (N + 1) | ¬v % 2 = j}.card = N + 1 - (N + 2 - j) / 2

... and the complementary count.

theorem GaugeHiggsUnification.CosetCensus.cosetClasses_eq (N : ℕ) : cosetClasses N = {c ∈ classes N | (c.1 % 2 = 0) = (c.2 % 2 = (N + 1) % 2)}

The census in the form filter_product_card wants it.

theorem GaugeHiggsUnification.CosetCensus.card_cosetClasses (N : ℕ) : (cosetClasses N).card = (N + 1) ^ 2 / 2

Proposition (Part V), the geometric half of the dichotomy. Of the (N+1)^2 equivalence classes of boundary conditions, exactly ⌊(N+1)^2/2⌋ admit a reflection-coset sector -- and in the other ⌈(N+1)^2/2⌉ the boundary sign is invisible to every multiplet, for reasons that have nothing to do with matter.

Sanity checks against the table for N = 2, …, 10

The first two are the control that matters: they do not touch the theorems above. They enumerate the actual [p;q,r;s] tuples of rank 3, take their labels, and compare with the grid -- so if witness or label_le were wrong, or the label missed part of the grid, these would fail and the census would still "prove".

def GaugeHiggsUnification.CosetCensus.BCs (N : ℕ) : Finset BC

All boundary conditions of rank N, by brute force.

Equations

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

And the controls are not vacuous. A label that looks equally natural -- (p+q, q+r), the two "off-diagonal" sums -- is not invariant under the move, so label_move is a real constraint and not bookkeeping: