Integrality of periods on spin four-manifolds

Arithmetic certificates for the quantization of couplings p A + q B + r C whose three periods A, B, C run over ℤ on a general four-manifold, while on a spin four-manifold the intersection form is even, so that the third period runs over 2ℤ. The geometric realization of the period triples and the evenness of the intersection pairing are inputs, not formalized. t is a common denominator in applications (nonzero); the statements remain valid as divisibility statements at t = 0.

Main results

• universal_basis, spin_basis: the periods lie in t ℤ iff t ∣ p, q, r, respectively t ∣ p, q, 2r.
• universal_implies_spin, half_square_spin, half_square_not_universal: the spin condition is strictly weaker.
• q6_congruence, q6_implies_six: for the q = 6 row of Table 1 of Choi–Forslund–Lam–Shao (with A = c₂(E₂), B = c₂(E₃), C = c₁(E₃)² and mathematical sign conventions for Chern classes) the spin condition is 18 K₂ + 24 K₃ + K₁ ≡ 0 (mod 36), and it forces 6 ∣ K₁.

References

• Y. Choi, M. Forslund, H. T. Lam, S.-H. Shao, Quantization of axion-gauge couplings and non-invertible higher symmetries, Phys. Rev. Lett. 132 (2024) 121601, arXiv:2309.03937, Table 1.

def AxionCouplings.SpinPeriod.universalPeriods (p q r t : ℤ) : Prop

p a + q b + r c ∈ t ℤ for all integer periods.

Equations

• AxionCouplings.SpinPeriod.universalPeriods p q r t = ∀ (a b c : ℤ), ∃ (k : ℤ), p * a + q * b + r * c = t * k

def AxionCouplings.SpinPeriod.spinPeriods (p q r t : ℤ) : Prop

p a + q b + 2 r c ∈ t ℤ for all integer periods (even third period).

Equations

• AxionCouplings.SpinPeriod.spinPeriods p q r t = ∀ (a b c : ℤ), ∃ (k : ℤ), p * a + q * b + 2 * r * c = t * k

theorem AxionCouplings.SpinPeriod.universal_basis (p q r t : ℤ) : universalPeriods p q r t ↔ ∃ (x : ℤ), ∃ (y : ℤ), ∃ (z : ℤ), p = t * x ∧ q = t * y ∧ r = t * z

The integral basis criterion on a general four-manifold.

theorem AxionCouplings.SpinPeriod.spin_basis (p q r t : ℤ) : spinPeriods p q r t ↔ ∃ (x : ℤ), ∃ (y : ℤ), ∃ (z : ℤ), p = t * x ∧ q = t * y ∧ 2 * r = t * z

The integral basis criterion on a spin four-manifold.

theorem AxionCouplings.SpinPeriod.universal_implies_spin (p q r t : ℤ) (h : universalPeriods p q r t) : spinPeriods p q r t

The general condition implies the spin condition.

theorem AxionCouplings.SpinPeriod.half_square_spin : spinPeriods 0 0 1 2

Half of the square satisfies the spin condition.

theorem AxionCouplings.SpinPeriod.half_square_not_universal : ¬universalPeriods 0 0 1 2

Half of the square does not satisfy the general condition.

theorem AxionCouplings.SpinPeriod.q6_congruence (K2 K3 K1 : ℤ) : spinPeriods (-72 * K2) (-72 * K3) (18 * K2 + 24 * K3 + K1) 72 ↔ ∃ (k : ℤ), 18 * K2 + 24 * K3 + K1 = 36 * k

The spin condition for the q = 6 row.

theorem AxionCouplings.SpinPeriod.q6_implies_six (K2 K3 K1 k : ℤ) (h : 18 * K2 + 24 * K3 + K1 = 36 * k) : ∃ (j : ℤ), K1 = 6 * j

The q = 6 spin condition forces 6 ∣ K₁.