# Formal proof scope

The source pins Lean and Mathlib to 4.19.0. The authorship update does not constitute a new Lean compilation.

`System k e` comprises k independent four-tuples of tiles in rotating coordinates and e independently rotating central tiles. `orbitCount` is the cardinality of the actual orbit quotient under the Fin 4 additive action. It is not defined as the proposed formula.

The declaration `cycle_model_formula` proves for all natural k and e:

\[
\operatorname{orbitCount}(k,e)=
\frac{1296^k6^e+36^k2^e+2\cdot6^k2^e}{4}.
\]

It uses Mathlib's Burnside theorem, explicit fixed-set equivalences for products and function spaces, and explicit bijections that parameterize fixed four-tuples by one or two free tiles. The local six-state calculation uses kernel reduction with `decide`, not `native_decide`.

| Declaration | Mathematical statement |
|---|---|
| AddAction instances | Tile and cyclic-shift actions satisfy group laws |
| fixedPi, fixedProd | Fixed assignments decompose into independent components |
| fixedOneEquiv, fixedTwoEquiv, fixedThreeEquiv | Constructive seed parameterizations |
| tile_fixed_counts | Counts 6, 2, 2, 2 |
| block_fixed_counts | Counts 1296, 6, 36, 6 |
| fixed_system_card | Fixed counts multiply and exponentiate |
| cycle_model_burnside | Four times the quotient cardinality is the fixed-count sum |
| cycle_model_formula | The general cycle-model count |
| two_by_two, three_by_three | Counts 336 and 2520108 in the appropriate cycle models |

The literal coordinate-grid-to-cycle equivariant equivalence is established in the treatise but is not a Lean declaration in this project. Encoding that equivalence for every n ≥ 1 is the remaining step to a fully coordinate-level formalization. Reflections, the orbit-size distribution, and the arbitrary-group cycle-product theorem also have written proofs rather than delivered Lean proofs.

## Reproduce

From the project root: `cd formal`, `lake update`, `lake exe cache get`, and `lake build`. The toolchain is pinned in `lean-toolchain` and the dependency in `lakefile.toml`.