This felt like a clear case for applying Burnside’s lemma. Six simple purple-and-white square tiles generate a surprisingly rich family of patterns. Once we identify patterns that differ only by rotation, the question becomes: how many distinct arrangements remain?
The essential detail is geometric. Turning a board moves its tiles and turns the diagonals inside them. A cell returning to its original position does not necessarily mean that its tile has returned to its original orientation.
For a 2 × 2 board, the six states give 1,296 oriented arrangements. The four rotations fix 1,296, 6, 36, and 6 patterns respectively. Burnside’s lemma averages these fixed counts:
The article explains where each fixed count comes from, constructs the symmetric patterns step by step, and develops formulas for every positive board size. It also considers reflections and a general rule for finite tile alphabets. The illustrations use exact geometry, and the companion explorer lets you rotate patterns and inspect their cycles.
The accompanying Lean development proves the rotation-orbit count in cycle coordinates. The bridge to explicit grid coordinates, the reflection extension, and the fully general cycle-product theorem remain written proofs rather than completed Lean formalizations.
I will explore similar patterns in the future and develop more music composition ideas. My next step is to see whether these visual transformations can be translated into musical structures: repeated motifs, cyclic shifts, inversions, and contrasting local states. The musical interpretation is an exploration to develop, rather than a result established by this article.
This is the first project prepared for Yamba Open Mathematics, a growing collection of mathematical ideas, reproducible software, and Lean proofs.
Lean source · Formal proof scope · Markdown article · Release checksums
