Weight moments of two 13-dimensional USp(4) contents

Finite weight and coefficient certificates, checked by decide, for two contents of dimension 13 written with the weights of the USp(4) representations 1, 4, 5: the original 5 + 4 + 4 and the alternative 1 + 1 + 1 + 5 + 5. Their weight moments agree up to degree three and first differ in degree four. The USp(4) interpretation of the weight lists is an input, not a formalized classification; no anomaly cancellation or continuum spectrum is stated.

Main results

• same_degree_zero … same_degree_three: the moment polynomials agree in degrees 0–3.
• degree_four_difference: in degree four they differ by (0, 0, 24, 0, 0).
• character_factor_coefficients: the difference of multiplicities factors as z(w₁) z(w₂) with z = (−1, 2, −1) on {−1, 0, 1}.
• fourth_moment_resolves_kernel: dimension, second and fourth moments determine the multiplicities (a, b, c) of (1, 5, 4).
• two_nonnegative_solutions: the only nonnegative contents with dimension 13 and second moment 8 are (0, 1, 2) and (3, 2, 0).

@[reducible, inline]

abbrev GaugeHiggsUnification.USp4WeightMoments.Weight : Type

A weight of rank two.

Equations

• GaugeHiggsUnification.USp4WeightMoments.Weight = (ℤ × ℤ)

def GaugeHiggsUnification.USp4WeightMoments.one : List Weight

The weights of the trivial representation.

Equations

• GaugeHiggsUnification.USp4WeightMoments.one = [(0, 0)]

def GaugeHiggsUnification.USp4WeightMoments.five : List Weight

The weights of the 5.

Equations

• GaugeHiggsUnification.USp4WeightMoments.five = [(0, 0), (1, 1), (1, -1), (-1, 1), (-1, -1)]

def GaugeHiggsUnification.USp4WeightMoments.four : List Weight

The weights of the 4.

Equations

• GaugeHiggsUnification.USp4WeightMoments.four = [(1, 0), (-1, 0), (0, 1), (0, -1)]

def GaugeHiggsUnification.USp4WeightMoments.original : List Weight

The original content 5 + 4 + 4.

Equations

• GaugeHiggsUnification.USp4WeightMoments.original = GaugeHiggsUnification.USp4WeightMoments.five ++ GaugeHiggsUnification.USp4WeightMoments.four ++ GaugeHiggsUnification.USp4WeightMoments.four

def GaugeHiggsUnification.USp4WeightMoments.alternative : List Weight

The alternative content 1 + 1 + 1 + 5 + 5.

Equations

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

def GaugeHiggsUnification.USp4WeightMoments.mixed (ws : List Weight) (p q : ℕ) : ℤ

The mixed moment Σ w₁^p w₂^q.

Equations

• GaugeHiggsUnification.USp4WeightMoments.mixed ws p q = List.foldl (fun (x1 x2 : ℤ) => x1 + x2) 0 (List.map (fun (w : GaugeHiggsUnification.USp4WeightMoments.Weight) => w.1 ^ p * w.2 ^ q) ws)

def GaugeHiggsUnification.USp4WeightMoments.binomial : ℕ → ℕ → ℕ

Binomial coefficients by Pascal's recursion.

Equations

• GaugeHiggsUnification.USp4WeightMoments.binomial 0 0 = 1
• GaugeHiggsUnification.USp4WeightMoments.binomial 0 n.succ = 0
• GaugeHiggsUnification.USp4WeightMoments.binomial n.succ 0 = 1
• GaugeHiggsUnification.USp4WeightMoments.binomial n.succ k.succ = GaugeHiggsUnification.USp4WeightMoments.binomial n k + GaugeHiggsUnification.USp4WeightMoments.binomial n (k + 1)

def GaugeHiggsUnification.USp4WeightMoments.coefficients (ws : List Weight) (degree : ℕ) : List ℤ

The coefficients of the moment polynomial Σ (x w₁ + y w₂)^degree.

Equations

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

def GaugeHiggsUnification.USp4WeightMoments.multiplicity (ws : List Weight) (w : Weight) : ℤ

The multiplicity of a weight in a list.

Equations

• GaugeHiggsUnification.USp4WeightMoments.multiplicity ws w = ↑(List.filter (fun (x : GaugeHiggsUnification.USp4WeightMoments.Weight) => x == w) ws).length

def GaugeHiggsUnification.USp4WeightMoments.delta (w : Weight) : ℤ

The difference of multiplicities, alternative minus original.

Equations

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

def GaugeHiggsUnification.USp4WeightMoments.zcoeff (n : ℤ) : ℤ

The one-variable factor (−1, 2, −1) on {−1, 0, 1}.

Equations

• GaugeHiggsUnification.USp4WeightMoments.zcoeff n = if (n == 0) = true then 2 else if (n == 1 || n == -1) = true then -1 else 0

def GaugeHiggsUnification.USp4WeightMoments.grid : List Weight

The grid {−1, 0, 1}².

Equations

• GaugeHiggsUnification.USp4WeightMoments.grid = List.flatMap (fun (x : ℤ) => List.map (fun (y : ℤ) => (x, y)) [-1, 0, 1]) [-1, 0, 1]

theorem GaugeHiggsUnification.USp4WeightMoments.dimensions : original.length = 13 ∧ alternative.length = 13

Both contents have dimension 13.

theorem GaugeHiggsUnification.USp4WeightMoments.same_degree_zero : coefficients original 0 = coefficients alternative 0

Equal moments in degree 0.

theorem GaugeHiggsUnification.USp4WeightMoments.same_degree_one : coefficients original 1 = coefficients alternative 1

Equal moments in degree 1.

theorem GaugeHiggsUnification.USp4WeightMoments.same_degree_two : coefficients original 2 = coefficients alternative 2

Equal moments in degree 2.

theorem GaugeHiggsUnification.USp4WeightMoments.same_degree_three : coefficients original 3 = coefficients alternative 3

Equal moments in degree 3.

theorem GaugeHiggsUnification.USp4WeightMoments.degree_four_difference : List.map (fun (i : ℕ) => (coefficients alternative 4)[i]! - (coefficients original 4)[i]!) (List.range 5) = [0, 0, 24, 0, 0]

In degree 4 the moments differ by (0, 0, 24, 0, 0).

theorem GaugeHiggsUnification.USp4WeightMoments.character_factor_coefficients : List.map delta grid = List.map (fun (w : Weight) => zcoeff w.1 * zcoeff w.2) grid

The difference of multiplicities factors on the grid.

theorem GaugeHiggsUnification.USp4WeightMoments.character_support : ((original ++ alternative).all fun (w : Weight) => grid.contains w) = true

All weights of both contents lie on the grid.

theorem GaugeHiggsUnification.USp4WeightMoments.representations_differ : delta (1, 1) = 1

The two contents are different.

theorem GaugeHiggsUnification.USp4WeightMoments.observation_kernel (a b c : ℤ) (h0 : a + 5 * b + 4 * c = 0) (h2 : 4 * b + 2 * c = 0) : a = 3 * b ∧ c = -2 * b

The common kernel of dimension and second moment.

theorem GaugeHiggsUnification.USp4WeightMoments.fourth_moment_resolves_kernel (a b c : ℤ) (h0 : a + 5 * b + 4 * c = 0) (h2 : 4 * b + 2 * c = 0) (h4 : 24 * b = 0) : a = 0 ∧ b = 0 ∧ c = 0

Adding the fourth moment, the kernel is trivial.

theorem GaugeHiggsUnification.USp4WeightMoments.augmented_determinant : 1 * (4 * 0 - 2 * 24) = -48

The augmented determinant.

theorem GaugeHiggsUnification.USp4WeightMoments.two_nonnegative_solutions (a b c : ℤ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (h0 : a + 5 * b + 4 * c = 13) (h2 : 4 * b + 2 * c = 8) : a = 0 ∧ b = 1 ∧ c = 2 ∨ a = 3 ∧ b = 2 ∧ c = 0

The two nonnegative solutions with dimension 13 and second moment 8.

theorem GaugeHiggsUnification.USp4WeightMoments.alternative_pairing_capacity : min 2 0 = 0 ∧ min 1 2 = 1 ∧ min 3 3 = 3

The pairing capacities of the alternative content.