Golomb 层级中的四臂多联骨牌：基于 Lean 验证的完整分类
Four-arm polyominoes in Golomb's hierarchy: A complete classification with Lean verification
浏览论文内容
中文总结 AI 辅助
本文对四臂多联骨牌按平铺能力进行完整分类，发现五种轮廓，并用 Lean 4 形式化验证了所有自然数四元组的情况。
中文摘要 AI 辅助
我们根据多联骨牌平铺矩形、半带、弯带、象限、带、半平面和平面的能力，对通过向单个正方形邻接四个直臂（允许臂长为零）所得到的多联骨牌进行分类。我们还分类了它们平铺自身整数放大的能力。瓷砖占据整个方格单元；允许平移、旋转和反射。恰好出现五种能力轮廓。对于族 $P(n,1,1,0)$，矩形轮廓在 $n\le3$ 时成立，而弯带轮廓（无半带或自平铺）在每一个 $n\ge4$ 时成立。具有四个正臂的十字形恰好当两个相对臂长度为 1 时平铺平面；它从不平铺半平面。显式的周期构造和几何障碍与有限的符号案例证书相结合。一个 Lean 4 开发验证了每个自然数四元组的完整分类，包括将证书解释为关于任意无限平铺的陈述。该说明纳入了作者 2020--2021 年的 L 型和 T 型多联骨牌工作，重构了 Dahlke 的枪式论证，并记录了后续的 AI 辅助证明开发和形式化。
英文摘要
We classify the polyominoes obtained by adjoining four straight arms to a single square, allowing zero arm lengths, according to their ability to tile rectangles, half-strips, bent strips, quadrants, strips, half-planes, and the plane. We also classify their ability to tile an integer enlargement of themselves. Tiles occupy whole square-grid cells; translations, rotations, and reflections are permitted. Exactly five capability profiles occur. For the family $P(n,1,1,0)$, the rectangle profile holds for $n\le3$ and the bent-strip profile, with no half-strip or rep-tiling, for every $n\ge4$. A cross with four positive arms tiles the plane precisely when two opposite arms have length one; it never tiles a half-plane. Explicit periodic constructions and geometric obstructions are combined with finite symbolic case certificates. A Lean 4 development verifies the full classification for every natural four-tuple, including the interpretation of the certificates as statements about arbitrary infinite tilings. The account incorporates the author's 2020--2021 L- and T-polyomino work, reconstructs Dahlke's gun argument, and documents the subsequent AI-assisted proof development and formalization.
