The Fourier criterion for tiling ℤ/12

A, B ⊆ ℤ/12 tile when every x is a + b with a ∈ A, b ∈ B in exactly one way. With the discrete convolution theorem 𝓕 (tileCount A B) k = Ahat A k * Ahat B k, proved here from the character sums, tiling is equivalent to #A * #B = 12 together with Ahat A k = 0 ∨ Ahat B k = 0 for every k ≠ 0.

Main results

• dft_tileCount, dft_const_one.
• tiles_iff_dft_product, tiles_iff_dft.
• chromatic_aug_tiles, chromatic_badtriad_not_tiles: examples.

References

• E. Amiot, Music Through Fourier Space, Springer (2016).
• E. M. Coven, A. Meyerowitz, Tiling the integers with translates of one finite set, J. Algebra 212 (1999).

def MusicTheory.Tiling.tileCount (A B : Finset (ZMod 12)) (x : ZMod 12) : ℕ

The tiling convolution count (1_A ⋆ 1_B)(x) = #{(a,b) ∈ A×B : a+b = x}: the number of ways to write x as a sum of an element of A and an element of B.

Equations

• MusicTheory.Tiling.tileCount A B x = ∑ a ∈ A, ∑ b ∈ B, if a + b = x then 1 else 0

def MusicTheory.Tiling.Tiles (A B : Finset (ZMod 12)) : Prop

A and B tile ℤ/12 iff every pitch class is hit exactly once by A + B.

Equations

• MusicTheory.Tiling.Tiles A B = ∀ (x : ZMod 12), MusicTheory.Tiling.tileCount A B x = 1

theorem MusicTheory.Tiling.dft_tileCount (A B : Finset (ZMod 12)) (k : ZMod 12) : ZMod.dft (fun (x : ZMod 12) => ↑(tileCount A B x)) k = Fourier.Ahat A k * Fourier.Ahat B k

The discrete convolution theorem. The DFT of the tiling-convolution count is the pointwise PRODUCT of the two DFTs: 𝓕(tileCount A B) k = Â A k · Â B k. Proved by expanding the product, merging the two character factors χ(-(a k))·χ(-(b k)) = χ(-((a+b) k)), and regrouping by the sum x = a + b (the discrete analogue of fourier_mul_convolution_eq, which Mathlib provides only for the continuous Schwartz-space transform).

theorem MusicTheory.Tiling.dft_const_one (k : ZMod 12) : ZMod.dft (fun (x : ZMod 12) => 1) k = if k = 0 then 12 else 0

DFT of the constant 1. 𝓕(fun _ => 1) k = if k = 0 then 12 else 0 (= 12·δ₀), by orthogonality of the standard additive character: the full character sum is 12 at k = 0 and vanishes for k ≠ 0 (Fourier.dft_one_apply_ne).

theorem MusicTheory.Tiling.tileCount_eq_one_iff_dft_eq (A B : Finset (ZMod 12)) : Tiles A B ↔ (fun (x : ZMod 12) => ↑(tileCount A B x)) = fun (x : ZMod 12) => 1

The constant function 1 and the convolution count have equal DFTs iff tileCount = 1 pointwise (ZMod.dft is a LinearEquiv, hence injective).

theorem MusicTheory.Tiling.tiles_iff_dft_product (A B : Finset (ZMod 12)) : Tiles A B ↔ ∀ (k : ZMod 12), Fourier.Ahat A k * Fourier.Ahat B k = if k = 0 then 12 else 0

Tiling ⟺ DFT product is 12·δ₀. A ⊕ B = ℤ/12 iff  A k ·  B k = if k=0 then 12 else 0 for every frequency k. (Apply the convolution theorem + DFT injectivity to tileCount = 1.)

theorem MusicTheory.Tiling.tiles_iff_dft (A B : Finset (ZMod 12)) : Tiles A B ↔ A.card * B.card = 12 ∧ ∀ (k : ZMod 12), k ≠ 0 → Fourier.Ahat A k = 0 ∨ Fourier.Ahat B k = 0

The DFT tiling criterion over ℤ/12. A ⊕ B = ℤ/12 (every pitch class uniquely a sum a+b, a∈A, b∈B) ⟺ |A|·|B| = 12 ∧ ∀ k ≠ 0, Â A k = 0 ∨ Â B k = 0. The cardinality condition is the k = 0 Fourier coefficient (Ahat_zero: ·0 = card); the zero-set condition is the k ≠ 0 coefficients, where ℂ has no zero divisors so the product vanishes iff a factor does. Known mathematics (Amiot 2016 / Coven–Meyerowitz 1999), NOT new.

Witnesses — a positive tiling and a same-cardinality NON-tiling, both via the criterion.

theorem MusicTheory.Tiling.chromatic_aug_tiles : Tiles {0, 1, 2, 3} {0, 4, 8}

Positive witness. A = {0,1,2,3} (a chromatic tetrachord) and B = {0,4,8} (the augmented triad) tile ℤ/12: 4·3 = 12 and every pc is uniquely a+b. The classic "block canon".

theorem MusicTheory.Tiling.chromatic_aug_tiles' : {0, 1, 2, 3}.card * {0, 4, 8}.card = 12 ∧ ∀ (k : ZMod 12), k ≠ 0 → Fourier.Ahat {0, 1, 2, 3} k = 0 ∨ Fourier.Ahat {0, 4, 8} k = 0

The positive witness also passes the Fourier criterion directly: 4·3 = 12 and at every nonzero frequency one of the two DFTs vanishes (B̂ kills k ∈ {1,2,4,5,7,8,10,11} by the augmented-triad symmetry, Â kills k ∈ {3,6,9}).

theorem MusicTheory.Tiling.chromatic_badtriad_not_tiles : ¬Tiles {0, 1, 2, 3} {0, 1, 8}

Negative witness. A = {0,1,2,3} and B = {0,1,8} do NOT tile, even though 4·3 = 12: the sum A + B covers 0 twice and misses 6. So the right cardinality product is NOT sufficient — the zero-set condition is the real content.

theorem MusicTheory.Tiling.chromatic_badtriad_fails_zeroset : ¬∀ (k : ZMod 12), k ≠ 0 → Fourier.Ahat {0, 1, 2, 3} k = 0 ∨ Fourier.Ahat {0, 1, 8} k = 0

The negative witness fails the Fourier criterion at the cardinality-correct level precisely in the zero-set clause: there is a nonzero k with both  A k ≠ 0 and  B k ≠ 0.