Coven and Meyerowitz proposed characterizing finite integer translational tiles by two cyclotomic conditions, T1 and T2. T1 was known to be necessary and T1 plus T2 sufficient, but T2 necessity was known only when |A| has at most two distinct prime factors.

The proof first reduces an integer tiling to a cyclic tiling, then uses strong induction on the cyclic period. Character identities on prime fibers produce periodic Boolean product stripes. Descent to a coprime quotient and a Frobenius identity in F_p[G] force a common row orientation. Independent phase shifts then give tilings of smaller period, from which the mixed cyclotomic zeros of the original factors are recovered.

Every finite tile of the integers satisfies T2, with no restriction on prime factors or exponents. Combined with the classical results, this gives the full Coven–Meyerowitz characterization of finite integer tiles. A companion Lean development verifies the T2 necessity theorem, while the two classical implications are cited rather than formalized.