Polyominoes formed by adjoining four straight arms to a central square are classified according to their ability to tile rectangles, half-strips, bent strips, quadrants, strips, half-planes, the plane, and integer self-enlargements. Determining these tiling capabilities for an infinite parametric family requires constructions and obstructions valid without bounds on parameters.

The family P(a,b,c,d) is analyzed with tiles occupying whole grid cells under translations, rotations, and reflections. Explicit periodic lattice constructions establish positive capabilities, while geometric arguments and finite symbolic case certificates (obstruction trees) establish negative ones. A soundness theorem justifies interpreting finite certificates as statements about arbitrary infinite tilings. A Lean 4 development verifies the full classification for every natural four-tuple, including certificate interpretation.

Exactly five capability profiles occur: rectangle, bent strip, strip, plane-only, and non-tiler. For P(n,1,1,0), the rectangle profile holds for n<=3 and the bent-strip profile for n>=4. A four-positive-arm cross tiles the plane precisely when two opposite arms have length one, and never tiles a half-plane. The Lean artifact checks explicit witnesses (e.g., all 552 cells of the 92-copy Y-hexomino rectangle) and the symbolic obstruction trees.