Aperiodic Order

Stream: mathlib4

[Newell Jensen]

Hi all — I’m working on formalizing Delone sets and early aperiodic order theory in mathlib.
My first PR is here:

#32030

A reviewer suggested that some of the foundational design choices might benefit from wider visibility, so I’m summarizing them here.
If you’d like more background or to see the earlier discussion in detail, the PR conversation contains the full review thread and motivations for the decisions below.

---

DeloneSet as a structure

The current design bundles:

• the underlying set carrier,

• a proof it is UniformlyDiscrete,

• a proof it is RelativelyDense.

The structure-based approach avoids the repeated extraction of existential witnesses required by an IsDelone predicate.
Since later theory (patches, hulls, repetitivity, tilings, etc.) continuously refers to specific radii (e.g., in patch definitions, repetitivity bounds, hull arguments), having these as explicit fields yields a far more convenient and readable API.

---

Working in MetricSpace

Classical Delone theory fundamentally relies on quantitative metric control:

• packing and covering radii,

• patch windows,

• tile diameters,

• repetitivity scales.

These real-valued bounds are fundamental to aperiodic order, so MetricSpace is the appropriate setting.

---

Roadmap

After this PR (basic Delone sets), the plan is to develop:

• finite local complexity (via difference sets),

• patches of Delone sets,

• hulls and minimality under translation,

• repetitivity and linear repetitivity,

• basic tiling structures and local finiteness,

• followed by substitution tilings, Meyer sets, and diffraction.

---

If anyone has thoughts on these foundational design choices, I’d appreciate feedback now so that the later PRs (I already have several in the pipeline but haven't proposed them yet) build on solid ground.
Thanks!

[Joseph Myers]

I don't have comments specifically on the design choices for Delone sets; what I have to say here relates only to later stages of the development.

I've also started developing some definitions relating to tilings in AperiodicMonotilesLean - which I do definitely intend to get back to working on more actively when I have time.

Now, so far I've only set up definitions there for tilings in a discrete context, on the basis that API setup in a continuous (metric space) context could follow later (with the API set up to parallel the discrete API as far as possible) when the discrete API is more developed - but my expectation would be to work with indexed families of closed sets under a group of isometries, requiring the interiors to be disjoint for it to be a tiling (some authors have other variants such as intersections of measure zero instead of interiors disjoint). I also haven't PRed any of the material about tilings to mathlib, on the basis that building more on top of it first might help confirm whether it's a good API or not (but if people think it's worth putting such material in mathlib before then, I could start PRing some of the 3000 lines of Lean I have there, at the risk that it ends up needing to be reworked later if there turn out to be problems with the API design).

For the benefit of readers on Zulip not familiar with the field, I should note that there are two different approaches to the idea of aperiodicity in tilings. One (which is the one I'm concerned with for AperiodicMonotilesLean) considers it as a local-to-global phenomenon, where you're concerned with how purely local constraints on how tiles fit together force a global lack of periodicity in the tiling. The other is concerned with structures that show certain kinds of order without being periodic and studies the properties of those structures, which include but aren't limited to tilings arising from sets of tiles that force a lack of periodicity. (You can extremely easily construct a substitution tiling with aperiodicity in the second sense starting from tiles that also admit periodic tilings, and so are not an aperiodic set of tiles in the first sense.) I would hope that common definitions of tiles and tilings can work for both approaches, but the kinds of things done after setting up the definitions may differ somewhat.