The Spectre Knot the proofPictures and ideas →
Draft proof, not peer reviewed. What has been checked

lean/SpectreKnot/ProofStrand.lean

749 lines · 40 declarations, each with its own page · on GitHub ·

Theorem B, final form (theoremB_strand): the ribbons of the nest tiling form one two-way infinite strand.

← SpectreKnot/ProofB.leanSpectreKnot/ProofChain.lean →

All 39 files, and the declarations of this one
1/-
2**Theorem B, final form** (`theoremB_strand`): the ribbons of the nest tiling form one two-way infinite strand.
3
4The nest tiling is built as one tiling (`Statement.lean` §6): its tiles are numbered so that every block `N_b` keeps
5its own numbering, and its gluing is read off the blocks (`nestModel`). Its ports, with the two pairings "other end of
6the piece" and "straight across the edge", form a `StrandSystem` (`nestSys`). In it no strand is closed, because a
7closed strand would stay inside one block, which has no closed strand (Theorem A); and any two ports lie on one strand,
8because they do in a large enough block (Theorem B (3)). Lemma 3.4 (`StrandSystem.closed_or_path`) then says the
9strand is a two-way infinite path, and it runs through every port.
10-/
14/-! ### The strand of a port, port by port (for any strand system) -/
16namespace SpectreKnot.StrandSystem
18variable {P : Type} (S : StrandSystem P)
20/-- `S.Same p q`: port `q` is reached from port `p` by moving along pieces and across edges, any number of times:
21`q` is on the strand of `p`. -/
22inductive Same (p : P) : P → Prop
23 | refl : Same p p
24 | inside {q : P} : Same p q → Same p (S.inside q)
25 | across {q : P} : Same p q → Same p (S.across q)
27/-- **A strand, port by port**: every port on the strand of `p` is reached by following it forwards or backwards
28from `p`, or is the other end of the piece of a port so reached. -/
29theorem same_orbit {p q : P} (same : S.Same p q) : ∃ k, q = S.walk p k ∨ q = iter S.prev k p ∨
30 q = S.inside (S.walk p k) ∨ q = S.inside (iter S.prev k p) := by
31 induction same with
32 | refl => exact ⟨0, Or.inl rfl⟩
33 | @inside q _ ih =>
34 -- the other end of the piece swaps the first two forms with the last two
35 obtain ⟨k, reached | reached | reached | reached⟩ := ih <;> subst reached
36 · exact ⟨k, Or.inr (Or.inr (Or.inl rfl))⟩
37 · exact ⟨k, Or.inr (Or.inr (Or.inr rfl))⟩
38 · exact ⟨k, Or.inl (S.inside_inside _)⟩
39 · exact ⟨k, Or.inr (Or.inl (S.inside_inside _))⟩
40 | @across q _ ih =>
41 obtain ⟨k, reached | reached | reached | reached⟩ := ih <;> subst reached
42 · cases k with
43 | zero =>
44 -- across the start: the other end of the piece of the port one step back
45 refine ⟨1, Or.inr (Or.inr (Or.inr ?_))⟩
46 show S.across p = S.inside (S.inside (S.across p))
47 rw [S.inside_inside]
48 | succ k =>
49 -- across a port reached forwards: the other end of the piece of the port before it
50 exact ⟨k, Or.inr (Or.inr (Or.inl (by rw [walk_succ, next, S.across_across])))⟩
51 · -- across a port reached backwards: the other end of the piece of the next port back
52 exact ⟨k + 1, Or.inr (Or.inr (Or.inr (by rw [iter_succ, prev, S.inside_inside])))⟩
53 · -- across the other end of the piece of a port reached forwards: one step further forwards
54 exact ⟨k + 1, Or.inl rfl⟩
55 · cases k with
56 | zero =>
57 -- across the other end of the start's piece: one step forwards
58 exact ⟨1, Or.inl rfl⟩
59 | succ k =>
60 -- across the other end of the piece of a port reached backwards: one step less back
61 refine ⟨k, Or.inr (Or.inl ?_)⟩
62 show S.next (iter S.prev (k + 1) p) = _
65end SpectreKnot.StrandSystem
67namespace SpectreKnot.Statement
69open Pattern Compose Gluing
71/-! ### How the blocks grow -/
73/-- Child 0 of `N_{b+1}`, which comes before `N_b`, has at least one tile. -/
74theorem nestShift_pos (b : Nat) : 1 ≤ nestShift b := by
75 rcases Nat.eq_zero_or_pos b with rfl | b_pos
76 · -- level 0: child 0 is a single tile
77 decide
78 · -- level b ≥ 1: a supertile with the signature has a tile
79 exact (good b .Xi b_pos).sig.tiles_pos
81/-- `N_{b+1}` holds child 0 (`nestShift b` tiles) and then `N_b`, so it has at least that many tiles. -/
82theorem tiles_succ (b : Nat) : (N b).tiles + nestShift b ≤ (N (b + 1)).tiles := by
83 rcases Nat.eq_zero_or_pos b with rfl | b_pos
84 · -- N_0 is one tile and N_1 has nine
85 decide
86 · rw [N_succ b_pos]
87 -- the first two children together: child 0, then child 1 = N_b
88 have first_two : offC (kidsD b) 2 = nestShift b + (N b).tiles := by
89 rw [offC_succ, offC_succ, show offC (kidsD b) 0 = 0 from rfl, Nat.zero_add]; rfl
90 -- the parent has at least the tiles of its first two children
91 have two_le_all := offC_mono (kidsD b) (show 2 ≤ nk .Delta by decide)
92 show _ ≤ offC (kidsD b) (nk .Delta)
93 omega
95/-- `N_b` has more than `b` tiles. -/
96theorem tiles_ge : ∀ b, b + 1 ≤ (N b).tiles
97 | 0 => by decide
98 | b + 1 => by
99 -- one more tile at least, at each level: `N_{b+1}` holds `N_b` and child 0
100 have grow := tiles_succ b
101 -- which has a tile
102 have shift_pos := nestShift_pos b
103 -- and `N_b` has more than `b` tiles
104 have before := tiles_ge b
105 omega
107/-! ### The numbering of the nest tiling's tiles -/
109/-- `gid b` sends the tiles of `N_b` into 0 … |N_b| - 1, and `loc b` undoes it. -/
110theorem loc_gid : ∀ b t, t < (N b).tiles → gid b t < (N b).tiles ∧ loc b (gid b t) = t
111 | 0, _, ht => ⟨ht, rfl⟩
112 | b + 1, t, ht => by
113 -- `N_{b+1}` holds `N_b` and child 0
114 have grow := tiles_succ b
115 by_cases in_child1 : nestShift b ≤ t ∧ t < nestShift b + (N b).tiles
116 · -- a tile of child 1 (that is, of N_b): numbered as in N_b
117 obtain ⟨bound, inverse⟩ := loc_gid b (t - nestShift b) (by omega)
118 simp only [gid, loc, ite_eq_left in_child1, ite_eq_left bound, inverse]
119 exact ⟨by omega, by omega⟩
120 · by_cases in_child0 : t < nestShift b
121 · -- a tile of child 0: numbered just after N_b
122 simp only [gid, loc, ite_eq_right in_child1, ite_eq_left in_child0]
123 rw [ite_eq_right (by omega), ite_eq_left (by omega)]
124 exact ⟨by omega, by omega⟩
125 · -- a tile of a later child: keeps its number
126 simp only [gid, loc, ite_eq_right in_child1, ite_eq_right in_child0]
127 rw [ite_eq_right (by omega), ite_eq_right (by omega)]
128 exact ⟨ht, rfl⟩
130/-- `loc b` sends 0 … |N_b| - 1 to tiles of `N_b`, and `gid b` undoes it. -/
131theorem gid_loc : ∀ b g, g < (N b).tiles → loc b g < (N b).tiles ∧ gid b (loc b g) = g
132 | 0, _, hg => ⟨hg, rfl⟩
133 | b + 1, g, hg => by
134 -- `N_{b+1}` holds `N_b` and child 0
135 have grow := tiles_succ b
136 by_cases old : g < (N b).tiles
137 · -- a number of N_b: its tile in child 1
138 obtain ⟨bound, inverse⟩ := gid_loc b g old
139 simp only [loc, ite_eq_left old, gid]
140 rw [ite_eq_left ⟨by omega, by omega⟩, Nat.add_sub_cancel, inverse]
141 exact ⟨by omega, rfl⟩
142 · by_cases from_child0 : g < (N b).tiles + nestShift b
143 · -- a number just after N_b: a tile of child 0
144 simp only [loc, ite_eq_right old, ite_eq_left from_child0, gid]
145 rw [ite_eq_right (by omega), ite_eq_left (by omega)]
146 exact ⟨by omega, by omega⟩
147 · -- a later number: a tile of a later child, same number
148 simp only [loc, ite_eq_right old, ite_eq_right from_child0, gid]
149 rw [ite_eq_right (by omega), ite_eq_right (by omega)]
150 exact ⟨hg, rfl⟩
152/-- `gid b` is one to one on the tiles of `N_b`. -/
153theorem gid_inj {b t t' : Nat} (ht : t < (N b).tiles) (ht' : t' < (N b).tiles) (same : gid b t = gid b t') :
154 t = t' := by
155 -- apply `loc b` to both sides: it takes `gid b t` back to `t`
156 have back := (loc_gid b t ht).2
157 -- and `gid b t'` back to `t'`
158 have back' := (loc_gid b t' ht').2
159 rw [← back, ← back', same]
161/-- One level up, a tile of `N_b` is still a tile, and keeps its number. -/
162theorem gid_up1 {b t : Nat} (ht : t < (N b).tiles) :
163 up b 1 t < (N (b + 1)).tiles ∧ gid (b + 1) (up b 1 t) = gid b t := by
164 -- `N_{b+1}` holds child 0 and then `N_b`
165 have grow := tiles_succ b
166 -- `up b 1 t` is `t` moved past child 0
167 show t + nestShift b < _ ∧ gid (b + 1) (t + nestShift b) = gid b t
168 refine ⟨by omega, ?_⟩
169 simp only [gid]
170 rw [ite_eq_left ⟨by omega, by omega⟩, Nat.add_sub_cancel]
172/-- Any number of levels up, a tile of `N_b` is still a tile, and keeps its number. -/
173theorem gid_up {b t : Nat} (ht : t < (N b).tiles) :
174 ∀ k, up b k t < (N (b + k)).tiles ∧ gid (b + k) (up b k t) = gid b t
175 | 0 => ⟨ht, rfl⟩
176 | k + 1 => by
177 -- one more level on top of `k` levels
178 obtain ⟨bound, same⟩ := gid_up ht k
179 obtain ⟨bound', same'⟩ := gid_up1 bound
181 exact ⟨bound', same'.trans same⟩
183/-! ### Gluing goes up the nest -/
185/-- An edge glued in `N_b` is glued the same way, renumbered, in `N_{b+1}`. -/
186theorem glue_lift1 {b t i t' j : Nat} (ht : t < (N b).tiles) (glued : (N b).glue t i = some (t', j)) :
187 (N (b + 1)).glue (up b 1 t) i = some (up b 1 t', j) := by
188 rcases Nat.eq_zero_or_pos b with rfl | b_pos
189 · -- `N_0` is a single tile: nothing is glued
190 exact absurd glued (by simp [N, super, tile])
191 · rw [N_succ b_pos]
192 -- the children of `N_{b+1}`
193 have kids := KD b_pos
194 -- the same gluing, seen in child 1
195 have glued_child : (kidsD b 1).glue t i = some (t', j) := glued
196 show (Par b).glue (t + offC (kidsD b) 1) i = some (t' + offC (kidsD b) 1, j)
197 rw [kids.glue_shift (c := 1) (by decide) ht]
198 unfold glueAt
199 rw [glued_child]
201/-- An edge glued in `N_b` is glued the same way any number of levels up. -/
202theorem glue_lift {b t i t' j : Nat} (ht : t < (N b).tiles) (glued : (N b).glue t i = some (t', j)) :
203 ∀ k, (N (b + k)).glue (up b k t) i = some (up b k t', j)
204 | 0 => glued
205 | k + 1 => by
206 rw [up_succ k b t, up_succ k b t']
207 exact glue_lift1 (gid_up ht k).1 (glue_lift ht glued k)
209/-! ### No tile is glued to itself -/
211/-- No edge of a tile is glued to an edge of the same tile. -/
212def NoSelf (P : Patch) : Prop := ∀ t i t' j, t < P.tiles → i < 14 → P.glue t i = some (t', j) → t' ≠ t
214/-- The kernel's check of the level-1 data. -/
215def level1NoSelf (K : Kind) : Bool :=
216 (List.range (level1 K).tiles).all fun t => (List.range 14).all fun i =>
217 match (level1 K).glue t i with
218 | none => true
219 | some (t', _) => t' != t
221/-- The check passes for all nine kinds. -/
222theorem level1NoSelf_all : ∀ K, level1NoSelf K = true := by intro K; cases K <;> decide +kernel
224/-- No level-1 supertile glues a tile to itself. -/
225theorem level1_noSelf (K : Kind) : NoSelf (level1 K) := by
226 intro t i t' j ht hi glued
227 -- the kernel's check
228 have check := level1NoSelf_all K
229 simp only [level1NoSelf, List.all_eq_true, List.mem_range] at check
230 -- at tile `t` and edge `i`
231 have at_edge := check t ht i hi
232 rw [glued] at at_edge
233 simpa using at_edge
235/-- A sibling glued to side `j` of child `c` is a different child. -/
236theorem mate_other_child {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool} (len_pos : ∀ c j, 1 ≤ L c j)
237 {c k c' k' : Nat} (hc : c < nk T) (hk : k < pos (L c) 6)
238 (mated : (Comp.ofLens T L d ω).toGluing.mate c k = some (c', k')) : c' ≠ c := by
239 -- the side `j` and offset `o` of the edge `k`
240 obtain ⟨j, o, hj, ho, rfl⟩ := decomp (L c) 6 (Nat.le_refl _) k hk
241 -- the gluing formula: across side `j` lies whatever Table 2 says
242 have formula := ofLens_mate (d := d) (ω := ω) (fun c _ j _ => len_pos c j) hc hj ho
243 change (Comp.ofLens T L d ω).mate c (pos (L c) j + o) = some (c', k') at mated
244 rw [formula] at mated
245 cases table : adjAt T c j with
246 | none => rw [table] at mated; contradiction
247 | some sib =>
248 obtain ⟨sib_child, sib_side⟩ := sib
249 rw [table] at mated
250 simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at mated
251 obtain ⟨rfl, _⟩ := mated
252 -- Table 2 never glues a child to itself
253 exact (adj_valid hc hj table).2.2.1
255/-- If no child glues a tile to itself, neither does the parent. -/
256theorem Kids.noSelf {T : Kind} {child : Nat → Patch} {L : Nat → Nat → Nat} {d : Nat} {ω o : Bool}
257 (kids : Kids T child L d ω o) (children : ∀ c, c < nk T → NoSelf (child c)) : NoSelf (compose T child) := by
258 -- the composition is well formed
259 have wf := kids.csig.wf
260 intro t i t' j ht hi glued
261 -- the child `c` that tile `t` belongs to, and its number `t₀` there
262 obtain ⟨c, hc, lo, hi_c⟩ := owner_exists child (nk T) t ht
263 obtain ⟨t₀, rfl⟩ : ∃ t₀, t = t₀ + offC child c := ⟨t - offC child c, by omega⟩
264 -- `t₀` is a tile of child `c`
265 have ht₀ : t₀ < (child c).tiles := by omega
266 -- which has the signature
267 have sig := kids.sig c hc
268 cases inside : (child c).glue t₀ i with
269 | some e =>
270 -- glued inside the child: the child's own tile, shifted
271 obtain ⟨t₂, j₂⟩ := e
272 rw [kids.glue_shift hc ht₀] at glued
273 simp only [glueAt, inside, Option.some.injEq, Prod.mk.injEq] at glued
274 obtain ⟨rfl, rfl⟩ := glued
275 -- the child glues it to a different tile
276 have differ := children c hc t₀ i t₂ j₂ ht₀ hi inside
277 omega
278 | none =>
279 -- on the child's rim, at rim edge `k`: glued to a sibling's edge
280 obtain ⟨k, hk, at_k⟩ := sig.rim_all t₀ i ht₀ hi inside
281 -- the parent glues rim edge `k` as the gluing's `mate` says
282 have formula := kids.glue_rimEdge hc hk
283 rw [at_k] at formula
284 rw [formula] at glued
285 cases mated : (Comp.ofLens T L d ω).toGluing.mate c k with
286 | none => rw [mated] at glued; contradiction
287 | some m =>
288 obtain ⟨c', k'⟩ := m
289 rw [mated] at glued
290 simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at glued
291 obtain ⟨rfl, rfl⟩ := glued
292 -- `c` is a child of the gluing
293 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact hc
294 -- the sibling is an actual child, and the edge a real rim edge of it
295 obtain ⟨sib_lt_n, sib_edge_lt, _⟩ := wf.mate_valid c k c' k' c_lt_n (by rw [kids.E_eq hc]; exact hk) mated
296 -- the sibling is a child of the composition
297 have sib_lt : c' < nk T := by rwa [ofLens_n] at sib_lt_n
298 -- its rim edge `k'` is an edge of an actual tile of it
299 have on_rim := (kids.sig c' sib_lt).rim_ok k' (by rw [← kids.E_eq sib_lt]; exact sib_edge_lt)
300 -- it is a different child
301 have other := mate_other_child (d := d) (ω := ω) kids.len_pos hc
302 (by rw [← ofLens_E (d := d) (ω := ω) hc, kids.E_eq hc]; exact hk) mated
303 intro same
304 -- two tiles of different children have different numbers in the parent
305 have same_child := owner_unique child on_rim.1 ht₀ (by omega)
306 exact other same_child.1
308/-- No supertile glues a tile to itself. -/
309theorem super_noSelf : ∀ m K, NoSelf (super m K)
310 | 0, _ => fun _ _ _ _ _ _ glued => by simp [super, tile] at glued
311 | 1, K => level1_noSelf K
312 | m + 2, T => (kids_at (m := m + 1) (by omega) T (fun K => good (m + 1) K (by omega))).noSelf
313 (fun c _ => super_noSelf (m + 1) _)
315/-! ### The nest tiling is a tiling -/
317/-- A gluing in `N_b` joins actual tiles and edges. -/
318theorem glue_ok_N (b : Nat) {t i t' j : Nat} (ht : t < (N b).tiles) (hi : i < 14)
319 (glued : (N b).glue t i = some (t', j)) : t' < (N b).tiles ∧ j < 14 := by
320 rcases Nat.eq_zero_or_pos b with rfl | b_pos
321 · -- `N_0` is a single tile: nothing is glued
322 exact absurd glued (by simp [N, super, tile])
323 · exact (good b .Delta b_pos).sig.glue_ok t i t' j ht hi glued
325/-- **Part (d)**: the nest tiling glues as every block does. -/
326theorem nestGlue_ext {b t i t' j : Nat} (ht : t < (N b).tiles) (hi : i < 14)
327 (glued : (N b).glue t i = some (t', j)) : nestGlue (gid b t) i = some (gid b t', j) := by
328 -- the far tile is an actual tile of `N_b`
329 have far_bound := (glue_ok_N b ht hi glued).1
330 generalize gid_eq : gid b t = g
331 -- `nestGlue` reads tile number `g` off `N_{g+3}`, where it is `up (g + 1) 2 (loc (g + 1) g)`
332 have big := tiles_ge (g + 1)
333 obtain ⟨loc_bound, gid_of_loc⟩ := gid_loc (g + 1) g (by omega)
334 obtain ⟨up_bound, gid_of_up⟩ := gid_up loc_bound 2
335 -- `N_{g+3}` glues every edge of that tile
336 have edge_glued := no_boundary (b := g + 1) (by omega) loc_bound hi
337 obtain ⟨⟨t'', j''⟩, glued''⟩ := Option.isSome_iff_exists.mp edge_glued
338 -- the far tile there is an actual tile of `N_{g+3}`
339 have far_bound'' := (glue_ok_N (g + 1 + 2) up_bound hi glued'').1
340 -- both gluings, seen in `N_{b+g+3}`, which contains both blocks: the gluing in `N_b`
341 have lift_b := glue_lift ht glued (g + 1 + 2)
342 -- and the gluing in `N_{g+3}`
343 have lift_g := glue_lift up_bound glued'' b
344 -- the tile keeps its number up there, from `N_b`
345 have tile_b := gid_up ht (g + 1 + 2)
346 -- and from `N_{g+3}`
347 have tile_g := gid_up up_bound b
348 -- so do the far tiles, from `N_b`
349 have far_b := gid_up far_bound (g + 1 + 2)
350 -- and from `N_{g+3}`
351 have far_g := gid_up far_bound'' b
352 rw [show g + 1 + 2 + b = b + (g + 1 + 2) by omega] at lift_g tile_g far_g
353 -- the tile has the same number either way, so it is the same tile up there
354 have same_tile : up (g + 1 + 2) b (up (g + 1) 2 (loc (g + 1) g)) = up b (g + 1 + 2) t := by
355 apply gid_inj tile_g.1 tile_b.1
356 rw [tile_g.2, tile_b.2, gid_of_up, gid_of_loc, gid_eq]
357 rw [same_tile, lift_b] at lift_g
358 -- so the two gluings agree: the same far tile, the same edge
359 simp only [Option.some.injEq, Prod.mk.injEq] at lift_g
360 obtain ⟨same_far, rfl⟩ := lift_g
361 -- the far tile's number, read off either block
362 have far_number := far_g.2
363 rw [← same_far, far_b.2] at far_number
364 unfold nestGlue
365 rw [show g + 3 = g + 1 + 2 from rfl, glued'']
366 simp only [Option.map_some, far_number]
368/-- **Part (e)**: every edge of every tile of the nest tiling is glued, to an edge of another tile, which is glued
369back to it. -/
370theorem nestGlue_some (g i : Nat) (hi : i < 14) :
371 ∃ g' j, nestGlue g i = some (g', j) ∧ g' ≠ g ∧ j < 14 ∧ nestGlue g' j = some (g, i) := by
372 -- tile number `g` as a tile of `N_{g+1}`, and of `N_{g+3}`
373 have big := tiles_ge (g + 1)
374 obtain ⟨loc_bound, gid_of_loc⟩ := gid_loc (g + 1) g (by omega)
375 obtain ⟨up_bound, gid_of_up⟩ := gid_up loc_bound 2
376 -- `N_{g+3}` glues the edge, to an actual edge of an actual tile
377 obtain ⟨⟨t', j⟩, glued⟩ := Option.isSome_iff_exists.mp (no_boundary (b := g + 1) (by omega) loc_bound hi)
378 obtain ⟨far_bound, hj⟩ := glue_ok_N (g + 1 + 2) up_bound hi glued
379 -- and glues it back
380 have back := super_glueSymm (g + 1 + 2) .Delta _ i t' j up_bound hi glued
381 -- the tile's number in the nest tiling is `g`
382 have number : gid (g + 1 + 2) (up (g + 1) 2 (loc (g + 1) g)) = g := by rw [gid_of_up, gid_of_loc]
383 refine ⟨gid (g + 1 + 2) t', j, ?_, ?_, hj, ?_⟩
384 · -- `nestGlue` reads exactly this gluing
385 unfold nestGlue
386 rw [show g + 3 = g + 1 + 2 from rfl, glued]
387 rfl
388 · -- a different tile of `N_{g+3}`, so a different number
389 intro same
390 -- `N_{g+3}` glues no tile to itself
391 have differ := super_noSelf (g + 1 + 2) .Delta _ i t' j up_bound hi glued
392 exact differ (gid_inj far_bound up_bound (same.trans number.symm))
393 · have glued_back := nestGlue_ext far_bound hj back -- the gluing back, read by part (d)
394 rw [number] at glued_back
395 exact glued_back
In the paper Theorem B The Ariadne Theorem
397/-- **`NestModel`**: the nest tiling is a tiling, and it is the union of the blocks. -/
398theorem nestModel : NestModel :=
399 ⟨fun g => by
400 -- `N_{g+1}` has more than `g + 1` tiles
401 have := tiles_ge (g + 1)
402 omega,
405 fun _ _ ht => (gid_up1 ht).2,
406 fun _ _ _ _ _ ht hi glued => nestGlue_ext ht hi glued,
409/-! ### The nest tiling's strands -/
411/-- The ports of the nest tiling: a tile number, a vertex `0 … 13` of the tile, and a hand. -/
412abbrev NPort := {p : Port // p.2.1 < 14}
414/-- The other end of a piece is a different port. -/
415theorem pieceEnd_ne (p : Port) : pieceEnd p ≠ p := by
416 obtain ⟨t, i, s⟩ := p
417 rcases i with _ | _ | i <;> cases s <;> simp [pieceEnd]
419/-- Across every port of the nest tiling there is a port of another tile, and across that one lies the first. -/
420theorem nestAcross_some {p : Port} (hp : p.2.1 < 14) :
421 ∃ q, nestTiling.across p = some q ∧ q.2.1 < 14 ∧ q.1 ≠ p.1 ∧ nestTiling.across q = some p := by
422 obtain ⟨g, i, s⟩ := p
423 simp only at hp
424 cases s with
425 | true =>
426 -- port `R(v_i)` lies on edge `e_i`
427 obtain ⟨g', j, glued, other, hj, back⟩ := nestGlue_some g i hp
428 refine ⟨(g', j, true), ?_, hj, other, ?_⟩
429 · show (nestGlue g i).map _ = _
430 rw [glued]; rfl
431 · show (nestGlue g' j).map _ = _
432 rw [back]; rfl
433 | false =>
434 -- port `L(v_i)` lies on edge `e_{i-1}`
435 obtain ⟨g', j, glued, other, hj, back⟩ := nestGlue_some g ((i + 13) % 14) (by omega)
436 refine ⟨(g', (j + 1) % 14, false), ?_, Nat.mod_lt _ (by omega), other, ?_⟩
437 · show (nestGlue g ((i + 13) % 14)).map _ = _
438 rw [glued]; rfl
439 · show (nestGlue g' (((j + 1) % 14 + 13) % 14)).map _ = _
440 -- vertex `i - 1`, then one on, is vertex `i` again
441 have round : ((i + 13) % 14 + 1) % 14 = i := by omega
442 rw [mod14 hj, back]
443 simp only [Option.map_some, round]
445/-- **The nest tiling's ports, with its two pairings**: the two ends of a piece (`pieceEnd`), and straight across an
446edge (`nestTiling.across`). Both pair every port with a different port, and undo themselves. -/
447def nestSys : StrandSystem NPort where
448 inside x := ⟨pieceEnd x.1, (pieceEnd_valid x.2).2⟩
449 across x := ⟨(nestTiling.across x.1).getD x.1, by
450 obtain ⟨q, across_x, q_valid, _, _⟩ := nestAcross_some x.2
451 rw [across_x]; exact q_valid⟩
452 inside_inside x := Subtype.ext (Patch.pieceEnd_pieceEnd x.1)
453 across_across x := by
454 obtain ⟨q, across_x, _, _, back⟩ := nestAcross_some x.2
455 apply Subtype.ext
456 show (nestTiling.across ((nestTiling.across x.1).getD x.1)).getD ((nestTiling.across x.1).getD x.1) = x.1
457 rw [across_x]
458 simp only [Option.getD_some, back]
459 inside_ne x same := pieceEnd_ne x.1 (congrArg Subtype.val same)
460 across_ne x same := by
461 obtain ⟨q, across_x, _, other, _⟩ := nestAcross_some x.2
462 -- the port across lies on another tile
463 have same_tile := congrArg (fun y : NPort => y.1.1) same
464 simp only [across_x, Option.getD_some] at same_tile
465 exact other same_tile
467/-! ### The blocks inside the nest tiling -/
469/-- Port `p` of `N_b`, as a port of the nest tiling. -/
470def gP (b : Nat) (p : Port) : Port := (gid b p.1, p.2.1, p.2.2)
472/-- The other end of a piece, before or after renumbering. -/
473theorem pieceEnd_gP (b : Nat) (p : Port) : pieceEnd (gP b p) = gP b (pieceEnd p) := by
474 obtain ⟨t, i, s⟩ := p
475 rcases i with _ | _ | i <;> rfl
477/-- Across a port of `N_b`, the nest tiling continues as `N_b` does. -/
478theorem across_gP {b : Nat} {p q : Port} (p_port : (N b).IsPort p) (across_p : (N b).across p = some q) :
479 nestTiling.across (gP b p) = some (gP b q) := by
480 obtain ⟨t, i, s⟩ := p
481 obtain ⟨ht, hi⟩ := p_port
482 simp only at ht hi
483 -- the port, renumbered
484 have renumbered : gP b (t, i, s) = (gid b t, i, s) := rfl
485 rw [renumbered]
486 cases s with
487 | true =>
488 simp only [Patch.across, straightThrough] at across_p
489 cases glued : (N b).glue t i with
490 | none => rw [glued] at across_p; contradiction
491 | some e =>
492 obtain ⟨t', j⟩ := e
493 rw [glued] at across_p
494 simp only [Option.map_some, Option.some.injEq] at across_p
495 subst across_p
496 show (nestGlue (gid b t) i).map _ = _
497 rw [nestGlue_ext ht hi glued]; rfl
498 | false =>
499 simp only [Patch.across, straightThrough] at across_p
500 cases glued : (N b).glue t ((i + 13) % 14) with
501 | none => rw [glued] at across_p; contradiction
502 | some e =>
503 obtain ⟨t', j⟩ := e
504 rw [glued] at across_p
505 simp only [Option.map_some, Option.some.injEq] at across_p
506 subst across_p
507 show (nestGlue (gid b t) ((i + 13) % 14)).map _ = _
508 rw [nestGlue_ext ht (by omega) glued]; rfl
510/-- Where every edge of a tile is glued, something lies across every port of it. -/
511theorem across_isSome {P : Patch} {t : Nat} (all_glued : ∀ i, i < 14 → (P.glue t i).isSome) {q : Port}
512 (on_tile : q.1 = t) (hi : q.2.1 < 14) : (P.across q).isSome := by
513 obtain ⟨t', i, s⟩ := q
514 simp only at on_tile hi
515 subst on_tile
516 cases s with
517 | true =>
518 -- port `R(v_i)` lies on edge `e_i`, which is glued
519 have edge := all_glued i hi
521 cases glued : P.glue t' i with
522 | none => rw [glued] at edge; contradiction
523 | some _ => rfl
524 | false =>
525 -- port `L(v_i)` lies on edge `e_{i-1}`, which is glued
526 have edge := all_glued ((i + 13) % 14) (by omega)
528 cases glued : P.glue t' ((i + 13) % 14) with
529 | none => rw [glued] at edge; contradiction
530 | some _ => rfl
532/-! ### No closed strand -/
534/-- A strand of the nest tiling cannot stay among the tiles of one block `N_B` (`B ≥ 1`): in `N_{B+2}` every edge of
535those tiles is glued, so following it from a port there would never reach the rim of `N_{B+2}`. -/
536theorem follow_bounded {B : Nat} (B_pos : 1 ≤ B) : ∀ p r, (N (B + 2)).Follow p r → (N (B + 2)).IsPort p →
537 ∀ x : NPort, gP (B + 2) p = x.1 → (∀ k, (nestSys.walk x k).1.1 < (N B).tiles) → False := by
538 -- `N_{B+2}` has the signature
539 have sig := (good (B + 2) .Delta (by omega)).sig
540 intro p r follows
541 induction follows with
542 | @leave p nothing_across =>
543 intro p_port x x_eq bounded
544 -- the tile of `p` is a tile of `N_B`, seen in `N_{B+2}`
545 have in_B : gid (B + 2) p.1 < (N B).tiles := by
546 -- the strand starts at `x`, on a tile of `N_B`
547 have start := bounded 0
548 change x.1.1 < _ at start
549 rw [← x_eq] at start; exact start
550 obtain ⟨loc_bound, gid_of_loc⟩ := gid_loc B _ in_B
551 obtain ⟨up_bound, gid_of_up⟩ := gid_up loc_bound 2
552 -- that tile, taken into `N_B` and back up to `N_{B+2}`, is the tile of `p`
553 have same_tile : up B 2 (loc B (gid (B + 2) p.1)) = p.1 :=
554 gid_inj up_bound p_port.1 (by rw [gid_of_up, gid_of_loc])
555 -- every edge of it is glued in `N_{B+2}`
556 have all_glued : ∀ i, i < 14 → ((N (B + 2)).glue p.1 i).isSome := by
557 intro i hi
558 rw [← same_tile]
559 exact no_boundary B_pos loc_bound hi
560 -- the other end of the piece is on the same tile
561 have end_valid := pieceEnd_valid p_port.2
562 -- so something lies across it, yet the strand leaves `N_{B+2}` there
563 have across_end := across_isSome all_glued end_valid.1 end_valid.2
564 rw [nothing_across] at across_end
565 contradiction
566 | @next p q r across_end _ ih =>
567 intro p_port x x_eq bounded
568 -- the next port of the strand, in `N_{B+2}` and in the nest tiling
569 -- the other end of the piece is on the same tile
570 have end_valid := pieceEnd_valid p_port.2
571 -- so it is a port of `N_{B+2}`
572 have end_port : (N (B + 2)).IsPort (pieceEnd p) := ⟨end_valid.1 ▸ p_port.1, end_valid.2⟩
573 -- and so is the port `q` across from it
574 have q_port : (N (B + 2)).IsPort q := Patch.across_valid sig end_port.1 end_port.2 across_end
575 -- `q` is the next port of the strand in the nest tiling
576 have next_is : (nestSys.next x).1 = gP (B + 2) q := by
577 show (nestTiling.across (pieceEnd x.1)).getD (pieceEnd x.1) = _
578 rw [← x_eq, pieceEnd_gP, across_gP end_port across_end]
579 rfl
580 -- the strand from there is the rest of the strand from `x`
581 refine ih q_port (nestSys.next x) next_is.symm (fun k => ?_)
582 -- its ports are ports of the strand from `x`, so on tiles of `N_B`
583 have later := bounded (k + 1)
585 exact later
587/-- **No strand of the nest tiling is closed.** A closed strand visits finitely many tiles, so it stays in one block.
588-/
589theorem not_closed (x : NPort) : ¬ nestSys.Closed x := by
590 rintro ⟨n, n_pos, back⟩
591 -- the strand only ever visits the ports reached in its first `n` steps
592 have periodic : ∀ k, ∃ j, j < n ∧ nestSys.walk x k = nestSys.walk x j := by
593 intro k
594 induction k with
595 | zero => exact ⟨0, n_pos, rfl⟩
596 | succ k ih =>
597 obtain ⟨j, hj, same⟩ := ih
598 by_cases wraps : j + 1 = n
599 · refine ⟨0, n_pos, ?_⟩
601 rfl
602 · exact ⟨j + 1, by omega, by rw [StrandSystem.walk_succ, same, ← StrandSystem.walk_succ]⟩
603 -- the tiles of those ports have numbers below some bound `M`
604 have bounded : ∀ m, ∃ M, ∀ j, j < m → (nestSys.walk x j).1.1 < M := by
605 intro m
606 induction m with
607 | zero => exact ⟨0, fun j hj => absurd hj (by omega)⟩
608 | succ m ih =>
609 obtain ⟨M, below⟩ := ih
610 refine ⟨M + (nestSys.walk x m).1.1 + 1, fun j hj => ?_⟩
611 by_cases earlier : j < m
612 · have := below j earlier -- an earlier port: below `M`
613 omega
614 · have is_m : j = m := by omega -- port `m` itself
615 subst is_m; omega
616 obtain ⟨M, below⟩ := bounded n
617 -- so they are all tiles of `N_{M+1}`, which has more than `M` tiles
618 have big := tiles_ge (M + 1)
619 -- every port of the strand is on a tile of `N_{M+1}`
620 have in_block : ∀ k, (nestSys.walk x k).1.1 < (N (M + 1)).tiles := by
621 intro k
622 obtain ⟨j, hj, same⟩ := periodic k
623 rw [same]
624 -- the `j`-th port is below `M`
625 have := below j hj
626 omega
627 -- start at the port `x`, seen in `N_{M+3}`
628 obtain ⟨loc_bound, gid_of_loc⟩ := gid_loc (M + 1) x.1.1 (in_block 0)
629 obtain ⟨up_bound, gid_of_up⟩ := gid_up loc_bound 2
630 -- it is a port of `N_{M+3}`
631 have start : (N (M + 1 + 2)).IsPort (up (M + 1) 2 (loc (M + 1) x.1.1), x.1.2.1, x.1.2.2) := ⟨up_bound, x.2⟩
632 -- Theorem A says the strand leaves `N_{M+3}`
633 obtain ⟨r, follows⟩ := theoremA (M + 1 + 2) .Delta _ start
634 refine follow_bounded (B := M + 1) (by omega) _ r follows start x ?_ in_block
635 show (gid (M + 1 + 2) (up (M + 1) 2 (loc (M + 1) x.1.1)), x.1.2.1, x.1.2.2) = x.1
636 rw [gid_of_up, gid_of_loc]
638/-! ### One strand -/
640/-- A strand of a block is part of a strand of the nest tiling. -/
641theorem linked_same {m : Nat} (m_pos : 1 ≤ m) {u v : Port} (linked : (N m).Linked u v) (u_port : (N m).IsPort u) :
642 ∀ x y : NPort, x.1 = gP m u → y.1 = gP m v → nestSys.Same x y := by
643 -- `N_m` has the signature
644 have sig := (good m .Delta m_pos).sig
645 intro x y x_eq y_eq
646 induction linked generalizing y with
647 | refl =>
648 -- the same port
649 have same_port : x = y := Subtype.ext (x_eq.trans y_eq.symm)
650 subst same_port
651 exact .refl
652 | @piece q reach ih =>
653 -- along the piece at `q`, a port of `N_m`
654 have q_port := reach.valid sig u_port
655 -- one move along the piece, in the nest tiling
656 have step := StrandSystem.Same.inside (S := nestSys) (ih ⟨gP m q, q_port.2⟩ rfl)
657 -- which lands on `y`
658 have is_y : nestSys.inside ⟨gP m q, q_port.2⟩ = y := Subtype.ext (by rw [y_eq]; exact pieceEnd_gP m q)
659 rwa [is_y] at step
660 | @edge q q' reach across_q ih =>
661 -- across the edge at `q`, a port of `N_m`
662 have q_port := reach.valid sig u_port
663 -- one move across the edge, in the nest tiling
664 have step := StrandSystem.Same.across (S := nestSys) (ih ⟨gP m q, q_port.2⟩ rfl)
665 -- which lands on `y`
666 have is_y : nestSys.across ⟨gP m q, q_port.2⟩ = y := Subtype.ext (by
667 show (nestTiling.across (gP m q)).getD _ = _
668 rw [across_gP q_port across_q, y_eq]; rfl)
669 rwa [is_y] at step
671/-- Port `z` of the nest tiling, as a port of the block `N_b`. -/
672def toBlock (b : Nat) (z : NPort) : Port := (loc b z.1.1, z.1.2.1, z.1.2.2)
674/-- Port `z` of the nest tiling is a port of `N_b` if its tile is. -/
675theorem toBlock_port {b : Nat} {z : NPort} (in_block : z.1.1 < (N b).tiles) : (N b).IsPort (toBlock b z) :=
676 ⟨(gid_loc b z.1.1 in_block).1, z.2⟩
678/-- Taken into `N_b` and then up `k` levels, port `z` keeps its number. -/
679theorem gP_toBlock {b : Nat} {z : NPort} (in_block : z.1.1 < (N b).tiles) (k : Nat) :
680 gP (b + k) (upPort b k (toBlock b z)) = z.1 := by
681 obtain ⟨loc_bound, gid_of_loc⟩ := gid_loc b z.1.1 in_block
682 simp only [gP, upPort, toBlock]
683 rw [(gid_up loc_bound k).2, gid_of_loc]
685/-- Two ports of the nest tiling whose tiles lie in `N_b` (`b ≥ 1`) lie on one strand: they do in `N_{b+4}`
686(Theorem B with the paper's bound). -/
687theorem same_in_block {b : Nat} (b_pos : 1 ≤ b) {x y : NPort} (x_in : x.1.1 < (N b).tiles)
688 (y_in : y.1.1 < (N b).tiles) : nestSys.Same x y := by
689 -- one strand of `N_{b+4}`
690 have linked := (theoremB_sharp b (toBlock b x) (toBlock b y) b_pos (toBlock_port x_in) (toBlock_port y_in)).1
691 -- with `x`, four levels up, a port of `N_{b+4}`
692 have x_port := isPort_upk b_pos (toBlock_port x_in) 4
693 -- read in the nest tiling
694 exact linked_same (m := b + 4) (by omega) linked x_port x y (gP_toBlock x_in 4).symm (gP_toBlock y_in 4).symm
696/-- **Any two ports of the nest tiling lie on one strand**: both tiles lie in a large enough block. -/
697theorem all_same (x y : NPort) : nestSys.Same x y := by
698 -- `N_{x+y+1}` contains both tiles
699 have big := tiles_ge (x.1.1 + y.1.1 + 1)
700 exact same_in_block (b := x.1.1 + y.1.1 + 1) (by omega) (by omega) (by omega)
702/-! ### Lemma 3.4 -/
In the paper Theorem B The Ariadne Theorem
704/-- **Theorem B, final form** (as stated in `Statement.lean`): the ribbons of the nest tiling form one two-way
705infinite strand. -/
707 -- the start: port `R(v_0)` of the original tile
708 let start : NPort := ⟨(0, 0, true), by decide⟩
709 -- following the strand forwards, as ports
710 have forwards : ∀ k, iter nestTiling.forward k (0, 0, true) = (nestSys.walk start k).1 := by
711 intro k
712 induction k with
713 | zero => rfl
714 | succ k ih => rw [iter_succ, ih]; rfl
715 -- and backwards
716 have backwards : ∀ k, iter nestTiling.backward k (0, 0, true) = (iter nestSys.prev k start).1 := by
717 intro k
718 induction k with
719 | zero => rfl
720 | succ k ih => rw [iter_succ, ih]; rfl
721 -- Lemma 3.4: the strand is closed or a two-way infinite path; it is not closed
722 obtain ⟨distinct, back_distinct, apart, no_piece_twice⟩ :=
723 (nestSys.closed_or_path start).resolve_left (not_closed start)
724 refine ⟨?_, ?_, ?_, ?_, ?_⟩
725 · -- (1) forwards, no port twice
726 intro i j same
727 rw [forwards, forwards] at same
728 exact distinct i j (Subtype.ext same)
729 · -- (2) backwards, no port twice
730 intro a a' same
731 rw [backwards, backwards] at same
732 exact back_distinct a a' (Subtype.ext same)
733 · -- (3) backwards never meets forwards, except at the start
734 intro a b same
735 rw [backwards, forwards] at same
736 exact apart a b (Subtype.ext same)
737 · -- (4) no piece twice
738 intro i j same
739 rw [forwards, forwards] at same
740 exact no_piece_twice i j (Subtype.ext same)
741 · -- (5) every port is on the strand
742 intro q hq
743 obtain ⟨k, reached | reached | reached | reached⟩ := nestSys.same_orbit (all_same start ⟨q, hq⟩)
744 · exact ⟨k, Or.inl (by rw [forwards]; exact congrArg Subtype.val reached)⟩
745 · exact ⟨k, Or.inr (Or.inl (by rw [backwards]; exact congrArg Subtype.val reached))⟩
746 · exact ⟨k, Or.inr (Or.inr (Or.inl (by rw [forwards]; exact congrArg Subtype.val reached)))⟩
747 · exact ⟨k, Or.inr (Or.inr (Or.inr (by rw [backwards]; exact congrArg Subtype.val reached)))⟩
749end SpectreKnot.Statement

← SpectreKnot/ProofB.leanSpectreKnot/ProofChain.lean →