AI 中文总结
本文通过互素条纹坍缩和强归纳法证明了有限整数平移铺砌满足无限制的 Coven-Meyerowitz T2 条件，并辅以 Lean 形式化验证，从而完成铺砌的完整刻画。
AI 中文摘要
我们证明了每个可通过平移铺砌的有限整数子集都满足 Coven-Meyerowitz 条件 T2，且对素因子个数或其指数没有任何限制。结合 Coven 和 Meyerowitz 已证明的 T1 必要性以及 T1 和 T2 的充分性，这给出了他们提出的有限整数铺砌的刻画。证明使用了对循环铺砌周期的强归纳法。特征恒等式产生周期性的布尔乘积条纹；积分下降到一个互素商以及 Frobenius 恒等式迫使它们具有共同的方向。随后，独立的相移给出更小周期的铺砌，从中可以恢复原始因子的混合分圆零点。一个配套的 Lean 形式化验证确认了无限制的 T2 必要性陈述。
英文摘要
We prove that every finite subset of the integers which tiles by translations satisfies the Coven-Meyerowitz condition T2, with no restriction on the number of prime factors or their exponents. Together with the necessity of T1 and the sufficiency of T1 and T2 proved by Coven and Meyerowitz, this gives their proposed characterization of finite integer tiles. The proof uses strong induction on a cyclic tiling period. Character identities produce periodic Boolean product stripes; integral descent to a coprime quotient and the Frobenius identity force a common orientation. Independent phase shifts then give smaller-period tilings from which the mixed cyclotomic zeros of the original factors can be recovered. A companion Lean formalization verifies the unrestricted T2 necessity statement.
Comments9 pages; companion Lean formalization and verification workflow available at https://github.com/infinityscroll/coven-meyerowitz-t2
