Integrality of quadratic forms on the cocharacters of S(U(2) × U(3))

Conditional arithmetic certificates for H = S(U(2) × U(3)). A cocharacter of H is (m, n; u, v, −m − n − u − v), and A = mn, B (the second elementary symmetric function of the U(3) entries) and C = (m + n)² are the three invariant quadratic forms on it. The dictionary between cocharacters and characteristic classes and the Green–Schwarz ansatz are inputs, not formalized.

Main results

• integral_basis_criterion: p A + q B + r C takes values in t ℤ on all cocharacters iff t ∣ p, t ∣ q, t ∣ r.
• quotient_witness, cover_witness, cover_misses_fraction: C takes the value 1, while C / 36 is not integral.
• no_standard_tensor_parent_match, residue_mod_three: the transfer coefficients (16 − 3p, −3q, −3r) never satisfy the parent relation x + y + 2z = 0; their combination is 1 modulo 3.

def GaugeHiggsUnification.ChargeQuantization.A (m n : ℤ) : ℤ

The form A = mn.

Equations

• GaugeHiggsUnification.ChargeQuantization.A m n = m * n

def GaugeHiggsUnification.ChargeQuantization.B (m n u v : ℤ) : ℤ

The form B, the second elementary symmetric function of (u, v, −m − n − u − v).

Equations

• GaugeHiggsUnification.ChargeQuantization.B m n u v = u * v + u * (-m - n - u - v) + v * (-m - n - u - v)

def GaugeHiggsUnification.ChargeQuantization.C (m n : ℤ) : ℤ

The form C = (m + n)².

Equations

• GaugeHiggsUnification.ChargeQuantization.C m n = (m + n) ^ 2

def GaugeHiggsUnification.ChargeQuantization.form (p q r m n u v : ℤ) : ℤ

The combination p A + q B + r C.

Equations

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

def GaugeHiggsUnification.ChargeQuantization.integralOnH (p q r t : ℤ) : Prop

p A + q B + r C takes values in t ℤ on every cocharacter.

Equations

• GaugeHiggsUnification.ChargeQuantization.integralOnH p q r t = ∀ (m n u v : ℤ), ∃ (k : ℤ), GaugeHiggsUnification.ChargeQuantization.form p q r m n u v = t * k

theorem GaugeHiggsUnification.ChargeQuantization.integral_basis_criterion (p q r t : ℤ) : integralOnH p q r t ↔ ∃ (a : ℤ), ∃ (b : ℤ), ∃ (c : ℤ), p = t * a ∧ q = t * b ∧ r = t * c

The integral basis criterion.

theorem GaugeHiggsUnification.ChargeQuantization.quotient_witness : form 0 0 1 1 0 (-1) 0 = 1

C takes the value 1.

theorem GaugeHiggsUnification.ChargeQuantization.cover_witness : form 0 0 1 (-3) (-3) 2 2 = 36

A value 36 of C.

theorem GaugeHiggsUnification.ChargeQuantization.cover_misses_fraction : ¬integralOnH 0 0 1 36

C does not take values in 36 ℤ.

theorem GaugeHiggsUnification.ChargeQuantization.parent_annihilator (s t : ℤ) : -2 * s + -2 * t + 2 * (s + t) = 0

The parent relation x + y + 2z = 0 annihilates (−2s, −2t, s + t).

theorem GaugeHiggsUnification.ChargeQuantization.standard_tensor_obstruction (p q r : ℤ) : 16 - 3 * p + -3 * q + 2 * (-3 * r) ≠ 0

With integer doubled tensor coefficients p, q, r, six times the transfer coefficients are (16 − 3p, −3q, −3r); they never satisfy the parent relation.

theorem GaugeHiggsUnification.ChargeQuantization.no_standard_tensor_parent_match : ¬∃ (p : ℤ), ∃ (q : ℤ), ∃ (r : ℤ), 16 - 3 * p + -3 * q + 2 * (-3 * r) = 0

No integer tensor coefficients match the parent relation.

theorem GaugeHiggsUnification.ChargeQuantization.residue_mod_three (p q r : ℤ) : (16 - 3 * p + -3 * q + 2 * (-3 * r)) % 3 = 1

The obstruction is the residue 1 modulo 3.