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

lean/SpectreKnot/NestStep.lean

273 lines · 27 declarations, each with its own page · on GitHub ·

The junction map at tile level. N_{m+1} is the Δ composition whose child 1 is N_m. A rim port of N_m (outside child 1's side 2) lies, in N_{m+1}, on the strand of the parent hook at the junction that StepMap.lean's map names (step_tile; the paper's Lemma 9.3). Also: where the pieces of the parent's rim start (jpos), lifting strands up the nest (lift_nest), and the hooks of N_m (hook).

← SpectreKnot/Linked.leanSpectreKnot/Turn.lean →

All 39 files, and the declarations of this one
1/-
2**The junction map at tile level.** `N_{m+1}` is the Δ composition whose child 1 is `N_m`. A rim port of `N_m`
3(outside child 1's side 2) lies, in `N_{m+1}`, on the strand of the parent hook at the junction that `StepMap.lean`'s
4map names (`step_tile`; the paper's Lemma 9.3). Also: where the pieces of the parent's rim start (`jpos`), lifting
5strands up the nest (`lift_nest`), and the hooks of `N_m` (`hook`).
6-/
9
10namespace SpectreKnot.Statement
12open Pattern Compose Gluing
14/-! ### Where the pieces of the Δ-supertile's rim start -/
16/-- Where piece `q` of the Δ-supertile's rim starts, for children's side lengths `L`. -/
17def jpos (L : Nat → Nat → Nat) (q : Nat) : Nat := totL L ((pcs .Delta).take q)
19/-- Table 3 lists 22 pieces for the Δ-supertile's rim. -/
20theorem pcs_len : (pcs .Delta).length = 22 := by decide
22/-- Piece `q < 22` of the flattened Table 3 is `pieceD q`. -/
23theorem pcs_get {q : Nat} (hq : q < 22) : (pcs .Delta)[q]? = some (pieceD q) := by
24 rw [List.getElem?_eq_getElem (by rw [pcs_len]; exact hq)]
25 simp only [pieceD, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem (show q < (pcs .Delta).length by
26 rw [pcs_len]; exact hq), Option.getD_some]
28/-- Piece `q + 1` starts where piece `q` starts, plus the length of piece `q`. -/
29theorem jpos_succ (L : Nat → Nat → Nat) {q : Nat} (hq : q < 22) :
30 jpos L (q + 1) = jpos L q + L (pieceD q).1 (pieceD q).2 := by
31 simp only [jpos]
32 rw [List.take_add_one, totL_append, pcs_get hq]
33 simp [totL]
35/-- With every side at least 5 edges long, the piece `k` places after piece `q` starts at least `5 k` edges later. -/
36theorem jpos_le_add (L : Nat → Nat → Nat) (len_ge : ∀ c j, 5 ≤ L c j) (q : Nat) :
37 ∀ k, q + k ≤ 22 → jpos L q + 5 * k ≤ jpos L (q + k) := by
38 intro k
39 induction k with
40 | zero => intro _; simp
41 | succ k ih =>
42 intro fits
43 -- the first `k` pieces
44 have := ih (by omega)
45 rw [← Nat.add_assoc, jpos_succ L (by omega)]
46 -- then piece `q + k`, of at least 5 edges
47 have := len_ge (pieceD (q + k)).1 (pieceD (q + k)).2
48 omega
50/-- With every side at least 5 edges long, piece `q'` starts at least `5 (q' - q)` edges after piece `q`. -/
51theorem jpos_le (L : Nat → Nat → Nat) (len_ge : ∀ c j, 5 ≤ L c j) {q q' : Nat} (q_le : q ≤ q') (q'_le : q' ≤ 22) :
52 jpos L q + 5 * (q' - q) ≤ jpos L q' := by
53 -- `q' - q` pieces on from piece `q`
54 have spread := jpos_le_add L len_ge q (q' - q) (by omega)
55 rwa [show q + (q' - q) = q' by omega] at spread
57/-- The 22 pieces make up the whole rim. -/
58theorem jpos_full (L : Nat → Nat → Nat) : jpos L 22 = rimN .Delta L := by
59 simp only [jpos, rimN]
60 rw [List.take_of_length_le (by rw [pcs_len]; exact Nat.le_refl _)]
62/-- The rim position `jpos q + i` lies on piece `q`, at its `i`-th edge (counted in the parent's sense). -/
63theorem ownGo_jpos (L : Nat → Nat → Nat) {q i : Nat} (hq : q < 22) (hi : i < L (pieceD q).1 (pieceD q).2) :
64 ownGo L (pcs .Delta) (jpos L q + i) =
65 ((pieceD q).1, pos (L (pieceD q).1) (pieceD q).2 + L (pieceD q).1 (pieceD q).2 - 1 - i) := by
66 -- the pieces from `q` on: piece `q`, then the rest
67 have drop_q : (pcs .Delta).drop q = pieceD q :: (pcs .Delta).drop (q + 1) := by
68 rw [List.drop_eq_getElem_cons (by rw [pcs_len]; exact hq)]
69 congr 1
70 -- piece `q` of the list
71 have get_q := pcs_get hq
72 rw [List.getElem?_eq_getElem (by rw [pcs_len]; exact hq)] at get_q
73 simpa using get_q
74 conv => lhs; rw [← List.take_append_drop q (pcs .Delta)]
75 rw [ownGo_append, drop_q, show totL L ((pcs .Delta).take q) = jpos L q from rfl, ite_eq_right (by omega),
76 Nat.add_sub_cancel_left]
77 simp only [ownGo]
78 rw [ite_eq_left hi]
80/-- Where side `J` of the Δ-supertile starts, as a piece number. -/
81def sJ (J : Nat) : Nat := [0, 5, 7, 11, 14, 19, 22].getD J 0
83/-- Table 3's pieces for sides `0 … J - 1` of the Δ-supertile are its first `sJ J` pieces. -/
84theorem pside_take : ∀ J, J ≤ 6 → ((pside .Delta).take J).flatMap id = (pcs .Delta).take (sJ J) := by decide
86/-- Side `J` of the Δ-supertile starts where piece `sJ J` does. -/
87theorem vpos_jpos (L : Nat → Nat → Nat) {J : Nat} (hJ : J ≤ 6) : pos (parentLen .Delta L) J = jpos L (sJ J) := by
88 rw [← totL_take L .Delta J hJ, pside_take J hJ]; rfl
90/-! ### The nest -/
92/-- `N_{m+1}`, as `compose` builds it. -/
93abbrev Par (m : Nat) : Patch := compose .Delta fun c => super m (kidAt .Delta c)
95/-- The children of `N_{m+1}`: the level-`m` supertiles of the kinds Table 1 lists for Δ. -/
96abbrev kidsD (m : Nat) : Nat → Patch := fun c => super m (kidAt .Delta c)
98/-- For `m ≥ 1`, `N_{m+1}` is the Δ composition of its level-`m` children. -/
99theorem N_succ {m : Nat} (m_pos : 1 ≤ m) : N (m + 1) = Par m := by
100 obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
101 rfl
103/-- Going `k + 1` levels up the nest is going `k` levels up, then one more. -/
104theorem up_succ : ∀ (k b t : Nat), up b (k + 1) t = up (b + k) 1 (up b k t)
105 | 0, _, _ => rfl
106 | k + 1, b, t => by
107 show up (b + 1) (k + 1) (t + nestShift b) = _
108 rw [up_succ k (b + 1) (t + nestShift b), show b + 1 + k = b + (k + 1) by omega]
109 rfl
111/-- The same for ports: `k + 1` levels up is `k` levels up, then one more. -/
112theorem upPort_succ (b k : Nat) (p : Port) : upPort b (k + 1) p = upPort (b + k) 1 (upPort b k p) := by
113 simp only [upPort]; rw [up_succ]
115/-- The children of `N_{m+1}`, with the bridge's hypotheses. -/
116theorem KD {m : Nat} (m_pos : 1 ≤ m) :
117 Kids .Delta (kidsD m) (Lk m .Delta) (dOff m) (ori m) (ori m) :=
118 kids_at m_pos .Delta (fun K => good m K m_pos)
120/-- Every side of a level-`m` supertile has at least 5 edges (Lemma 6.5). -/
121theorem len5 {m : Nat} (m_pos : 1 ≤ m) (c j : Nat) : 5 ≤ Lk m .Delta c j := (bounds m m_pos).1 _
123/-- One level up, a port of `N_m` is still a port. -/
124theorem isPort_up {m : Nat} (m_pos : 1 ≤ m) {x : Port} (x_port : (N m).IsPort x) :
125 (N (m + 1)).IsPort (upPort m 1 x) := by
126 rw [N_succ m_pos]
127 exact ⟨tile_lt (kidsD m) (show 1 < nk .Delta by decide) x_port.1, x_port.2⟩
129/-- **A strand of `N_m` is part of a strand of `N_{m+1}`.** -/
130theorem lift_nest {m : Nat} (m_pos : 1 ≤ m) {x y : Port} (linked : (N m).Linked x y) (x_port : (N m).IsPort x) :
131 (N (m + 1)).Linked (upPort m 1 x) (upPort m 1 y) := by
132 rw [N_succ m_pos]
133 exact (KD m_pos).linked_lift (c := 1) (by decide) linked x_port
135/-- The rim of `N_m` has the length that its side lengths give. -/
136theorem E_N {m : Nat} (m_pos : 1 ≤ m) : (N m).E = pos (Lk m .Delta 1) 6 := (good m .Delta m_pos).len
138/-- The corners of `N_m`: `A = 0`, and `B` is `1` or `E - 1`. -/
139theorem corners_N {m : Nat} (m_pos : 1 ≤ m) :
140 aPos m .Delta = 0 ∧ (bPos m .Delta = 1 ∨ bPos m .Delta = pos (Lk m .Delta 1) 6 - 1) := by
141 -- a Δ is not a Σ, so `A = 0`
142 have A_zero : aPos m .Delta = 0 := by simp [aPos]
143 -- the rim has at least two edges
144 have rim_two : 2 ≤ pos (Lk m .Delta 1) 6 := by
145 -- side 0 has at least 5 edges
146 have := len5 m_pos 1 0
147 -- and ends no later than the rim
148 have := pos_mono (Lk m .Delta 1) (show 1 ≤ 6 by omega)
149 simp only [pos] at *; omega
150 refine ⟨A_zero, ?_⟩
151 simp only [bPos, A_zero]
152 show (if ori m = true then nxt (pos (Lk m .Delta 1) 6) 0 else prv (pos (Lk m .Delta 1) 6) 0) = 1 ∨ _
153 split
154 · left; simp only [nxt]; rw [ite_eq_right (by omega)]
155 · right; simp only [prv, ite_true]; rfl
157/-- **A hook**: at a rim vertex of `N_m` other than the corners, the two ports lie on one strand. -/
158theorem hook {m : Nat} (m_pos : 1 ≤ m) {v : Nat} (two_le_v : 2 ≤ v) (v_le : v + 2 ≤ pos (Lk m .Delta 1) 6) :
159 (N m).Linked ((N m).bport (ori m) (v, false)) ((N m).bport (ori m) (v, true)) := by
160 -- `N_m` has the signature
161 have good_m := good m .Delta m_pos
162 -- with corners `0` and `1` or `E - 1`
163 obtain ⟨A_zero, B_next⟩ := corners_N m_pos
164 -- and its rim length
165 have rim_len := E_N m_pos
166 unfold N at rim_len
167 -- from `L(v)` the ribbon leads to the port the signature pairs it with
168 have follows := good_m.sig.sig v false (by rw [rim_len]; omega)
169 -- which is `R(v)`, since `v` is not a corner
170 have paired : btau (aPos m .Delta) (bPos m .Delta) (v, false) = (v, true) := by
171 simp only [btau]
172 rw [ite_eq_right (by omega), ite_eq_right (by omega)]; rfl
173 rw [paired] at follows
174 exact .of_follow follows
176/-! ### One level up, at tile level -/
178/-- The gluing's port at the parent's port `R` of the junction where piece `q` starts is `jR`. -/
179theorem gR_jpos {m : Nat} (m_pos : 1 ≤ m) {q : Nat} (hq : q < 22) :
180 gR .Delta (Lk m .Delta) (dOff m) (ori m) (jpos (Lk m .Delta) q) = jR (Lk m .Delta) q := by
181 -- piece `q` is a side of an actual child
182 obtain ⟨hc, hj⟩ := piece_ok q hq
183 -- which has an edge
184 have len_pos : 0 < Lk m .Delta (pieceD q).1 (pieceD q).2 := by
185 -- at least 5, in fact
186 have := len5 m_pos (pieceD q).1 (pieceD q).2
187 omega
188 -- the first edge of piece `q` (the last edge of the child's side)
189 have first_edge := ownGo_jpos (Lk m .Delta) hq len_pos
190 rw [Nat.add_zero] at first_edge
191 simp only [gR, first_edge, Nat.sub_zero, ofLens_E hc]
192 rw [nxt_last (fun i => by
193 -- every side of the child has an edge
194 have := len5 m_pos (pieceD q).1 i
195 omega) hj]
196 rfl
198/-- Piece `q ≥ 1` starts at least 5 edges along the rim. -/
199theorem jpos_pos {m : Nat} (m_pos : 1 ≤ m) {q : Nat} (q_pos : 1 ≤ q) (hq : q ≤ 22) : 5 ≤ jpos (Lk m .Delta) q := by
200 -- `q` pieces from the start, each of at least 5 edges
201 have spread := jpos_le_add (Lk m .Delta) (len5 m_pos) 0 q (by omega)
202 simp only [Nat.zero_add] at spread
203 omega
205/-- The gluing's port at the parent's port `L` of the junction where piece `q ≥ 1` starts is `jL`. -/
206theorem gL_jpos {m : Nat} (m_pos : 1 ≤ m) {q : Nat} (q_pos : 1 ≤ q) (hq : q < 22) :
207 gL .Delta (Lk m .Delta) (jpos (Lk m .Delta) q) = jL (Lk m .Delta) q := by
208 -- piece `q - 1` has at least 5 edges
209 have prev_len := len5 m_pos (pieceD (q - 1)).1 (pieceD (q - 1)).2
210 -- and piece `q` starts where it ends
211 have prev_end := jpos_succ (Lk m .Delta) (show q - 1 < 22 by omega)
212 rw [show q - 1 + 1 = q by omega] at prev_end
213 -- the rim position just before piece `q` is the last edge of piece `q - 1`
214 have before_start : prv (rimN .Delta (Lk m .Delta)) (jpos (Lk m .Delta) q) =
215 jpos (Lk m .Delta) (q - 1) + (Lk m .Delta (pieceD (q - 1)).1 (pieceD (q - 1)).2 - 1) := by
216 simp only [prv]; rw [ite_eq_right (by omega)]; omega
217 -- that edge, as an edge of the child (the first edge of its side)
218 have last_edge := ownGo_jpos (Lk m .Delta) (show q - 1 < 22 by omega)
219 (show Lk m .Delta (pieceD (q - 1)).1 (pieceD (q - 1)).2 - 1 < _ by omega)
220 simp only [gL, before_start, last_edge]
221 simp only [jL]
222 congr 2
223 omega
In the paper Lemma 9.3 The junction map
225/-- **The junction map at tile level**: a rim port of `N_m` (outside child 1's side 2) lies, in `N_{m+1}`, on the
226strand of the parent hook at junction `q`. -/
227theorem step_tile {m : Nat} (m_pos : 1 ≤ m) {u : Nat} (hu : u < pos (Lk m .Delta 1) 6) {s : Bool} {q : Nat}
228 (tgt_eq : tgt (ori m) (Lk m .Delta 1) u s = some q) :
229 (N (m + 1)).Linked (upPort m 1 ((N m).bport (ori m) (u, s)))
230 ((N (m + 1)).bport (ori (m + 1)) (jpos (Lk m .Delta) q, true)) := by
231 -- the junction is one of the pieces `1 … 21`
232 obtain ⟨q_pos, q_lt⟩ := tgt_lt tgt_eq
233 -- the children of `N_{m+1}`
234 have kids := KD m_pos
235 -- the pieces end where the rim does
236 have pieces_end := jpos_full (Lk m .Delta)
237 -- so the junction is on the rim
238 have junction_lt : jpos (Lk m .Delta) q < rimN .Delta (Lk m .Delta) := by
239 -- the pieces from `q` to the end
240 have spread := jpos_le_add (Lk m .Delta) (len5 m_pos) q (22 - q) (by omega)
241 rw [show q + (22 - q) = 22 by omega] at spread; omega
242 -- the rim of `N_{m+1}`
243 have rim_len : (N (m + 1)).E = rimN .Delta (Lk m .Delta) := by
244 rw [N_succ m_pos, compose_E kids.shape]
245 -- the junction is a hook of `N_{m+1}`: its two ports lie on one strand
246 have junction_hook : (N (m + 1)).Linked ((N (m + 1)).bport (ori (m + 1)) (jpos (Lk m .Delta) q, false))
247 ((N (m + 1)).bport (ori (m + 1)) (jpos (Lk m .Delta) q, true)) := by
248 -- the last piece has at least 5 edges
249 have := len5 m_pos (pieceD 21).1 (pieceD 21).2
250 -- piece 21 starts at least `5 (21 - q)` edges after piece `q`
251 have to_last := jpos_le_add (Lk m .Delta) (len5 m_pos) q (21 - q) (by omega)
252 rw [show q + (21 - q) = 21 by omega] at to_last
253 -- and the rim ends where piece 21 does
254 have last_end : jpos (Lk m .Delta) 22 = jpos (Lk m .Delta) 21 + Lk m .Delta (pieceD 21).1 (pieceD 21).2 :=
255 jpos_succ (Lk m .Delta) (q := 21) (by omega)
256 refine hook (by omega) (by
257 -- the junction is at least 5 edges along
258 have := jpos_pos m_pos q_pos (by omega)
259 omega) ?_
260 rw [← E_N (by omega), rim_len]; omega
261 -- the junction map: the walk from `(1, u, s)` ends at a port of the junction's hook
262 obtain ⟨r, walk, at_junction⟩ := step_level m m_pos (ori m) u hu s q tgt_eq
263 -- at tile level: following the ribbon from the port of `N_m` leads there
264 have follows := kids.follow_of_fullReach walk ⟨by rw [ofLens_n]; exact (by decide : 1 < nk .Delta),
265 show u < _ by rw [ofLens_E (c := 1) (by decide)]; exact hu⟩
266 rw [N_succ m_pos, ori_succ] at junction_hook ⊢
267 rcases at_junction with rfl | rfl
268 · rw [kids.bport_R junction_lt, gR_jpos m_pos q_lt]
269 exact .of_follow follows
270 · rw [kids.bport_L junction_lt, gL_jpos m_pos q_pos q_lt] at junction_hook
271 exact (Patch.Linked.of_follow follows).trans junction_hook
273end SpectreKnot.Statement

← SpectreKnot/Linked.leanSpectreKnot/Turn.lean →