Worked solution: Smith–Myers–Kaplan–Goodman-Strauss's aperiodic monotiles: the hat and the Spectre (2023)

Step 5 of 8: Computer-assisted case analysis confirms the classification is forced everywhere

In plain words

Verifying that the eight classification rules and the matching checks really cover every possible local arrangement of hats — with no gaps, no ambiguity, and no arrangement left unclassified — means checking an enormous but finite number of small local pictures by brute force. The authors did this with two independent computer programs, written separately by two of the four authors without consulting each other, and cross-checked that both gave the same answer.

\text{8 classification rules} + \text{exhaustive case analysis} \implies \text{unique metatile label per hat}

Detailed analysis

Because the classification rules and the matching checks between clusters must be verified against every locally possible $2$ -patch (a tile together with two rings of surrounding neighbours), the case analysis is combinatorially large: it covers all admissible neighbour configurations consistent with the hat's geometry and the matching rules established so far. Doing this correctly by hand, without missing a case, is not realistic.

Smith, Myers, Kaplan and Goodman-Strauss therefore implemented the case enumeration as software, and — learning from the historical controversy around the original four colour theorem proof — two of the authors independently wrote separate programs without collaborating on the implementation, then compared results, finding full agreement (2023, §4, remark on verification). This exhaustive, machine-checked case analysis is the second major computer-assisted step in the paper (the first being the earlier Heesch-number and isohedral-number computations that motivated the search).

With the classification confirmed to be complete and unambiguous, every tiling by the hat is now known to decompose, without exception, into the four metatiles $H, T, P, F$ satisfying the inherited matching rules — the stage is set for the substitution argument in the next step.

Common mistake. This computer-assisted step, like the four colour theorem's computer verification, checks a finite but very large number of cases mechanically; the authors' response to concerns about reliability was independent cross-verification by two separately written programs, a lighter-weight version of the same idea later realised fully by machine-checked formal proofs in other settings (such as the Coq formalisation of the four colour theorem).