Discussion - Definition of tilings

Stream: maths

[Eric Vergo]

I'm interested in developing tiling theory for eventual submission to Mathlib. There has been previous but unresolved discussion, which seems worth continuing. Based on that discussion, it seems like a tiling should exist in a topological space, with its associated symmetry group being a subgroup of the automorphisms of that space. Beyond this, however, it’s not clear how other aspects of the definition should be formulated. Given that, there are several foundational questions that merit discussion:

• Should we have separate definitions for discrete and continuous tilings?
• Can/should we use the same definition for finite and infinite tilings? (I believe the answer is yes for both)
• How should a tile be defined?

There are additional considerations such as defining protosets, decorations, matching rules, equivalence relations, etc. but these seem downstream of the core definitional choices above. Joseph Meyers has made suggestions answering these questions by offering a formalization outline. Are there any reasons why his outline may not be the best way to go about things?

[Joseph Myers]

As I said in #mathlib4 > Aperiodic Order @ 💬 I could start PRing definitions and basic API from AperiodicMonotilesLean (which represents my current view of how to set up the theory in the discrete case) to mathlib if people think doing so is worthwhile even before there's more mathematically substantial material built on top of it. (33 PRs of dependencies elsewhere in mathlib - more basic material about group actions, quotients etc. rather than specifically about tilings - have already gone in.)

• Should I start PRing that material without waiting until I've built anything more substantial on top of it?
• Is the design of defining things in the discrete case first, with a view to setting up parallel but separate API for the continuous case after discrete material has started going into mathlib, appropriate? (If continuous material is set up in the very general case of a topological space with a docs#ContinuousConstSMul action rather than a metric context with a docs#IsIsometricSMul action, then some of the most basic discrete API probably corresponds to the continuous API with the discrete topology. But I think needing to deal with an irrelevant topology all the time would be a pain when working with discrete tilings. The interesting case of relating continuous and discrete tilings isn't the one with the discrete topology, it's the one of genuinely continuous tilings where all the tiles can be expressed as unions of the tiles from some underlying tiling and so a translation to the discrete context done that way.)
• Is Mathlib.Combinatorics.Tiling an appropriate place for the discrete material? What about the continuous material?
• Is setting things up specifically with a multiplicative group action appropriate? I think that's a lot more natural than an additive group action for the typically noncommutative cases I'm concerned with, but does mean that anyone formalizing things about translational tilings of $\mathbb{Z}^n$ (Greenfeld-Tao etc.) would need to make a lot of use of Multiplicative (or else set up to_additive to duplicate the whole theory for additive tilings).

I think AperiodicMonotilesLean already has answers for decorations, matching rules and similar, though it may not be very obvious at a glance. The fact that a protoset is an indexed family of tiles means that multiple prototiles that are otherwise identical can be distinguished; the fact that a prototile comes with a subgroup of its stabilizer corresponds to a tile possibly having asymmetrical markings. The TileSetFunction abstraction covers matching rules, because rather than using basic functions such as IsTiling you can use ones that mean "is a tiling satisfying the matching rules"; definitions such as "aperiodic" all take a TileSetFunction that says what the rules are for permitted tilings. (The intent is to have predicates on TileSetFunctions for things such as "this is a local property, i.e. only depends on bounded patches of the tiling".)

[Yaël Dillies]

Joseph Myers said:

• anyone formalizing things about translational tilings of $\mathbb{Z}^n$ (Greenfeld-Tao etc.) would need to make a lot of use of Multiplicative (or else set up to_additive to duplicate the whole theory for additive tilings).

Have you tried out the to_additive approach? Is there any reason to believe it would be difficult? If not, that would be my preferred solution

[Joseph Myers]

I haven't tried the to_additive approach. The only complication I'd expect is for definitions for periodicity that involve Multiplicative ℤ; if to_additive can't convert between Multiplicative ℤ and ℤ, various proofs might need duplicating.

If we wish to use to_additive to make tilings of $\mathbb{Z}^n$ convenient, then some further questions follow:

• Should everything be set up with to_additive from the start, or only when someone actually wishes to use additive tilings?
• When additive tilings are defined, should everything be set up at the same time to support use of Additive and Multiplicative type tags for translating between additive and multiplicative versions of the same tiling?

[Yaël Dillies]

Joseph Myers said:

Should everything be set up with to_additive from the start, or only when someone actually wishes to use additive tilings?

My take is that we should make sure to_additive could be used later. I would rather avoid settling on a design that's completely non-additivisable

[Joseph Myers]

I expect that what I have would work with to_additive, modulo any complications where Multiplicative ℤ is used.

[Eric Vergo]

Joseph Myers said:

• When additive tilings are defined, should everything be set up at the same time to support use of Additive and Multiplicative type tags for translating between additive and multiplicative versions of the same tiling?

To confirm my understanding: In the statement "... additive and multiplicative versions of the same tiling" the two different versions are the same from a mathematical/structural perspective. Meaning the additive/multiplicative distinction is essentially bookkeeping needed to properly integrate with mathlib.

[Joseph Myers]

Yes. This is just like how monoids and groups are set up in mathlib (the basic material about tilings I have in AperiodicMonotilesLean is after all largely about manipulation of group actions and quotients).

The difference between additive and multiplicative objects is more one of conventions about what operations tend to be written + and what operations tend to be written *. When working with tilings under a noncommutative group of isometries (including discrete cases with such a group), it's natural to work with *. When working in $\mathbb{Z}^n$, it's natural to work with +. (Though section 11 of https://arxiv.org/pdf/2108.07902 for example does use + in a noncommutative case, with a bold warning about + not being commutative in that section.)

[Eric Vergo]

ok, good; everything here tracks.

It sounds like making sure we can use to_additive is the right way to go. As an exercise I will try this out with what you currently have and report back. It may take some time as I'm using this as a learning opportunity, but I have some time today and tomorrow to work through it.

P.S. the docs for to_additive are exceptional.

[Joseph Myers]

Do people have comments on the other questions? That is, when to start PRing this material (or at least the more basic parts of it that are plausibly ready, some parts are in an earlier stage of development), whether having separate definitions for the discrete and continuous cases is appropriate, and where to put it in mathlib.

[Ruben Van de Velde]

PR sooner than later, I think. No comment on your other questions

[Joseph Myers]

I've opened #33523 with the first file of definitions / API lemmas (several more files are plausibly ready, but I think it makes sense to get through review for one file before PRing any more).

[Joseph Myers]

Note that there is a question raised in review of that PR about namespace usage (I put things in the Discrete namespace to distinguish the material about tilings in a discrete context from future material about tilings in a continuous context, using the same names but in a different namespace). I can of course put things in a different namespace if preferred, so if you have views about how namespaces should be set up for tilings, then comment in the PR accordingly.

[Eric Vergo]

I have some time to code today, should I piggy back on this PR for the to_additive work? FYI, your suspicions were correct in that it works 'out of the box', but there are challenges with Multiplicative ℤ

[Joseph Myers]

I don't think complicating the initial PR with extra to_additive material is a good idea; it seems better to add support for additive tilings in a followup (and while you could set up a PR now with a dependency on my PR, it's entirely possible my PR will go through further major changes in the course of review).

Do you have particular material you're looking to formalize for which you want additive tilings? For example, are you planning to formalize some of the Greenfeld-Tao papers?

[Joseph Myers]

Of course, you don't need to be a maintainer or reviewer to contribute to review of PRs, if you find any issues with the material in this PR or subsequent PRs in this area.

[Eric Vergo]

Joseph Myers said:

I don't think complicating the initial PR with extra to_additive material is a good idea; it seems better to add support for additive tilings in a followup (and while you could set up a PR now with a dependency on my PR, it's entirely possible my PR will go through further major changes in the course of review).

That makes sense, I will wait and do it after. Also, sorry for going MIA; I was pretty under the weather. Spending time around the nieces and nephews for the holidays has its price!

Do you have particular material you're looking to formalize for which you want additive tilings? For example, are you planning to formalize some of the Greenfeld-Tao papers?

Actually I was hoping you could tell me. After the mono tile discovery my friend and I spent time trying to make a puzzle with solid 'monotile pieces'. Meaning each piece is the 3D solid where each 2D slice  was part of the infinite family, but got scooped by Oskar (1). Doing that involved writing software to simulate everything, and we were going to use a recreated patch from one of the original renders:

patch.mov

During that effort I got completely sidetracked by the following observation: under certain constraints, when transitioning through the infinite family, all of the vertices follow circular arcs. I had the opportunity to speak with Chaim about this a number of times and we could not get a handle on things. A lot of our unease was centered around how the underlying grid(s) are defined and determining which vertices of the tiling are fixed as a result. Here is the bottom left tile from that animation, isolated with its circular arcs overlaid.
uuid=894269C6-34C5-430F-892E-7CEA1BCE9809&code=001&library=3&type=3&mode=1&loc=true&cap=true.mov

Now here is the relevant part: In addition to lying on circular arcs, all of the vertices travel around at the same angular velocity, w.r.t. their circle. This naturally leads you to making the variation where vertices complete a full revolution. I really have no idea how to think about this because it feels like a natural extension of the monotile object, but it’s self-intersecting, and neighbors overlap. Should we think of this as a tile?

uuid=05A8A808-40F9-4E0A-97A4-ABC760A5A79C&code=001&library=3&type=3&mode=1&loc=true&cap=true.mov

1: https://www.youtube.com/watch?v=MQCvu8F8GYA

[Joseph Myers]

Eric Vergo said:

Do you have particular material you're looking to formalize for which you want additive tilings? For example, are you planning to formalize some of the Greenfeld-Tao papers?

Actually I was hoping you could tell me.

Tiling is a large field with a lot of activity in recent years, so it helps if you have an idea of things you're aiming to formalize. You could take almost any result from Tilings and Patterns, or from any paper in the subject since that book was written in the 1970s, for example. Some things might focus heavily on the combinatorial side (say if you wanted to formalize Berger's theorem that whether a set of Wang tiles admits a tiling is undecidable, possibly using one of the later presentations of the proof such as Robinson's). Some things might depend heavily on the geometrical and topological side (say if you wanted to formalize a proof that all topological discs that tile the plane using translated copies only can also do so with the tiles arranged in a lattice; Kenyon and others). Some things might heavily involve the computational side.

[Joseph Myers]

Eric Vergo said:

I really have no idea how to think about this because it feels like a natural extension of the monotile object, but it’s self-intersecting, and neighbors overlap. Should we think of this as a tile?

I don't think we can really consider tiles-as-possibly-self-intersecting-boundary (like section 12.3 of Tilings and Patterns) as being the same kind of formal object as tiles-as-solid-bodies. (Just as when talking about formalizing the notion of polygon in other Zulip discussions, we see how there are many things that informally get referred to as polygons that are different in the formal context.)

[Joseph Myers]

I think the fact that you get circular arcs all at the same angular velocity from such animations of the Tile(a,b) family (once you precisely tie down the details of how such an animation is defined - Craig's original animations are based on an approximation that was simpler to implement, but we already knew that, and what the precise version should be, at the time) is a consequence of the converse of angles in the same segment (modulo checking the details of the recurrences satisfied by edge vectors of supertiles, and the associated eigenvalues, to show that you're in the "circular arcs" case not the "straight line segments" case).

[Eric Vergo]

Joseph Myers said:

Eric Vergo said:

Do you have particular material you're looking to formalize for which you want additive tilings? For example, are you planning to formalize some of the Greenfeld-Tao papers?

Actually I was hoping you could tell me.

Tiling is a large field with a lot of activity in recent years, so it helps if you have an idea of things you're aiming to formalize. You could take almost any result from Tilings and Patterns, or from any paper in the subject since that book was written in the 1970s, for example. Some things might focus heavily on the combinatorial side (say if you wanted to formalize Berger's theorem that whether a set of Wang tiles admits a tiling is undecidable, possibly using one of the later presentations of the proof such as Robinson's). Some things might depend heavily on the geometrical and topological side (say if you wanted to formalize a proof that all topological discs that tile the plane using translated copies only can also do so with the tiles arranged in a lattice; Kenyon and others). Some things might heavily involve the computational side.

There are many things in this space I'm looking to formalize. Beyond verification, my intent in formalizing is to strengthen my understanding. I 'learn by doing' and the hope is that formalizing tiling theory will help me understand both the established results I half-understand and things I have found like the one above. That being said, it really looks like we may not have a ‘one size fits all’ definition. 

One 'intermediate' result I was considering going after was the classification of frieze/wallpaper groups. After reading and thinking about it more, I'm now realizing the following: we theoretically could come up with some definition of tiling and use it in those classification theorems, but it isn't required. I bring this up because we are discussing 'how should we define tiling' and it has caused me to realize that something I thought was about tilings isn't. Is it fair to say that these theorems "are really about the underlying symmetry groups of the space, and tiles are just a convenient way to think about them"?

[Joseph Myers]

Indeed, those theorems are about discrete isometry groups (that are also cocompact, in the wallpaper groups case) in the plane. There's a remark in Tilings and Patterns (page 291) that you can prove the classification of 17 wallpaper groups via the classification of 93 types of marked isohedral tilings in the plane, but I don't have any real sense of what approaches to the classification of wallpaper groups are best for formalization (any theorem that is an "or" with 93 alternatives seems like it would be even more painful to work with than an "or" with 17 alternatives, but in both cases you could split them up with appropriate intermediate definitions so you aren't dealing directly with a single huge term listing all the alternatives).

[Eric Vergo]

Joseph Myers said:

Indeed, those theorems are about discrete isometry groups (that are also cocompact, in the wallpaper groups case) in the plane.

I see. The natural question is:

"Is it always the case that the tiles are just a convenient way to think about underlying isometry groups?".

[Eric Vergo]

... but I don't have any real sense of what approaches to the classification of wallpaper groups are best for formalization

Nothing looked good to me, so when the rate limits were doubled during the holidays I had Claude-code put stub files together for a proof via lattice extensions. because that is what it thought was best. There is still a lot of slop in there, but given enough time/tokens I think that it would probably work out.

[Joseph Myers]

Eric Vergo said:

Joseph Myers said:

Indeed, those theorems are about discrete isometry groups (that are also cocompact, in the wallpaper groups case) in the plane.

I see. The natural question is:

"Is it always the case that the tiles are just a convenient way to think about underlying isometry groups?".

There are lots of things you can do with tiles and tilings. Some might just be ways to think about the underlying isometry group, most involve various combinatorial elements as well. The basic API I've set up so far in AperiodicMonotilesLean (reminder: #33523 needs more review) is largely closely connected to group actions simply because the combinatorial aspects appear more as you move to more specific results rather than things about all tilings (or all periodic tilings, etc.), which I haven't got to yet.

[Joseph Myers]

Eric Vergo said:

... but I don't have any real sense of what approaches to the classification of wallpaper groups are best for formalization

Nothing looked good to me, so when the rate limits were doubled during the holidays I had Claude-code put stub files together for a proof via lattice extensions. because that is what it thought was best. There is still a lot of slop in there, but given enough time/tokens I think that it would probably work out.

For mathlib I strongly advise considering for each lemma whether a version makes sense in an n-dimensional context and trying to prove the n-dimensional version if possible. For example, prove Bieberbach's first theorem on space groups in n dimensions rather than just that a discrete cocompact isometry group in two dimensions has two linearly independent translations. Similarly, prove the n-dimensional crystallographic restriction theorem and deduce the 2-dimensional version, rather than just proving the 2-dimensional version.

[Joseph Myers]

The next PR in my series with basic definitions for tilings in a discrete context is #33928 - that PR gives you the type for indexed families of tiles intended to be used for tilings (but not yet a predicate to say "this indexed family of tiles is actually a tiling", that comes in later files).

[Eric Vergo]

Similarly, prove the n-dimensional crystallographic restriction theorem and deduce the 2-dimensional version, rather than just proving the 2-dimensional version.

It was a bit of a struggle, but I was able to get the general theorem proven following some proof outlines.

[Joseph Myers]

I definitely encourage PRing the material from these projects to mathlib (starting of course with basic lemmas in existing parts of mathlib, and generally applicable definitions / API that don't depend on anything not yet in mathlib).

[Eric Vergo]

Will do.

FYI that entire repo was vibe-coded and contains some math which I'm not 100% on top of. I'm going to continue the classification work, but am unsure about a few things. I'll need some help developing things in a way that sets us up well for things like Bierbach's first theorem. If it's alright with you I can continue to make naive attempts and share them for your feedback. (maybe this should get its own thread as its not about tiling?)

[Joseph Myers]

Certainly start PRing with small lemmas in existing parts of mathlib, before getting onto definitions / API that might be reworked more in review.

Even how to define a discrete isometry group requires some thought since there are lots of possible definitions that are the same for Euclidean spaces but may be different in general. My inclination is "discrete orbits", but you also have alternatives such as "properly discontinuous action", or, given a topology on the group of all isometries, being discrete in that topology. (And whichever option is chosen, it would make sense to prove that the others are equivalent in this context so that the choice of definition doesn't affect the results.)