Locked tromino tilings of rectangles

A tromino is a set of three grid cells connected through shared sides. A tiling of a grid by trominoes is locked if no two of its tiles can be removed and their six cells covered again by two trominoes in a different way, and the grid has at least one other tromino tiling. A locked tiling is a state that no step of the recombination (ReCom) Markov chain used in redistricting can change, on a grid with districts of three cells. Tucker-Foltz (2023) showed that no m× n grid with min(m,n)≤3 has a locked tromino tiling, constructed locked tilings whenever 3 m, m≥6 and n≥100, and conjectured that n≥4 suffices. We prove this conjecture. Together with his theorem it follows that an m× n rectangle has a locked tromino tiling if and only if 3 mn and min(m,n)≥4. As in his proof, we glue explicit locked blocks, mostly of heights 6 and 9, along full rows and columns; the new ingredients are a pair of blocks for each width from 4 to 55 (with heights 9 and 12, and two single tilings, at width 5) and four blocks of widths 8 and 9 for all larger widths. The gluing argument and every block are checked in Lean 4. Computer-assisted, with a Lean proof; not yet reviewed by experts. Produced by AI models under the author's direction.