README

This is a personal staging repository for work on Lean formalization
of the main results of the papers

  [hat] David Smith, Joseph Samuel Myers, Craig S. Kaplan and Chaim
  Goodman-Strauss, An aperiodic monotile.  Combinatorial Theory 4 (1)
  (2024), #6.  https://escholarship.org/uc/item/3317z9z9

  [spectre] David Smith, Joseph Samuel Myers, Craig S. Kaplan and
  Chaim Goodman-Strauss, A chiral aperiodic monotile.  Combinatorial
  Theory 4 (2) (2024), #13.  https://escholarship.org/uc/item/4xn41982

being developed and prepared for mathlib by the second author of those
papers.  All the material is intended to end up in mathlib or the
mathlib archive eventually in some form; this repository should not be
thought of as a long-term home for any of it, and mathlib is also the
appropriate location for any work by other people improving or
building on the material initially developed here.

I have a reasonable idea of the general form definitions and lemma
statements should take in this work, though there may be changes to
such definitions and lemma statements based on experience building
upon them.  Work in the field of tilings does not generally try to
define or state things in any kind of maximal generality (it's more
likely that the reader will be expected to understand how an argument
might be adapted to a different context as needed; see footnote 1 in
<https://strauss.hosted.uark.edu/papers/survey.pdf>); thus,
definitions and statements used in this work may not correspond
precisely to those found in a particular reference, but rather reflect
an educated guess at what a suitably general form is to cover the
various contexts in which a given definition or lemma may be used.
Despite the attempts at appropriate generalization in the course of
formalization, it is likely that further generalizations of some
definitions and results may arise in future as people build upon the
work in different contexts.

The following is an outline of the main intended steps in this work,
where in most cases the material from each step should be PRed to
mathlib as soon as it is written and all dependencies are in mathlib,
or as soon as it has been tested by material from subsequent steps
building upon it in cases that seem to need such testing of practical
convenience for developing subsequent theory.  (As usual, it seems
inevitable that formalizing each later step will show up omissions
from earlier steps that then need PRing to mathlib as they are found.)
This outline does not try to go into the details of what I think the
form of the definitions and lemma statements in each step should be.
Most of the proposed work is unlikely to start before August 2024 at
the earliest.

1. General definitions about tilings, in a discrete context, with
lemmas with little to no mathematical content.  In progress in this
repository (not yet ready to PR to mathlib, but background material
not specifically related to tilings is being PRed as I go along, once
all its dependencies are in mathlib).

2. Discrete versions of definitions and results about periodicity,
including relations between weak and strong periodicity of tilings,
and between weak and strong aperiodicity of protosets, in contexts
that can be considered two-dimensional (more generally: periodicity in
(n-1) directions in an n-dimensional space implying existence of a
strongly periodic tiling); a discrete analogue of Theorem 3.7.1 of
Tilings and Patterns.  In progress in this repository (not yet ready
to PR to mathlib; again, background material not specifically related
to tilings is being PRed as I go along).

3. A discrete version of unique hierarchical structure in a tiling
implying it is not periodic (for a more limited case for certain
substitution tilings in the plane, see Theorem 10.1.1 of Tilings and
Patterns).

4. A discrete version of the Extension Theorem (Theorem 3.8.1 of
Tilings and Patterns), that tiling arbitrarily large patches implies
tiling the whole space.

5. Constructing tilings based on local information on the relations
between neighbouring tiles, where that local information is locally
consistent around a suitable collection of loops (in a general context
not necessarily corresponding to any kind of surface).

6. Constructing tilings based on local information in the specific
case of two-dimensional tiles given by boundary markings and
combinatorial angles that must add up appropriately at vertices.

(It is possible that there may be room for something about tiles given
by some kind of markings on an n-dimensional combinatorial map, so
more general than step 6 but less so than step 5, but I don't think
anything like that is relevant to this project.)

Steps 5 and 6 are in particular need of testing through being applied
in practice, so might sensibly not be PRed to mathlib until after
substantial work has been done on steps 7 through 9.

7. Defining a type corresponding to the tiles of the Laves tiling
[3.4.6.4], the group of its symmetries, and the hat as a set of kites
from that tiling.

8. Computer-generated case analysis of patches of hats showing they
form certain clusters (Section 4 of [hat]).  Initially, this would
involve generated Lean code, generated by an adaptation of the Python
code used for the original analysis in that paper (not the same as
Craig Kaplan's Python code used for independent verification of the
case analysis).  This would use the version of the analysis in
Appendix B of [hat] to avoid needing to generate or check 2-patches.

9. Proof of aperiodicity for the four-tile system in Section 5 of
[hat], via that four-tile system forcing a combinatorial substitution
tiling structure, and thus (with existence of a tiling included
somewhere along the way) of the hat itself when considered in a purely
discrete context.

10. Defining the group of orientation-preserving symmetries of
[3.4.6.4] and the {hat, turtle} protoset in the context of that group
of symmetries.

11. A series of computer-generated case analyses as described in
[spectre] to show that {hat, turtle} is an aperiodic protoset in the
context of that group of symmetries.  As in step 8, this would involve
generated Lean code; as in step 9, existence of a tiling must be shown
along the way.

12. General definitions and lemmas about tilings, in a metric space
context, analogous to those for a discrete context from step 1.

Although definitions may make sense in even more general contexts
(such as a topological space context), those do not seem particularly
useful at present.

I do not know whether it will be possible to set up some common
abstraction of type classes so that some lemmas can be stated and
proved for both discrete tilings (no intersections between tiles) and
metric tilings (interiors of tiles disjoint, boundaries may
intersect), but if it is, I don't expect it to be possible to identify
a suitable form for such an abstraction until a substantial amount of
theory has been developed separately for both cases.

13. The connection between geometric and discrete tilings for the hat,
based on the series of more general lemmas in Appendix A of [hat],
thereby showing the hat is an aperiodic monotile in a geometric
context.  (The fact that it is a closed topological disk should also
be shown here, since that is a key thing that is new for the hat
compared to previous candidates for aperiodic monotiles.)

It seems plausible that step 13 could involve as much work to
formalize as all the other steps in this list put together; it also
seems the most likely to benefit from a more detailed list of small
lemmas and associated proofs than in the original paper.  It may also
involve significant dependencies on other mathematics not currently in
mathlib (for example, Appendix A uses Euler's theorem for plane maps,
and some of the "obvious" properties used of divisions of the plane
into regions by (polygonal) curves might turn out to depend on the
Jordan Curve Theorem or related results for formal proof).

14. Constructing tilings based on local information on the relations
between neighbouring tiles, in a simply-connected geometric context;
analogous to step 5 above.  Note that [hat] and [spectre] reference
this to a paper justifying it (in certain contexts such as the plane)
using fairly heavyweight theory of manifolds, but it should be doable
in a form not depending on anything so heavyweight (and so also more
general than the manifold context).

15. The family of aperiodic monotiles in Section 6 of [hat], including
that all those tiles are closed topological disks and that the spectre
is not aperiodic if reflections are allowed.

16. The connection between geometric and discrete tilings for the
spectre considered as Tile(1,1) with a restriction on the group of
permitted isometries, thereby showing that form of the spectre is an
aperiodic monotile in a geometric context when that restriction on the
group of permitted isometries applies.

17. Aperiodicity of the spectre with C^1 curves for boundary segments,
even when reflections are allowed (via mixing of reflected and
unreflected copies of the tile being impossible when the 14 boundary
segments are C^1 curves that are not straight line segments).

18. Step 8 (the case analysis for the hat) involves Lean code
generated by an external program.  Learn enough Lean metaprogramming
to write a replacement in the form of Lean tactics or similar.  This
is likely to be necessary to make the proof of aperiodicity by case
analysis suitable for the mathlib archive, where generated code
produced by another language would probably not be suitable.

19. Likewise, for step 11 (the case analysis for the spectre).  The
original case analysis involved much more computation than for the
hat, so the same is likely to be the case for any Lean version of that
case analysis.

20. It is possible that step 13 (Appendix A of [hat]) involves using
obvious properties of e.g. tilings of the plane by closed topological
disks, that are only needed or proved in that step for certain
polygonal cases but are actually true more generally.  If step 13's
proofs do turn out like that, then in this step the results should be
proved more generally to make the overall set of lemmas from step 13
more suitable for mathlib.  (This step might well end up depending on
results such as the Jordan Curve Theorem, and so being deferred until
such results are in mathlib.)

The following steps are not strictly needed for the main results of
[hat] and [spectre], but are sufficiently closely related that they
seem appropriate to list here as potential future uses of this
repository.

21. Formalize Section 3 (Aperiodicity via coupling of polyiamond
tilings) of [hat].  Strictly the result of Section 3 is weaker than
that achieved by case analysis (only the latter shows that the hat
forces a certain hierarchical / substitution structure; the former
merely gives the lack of periodic tilings without further information
on the structure of tilings).  But it seems reasonable to formalize
both approaches to proving aperiodicity as part of formalizing the
paper.

22. Relation between weak and strong periodicity of tilings, and weak
and strong aperiodicity of protosets, in the two-dimensional geometric
context; Theorem 3.7.1 of Tilings and Patterns; analogous to step 2
above.

23. A metric version of unique hierarchical structure in a tiling
implying it is not periodic (a more general form of 10.1.1 of Tilings
and Patterns; analogous to step 3 above).

24. The Extension Theorem (Theorem 3.8.1 of Tilings and Patterns),
that tiling arbitrarily large patches implies tiling the whole space
(subject to appropriate conditions on the protoset and the space
tiled); analogous to step 4 above.

The following are definitely outside the scope of this work and so
should not be formalized here (but formalizing elsewhere, aiming for
inclusion in mathlib or the mathlib archive, is appropriate):

* Work on the hat, turtle and spectre by various authors that has been
  released in response to the original preprints.

* Showing that the hat and turtle are the smallest aperiodic polykites
  (the large case analysis involved of other polykites through
  10-kites might just about be feasible for formalization through
  auto-generated Lean code or suitably efficient Lean metaprogramming,
  though the larger computer search through 24-kites mentioned in
  Section 6 of [hat] would not be).

* Properties of any other well-known aperiodic protoset.

* Undecidability of tilings by Wang tiles, as proved by Berger (some
  other proofs appear in the literature, and versions of Berger's
  proof such as that by Robinson).

* Results on tilings other than aperiodicity, its dependencies and
  results analogous to those dependencies.