Integrality of the `U(2)` anomaly quadratic form #

Integer arithmetic for the U(2) example of Monnier–Moore–Park on the quantization of anomaly coefficients in six-dimensional 𝒩 = (1, 0) supergravity (§3, equations (3.32)–(3.34)). On the cocharacters (m, n) of U(2) the relevant quadratic form is (2 b₀ (m − n)² + b₁ (m + n)²) / 8. The translation from Lie theory to this quadratic numerator is an input; nothing is stated about a complete supergravity spectrum.

Main results #

joint_criterion: the form is integer-valued iff 2 b₀ + b₁ ≡ 0 (mod 8).
separate_sufficient: 4 ∣ b₀ and 8 ∣ b₁ together are sufficient.
positive_joint, positive_not_separate, joint_does_not_imply_separate: (b₀, b₁) = (1, 6) is integer-valued, with (1 / 8)(2 (m − n)² + 6 (m + n)²) = m² + mn + n², but 4 ∤ b₀; so the separate conditions are not necessary.
rational_joint_criterion, two_samples_suffice: with rational coefficients b₀ = p/t, b₁ = q/t, integrality is decided by the two samples (1, 0) and (1, 1).

References #

S. Monnier, G. W. Moore, D. S. Park, Quantization of anomaly coefficients in 6D 𝒩 = (1, 0) supergravity, JHEP 02 (2018) 020, arXiv:1711.04777, §3.

source

def AnomalyQuantization.U2Example.numerator (b0 b1 m n : ℤ) :

ℤ

The numerator 2 b₀ (m − n)² + b₁ (m + n)².

Equations

AnomalyQuantization.U2Example.numerator b0 b1 m n = 2 * b0 * (m - n) ^ 2 + b1 * (m + n) ^ 2

Instances For

source

def AnomalyQuantization.U2Example.jointIntegral (b0 b1 : ℤ) :

Prop

The quadratic form is integer-valued.

Equations

AnomalyQuantization.U2Example.jointIntegral b0 b1 = ∀ (m n : ℤ), ∃ (k : ℤ ), AnomalyQuantization.U2Example.numerator b0 b1 m n = 8 * k

Instances For

source

def AnomalyQuantization.U2Example.separateIntegral (b0 b1 : ℤ) :

Prop

The separate conditions 4 ∣ b₀, 8 ∣ b₁.

Equations

AnomalyQuantization.U2Example.separateIntegral b0 b1 = ((∃ (k : ℤ ), b0 = 4 * k) ∧ ∃ (k : ℤ ), b1 = 8 * k)

Instances For

source

theorem AnomalyQuantization.U2Example.positive_identity (m n : ℤ) :

numerator 1 6 m n = 8 * (m * m + m * n + n * n)

For (b₀, b₁) = (1, 6) the form is m² + mn + n².

source

theorem AnomalyQuantization.U2Example.positive_joint :

jointIntegral 1 6

(1, 6) is integer-valued.

source

theorem AnomalyQuantization.U2Example.positive_not_separate :

¬separateIntegral 1 6

(1, 6) does not satisfy the separate conditions.

source

theorem AnomalyQuantization.U2Example.joint_criterion (b0 b1 : ℤ) :

jointIntegral b0 b1 ↔ ∃ (d : ℤ ), 2 * b0 + b1 = 8 * d

The form is integer-valued iff 2 b₀ + b₁ ≡ 0 (mod 8).

source

theorem AnomalyQuantization.U2Example.separate_sufficient (b0 b1 : ℤ) :

separateIntegral b0 b1 → jointIntegral b0 b1

The separate conditions are sufficient.

source

theorem AnomalyQuantization.U2Example.joint_does_not_imply_separate :

¬∀ (b0 b1 : ℤ), jointIntegral b0 b1 → separateIntegral b0 b1

The separate conditions are not necessary.

source

def AnomalyQuantization.U2Example.scaledJoint (p q t : ℤ) :

Prop

Rational coefficients b₀ = p/t, b₁ = q/t with a common denominator t ≠ 0: the form is integer-valued iff numerator p q m n ∈ 8 t ℤ. (Valid also for t = 0, which does not encode rationals.)

Equations