lean/SpectreKnot/ProofChain.lean
717 lines · 45 declarations, each with its own page · on GitHub ·
Theorem A in strand form (theoremA_strand): in a tiling whose hierarchy covers the plane, every strand is a two-way infinite path.
← SpectreKnot/ProofStrand.leanSpectreKnot/ProofExact.lean →
All 39 files, and the declarations of this one
1/-
2**Theorem A in strand form** (`theoremA_strand`): in a tiling whose hierarchy covers the plane, every strand is a
3two-way infinite path.
5The tiling is the union of a chain X_1 ⊂ X_2 ⊂ ⋯ of supertiles (`Statement.lean` §7). Its tiles are numbered so that
6every block keeps its own numbering, and any tiling `T` that contains every block glues every edge (`chainModel`).
7Its ports, with the two pairings "other end of the piece" and "straight across the edge", form a `StrandSystem`
8(`tilingSys`). A closed strand would visit finitely many tiles. Every edge of each of them is glued in some block, so
9all of them are glued in one block X_L; following the strand inside X_L would then never reach the rim of X_L, but by
10Theorem A it does. So no strand is closed, and Lemma 3.4 (`StrandSystem.closed_or_path`) says that each strand is a
11two-way infinite path. This is the nest argument of `ProofStrand.lean` without Theorem B: for a chain the level at
12which an edge is glued has no fixed bound, so the closed strand's tiles are handled together (`all_glued_at`).
13-/
14import SpectreKnot.ProofStrand
16namespace SpectreKnot.Statement
18open Pattern Compose Gluing
20namespace Chain
22/-! ### The blocks as compositions -/
24/-- The children of X_{m+1}: the level-`m` supertiles of the kinds that Table 1 lists for `K (m + 1)`. -/
27/-- For `m ≥ 1`, X_{m+1} is the composition of its level-`m` children. -/
28theorem block_succ (X : Chain) {m : Nat} (m_pos : 1 ≤ m) : X.block (m + 1) = compose (X.K (m + 1)) (X.kidsAt m) := by
29 obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
30 rfl
32/-- Child `c m` of X_{m+1} is X_m. -/
37/-- X_m starts at tile `X.shift m` of X_{m+1}: after the tiles of the children before it. -/
40/-- The children of X_{m+1}, with the bridge's hypotheses. -/
45/-! ### How the blocks grow -/
47/-- Every supertile has at least seven children. -/
48theorem seven_kids : ∀ T : Kind, 7 ≤ nk T := by intro T; cases T <;> decide
50/-- X_{m+1} holds the children before X_m (`X.shift m` tiles) and then X_m; and it has more tiles than X_m. -/
51theorem tiles_succ (X : Chain) {m : Nat} (m_pos : 1 ≤ m) :
52 (X.block m).tiles + X.shift m ≤ (X.block (m + 1)).tiles ∧ (X.block m).tiles < (X.block (m + 1)).tiles := by
53 -- the children of X_{m+1}
54 have kids := X.kids_ok m_pos
55 -- X_m is child `c m`
57 -- which has the tiles of X_m
58 have child_tiles : (X.kidsAt m (X.c m)).tiles = (X.block m).tiles := by rw [X.kid_eq m_pos]
59 -- the children up to and including X_m
61 -- are among all the children
63 rw [X.block_succ m_pos, X.shift_eq]
65 refine ⟨by omega, ?_⟩
67 · -- X_m is the last child: there is a child before it, with a tile
68 have seven := seven_kids (X.K (m + 1))
69 -- the children before X_m include child 0
71 -- whose tiles come first
73 -- child 0 has a tile
74 have first_pos := kids.tiles_pos 0 (by omega)
76 omega
77 · -- X_m is not the last child: the next child has a tile
79 -- the tiles of the next child come after X_m
81 -- the next child has a tile
82 have next_pos := kids.tiles_pos (X.c m + 1) (by omega)
83 omega
85/-- Every level-1 supertile has at least two tiles. -/
86theorem level1_two : ∀ K, 2 ≤ (super 1 K).tiles := by intro K; cases K <;> decide
88/-- X_{m+1} has at least `m + 2` tiles. -/
90 | 0 => level1_two (X.K 1)
91 | m + 1 => by
92 -- one more tile at least, at each level
93 have grow := (X.tiles_succ (m := m + 1) (by omega)).2
94 -- and X_{m+1} has at least `m + 2`
95 have before := X.tiles_ge m
96 omega
98/-- Larger blocks have at least as many tiles. -/
99theorem tiles_mono (X : Chain) {m : Nat} (m_pos : 1 ≤ m) : ∀ k, (X.block m).tiles ≤ (X.block (m + k)).tiles
100 | 0 => Nat.le_refl _
101 | k + 1 => by
102 -- up to X_{m+k}
103 have before := X.tiles_mono m_pos k
104 -- and one more level
105 have grow := (X.tiles_succ (m := m + k) (by omega)).2
106 show _ ≤ (X.block (m + k + 1)).tiles
107 omega
109/-! ### The numbering of the union's tiles -/
111/-- `X.gid m` sends the tiles of X_m into 0 … |X_m| - 1, and `X.loc m` undoes it. -/
113 X.gid m t < (X.block m).tiles ∧ X.loc m (X.gid m t) = t
114 | 0, _, m_pos, _ => absurd m_pos (by decide)
115 | 1, _, _, ht => ⟨ht, rfl⟩
116 | m + 2, t, _, ht => by
117 -- X_{m+2} holds X_{m+1} and the children before it
118 have grow : (X.block (m + 1)).tiles + X.shift (m + 1) ≤ (X.block (m + 2)).tiles :=
119 (X.tiles_succ (m := m + 1) (by omega)).1
120 by_cases in_child : X.shift (m + 1) ≤ t ∧ t < X.shift (m + 1) + (X.block (m + 1)).tiles
121 · -- a tile of X_{m+1}: numbered as in X_{m+1}
122 obtain ⟨bound, inverse⟩ := X.loc_gid (m + 1) (t - X.shift (m + 1)) (by omega) (by omega)
124 exact ⟨by omega, by omega⟩
125 · by_cases before : t < X.shift (m + 1)
126 · -- a tile of an earlier child: numbered just after X_{m+1}
128 rw [ite_eq_right (by omega), ite_eq_left (by omega)]
129 exact ⟨by omega, by omega⟩
130 · -- a tile of a later child: keeps its number
132 rw [ite_eq_right (by omega), ite_eq_right (by omega)]
133 exact ⟨ht, rfl⟩
135/-- `X.loc m` sends 0 … |X_m| - 1 to tiles of X_m, and `X.gid m` undoes it. -/
137 X.loc m g < (X.block m).tiles ∧ X.gid m (X.loc m g) = g
138 | 0, _, m_pos, _ => absurd m_pos (by decide)
139 | 1, _, _, hg => ⟨hg, rfl⟩
140 | m + 2, g, _, hg => by
141 -- X_{m+2} holds X_{m+1} and the children before it
142 have grow : (X.block (m + 1)).tiles + X.shift (m + 1) ≤ (X.block (m + 2)).tiles :=
143 (X.tiles_succ (m := m + 1) (by omega)).1
144 by_cases old : g < (X.block (m + 1)).tiles
145 · -- a number of X_{m+1}: its tile in X_{m+1}
146 obtain ⟨bound, inverse⟩ := X.gid_loc (m + 1) g (by omega) old
148 rw [ite_eq_left ⟨by omega, by omega⟩, Nat.add_sub_cancel, inverse]
149 exact ⟨by omega, rfl⟩
150 · by_cases from_before : g < (X.block (m + 1)).tiles + X.shift (m + 1)
151 · -- a number just after X_{m+1}: a tile of an earlier child
153 rw [ite_eq_right (by omega), ite_eq_left (by omega)]
154 exact ⟨by omega, by omega⟩
155 · -- a later number: a tile of a later child, same number
157 rw [ite_eq_right (by omega), ite_eq_right (by omega)]
158 exact ⟨hg, rfl⟩
160/-- `X.gid m` is one to one on the tiles of X_m. -/
162 (ht' : t' < (X.block m).tiles) (same : X.gid m t = X.gid m t') : t = t' := by
163 -- apply `X.loc m` to both sides: it takes `X.gid m t` back to `t`
164 have back := (X.loc_gid m t m_pos ht).2
165 -- and `X.gid m t'` back to `t'`
166 have back' := (X.loc_gid m t' m_pos ht').2
167 rw [← back, ← back', same]
169/-- Going `k + 1` levels up the chain is going `k` levels up, then one more. -/
171 | 0, _, _ => rfl
172 | k + 1, m, t => by
173 show X.up (m + 1) (k + 1) (t + X.shift m) = _
174 rw [X.up_succ k (m + 1) (t + X.shift m), show m + 1 + k = m + (k + 1) by omega]
175 rfl
177/-- One level up, a tile of X_m is still a tile, and keeps its number. -/
179 X.up m 1 t < (X.block (m + 1)).tiles ∧ X.gid (m + 1) (X.up m 1 t) = X.gid m t := by
180 -- X_{m+1} holds the children before X_m, then X_m
181 have grow := (X.tiles_succ m_pos).1
182 obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
183 -- `X.up m 1 t` is `t` moved past the children before X_m
184 show t + X.shift (m' + 1) < _ ∧ X.gid (m' + 2) (t + X.shift (m' + 1)) = _
185 refine ⟨by omega, ?_⟩
187 rw [ite_eq_left ⟨by omega, by omega⟩, Nat.add_sub_cancel]
189/-- Any number of levels up, a tile of X_m is still a tile, and keeps its number. -/
191 ∀ k, X.up m k t < (X.block (m + k)).tiles ∧ X.gid (m + k) (X.up m k t) = X.gid m t
192 | 0 => ⟨ht, rfl⟩
193 | k + 1 => by
194 -- `k` levels up
195 obtain ⟨bound, same⟩ := X.gid_up m_pos ht k
196 -- and one more
197 obtain ⟨bound', same'⟩ := X.gid_up1 (m := m + k) (by omega) bound
198 rw [X.up_succ]
199 exact ⟨bound', same'.trans same⟩
201/-- The tile numbered `g`, found in X_{m+k}, is the one found in X_m, taken `k` levels up. -/
203 X.loc (m + k) g = X.up m k (X.loc m g) := by
204 -- the tile of X_m numbered `g`
205 obtain ⟨loc_bound, gid_of_loc⟩ := X.gid_loc m g m_pos hg
206 -- taken `k` levels up, it keeps its number
207 obtain ⟨up_bound, gid_of_up⟩ := X.gid_up m_pos loc_bound k
208 -- so `X.loc (m + k)` finds it
209 have found := (X.loc_gid (m + k) _ (by omega) up_bound).2
210 rw [gid_of_up, gid_of_loc] at found
211 exact found
213/-! ### Gluing goes up the chain -/
215/-- An edge glued in X_m is glued the same way, renumbered, in X_{m+1}. -/
216theorem glue_lift1 (X : Chain) {m t i t' j : Nat} (m_pos : 1 ≤ m) (ht : t < (X.block m).tiles)
217 (glued : (X.block m).glue t i = some (t', j)) : (X.block (m + 1)).glue (X.up m 1 t) i = some (X.up m 1 t', j) := by
218 -- the children of X_{m+1}
219 have kids := X.kids_ok m_pos
220 -- `t` is a tile of child `c m`, which is X_m
221 have ht_child : t < (X.kidsAt m (X.c m)).tiles := by rw [X.kid_eq m_pos]; exact ht
222 -- and the child glues it as X_m does
223 have glued_child : (X.kidsAt m (X.c m)).glue t i = some (t', j) := by rw [X.kid_eq m_pos]; exact glued
224 rw [X.block_succ m_pos]
227 rw [kids.glue_shift (X.child_lt m m_pos) ht_child]
229 rw [glued_child]
231/-- An edge glued in X_m is glued the same way any number of levels up. -/
233 (glued : (X.block m).glue t i = some (t', j)) : ∀ k, (X.block (m + k)).glue (X.up m k t) i = some (X.up m k t', j)
234 | 0 => glued
235 | k + 1 => by
236 rw [X.up_succ k m t, X.up_succ k m t']
237 exact X.glue_lift1 (m := m + k) (by omega) (X.gid_up m_pos ht k).1 (X.glue_lift m_pos ht glued k)
239/-- A gluing in X_m joins actual tiles and edges. -/
240theorem glue_ok (X : Chain) {m t i t' j : Nat} (m_pos : 1 ≤ m) (ht : t < (X.block m).tiles) (hi : i < 14)
241 (glued : (X.block m).glue t i = some (t', j)) : t' < (X.block m).tiles ∧ j < 14 :=
244/-- **Two blocks agree.** If X_m and X_{m'} both glue edge `e_i` of the tile numbered `g`, they glue it to the same
245edge of the same numbered tile. -/
246theorem glue_agree (X : Chain) {m m' t t₂ i u j u₂ j₂ : Nat} (m_pos : 1 ≤ m) (m'_pos : 1 ≤ m')
247 (ht : t < (X.block m).tiles) (ht₂ : t₂ < (X.block m').tiles) (hi : i < 14) (same : X.gid m t = X.gid m' t₂)
248 (glued : (X.block m).glue t i = some (u, j)) (glued₂ : (X.block m').glue t₂ i = some (u₂, j₂)) :
249 X.gid m u = X.gid m' u₂ ∧ j = j₂ := by
250 -- the far tiles are actual tiles
251 have far := (X.glue_ok m_pos ht hi glued).1
252 -- in both blocks
253 have far₂ := (X.glue_ok m'_pos ht₂ hi glued₂).1
254 -- both gluings, seen in X_{m+m'}, which contains both blocks: the gluing in X_m
255 have lift := X.glue_lift m_pos ht glued m'
256 -- and the gluing in X_{m'}
257 have lift₂ := X.glue_lift m'_pos ht₂ glued₂ m
258 -- the tile keeps its number up there, from X_m
259 have tile := X.gid_up m_pos ht m'
260 -- and from X_{m'}
261 have tile₂ := X.gid_up m'_pos ht₂ m
262 -- so do the far tiles, from X_m
263 have far_up := X.gid_up m_pos far m'
264 -- and from X_{m'}
265 have far_up₂ := X.gid_up m'_pos far₂ m
266 rw [show m' + m = m + m' from Nat.add_comm _ _] at lift₂ tile₂ far_up₂
267 -- the tile has the same number either way, so it is the same tile up there
268 have same_tile : X.up m' m t₂ = X.up m m' t := by
269 apply X.gid_inj (m := m + m') (by omega) tile₂.1 tile.1
270 rw [tile₂.2, tile.2, same]
271 rw [same_tile, lift] at lift₂
272 -- so the two gluings agree: the same far tile, the same edge
273 simp only [Option.some.injEq, Prod.mk.injEq] at lift₂
274 obtain ⟨same_far, same_edge⟩ := lift₂
275 refine ⟨?_, same_edge⟩
276 rw [← far_up.2, ← far_up₂.2, same_far]
278/-! ### Every edge is glued in some block, and finitely many edges in one block -/
280/-- `X.GluedAt L g i`: the tile numbered `g` is a tile of X_L, and X_L glues its edge `e_i`. -/
281def GluedAt (X : Chain) (L g i : Nat) : Prop := g < (X.block L).tiles ∧ ((X.block L).glue (X.loc L g) i).isSome
283/-- An edge glued in X_L stays glued in every larger block. -/
284theorem gluedAt_up (X : Chain) {L g i : Nat} (L_pos : 1 ≤ L) (glued : X.GluedAt L g i) (k : Nat) :
285 X.GluedAt (L + k) g i := by
286 obtain ⟨hg, is_glued⟩ := glued
287 -- the tile of X_L numbered `g`
288 have loc_bound := (X.gid_loc L g L_pos hg).1
289 obtain ⟨⟨u, j⟩, glued⟩ := Option.isSome_iff_exists.mp is_glued
290 refine ⟨?_, ?_⟩
291 · -- larger blocks have more tiles
292 have more := X.tiles_mono L_pos k
293 omega
294 · rw [X.loc_up L_pos hg, X.glue_lift L_pos loc_bound glued k]; rfl
296/-- **Where the chain covers the plane, every edge of every tile is glued in some block.** -/
297theorem gluedAt_exists (X : Chain) (covers : X.Covers) {g i : Nat} (hi : i < 14) : ∃ L, 1 ≤ L ∧ X.GluedAt L g i := by
298 -- the tile numbered `g` is a tile of X_{g+1}
299 have big := X.tiles_ge g
300 -- found there
301 obtain ⟨loc_bound, gid_of_loc⟩ := X.gid_loc (g + 1) g (by omega) (by omega)
302 -- some block X_{g+1+k} glues its edge `e_i`
303 obtain ⟨k, is_glued⟩ := covers (g + 1) _ i (by omega) loc_bound hi
304 refine ⟨g + 1 + k, by omega, ?_, ?_⟩
305 · -- larger blocks have more tiles
306 have more := X.tiles_mono (m := g + 1) (by omega) k
307 omega
308 · rw [X.loc_up (by omega) (by omega)]; exact is_glued
310/-- If each of finitely many claims holds from some level on, all of them hold from one level on. -/
311theorem exists_common {P : Nat → Nat → Prop} (mono : ∀ L k x, P L x → P (L + k) x) :
312 ∀ n, (∀ x, x < n → ∃ L, P L x) → ∃ L, ∀ x, x < n → P L x
313 | 0, _ => ⟨0, fun _ hx => absurd hx (Nat.not_lt_zero _)⟩
314 | n + 1, each => by
315 -- a common level for the first `n`
316 obtain ⟨L₁, below⟩ := exists_common mono n (fun x hx => each x (by omega))
317 -- a level for the last one
318 obtain ⟨L₂, at_n⟩ := each n (by omega)
319 refine ⟨L₁ + L₂, fun x hx => ?_⟩
320 by_cases earlier : x < n
321 · exact mono L₁ L₂ x (below x earlier)
322 · have is_n : x = n := by omega -- the last one
323 subst is_n
324 rw [Nat.add_comm]; exact mono L₂ L₁ x at_n
326/-- **All edges of the first `M` tiles are glued in one block** X_L, which contains those tiles. -/
327theorem all_glued_at (X : Chain) (covers : X.Covers) (M : Nat) :
328 ∃ L, 1 ≤ L ∧ M ≤ (X.block L).tiles ∧ ∀ g i, g < M → i < 14 → X.GluedAt L g i := by
329 -- number the edges `e_i` of the tiles `g < M` as `14 g + i`, and find one level for all of them
330 obtain ⟨L, all⟩ := exists_common (P := fun L x => X.GluedAt (L + 1) (x / 14) (x % 14))
331 (fun L k x glued => by
332 rw [show L + k + 1 = L + 1 + k by omega]
333 exact X.gluedAt_up (by omega) glued k)
334 (14 * M) (fun x _ => by
335 obtain ⟨L, L_pos, glued⟩ := X.gluedAt_exists covers (g := x / 14) (Nat.mod_lt x (by decide))
336 exact ⟨L - 1, by rw [show L - 1 + 1 = L by omega]; exact glued⟩)
337 -- go up `M` more levels, so that the block has at least `M` tiles
338 refine ⟨L + 1 + M, by omega, ?_, fun g i hg hi => ?_⟩
339 · have big := X.tiles_ge (L + M) -- X_{L+M+1} has at least `L + M + 2` tiles
340 rw [show L + 1 + M = L + M + 1 by omega]
341 omega
342 · -- the edge `14 g + i`
343 have glued := all (14 * g + i) (by omega)
344 rw [show (14 * g + i) / 14 = g by omega, show (14 * g + i) % 14 = i by omega] at glued
345 exact X.gluedAt_up (by omega) glued M
347end Chain
349/-! ### Any tiling as a strand system -/
351/-- `T` glues every edge of every tile to an edge of a different tile, and that edge back to it. -/
353 ∀ g i, i < 14 → ∃ g' j, T.glue g i = some (g', j) ∧ g' ≠ g ∧ j < 14 ∧ T.glue g' j = some (g, i)
355/-- Across every port of a tiling there is a port of another tile, and across that one lies the first. -/
356theorem tilingAcross_some {T : Tiling} (tiling : IsTiling T) {p : Port} (hp : p.2.1 < 14) :
357 ∃ q, T.across p = some q ∧ q.2.1 < 14 ∧ q.1 ≠ p.1 ∧ T.across q = some p := by
358 obtain ⟨g, i, s⟩ := p
359 simp only at hp
360 cases s with
361 | true =>
362 -- port `R(v_i)` lies on edge `e_i`
363 obtain ⟨g', j, glued, other, hj, back⟩ := tiling g i hp
364 refine ⟨(g', j, true), ?_, hj, other, ?_⟩
365 · show (T.glue g i).map _ = _
366 rw [glued]; rfl
367 · show (T.glue g' j).map _ = _
368 rw [back]; rfl
369 | false =>
370 -- port `L(v_i)` lies on edge `e_{i-1}`
371 obtain ⟨g', j, glued, other, hj, back⟩ := tiling g ((i + 13) % 14) (by omega)
372 refine ⟨(g', (j + 1) % 14, false), ?_, Nat.mod_lt _ (by omega), other, ?_⟩
373 · show (T.glue g ((i + 13) % 14)).map _ = _
374 rw [glued]; rfl
375 · show (T.glue g' (((j + 1) % 14 + 13) % 14)).map _ = _
376 -- vertex `i - 1`, then one on, is vertex `i` again
377 have round : ((i + 13) % 14 + 1) % 14 = i := by omega
379 simp only [Option.map_some, round]
381/-- **A tiling's ports, with its two pairings**: the two ends of a piece (`pieceEnd`), and straight across an edge.
382Both pair every port with a different port, and undo themselves. -/
383def tilingSys {T : Tiling} (tiling : IsTiling T) : StrandSystem NPort where
384 inside x := ⟨pieceEnd x.1, (pieceEnd_valid x.2).2⟩
385 across x := ⟨(T.across x.1).getD x.1, by
386 obtain ⟨q, across_x, q_valid, _, _⟩ := tilingAcross_some tiling x.2
387 rw [across_x]; exact q_valid⟩
388 inside_inside x := Subtype.ext (Patch.pieceEnd_pieceEnd x.1)
389 across_across x := by
390 obtain ⟨q, across_x, _, _, back⟩ := tilingAcross_some tiling x.2
391 apply Subtype.ext
392 show (T.across ((T.across x.1).getD x.1)).getD ((T.across x.1).getD x.1) = x.1
393 rw [across_x]
394 simp only [Option.getD_some, back]
395 inside_ne x same := pieceEnd_ne x.1 (congrArg Subtype.val same)
396 across_ne x same := by
397 obtain ⟨q, across_x, _, other, _⟩ := tilingAcross_some tiling x.2
398 -- the port across lies on another tile
399 have same_tile := congrArg (fun y : NPort => y.1.1) same
400 simp only [across_x, Option.getD_some] at same_tile
401 exact other same_tile
403namespace Chain
405/-! ### The union of the chain is a tiling -/
407/-- **A gluing that contains every block** (chosen, not computed). For the tile numbered `g` and its edge `e_i`: if
408some block X_{g+1+k} glues that edge, read the gluing off one such block (`Classical.choose` picks the `k`);
409otherwise nothing is glued. -/
411 open Classical in
412 if found : ∃ k, ((X.block (g + 1 + k)).glue (X.loc (g + 1 + k) g) i).isSome then
413 ((X.block (g + 1 + Classical.choose found)).glue (X.loc (g + 1 + Classical.choose found) g) i).map
414 fun e => (X.gid (g + 1 + Classical.choose found) e.1, e.2)
415 else none
417/-- The tile numbered `X.gid m t`, found in X_{m+k}, is tile `t` taken `k` levels up. -/
418theorem loc_gid_up (X : Chain) {m t : Nat} (m_pos : 1 ≤ m) (ht : t < (X.block m).tiles) (k : Nat) :
419 X.loc (m + k) (X.gid m t) = X.up m k t := by
420 -- tile `t` taken up keeps its number
421 obtain ⟨up_bound, gid_of_up⟩ := X.gid_up m_pos ht k
422 -- so `X.loc (m + k)` finds it
423 have found := (X.loc_gid (m + k) _ (by omega) up_bound).2
424 rw [gid_of_up] at found
425 exact found
427/-- **The tiling glued by `chainGlue`.** -/
428noncomputable def chainTiling (X : Chain) : Tiling := ⟨X.chainGlue⟩
430/-- **`chainTiling` contains every block.** -/
431theorem chainTiling_contains (X : Chain) : X.Contains X.chainTiling := by
432 intro m t i t' j m_pos ht hi glued
433 show X.chainGlue (X.gid m t) i = some (X.gid m t', j)
434 -- the far tile is an actual tile
435 have far := (X.glue_ok m_pos ht hi glued).1
436 -- the number of the tile
437 generalize number : X.gid m t = g
438 -- the tile numbered `g` is a tile of X_{g+1}
439 have big := X.tiles_ge g
440 -- the edge is glued in some block above X_{g+1}: in X_{g+1+m}, which also lies above X_m
441 have found : ∃ k, ((X.block (g + 1 + k)).glue (X.loc (g + 1 + k) g) i).isSome := by
442 refine ⟨m, ?_⟩
443 rw [show g + 1 + m = m + (g + 1) by omega, ← number, X.loc_gid_up m_pos ht, X.glue_lift m_pos ht glued]
444 rfl
446 rw [dite_eq_left found]
447 -- the block that `chainGlue` reads glues the edge
448 have spec := Classical.choose_spec found
449 generalize Classical.choose found = k at spec ⊢
450 obtain ⟨⟨u, j₂⟩, glued₂⟩ := Option.isSome_iff_exists.mp spec
451 -- there the tile numbered `g` is found
452 obtain ⟨loc_bound, gid_of_loc⟩ := X.gid_loc (g + 1 + k) g (by omega)
453 (by have more := X.tiles_mono (m := g + 1) (by omega) k; omega) -- X_{g+1+k} is at least as large as X_{g+1}
454 -- and X_m and that block glue the edge alike
455 have agree := X.glue_agree m_pos (by omega) ht loc_bound hi (by rw [number, gid_of_loc]) glued glued₂
456 rw [glued₂, agree.1, agree.2]
457 rfl
459/-- **Where the chain covers the plane, a gluing that contains every block is a tiling**: every edge of every tile is
460glued, to an edge of another tile, which is glued back. -/
461theorem isTiling (X : Chain) (covers : X.Covers) {T : Tiling} (contains : X.Contains T) : IsTiling T := by
462 intro g i hi
463 -- some block X_L glues the edge
464 obtain ⟨L, L_pos, hg, is_glued⟩ := X.gluedAt_exists covers (g := g) hi
465 obtain ⟨⟨t', j⟩, glued⟩ := Option.isSome_iff_exists.mp is_glued
466 -- the tile numbered `g` in X_L
467 obtain ⟨loc_bound, gid_of_loc⟩ := X.gid_loc L g L_pos hg
468 -- the far tile and edge are actual ones
469 obtain ⟨far, hj⟩ := X.glue_ok L_pos loc_bound hi glued
470 refine ⟨X.gid L t', j, ?_, ?_, hj, ?_⟩
471 · -- `T` glues as X_L does
472 have read := contains L _ i t' j L_pos loc_bound hi glued
473 rwa [gid_of_loc] at read
474 · -- X_L glues no tile to itself, and different tiles have different numbers
475 intro same
476 -- the far tile differs from the tile
477 have differ := super_noSelf L (X.K L) _ i t' j loc_bound hi glued
478 exact differ (X.gid_inj L_pos far loc_bound (same.trans gid_of_loc.symm))
479 · -- X_L glues the edge back, and `T` reads that too
480 have back := super_glueSymm L (X.K L) _ i t' j loc_bound hi glued
481 -- read by `T`
482 have read := contains L t' j _ i L_pos far hj back
483 rwa [gid_of_loc] at read
485/-! ### The blocks inside the tiling -/
487/-- Port `p` of X_m, as a port of the whole tiling. -/
490/-- The other end of a piece, before or after renumbering. -/
491theorem pieceEnd_gP (X : Chain) (m : Nat) (p : Port) : pieceEnd (X.gP m p) = X.gP m (pieceEnd p) := by
492 obtain ⟨t, i, s⟩ := p
493 rcases i with _ | _ | i <;> rfl
495/-- Across a port of X_m, the tiling continues as X_m does. -/
497 (m_pos : 1 ≤ m) {p q : Port} (p_port : (X.block m).IsPort p) (across_p : (X.block m).across p = some q) :
498 T.across (X.gP m p) = some (X.gP m q) := by
499 obtain ⟨t, i, s⟩ := p
500 obtain ⟨ht, hi⟩ := p_port
501 simp only at ht hi
502 -- the port, renumbered
503 have renumbered : X.gP m (t, i, s) = (X.gid m t, i, s) := rfl
504 rw [renumbered]
505 cases s with
506 | true =>
507 simp only [Patch.across, straightThrough] at across_p
508 cases glued : (X.block m).glue t i with
509 | none => rw [glued] at across_p; contradiction
510 | some e =>
511 obtain ⟨t', j⟩ := e
512 rw [glued] at across_p
513 simp only [Option.map_some, Option.some.injEq] at across_p
514 subst across_p
515 show (T.glue (X.gid m t) i).map _ = _
516 rw [contains m t i t' j m_pos ht hi glued]; rfl
517 | false =>
518 simp only [Patch.across, straightThrough] at across_p
519 cases glued : (X.block m).glue t ((i + 13) % 14) with
520 | none => rw [glued] at across_p; contradiction
521 | some e =>
522 obtain ⟨t', j⟩ := e
523 rw [glued] at across_p
524 simp only [Option.map_some, Option.some.injEq] at across_p
525 subst across_p
526 show (T.glue (X.gid m t) ((i + 13) % 14)).map _ = _
527 rw [contains m t _ t' j m_pos ht (by omega) glued]; rfl
529/-! ### No closed strand -/
531/-- A strand of the tiling cannot stay among the first `M` tiles if all their edges are glued in one block X_L:
532following it from a port of X_L would never reach the rim of X_L. -/
533theorem follow_stays (X : Chain) {T : Tiling} (contains : X.Contains T)
534 (tiling : IsTiling T) {L M : Nat} (L_pos : 1 ≤ L) (all_glued : ∀ g i, g < M → i < 14 → X.GluedAt L g i) :
535 ∀ p r, (X.block L).Follow p r → (X.block L).IsPort p →
537 -- X_L has the signature
539 intro p r follows
540 induction follows with
541 | @leave p nothing_across =>
542 intro p_port x x_eq bounded
543 -- the tile of `p` is among the first `M`
544 have below : X.gid L p.1 < M := by
545 -- the strand starts at `x`, on one of them
546 have start := bounded 0
547 change x.1.1 < _ at start
548 rw [← x_eq] at start; exact start
549 -- X_L finds the tile of `p` by its number
550 have found := (X.loc_gid L p.1 L_pos p_port.1).2
551 -- every edge of it is glued in X_L
552 have edges_glued : ∀ i, i < 14 → ((X.block L).glue p.1 i).isSome := by
553 intro i hi
554 have glued := (all_glued _ i below hi).2 -- glued at the tile numbered `X.gid L p.1`
555 rwa [found] at glued
556 -- the other end of the piece is on the same tile
557 have end_valid := pieceEnd_valid p_port.2
558 -- so something lies across it, yet the strand leaves X_L there
559 have across_end := across_isSome edges_glued end_valid.1 end_valid.2
560 rw [nothing_across] at across_end
561 contradiction
562 | @next p q r across_end _ ih =>
563 intro p_port x x_eq bounded
564 -- the other end of the piece is on the same tile
565 have end_valid := pieceEnd_valid p_port.2
566 -- so it is a port of X_L
568 -- and so is the port `q` across from it
569 have q_port : (X.block L).IsPort q := Patch.across_valid sig end_port.1 end_port.2 across_end
570 -- `q` is the next port of the strand in the tiling
573 rw [← x_eq, X.pieceEnd_gP, X.across_gP contains L_pos end_port across_end]
574 rfl
575 -- the strand from there is the rest of the strand from `x`
577 -- its ports are ports of the strand from `x`, so on the first `M` tiles
578 have later := bounded (k + 1)
579 rw [StrandSystem.walk, iter_succ'] at later
580 exact later
582/-- **No strand of the tiling is closed.** A closed strand visits finitely many tiles; all their edges are glued in
583one block, and following the strand there never reaches the rim, against Theorem A. -/
584theorem not_closed (X : Chain) (covers : X.Covers) {T : Tiling} (contains : X.Contains T)
586 rintro ⟨n, n_pos, back⟩
587 -- the strand only ever visits the ports reached in its first `n` steps
588 have periodic : ∀ k, ∃ j, j < n ∧ (tilingSys tiling).walk x k = (tilingSys tiling).walk x j := by
589 intro k
590 induction k with
591 | zero => exact ⟨0, n_pos, rfl⟩
592 | succ k ih =>
593 obtain ⟨j, hj, same⟩ := ih
594 by_cases wraps : j + 1 = n
595 · refine ⟨0, n_pos, ?_⟩
596 rw [StrandSystem.walk_succ, same, ← StrandSystem.walk_succ, wraps, back]
597 rfl
598 · exact ⟨j + 1, by omega, by rw [StrandSystem.walk_succ, same, ← StrandSystem.walk_succ]⟩
599 -- the tiles of those ports have numbers below some bound `M`
601 intro m
602 induction m with
603 | zero => exact ⟨0, fun j hj => absurd hj (by omega)⟩
604 | succ m ih =>
605 obtain ⟨M, below⟩ := ih
607 by_cases earlier : j < m
608 · have := below j earlier -- an earlier port: below `M`
609 omega
610 · have is_m : j = m := by omega -- port `m` itself
611 subst is_m; omega
612 obtain ⟨M, below⟩ := bounded n
613 -- every port of the strand is on one of the first `M` tiles
615 intro k
616 obtain ⟨j, hj, same⟩ := periodic k
617 rw [same]; exact below j hj
618 -- one block X_L glues every edge of those tiles, and contains them
619 obtain ⟨L, L_pos, M_le, all_glued⟩ := X.all_glued_at covers M
620 -- the start `x`, as a port of X_L
621 obtain ⟨loc_bound, gid_of_loc⟩ := X.gid_loc L x.1.1 L_pos (by have := in_first 0; exact Nat.lt_of_lt_of_le this M_le)
622 -- it is a port of X_L
623 have start : (X.block L).IsPort (X.loc L x.1.1, x.1.2.1, x.1.2.2) := ⟨loc_bound, x.2⟩
624 -- Theorem A says the strand leaves X_L
626 refine X.follow_stays contains tiling L_pos all_glued _ r follows start x ?_ in_first
627 show (X.gid L (X.loc L x.1.1), x.1.2.1, x.1.2.2) = x.1
628 rw [gid_of_loc]
630end Chain
632/-! ### The theorems -/
634/-- **`ChainModel`**: the union of a chain is a tiling. -/
635theorem chainModel : ChainModel := fun X =>
636 ⟨fun g => by
637 -- X_{g+1} has at least `g + 2` tiles
638 have := X.tiles_ge g
639 omega,
640 fun m t m_pos ht => X.loc_gid m t m_pos ht,
641 fun m g m_pos hg => X.gid_loc m g m_pos hg,
642 fun _ _ m_pos ht => (X.gid_up1 m_pos ht).2,
643 ⟨X.chainTiling, X.chainTiling_contains⟩,
644 fun covers _ contains => X.isTiling covers contains⟩
646/-- **Theorem A in strand form** (as stated in `Statement.lean`): in a tiling whose hierarchy covers the plane, every
647strand is a two-way infinite path. -/
648theorem theoremA_strand : TheoremA_strand := by
649 intro X T covers contains p hp
650 -- the union of the chain is a tiling
651 have tiling := X.isTiling covers contains
652 -- its strand system, and the start
655 -- following the strand forwards, as ports
657 intro k
658 induction k with
659 | zero => rfl
661 -- and backwards
663 intro k
664 induction k with
665 | zero => rfl
667 -- Lemma 3.4: the strand is closed or a two-way infinite path; it is not closed
668 obtain ⟨distinct, back_distinct, apart, no_piece_twice⟩ :=
669 (S.closed_or_path start).resolve_left (X.not_closed covers contains tiling start)
670 refine ⟨?_, ?_, ?_, ?_⟩
671 · -- (1) forwards, no port twice
672 intro i j same
673 rw [forwards, forwards] at same
674 exact distinct i j (Subtype.ext same)
675 · -- (2) backwards, no port twice
676 intro a a' same
677 rw [backwards, backwards] at same
678 exact back_distinct a a' (Subtype.ext same)
679 · -- (3) backwards never meets forwards, except at the start
680 intro a b same
681 rw [backwards, forwards] at same
682 exact apart a b (Subtype.ext same)
683 · -- (4) no piece twice
684 intro i j same
685 rw [forwards, forwards] at same
686 exact no_piece_twice i j (Subtype.ext same)
688/-! ### The nest is a chain that covers -/
690/-- **The nest as a chain**: every block a Δ, child 1 of the next (Table 1: child 1 of a Δ is a Δ). -/
692 K _ := .Delta
693 c _ := 1
694 child_lt _ _ := show 1 < (Pattern.kids .Delta).length by decide
695 child_kind _ _ := rfl
697/-- In the nest chain, a block starts where it does in the nest: after child 0, a Ξ. -/
698theorem nestChain_shift (b : Nat) : nestChain.shift b = nestShift b := rfl
700/-- In the nest chain, a tile goes up as in the nest. -/
701theorem nestChain_up : ∀ k b t, nestChain.up b k t = up b k t
702 | 0, _, _ => rfl
703 | k + 1, b, t => by
705 rw [nestChain_shift]
706 exact nestChain_up k (b + 1) _
708/-- **`NestCovers`** (as stated in `Statement.lean`): the nest chain covers, since every edge of `N_b` is glued in
709`N_{b+2}` (`no_boundary`, the paper's Lemma 8.3(b)). -/
710theorem nestCovers : NestCovers := by
712 -- two levels up, as in the nest
713 rw [nestChain_up]
714 -- where the edge is glued
715 exact no_boundary b_pos ht hi
717end SpectreKnot.Statement