The even-m notch of an SU(4) irrep and the ℤ₄ centre charge

For Dynkin labels (a, b, c) put λ = (a+b+c, b+c, c, 0) and let D(t) = s_λ(1, −1, t, t⁻¹) be the signed generating function of the orbifold histogram of the SU(4) irrep; the notch holds iff D is an odd Laurent polynomial. Writing D = N / V as a bialternant with the ordered alphabet y = (1, −1, T, T⁻¹) and exponents μ = (a+b+c+3, b+c+2, c+1, 0), everything is controlled by the 4 × 4 determinant N = det (y i ^ μ j) over ℤ[T;T⁻¹].

The non-vanishing half of notch_degenerate_iff extracts the single Laurent coefficient at the strictly largest bracket argument (co): a finite replacement for the linear independence of the brackets [x] = T^x − T^{−x}, x > 0.

Main results

• notch_degenerate_iff: N a b c = 0 ↔ Odd b ∧ ((Odd a ∧ Odd c) ∨ a = c), by Laplace expansion along the two constant rows (det_four_first_row_one), reduction of every complementary 2 × 2 minor to a bracket (brmul) and an eight-way parity split.
• V_ne_zero: the Vandermonde denominator V = N 0 0 0 is non-zero.
• N_neg_alphabet, Ntilde_eq, notch_parity: the bialternant form of s_λ(−x) = (−1)^{|λ|} s_λ(x), and D(−t) = (−1)^{|λ|} D(t) cross-multiplied.
• degenerate_centre_charge_even, degenerate_disjoint_admissible: every degenerate (a, b, c) has even centre charge a + 2b + 3c, so it is disjoint from the set where the centre charge is odd.

Related

Mathlib has Laurent polynomials and determinants but, at the pinned commit, no Schur polynomials or bialternants.

References

• C. Marín, A Centre-Charge Selection Rule for the Wilson-Line Potential: The Fundamental Domain of Gauge-Higgs Unification Is Representation-Dependent (Part III), Zenodo, doi:10.5281/zenodo.21438226.

@[reducible, inline]

abbrev GaugeHiggsUnification.NotchCentreCharge.L : Type

Laurent polynomials with integer coefficients, ℤ[T;T⁻¹].

Equations

• GaugeHiggsUnification.NotchCentreCharge.L = LaurentPolynomial ℤ

Coefficient extraction

def GaugeHiggsUnification.NotchCentreCharge.co (f : L) (k : ℤ) : ℤ

The coefficient of T ^ k in a Laurent polynomial.

Equations

• GaugeHiggsUnification.NotchCentreCharge.co f k = f.coeff k

@[simp]

theorem GaugeHiggsUnification.NotchCentreCharge.co_zero (k : ℤ) : co 0 k = 0

@[simp]

theorem GaugeHiggsUnification.NotchCentreCharge.co_add (f g : L) (k : ℤ) : co (f + g) k = co f k + co g k

@[simp]

theorem GaugeHiggsUnification.NotchCentreCharge.co_sub (f g : L) (k : ℤ) : co (f - g) k = co f k - co g k

@[simp]

theorem GaugeHiggsUnification.NotchCentreCharge.co_neg (f : L) (k : ℤ) : co (-f) k = -co f k

@[simp]

theorem GaugeHiggsUnification.NotchCentreCharge.co_T (n k : ℤ) : co (LaurentPolynomial.T n) k = if n = k then 1 else 0

theorem GaugeHiggsUnification.NotchCentreCharge.ne_zero_of_co {f : L} {k : ℤ} (h : co f k ≠ 0) : f ≠ 0

The bracket [x] = T^x - T^(-x)

noncomputable def GaugeHiggsUnification.NotchCentreCharge.br (x : ℤ) : L

br x = T^x - T^(-x), the complementary 2x2 minor on the rows (T, T⁻¹).

Equations

• GaugeHiggsUnification.NotchCentreCharge.br x = LaurentPolynomial.T x - LaurentPolynomial.T (-x)

@[simp]

theorem GaugeHiggsUnification.NotchCentreCharge.co_br (x k : ℤ) : co (br x) k = (if x = k then 1 else 0) - if -x = k then 1 else 0

theorem GaugeHiggsUnification.NotchCentreCharge.brmul (m n : ℤ) : LaurentPolynomial.T m * LaurentPolynomial.T (-n) - LaurentPolynomial.T n * LaurentPolynomial.T (-m) = br (m - n)

Every complementary 2x2 minor of the bottom two rows is a bracket.

Laplace expansion along the first two rows

theorem GaugeHiggsUnification.NotchCentreCharge.det_four_first_row_one {R : Type u_1} [CommRing R] (A : Matrix (Fin 4) (Fin 4) R) (h : ∀ (j : Fin 4), A 0 j = 1) : A.det = (A 1 1 - A 1 0) * (A 2 2 * A 3 3 - A 2 3 * A 3 2) - (A 1 2 - A 1 0) * (A 2 1 * A 3 3 - A 2 3 * A 3 1) + (A 1 3 - A 1 0) * (A 2 1 * A 3 2 - A 2 2 * A 3 1) + (A 1 2 - A 1 1) * (A 2 0 * A 3 3 - A 2 3 * A 3 0) - (A 1 3 - A 1 1) * (A 2 0 * A 3 2 - A 2 2 * A 3 0) + (A 1 3 - A 1 2) * (A 2 0 * A 3 1 - A 2 1 * A 3 0)

Laplace expansion of a 4x4 determinant along rows 0 and 1, when row 0 is constant equal to 1. Pure ring identity.

The bialternant

noncomputable def GaugeHiggsUnification.NotchCentreCharge.y : Fin 4 → L

The ordered alphabet y = (1, -1, T, T⁻¹).

Equations

• GaugeHiggsUnification.NotchCentreCharge.y = ![1, -1, LaurentPolynomial.T 1, LaurentPolynomial.T (-1)]

def GaugeHiggsUnification.NotchCentreCharge.mu (a b c : ℕ) : Fin 4 → ℕ

The exponents mu = (a+b+c+3, b+c+2, c+1, 0) (strictly decreasing).

Equations

• GaugeHiggsUnification.NotchCentreCharge.mu a b c = ![a + b + c + 3, b + c + 2, c + 1, 0]

noncomputable def GaugeHiggsUnification.NotchCentreCharge.M (a b c : ℕ) : Matrix (Fin 4) (Fin 4) L

The bialternant matrix M i j = y i ^ mu j.

Equations

• GaugeHiggsUnification.NotchCentreCharge.M a b c i j = GaugeHiggsUnification.NotchCentreCharge.y i ^ GaugeHiggsUnification.NotchCentreCharge.mu a b c j

noncomputable def GaugeHiggsUnification.NotchCentreCharge.N (a b c : ℕ) : L

N a b c = det (y i ^ mu j); D = N / V and D = 0 ↔ N = 0.

Equations

• GaugeHiggsUnification.NotchCentreCharge.N a b c = (GaugeHiggsUnification.NotchCentreCharge.M a b c).det

theorem GaugeHiggsUnification.NotchCentreCharge.neg_one_pow_even {n : ℕ} (h : n % 2 = 0) : (-1) ^ n = 1

theorem GaugeHiggsUnification.NotchCentreCharge.neg_one_pow_odd {n : ℕ} (h : n % 2 = 1) : (-1) ^ n = -1

theorem GaugeHiggsUnification.NotchCentreCharge.N_expand (a b c : ℕ) : N a b c = ((-1) ^ (b + c + 2) - (-1) ^ (a + b + c + 3)) * br (↑c + 1) - ((-1) ^ (c + 1) - (-1) ^ (a + b + c + 3)) * br (↑b + ↑c + 2) + (1 - (-1) ^ (a + b + c + 3)) * br (↑b + 1) + ((-1) ^ (c + 1) - (-1) ^ (b + c + 2)) * br (↑a + ↑b + ↑c + 3) - (1 - (-1) ^ (b + c + 2)) * br (↑a + ↑b + 2) + (1 - (-1) ^ (c + 1)) * br (↑a + 1)

Laplace expansion of N, with every minor written as a bracket.

T1: the exact degeneracy condition

theorem GaugeHiggsUnification.NotchCentreCharge.notch_degenerate_iff (a b c : ℕ) : N a b c = 0 ↔ Odd b ∧ (Odd a ∧ Odd c ∨ a = c)

theorem GaugeHiggsUnification.NotchCentreCharge.V_ne_zero : N 0 0 0 ≠ 0

The Vandermonde denominator V = N 0 0 0 is non-zero, so D = N/V is legitimate.

T2: the parity (homogeneity) lemma

theorem GaugeHiggsUnification.NotchCentreCharge.N_neg_alphabet (a b c : ℕ) : (Matrix.of fun (i j : Fin 4) => (-y i) ^ mu a b c j).det = (-1) ^ (a + 2 * b + 3 * c) * N a b c

Negating the whole alphabet scales the bialternant by (-1)^(a+2b+3c).

noncomputable def GaugeHiggsUnification.NotchCentreCharge.ytilde : Fin 4 → L

The alphabet with t replaced by -t.

Equations

• GaugeHiggsUnification.NotchCentreCharge.ytilde = ![1, -1, -LaurentPolynomial.T 1, -LaurentPolynomial.T (-1)]

noncomputable def GaugeHiggsUnification.NotchCentreCharge.Ntilde (a b c : ℕ) : L

Ntilde a b c is N a b c with t replaced by -t.

Equations

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

theorem GaugeHiggsUnification.NotchCentreCharge.Ntilde_eq (a b c : ℕ) : Ntilde a b c = (-1) ^ (a + 2 * b + 3 * c + 1) * N a b c

The finite bialternant form of D(-t) = (-1)^|lambda| D(t): t -> -t scales N by (-1)^(a+2b+3c+1) (the extra sign is the transposition of the two constant letters, and it cancels in the quotient N/V).

theorem GaugeHiggsUnification.NotchCentreCharge.notch_parity (a b c : ℕ) : Ntilde a b c * N 0 0 0 = (-1) ^ (a + 2 * b + 3 * c) * (N a b c * Ntilde 0 0 0)

The parity lemma at the level of D = N/V, cross-multiplied (no division): D(-t) = (-1)^(a+2b+3c) D(t).

T3: the bridge to Gate 1 (the Z4 centre charge)

theorem GaugeHiggsUnification.NotchCentreCharge.degenerate_centre_charge_even (a b c : ℕ) (h : Odd b ∧ (Odd a ∧ Odd c ∨ a = c)) : Even (a + 2 * b + 3 * c)

Every degenerate (a,b,c) has even centre charge a + 2b + 3c.

theorem GaugeHiggsUnification.NotchCentreCharge.degenerate_disjoint_admissible (a b c : ℕ) (hadm : Odd (a + 2 * b + 3 * c)) : N a b c ≠ 0

Hence the degenerate set is disjoint from the SM-admissible set, whose Gate 1 is exactly "a + 2b + 3c odd".

Sanity checks against the Sage verification