Four-arm polyominoes in Golomb's hierarchy: A complete classification with Lean verification
Abstract
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≤3 and the bent-strip profile, with no half-strip or rep-tiling, for every n≥4. 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.
Related
- Some complete ω-powers of a one-counter language in the difference hierarchy
- A complete classification for n-species Lotka-Volterra stably dissipative systems based on a generalized AHU algorithm
- Complete classification of algebraically primitive Teichmüller curves in Ωℳg(g−1,g−1)hyp
- Short permutation pattern waves: The complete length-five classification
- Primality of dilated closed path polyominoes
BibTeX
@misc{raychev2026fourarm,
title = {{Four-arm polyominoes in Golomb's hierarchy: A complete classification with Lean verification}},
author = {Angel Ivanov Raychev},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.13641},
eprint = {2609.13641},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.13641},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Four-arm polyominoes in Golomb's hierarchy: A complete classification with Lean verification
AU - Angel Ivanov Raychev
PY - 2026
DA - 2026/09/12
PB - arXiv
DO - 10.48550/arxiv.2609.13641
UR - https://arxiv.org/abs/2609.13641
AB - 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≤3 and the bent-strip profile, with no half-strip or rep-tiling, for every n≥4. 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.
ER -