Locked tromino tilings of rectangles

An $m\times n$ rectangle has a locked tromino tiling if and only if $3\mid mn$ and $\min(m,n)\ge4$. A tromino consists of three grid cells connected through shared sides; a tiling is locked if no pair of tiles can be recombined into a different pair and the rectangle has another tiling. We prove the existence direction of Tucker-Foltz's conjecture. Tucker-Foltz showed that rectangles with a side of length at most three have none, constructed locked tilings when one side is divisible by three and at least six and the other is at least one hundred, and conjectured that four suffices. Following Tucker-Foltz's construction by compatible rectangular blocks, we supply the remaining cases and glue them along full rows and columns. Aanjaneya and Pal earlier proved existence on the same rectangles for the different condition of fault-free L-tromino tilings. Lean formalizes the existence theorem for $3\mid m$, $m\ge6$, $n\ge4$, including the gluing argument, arithmetic and finite blocks, using only propext, Classical.choice and Quot.sound. Two separately written programs, sharing no code, check the blocks and seams. The classification uses Tucker-Foltz's preprint theorem for narrow rectangles, whose proof leaves the $m=3$ frontier check to the reader there; we neither repeat nor formalize that check.

Checked in Lean from the definitions; not yet reviewed by experts. Produced by AI models under the author's direction.