Four-arm polyominoes and Golomb’s hierarchy

14 Sep 2026

A complete classification for nonnegative integer arm lengths, with explicit constructions, impossibility proofs, independently checked certificates, and an unconditional Lean proof of all eight capabilities for every four-tuple.

Start with one square and attach straight arms in the four compass directions. How much of the square grid can repeated copies cover? A rectangle is a much stronger achievement than the whole plane: its corners and edges impose constraints that an infinite tiling can avoid.

This article studies a family that includes bars, L shapes, T shapes, and crosses. Angel Raychev’s original research, from October 2020 to March 2021, classified the L shapes and all T shapes except two cases. The subsequent AI-assisted investigation reconstructed those results, completed the two cases, analyzed genuine crosses, and formalized the complete classification. The paper page records the contributions and prior literature.

Read the paper on arXiv:2609.13641 (math.CO), download the PDF or LaTeX sources, or see citation and formal artifacts.

The shapes and the rules

We identify a unit square with its integer coordinate. For nonnegative integers $a,b,c,d$, define

The parameters count squares beyond the shared central square, in east, north, west, south order. Thus the area is $1+a+b+c+d$. Rotations, reflections, and integer translations are permitted. Tiles must cover the requested region exactly, without gaps or overlaps.

Cyclic shifts and reversal of the tuple describe congruent shapes. Degenerate bars have further descriptions: $P(1,0,2,0)$ and $P(0,0,0,3)$ are the same straight tetromino. For a genuine T shape we set $d=0$ and normalize $a\ge c\ge1$, with $b\ge1$ the stem length. These conventions distinguish the geometry without pretending that every tuple is a unique name.

What counts as a level?

The seven regions used here are:

Here $\mathbb N=\{0,1,2,\ldots\}$. Widths are existential: a shape tiles a strip if some finite positive width works. This is a branching hierarchy. In particular,

A plane-only tile covers the plane but not a half-plane. A non-tiler does not even cover the plane. A separate classical branch asks whether congruent copies of a tile can tile an enlarged copy of itself, a rep-tile. Here the linear enlargement factor is a natural integer at least two, with all copies placed on the square grid. Rectangle tilings imply this property, and the property implies quadrant tileability. This branch is included in the classification below.

These are capability implications, not permission to reverse the arrows. Nor does a failed search through several widths prove failure for all widths. For the original hierarchy and its subtleties, see Golomb’s paper and Winslow’s 2018 problem survey.

The complete classification

Classification theorem. Every shape in this family has exactly one of the following five capability profiles. A check means that some region of the indicated kind is tileable; a dash means that none is. The column I denotes the rep-tile property.

To classify a tuple, first rotate or reflect the shape into the normal form in the table. A shape whose cells lie on one straight line is a bar, even if two opposite tuple entries are positive.

In particular, a genuine T tiles the plane exactly when

A genuine cross tiles the plane exactly when two opposite arms have length one. Thus four arms all longer than one always give a non-tiler.

The two initially exceptional cases, $P(4,1,1,0)$ and $P(5,1,1,0)$, both have profile BS: they tile bent strips, quadrants, full strips, half-planes, and the plane, but no half-strip, rectangle, or enlarged copy of themselves. There are no unresolved tuples in the table. The L obstruction results are credited to the supplied 2021 papers and now also have complete Lean reconstructions; the following sections and proof appendix establish the T and cross cases.

A two-row strip and a bent strip

Theorem. Every $P(a,1,c,0)$ tiles a strip of width two.

Put $T=P(a,1,c,0)$, $L=a+c+1$, and $n=L+1$. For every $k\in\mathbb Z$, place

On row zero, the first tile contributes $L$ consecutive cells and the second fills the next cell. On row one, their roles reverse, with the start shifted by $c$. Each row is partitioned into blocks of length $n$; all tiles stay within these two rows. This proves exact coverage.

When $c=1$, restrict the same construction to $k\ge0$. It covers the jagged half-strip

Reflect $H$ across the diagonal and shift it upward by one cell. The resulting region is

These two regions are disjoint. Their union is precisely the bent strip with both arm widths two. Thus every $P(a,1,1,0)$ tiles a bent strip, including both initially exceptional shapes.

In contrast, if both crossbar arms are at least two, a quadrant is impossible. A tile at the corner must put a crossbar endpoint there. Suppose that bar lies along the bottom boundary. The tile covering the next cell up the left boundary must put a vertical crossbar there. The cell $(1,1)$ then cannot be covered: either kind of crossbar hits an existing stem, while either kind of perpendicular stem forces its crossbar outside the quadrant. This checks all possible orientations and uses only the first four corner cells.

Why the two exceptions cannot tile a half-strip

Theorem. For every $a\ge4$, $P(a,1,1,0)$ tiles a bent strip but no half-strip, no rectangle, and no enlarged copy of itself by congruent copies.

The positive construction is above. The obstruction follows a corner through a hypothetical tiling. It uses five small states, each consisting of an occupied vertical wall immediately left of an empty quadrant and an occupied floor immediately below it:

Here the wall cells are $(-1,0),\ldots,(-1,w-1)$ and the floor cells are $(0,-1),\ldots,(f-1,-1)$. The superscript means reflection across the diagonal.

The finite case analysis has a precise conclusion: every completion of any state either overlaps an occupied cell or creates one of these states at a new origin $(\Delta x,\Delta y)$, where both coordinates are nonnegative and their sum is positive. Previously placed tiles leave that new quadrant empty except for its listed decoration. The first transition from $\alpha$ increases both coordinates strictly.

Moreover, transitions with $\Delta y=0$ can only follow

Some of these arrows are absent at $a=4$. There is no directed cycle consisting only of zero-height moves. An infinite sequence of corner states must therefore reach arbitrarily large heights.

Suppose a half-strip of some positive integer height $H$ were tiled. Stacking four copies gives a tiled half-strip of height $4H\ge4$, enough to support the initial four-cell corner walls. At each step, the queried cell lies inside this half-strip. Follow the actual tile covering it; the checked local cases supply a new clean corner, still below height $4H$.

There is a finite descent proof. Assign the five states ranks $r=(0,1,2,1,0)$ in the table’s order. A transition with no height increase strictly decreases $r$; a positive height increase lowers $3(4H-Y)+r$ even if $r$ increases. This nonnegative integer therefore strictly decreases at every step, which is impossible indefinitely. Lean checks both the local cases and this arbitrary-height deduction. A rectangle would yield a half-strip by repetition, so it is impossible too.

The case analysis is available as explicit proof trees: 1,750 nodes for $a=4$ and 872 for $a=5$. A separate symbolic tree handles every integer $a\ge6$ without an upper bound. Independent checkers verify every possible whole-tile placement through each queried cell, including overhangs, and the exact geometry of every successor corner. These are exhaustive proofs; testing a long list of strip widths would not establish the theorem.

The rep-tile obstruction requires an additional argument. Assign the five states potentials $h=0,2,2,1,0$, respectively. Every transition satisfies

Thus a corner at $(X,Y)$ reached from the initial state satisfies $X-4Y\le-h$. These inequalities and all query bounds are checked by exact integer arithmetic.

If a rep-tiling existed with scale factor $k$, an original unit-length boundary segment would become a segment of length $k$ on the boundary of a union of lattice tiles. Thus $k$ would be an integer. Iteration would then tile arbitrarily large integer enlargements. At the lower-right corner of an enlargement by factor $k$, measure $X$ to the left and $Y$ upward. The long horizontal arm has height $k$ and the stem starts at $X=ak$. An interior corner before the stem has an occupied wall of height $w\ge4$, hence $Y+w\le k$. Therefore

Every queried cell has relative horizontal coordinate at most seven; a whole tile through it extends at most $a+1$ farther. Consequently every tile used by the corner argument remains strictly before the stem. The supported queries stay inside the rectangular arm, and the next corner does too. The same unbounded-height contradiction applies. The initial exterior corner is handled by choosing $k\ge a+2$. This proves the sharp $a=4$ case as well as all longer cases.

The corner configurations come directly from section 23 of Karl Dahlke’s Gun Theorem, which already proves rectangle nonrectifiability for the whole family, including $a=4,5$. The certificates reconstruct the local alternatives and establish the additional rank and containment statements used here. This account does not claim that the half-strip or rep-tile conclusions could not be extracted from Dahlke’s argument. The theorem was documented by 19 May 2019; its original composition date is unknown. See the paper’s research history and bibliography for the full attribution.

Three plane constructions for T shapes

T boundary theorem. A genuine $P(a,b,c,0)$ tiles a half-plane if and only if $b=1$. The forward obstruction is proved by exhaustive boundary-contact cases in the proof appendix; the reverse direction is the two-row strip above. Consequently every plane construction in this section with $b\ge2$ has exact profile Plane-only.

A convenient way to prove an infinite tiling is to give finitely many tiles and two translation vectors. If their cells represent each residue class of the translation lattice exactly once, repeating them gives an exact plane tiling.

A unit crossbar arm. For $T=P(a,b,1,0)$ put $n=a+b+2$. Repeat

over the lattice generated by $(2n,0)$ and $(2,1)$. The quotient coordinate is $x-2y\pmod{2n}$. The two horizontal bars cover all integers from $-1$ through $2a+2$. The remaining stem cells supply the missing even and odd residues, respectively. Every residue appears once.

A stem of length two. For $T=P(a,2,c,0)$ put $n=a+c+3$. Repeat

over the lattice generated by $(n,0)$ and $(c+1,2)$. Use row parity $j=y\bmod2$ and horizontal residue $x-\lfloor y/2\rfloor(c+1)\pmod n$. In the even row class the cells form the consecutive residue interval $[-c-1,a+1]$. In the odd class the horizontal bar gives $1,\ldots,n-2$ and the stems give $0,n-1$. Again every class occurs exactly once.

An exceptional four-copy construction. There is a further family, $T=P(a,a+3,2,0)$ for every $a\ge2$. Write $b=a+3$ and $\sigma(x,y)=(y,x)$. Repeat

over the lattice generated by $(4,4)$ and $(b,-b)$. Each tile has area $2b$, so the four tiles contain $8b$ cells, the index of the lattice. Exact coverage follows by reducing $x-y$ modulo $2b$ and then the transverse coordinate modulo four. The detailed eight-interval partition is retained with the research proofs; it verifies every parameter, not just the illustrated example.

Crosses cannot touch a straight infinite boundary

Theorem. No collection of crosses whose four arms are positive can tile a half-plane. The crosses need not even have the same arm lengths.

Suppose such a tiling covers $y\ge0$. A tile meeting the boundary must do so at the tip of its downward arm. If its horizontal bar met the boundary, its downward arm would leave the region.

The tiles covering $(0,0)$ and $(1,0)$ therefore have junctions $(0,r)$ and $(1,s)$, with $r,s\ge1$. If $r\le s$, the first tile’s right arm contains $(1,r)$, which is already on the second tile’s vertical arm. If $s\le r$, the second tile’s left arm intersects the first. Both alternatives are impossible.

This entire statement, with arbitrary infinite indexed families, is checked in Lean. It immediately excludes every region above HP in the hierarchy for a genuine four-arm cross.

Opposite unit arms tile the plane

Theorem. If two opposite arms have length one, the cross is plane-only.

After rotation write $C=P(a,1,c,1)$ and put $n=a+c+3$. Repeat

over the lattice generated by $(n,0)$ and $(1,2)$.

To check the tiling, reduce each cell by row parity $j=y\bmod2$ and the residue $x-(y-j)/2\pmod n$. In the even class, the first horizontal bar gives $n-2$ consecutive residues $-c,\ldots,a$ and the second tile’s tips give the two missing residues $a+1,a+2$. In the odd class, the second bar gives $2,\ldots,n-1$ and the first tile’s tips give $0,1$. These are disjoint complete partitions. The preceding theorem excludes a half-plane, so the classification is exact.

Four long arms cannot tile the plane

Theorem. If $a,b,c,d\ge2$, then $P(a,b,c,d)$ is a non-tiler.

Suppose a plane tiling exists. Let $M$ be the longest arm length. Choose a tile $O$, rotate the entire tiling so that one of its longest arms points east, and translate its junction to $(0,0)$.

Consider the four diagonal cells $(\pm1,\pm1)$ around that junction. A tile covering the northeast cell must end an arm there: extending farther west or south would hit $O$. Its junction must lie beyond the tip of $O$‘s east arm or beyond the tip of its north arm. Assign this diagonal to east or north accordingly. Assign the other diagonals in the same way.

Two diagonals cannot be assigned to the same direction. For example, if both eastern diagonals were supplied from the east, their covering junctions would be $(r,1)$ and $(s,-1)$. If $r\le s$, the first tile’s downward arm, of length at least two, meets the second tile’s horizontal arm at $(r,-1)$. If $s\le r$, reverse their roles.

The four assignments must therefore use all four directions exactly once. Reflect vertically if necessary so the northeast diagonal is assigned east. Its covering tile $U$ has west tip $(1,1)$ and junction $(r,1)$ with $r>M$. Since its west arm has length at most $M$, we have $r-1\le M$, forcing $r=M+1$.

Now inspect $(1,2)$ and $(2,2)$. Neither can lie on another tile’s horizontal bar. A bar extending past either side would hit $O$‘s vertical arm at $x=0$ or $U$‘s vertical arm at $x=M+1$. A junction between those walls would send a downward arm into $U$‘s horizontal bar at height one.

Thus the two cells must be covered by distinct vertical arms coming from above. If their junction heights are $h\le k$, the first tile’s right arm meets the second vertical arm at height $h$. For $k\le h$, the second tile’s left arm gives the same contradiction. No tiling exists.

Completing the cross classification

The only positive crosses not covered by the all-long-arm obstruction or the opposite-unit-arm construction have either exactly one unit arm or exactly two adjacent unit arms. Up to rotation and reflection these are

and

Both families are non-tilers. Their proofs are finite symbolic case trees with 89 and 57 nodes, respectively. A node names a cell near the already placed crosses and lists every possible next cross covering it without overlap. Coordinates and arms remain arbitrary integers subject to the displayed inequalities. No maximum arm length is imposed.

All branches terminate in an uncovered cell. The independent checker allows an arbitrary integer junction for the proposed covering cross, so the proof does not rely on assuming that an initially plausible list of tip placements is complete. Lean then checks the arithmetic alternatives and replays the whole geometric argument for an arbitrary infinite family of disjoint crosses covering every integer cell. The translation and D4 normalization from an arbitrary tiling to the origin are also proved in Lean.

Thus a genuine cross tiles the plane if and only if two opposite arms have length one. It never tiles a half-plane.

Completing the plane classification for T shapes

Theorem. A T shape whose three positive arms are all at least three cannot tile the plane.

The useful local object is a run of empty cells with an occupied floor and occupied cells at both ends. Write $A=a+c+1$ for the crossbar length. When $b<A$, a run of length $3\le g<A$ is impossible: a horizontal crossbar cannot fit; a horizontal stem would put its junction’s downward arm into the floor. The cells must therefore start vertical crossbars or vertical stems. A vertical stem’s top crossbar meets its neighbor, while three adjacent vertical-crossbar starters cannot point their stems away from each other.

When $b\ge A$, the corresponding argument permits vertical-crossbar starters only at the two ends. Four or more starters force adjacent vertical stems, which overlap. A three-cell run is also impossible when one side wall reaches both possible crossbar-junction heights. A longer run of length $b$ is excluded by examining its first horizontal crossbar: the cells just above that bar form one of the forbidden shorter runs, with the new long stem supplying the necessary tall wall.

Apply these gap facts to the two cells diagonally above the junction of an upright T. The legal alternatives force at least one of them to be the endpoint of a horizontal crossbar whose stem points down. Reflect so this second bar occupies $(-A,1),\ldots,(-1,1)$. The next cell $(-1,2)$ is then forced to start a vertical crossbar pointing its stem right. If $b\ge A$, that stem immediately overlaps the original tile. If $b<A$, the next cell $(-2,2)$ has no legal cover: each orientation either intersects an existing piece or creates a forbidden gap. The endpoint case $b=A-1$ creates a gap of length $A-1$ one row higher. The proof appendix supplies every coordinate case and wall-height hypothesis.

Theorem. For $a\ge2$ and $b\ge3$, $P(a,b,2,0)$ tiles the plane if and only if $b=a+3$.

The equality case has the four-copy construction above. The shorter-stem complement $3\le b<a+3$ has a 300-node symbolic obstruction, independently checked with arbitrary integer junctions and no upper bound on either parameter. Lean also verifies the full geometric deduction for an arbitrary infinite tiling, using 2,700 arithmetic lemmas. Translation and D4 normalization of an arbitrary tiling to the anchor are also checked in Lean.

The longer-stem complement $b>a+3$ admits a geometric proof. Here $A=a+3$. A useful stronger gap lemma says that a run of any length $g\ge3$ is impossible when its floor and endpoints are occupied and one endpoint is a straight wall reaching $a+1$ rows above the run. The supporting tiles must leave the run clear, and the tall wall’s tile must have no cells inside the run’s horizontal span in the next row. To see this, take the first horizontal crossbar, if there is one. The cells just above its left arm form a gap of length two or $a$, with two sufficiently tall walls. No horizontal bar fits there; the remaining vertical starters intersect each other or a wall. If there is no horizontal bar, only the two endpoint cells can start vertical crossbars. The interior cells must start perpendicular stems, and two adjacent such stems have overlapping crossbars. For a three-cell run the tall wall also excludes the endpoint crossbar on that side.

This lemma first excludes an antiparallel pair of horizontal crossbars at a concave corner. Checking the remaining arm-tip covers then forces some upright tile $O$ to have the following neighbor: a vertical crossbar in column one, rows $1,\ldots,A$, with junction $(1,3)$ and a long stem pointing right. The two cells $(2,1),(2,2)$ jointly force a downward-stem horizontal bar $R$ in row one and a leftward perpendicular stem $W$ in row two. The other concave corner of $W$ forces a second downward-stem bar $Z$ at the far end.

The resulting finite interval of $b$ cells in row one lies below $W$‘s stem, with $R$ and $Z$ covering its two ends. A vertical-crossbar starter at an interior cell intersects its next neighbor. A perpendicular-stem starter either intersects its neighbor or encloses an $a$-by-$(b-1)$ rectangle into which no orientation fits. Hence the entire interval consists of adjacent horizontal bars of length $A$.

There are at least two such bars because $b>A$. For any consecutive pair with junction offsets $r,s\in\{2,a\}$, the run just below their bars and between their downward stems has length

Their stems supply straight walls taller than the gap lemma requires. The lemma gives a contradiction. This closes every remaining T case. The full proof records the exact forced placements, including both possible arm orders of $O$, $R$, and $W$; it does not rely on a numerical search or an assumed periodicity.

A small shape can require a large rectangle

The first three members of $P(a,1,1,0)$ tile rectangles. For $a=3$, the Y hexomino, there is a $24\times23$ rectangle made from 92 copies. The historical arrangement was extracted into explicit coordinates and independently checked: all 552 cells are covered once, and every piece is a congruent copy of the intended shape.

This example explains why small rectangle searches are weak evidence: a simple six-cell shape can hide its first successful construction surprisingly far away.

How the computation is checked

Positive certificates specify whole tile placements and, for infinite constructions, their translation lattice. Verification checks both the shape of every tile and exact coverage. The written residue arguments extend these constructions to arbitrary parameter values.

Negative finite certificates enumerate every legal placement that could cover each required cell, including tiles extending beyond an artificial search box. Each branch chooses a still-uncovered cell and tries every nonoverlapping placement; a branch ends only when some required cell has no legal cover. A second checker regenerates the placement universe and verifies every branch. Such a certificate proves non-tileability for its stated parameters and region. It does not prove an unbounded parameter family.

For a fixed strip width, a different finite graph records occupancy across a moving cut. Its cycles describe periodic continuations. Exhausting the graph can rule out every possible length at that width; exhausting several widths still does not rule out all widths. Boundary-prefix certificates can sometimes exclude all half-strip heights at once, but that stronger inference is stated only where its hypotheses have been checked.

For unbounded parameter families, symbolic certificates add a further obligation: every branch implication must hold for all integers in the stated domain. Lean 4.33.1 verifies the unconditional eight-capability classification for every tuple of natural arm lengths $(a,b,c,d)$, including zero arms, all degenerate shapes, and the rep-tile branch. The final theorem is PolyominoFormal.all_tuples_classified; it has no remaining obstruction premise. The half-strip proof includes the entire infinite-propagation argument for arbitrary widths. The unequal long-arm L half-plane obstruction is also fully formalized, completing the Lean reconstruction of the supplied 2021 L results.

Start with the unconditional all-tuples theorem, or the short statements for the two disputed cases, the complete gun family, and all genuine T shapes. The Lean source package contains every dependency, and the rebuild guide states the exact proof scope and commands. The proofs use ordinary whole-cell tilings, arbitrary integer translations, and all rotations and reflections. Rep-tiling here uses a natural linear enlargement factor at least two. Final theorem reports contain only Lean’s standard axioms; there are no admitted proofs or trusted solver answers.

The research log keeps failed conjectures, counterexamples, proof revisions, and independent attacks. There is no claim of novelty merely because a construction was independently rediscovered during this investigation. The classification has no remaining proof gaps under the tiling conventions stated above.

Proofs, source files, and the earlier papers

The full proof appendix supplies the coordinate cases, lattice residue partitions, corner propagation, and precise formalization boundaries. It is also available as a Markdown download. The research archive contains the manuscript, log, exact tile coordinates, finite and symbolic proof trees, independent checkers, and Lean sources, with a file-integrity manifest.

The earlier results are documented in Raychev’s 2021 L-polyomino paper and 2021 half-plane paper, both in Bulgarian. The present write-up uses arm lengths, so bounding dimensions $m\times n$ become arms $m-1,n-1$.

One dimensional correction emerged from reconstructing the second paper’s figure: its $4\times5$ L construction is a strip of width eight and period eight, although page four calls the width six. The exact eight-tile motif was checked cell by cell. This leaves the classification theorem unchanged.