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

lean/SpectreKnot/ProofB.lean

550 lines · 38 declarations, each with its own page · on GitHub ·

Theorem B (theoremB, theoremB_sharp): the nest has no boundary, no closed strand, and any two ports of a block lie on one strand of the block three levels up (b even) or four (b odd).

← SpectreKnot/ProofA.leanSpectreKnot/ProofStrand.lean →

All 39 files, and the declarations of this one
1/-
2**Theorem B** (`theoremB`, `theoremB_sharp`): the nest has no boundary, no closed strand, and any two ports of a
3block lie on one strand of the block three levels up (`b` even) or four (`b` odd).
4
5The merging (the paper's proof of Thm 9.1): a strand of `N_m` leaves it at a rim port; in `N_{m+1}` it runs on to the
6parent hook at the junction that the junction map names (`step_tile`, `NestStep.lean`), or, on child 1's side 2, the
7rim port is itself a parent hook (`stretch_eq`) (Lemma 9.3). The junctions lie inside the parent's sides 2–5
8(Lemma 9.4), and inside side `J` the map depends only on `J` (`adv_some`, `adv_none`). Following the sides level by
9level, every strand of `N_b` reaches the hook at junction 12 of `N_{b+3}` (even `b`) or `N_{b+4}` (odd `b`).
10-/
13namespace SpectreKnot.Statement
15open Pattern Compose Gluing
17/-! ### Child 1's side 2: its rim ports are parent hooks -/
19/-- The parent vertex at child 1's vertex `u` on its side 2 (piece 16 of the parent's rim, traversed backwards). -/
20def stp (L : Nat → Nat → Nat) (u : Nat) : Nat := jpos L 16 + (pos (L 1) 3 - u)
22/-- Piece 16 of the Δ-supertile's rim is child 1's side 2. -/
23theorem piece16 : pieceD 16 = (1, 2) := by decide
25/-- Piece 17 starts where piece 16, child 1's side 2, ends. -/
26theorem jpos17 (L : Nat → Nat → Nat) : jpos L 17 = jpos L 16 + L 1 2 := by
27 -- piece 17 starts where piece 16 does, plus its length
28 have next_start := jpos_succ L (q := 16) (by omega)
29 rw [piece16] at next_start
30 exact next_start
32/-- Rim position `jpos 16 + i` of the Δ-supertile is child 1's edge `pos 2 + L 1 2 - 1 - i`, on its side 2. -/
33theorem ownGo16 (L : Nat → Nat → Nat) {i : Nat} (hi : i < L 1 2) :
34 ownGo L (pcs .Delta) (jpos L 16 + i) = (1, pos (L 1) 2 + L 1 2 - 1 - i) := by
35 -- the `i`-th edge of piece 16
36 have on_piece := ownGo_jpos L (q := 16) (by omega) (by rw [piece16]; exact hi)
37 rw [piece16] at on_piece
38 exact on_piece
40/-- The gluing's port `(1, u, s)` of `N_{m+1}` is port `(u, s)` of `N_m`, taken one level up. -/
41theorem iota1 (m : Nat) (u : Nat) (s : Bool) :
42 ιP (kidsD m) (ori m) (1, u, s) = upPort m 1 ((N m).bport (ori m) (u, s)) := rfl
In the paper Lemma 9.3 The junction map
44/-- **On child 1's side 2, rim ports of `N_m` are rim ports of `N_{m+1}`**: for `u` strictly inside side 2, port
45`(u, s)` of `N_m`, one level up, is port `(stp u, !s)` of `N_{m+1}` (the hand swaps with the orientation). -/
46theorem stretch_eq {m : Nat} (m_pos : 1 ≤ m) {u : Nat} (after_two : pos (Lk m .Delta 1) 2 < u)
47 (before_three : u < pos (Lk m .Delta 1) 3) (s : Bool) :
48 upPort m 1 ((N m).bport (ori m) (u, s)) = (N (m + 1)).bport (ori (m + 1)) (stp (Lk m .Delta) u, !s) := by
49 -- the children of `N_{m+1}`
50 have kids := KD m_pos
51 -- child 1's side 2 ends `L 1 2` edges after it starts
52 have side_two_len : pos (Lk m .Delta 1) 3 = pos (Lk m .Delta 1) 2 + Lk m .Delta 1 2 := pos_succ _ 2
53 -- and no later than the rim
54 have three_le_six := pos_mono (Lk m .Delta 1) (show 3 ≤ 6 by omega)
55 -- piece 17 starts where piece 16 ends
56 have piece17 := jpos17 (Lk m .Delta)
57 -- and the rim ends at least 25 edges later
58 have to_end := jpos_le (Lk m .Delta) (len5 m_pos) (q := 17) (q' := 22) (by omega) (by omega)
59 -- so the parent vertex is on the parent's rim
60 have stp_lt : stp (Lk m .Delta) u < rimN .Delta (Lk m .Delta) := by
61 rw [← jpos_full]; simp only [stp]; omega
62 -- piece 16 starts at least 5 edges along
63 have piece16_far := jpos_pos m_pos (q := 16) (by omega) (by omega)
64 rw [N_succ m_pos, ori_succ]
65 cases s
66 · rw [Bool.not_false, kids.bport_R stp_lt]
67 -- the parent's rim edge at `stp u` is child 1's edge `u - 1`
68 have edge_at := ownGo16 (Lk m .Delta) (i := pos (Lk m .Delta 1) 3 - u) (by omega)
69 -- so the gluing's port there is `L` at child 1's vertex `u`
70 have gR_eq : gR .Delta (Lk m .Delta) (dOff m) (ori m) (stp (Lk m .Delta) u) = (1, u, false) := by
71 -- the end of edge `u - 1` is vertex `u`
72 have next_vertex : nxt (pos (Lk m .Delta 1) 6) (pos (Lk m .Delta 1) 2 + Lk m .Delta 1 2 - 1 -
73 (pos (Lk m .Delta 1) 3 - u)) = u := by
74 simp only [nxt]; rw [ite_eq_right (by omega)]; omega
75 simp only [gR, stp, edge_at, ofLens_E (show 1 < nk .Delta by decide), next_vertex]
76 rw [gR_eq, iota1]
77 · rw [Bool.not_true, kids.bport_L stp_lt]
78 -- the rim position before `stp u`
79 have before_stp : prv (rimN .Delta (Lk m .Delta)) (stp (Lk m .Delta) u) =
80 jpos (Lk m .Delta) 16 + (pos (Lk m .Delta 1) 3 - u - 1) := by
81 -- `stp u` is not rim position 0
82 have stp_ne : stp (Lk m .Delta) u ≠ 0 := by simp only [stp]; omega
83 simp only [prv]; rw [ite_eq_right stp_ne]; simp only [stp]; omega
84 -- the parent's rim edge there is child 1's edge `u`
85 have edge_at := ownGo16 (Lk m .Delta) (i := pos (Lk m .Delta 1) 3 - u - 1) (by omega)
86 -- so the gluing's port there is `R` at child 1's vertex `u`
87 have gL_eq : gL .Delta (Lk m .Delta) (stp (Lk m .Delta) u) = (1, u, true) := by
88 -- the edge's number is `u`
89 have edge_u : pos (Lk m .Delta 1) 2 + Lk m .Delta 1 2 - 1 - (pos (Lk m .Delta 1) 3 - u - 1) = u := by omega
90 simp only [gL, before_stp, edge_at, edge_u]
91 rw [gL_eq, iota1]
93/-! ### Sides -/
95/-- `v` lies inside side `J` of `N_n`, at least two vertices from either end. -/
96def Inside (n J v : Nat) : Prop := pos (Lk n .Delta 1) J + 2 ≤ v ∧ v + 2 ≤ pos (Lk n .Delta 1) (J + 1)
98/-- Side `J` of `N_{n+1}` starts where piece `sJ J` of its rim starts (with the level-`n` lengths). -/
99theorem pos_up {n : Nat} (n_pos : 1 ≤ n) {J : Nat} (hJ : J ≤ 6) :
100 pos (Lk (n + 1) .Delta 1) J = jpos (Lk n .Delta) (sJ J) := by
101 rw [show pos (Lk (n + 1) .Delta 1) J = vpos (n + 1) .Delta J from rfl, vpos_eq n_pos .Delta hJ, vpos_jpos _ hJ]
103/-- The sides start at pieces `0 … 22`. -/
104theorem sJ_le : ∀ J, J ≤ 6 → sJ J ≤ 22 := by decide
106/-- A junction `q` at least one piece after the start of side `J` and one piece before its end lies inside side `J`
107of `N_{n+1}`. -/
108theorem inside_of {n J q k₁ k₂ : Nat} (n_pos : 1 ≤ n) (hJ : J < 6) (after_start : sJ J + k₁ = q)
109 (before_end : q + k₂ = sJ (J + 1)) (k₁_pos : 1 ≤ k₁) (k₂_pos : 1 ≤ k₂) :
110 Inside (n + 1) J (jpos (Lk n .Delta) q) := by
111 -- the side ends within the rim's 22 pieces
112 have end_le := sJ_le (J + 1) (by omega)
113 -- `k₁` pieces from the side's start to `q`, each of at least 5 edges
114 have from_start := jpos_le_add (Lk n .Delta) (len5 n_pos) (sJ J) k₁ (by omega)
115 -- and `k₂` pieces from `q` to the side's end
116 have to_end := jpos_le_add (Lk n .Delta) (len5 n_pos) q k₂ (by omega)
117 rw [after_start] at from_start
118 rw [before_end] at to_end
119 refine ⟨?_, ?_⟩
120 · rw [pos_up n_pos (by omega)]; omega
121 · rw [pos_up n_pos (by omega)]; omega
In the paper Lemma 9.4 Where the junctions lie
123/-- Junction 9 lies inside side 2 of `N_{n+1}`. -/
124theorem inside_9 {n : Nat} (n_pos : 1 ≤ n) : Inside (n + 1) 2 (jpos (Lk n .Delta) 9) :=
125 inside_of n_pos (k₁ := 2) (k₂ := 2) (by omega) rfl rfl (by omega) (by omega)
In the paper Lemma 9.4 Where the junctions lie
126/-- Junction 12 lies inside side 3 of `N_{n+1}`. -/
127theorem inside_12 {n : Nat} (n_pos : 1 ≤ n) : Inside (n + 1) 3 (jpos (Lk n .Delta) 12) :=
128 inside_of n_pos (k₁ := 1) (k₂ := 2) (by omega) rfl rfl (by omega) (by omega)
In the paper Lemma 9.4 Where the junctions lie
129/-- Junction 16 lies inside side 4 of `N_{n+1}`. -/
130theorem inside_16 {n : Nat} (n_pos : 1 ≤ n) : Inside (n + 1) 4 (jpos (Lk n .Delta) 16) :=
131 inside_of n_pos (k₁ := 2) (k₂ := 3) (by omega) rfl rfl (by omega) (by omega)
In the paper Lemma 9.4 Where the junctions lie
132/-- Junction 17 lies inside side 4 of `N_{n+1}`. -/
133theorem inside_17 {n : Nat} (n_pos : 1 ≤ n) : Inside (n + 1) 4 (jpos (Lk n .Delta) 17) :=
134 inside_of n_pos (k₁ := 3) (k₂ := 2) (by omega) rfl rfl (by omega) (by omega)
In the paper Lemma 9.4 Where the junctions lie
135/-- Junction 21 lies inside side 5 of `N_{n+1}`. -/
136theorem inside_21 {n : Nat} (n_pos : 1 ≤ n) : Inside (n + 1) 5 (jpos (Lk n .Delta) 21) :=
137 inside_of n_pos (k₁ := 2) (k₂ := 1) (by omega) rfl rfl (by omega) (by omega)
In the paper Lemma 9.4 Where the junctions lie
139/-- The parent vertex at a vertex strictly inside child 1's side 2 lies inside side 4 of `N_{n+1}`. -/
140theorem inside_stp {n : Nat} (n_pos : 1 ≤ n) {u : Nat} (after_two : pos (Lk n .Delta 1) 2 < u)
141 (before_three : u < pos (Lk n .Delta 1) 3) : Inside (n + 1) 4 (stp (Lk n .Delta) u) := by
142 -- child 1's side 2 ends `L 1 2` edges after it starts
143 have side_two_len : pos (Lk n .Delta 1) 3 = pos (Lk n .Delta 1) 2 + Lk n .Delta 1 2 := pos_succ _ 2
144 -- piece 17 starts where piece 16 ends
145 have piece17 := jpos17 (Lk n .Delta)
146 -- side 4 starts (at piece 14) at least 10 edges before piece 16
147 have side4_start := jpos_le (Lk n .Delta) (len5 n_pos) (q := 14) (q' := 16) (by omega) (by omega)
148 -- and ends (at piece 19) at least 10 edges after piece 17
149 have side4_end := jpos_le (Lk n .Delta) (len5 n_pos) (q := 17) (q' := 19) (by omega) (by omega)
150 refine ⟨?_, ?_⟩
151 · rw [pos_up n_pos (by omega)]
152 show jpos (Lk n .Delta) 14 + 2 ≤ jpos (Lk n .Delta) 16 + (pos (Lk n .Delta 1) 3 - u)
153 omega
154 · rw [pos_up n_pos (by omega)]
155 show jpos (Lk n .Delta) 16 + (pos (Lk n .Delta 1) 3 - u) + 2 ≤ jpos (Lk n .Delta) 19
156 omega
158/-- A vertex inside a side is at least two vertices from both ends of the rim. -/
159theorem inside_bounds {n J v : Nat} (hJ : J < 6) (inside : Inside n J v) :
160 2 ≤ v ∧ v + 2 ≤ pos (Lk n .Delta 1) 6 := by
161 -- `v` is at least two vertices after the start of side `J`
162 have after_start := inside.1
163 exact ⟨by omega, Nat.le_trans inside.2 (pos_mono _ (by omega))⟩
165/-! ### The map read side by side -/
167/-- From a vertex inside side `J` of `N_n` where the map names junction `q`, the strand runs on, one level up, to
168the hook at junction `q` of `N_{n+1}`. -/
169theorem adv_some {n : Nat} (n_pos : 1 ≤ n) {J v q : Nat} (hJ : J < 6) (inside : Inside n J v)
170 (side_tgt : sideTgt (ori n) J = some q) :
171 (N (n + 1)).Linked (upPort n 1 ((N n).bport (ori n) (v, true)))
172 ((N (n + 1)).bport (ori (n + 1)) (jpos (Lk n .Delta) q, true)) := by
173 -- `v` is a rim vertex of `N_n`, away from the corners
174 have v_bounds := inside_bounds hJ inside
175 exact step_tile n_pos (by omega) (by rw [tgt_side true hJ inside.1 inside.2]; exact side_tgt)
177/-- From a vertex inside side 2 of `N_n` (on the parent's rim), the strand is, one level up, on the hook at the same
178vertex of `N_{n+1}`. -/
179theorem adv_none {n : Nat} (n_pos : 1 ≤ n) {v : Nat} (inside : Inside n 2 v) :
180 (N (n + 1)).Linked (upPort n 1 ((N n).bport (ori n) (v, true)))
181 ((N (n + 1)).bport (ori (n + 1)) (stp (Lk n .Delta) v, true)) := by
182 -- `v` lies at least two vertices after the start of side 2
183 have after_start := inside.1
184 -- and two before its end, vertex `pos 3`
185 have before_three : v + 2 ≤ pos (Lk n .Delta 1) 3 := inside.2
186 rw [stretch_eq n_pos (by omega) (by omega), Bool.not_true]
187 -- the parent vertex lies inside side 4 of `N_{n+1}`, so it is a hook
188 have stp_inside := inside_stp n_pos (show pos (Lk n .Delta 1) 2 < v by omega) (by omega)
189 exact hook (by omega) (inside_bounds (by omega) stp_inside).1 (inside_bounds (by omega) stp_inside).2
191/-- `x` is on the strand of the hook at a vertex inside side `J` of `N_n`. -/
192def Reach (n J : Nat) (x : Port) : Prop :=
193 (N n).IsPort x ∧ ∃ v, Inside n J v ∧ (N n).Linked x ((N n).bport (ori n) (v, true))
195/-- A strand that reaches a hook inside side `J` of `N_n` reaches, one level up, the hook at the junction the map
196names for side `J`. -/
197theorem reach_some {n : Nat} (n_pos : 1 ≤ n) {J q : Nat} (hJ : J < 6) {x : Port} (reach : Reach n J x)
198 (side_tgt : sideTgt (ori n) J = some q) :
199 (N (n + 1)).Linked (upPort n 1 x) ((N (n + 1)).bport (ori (n + 1)) (jpos (Lk n .Delta) q, true)) := by
200 obtain ⟨x_port, v, inside, linked⟩ := reach
201 exact (lift_nest n_pos linked x_port).trans (adv_some n_pos hJ inside side_tgt)
203/-- A strand that reaches a hook inside side 2 of `N_n` (on the parent's rim) reaches, one level up, a hook inside
204side 4 of `N_{n+1}`. -/
205theorem reach_none {n : Nat} (n_pos : 1 ≤ n) {x : Port} (reach : Reach n 2 x) : Reach (n + 1) 4 (upPort n 1 x) := by
206 obtain ⟨x_port, v, inside, linked⟩ := reach
207 -- `v` lies at least two vertices after the start of side 2
208 have after_start := inside.1
209 -- and two before its end, vertex `pos 3`
210 have before_three : v + 2 ≤ pos (Lk n .Delta 1) 3 := inside.2
211 exact ⟨isPort_up n_pos x_port, _, inside_stp n_pos (by omega) (by omega),
212 (lift_nest n_pos linked x_port).trans (adv_none n_pos inside)⟩
214/-- A port of `N_{n+1}` on the strand of the hook at a junction inside side `J` reaches side `J`. -/
215theorem reach_of {n J q : Nat} {y : Port} (y_port : (N (n + 1)).IsPort y)
216 (inside : Inside (n + 1) J (jpos (Lk n .Delta) q))
217 (linked : (N (n + 1)).Linked y ((N (n + 1)).bport (ori (n + 1)) (jpos (Lk n .Delta) q, true))) :
218 Reach (n + 1) J y :=
219 ⟨y_port, _, inside, linked⟩
221/-! ### The first step: from a port of `N_b` -/
223/-- The map names no junction only strictly inside side 2. -/
224theorem tgt_none {ω : Bool} {f : Nat → Nat} {u : Nat} {s : Bool} (tgt_eq : tgt ω f u s = none) :
225 pos f 2 < u ∧ u < pos f 3 := by
226 unfold tgt at tgt_eq
227 revert tgt_eq
228 cases ω <;> simp only [Bool.false_eq_true, ite_false, ite_true] <;> (repeat' split) <;> intro tgt_eq <;>
229 first | omega | (exfalso; simp at tgt_eq)
231/-- For `ω = true` the map names only junctions 17, 9, 16 and 12. -/
232theorem tgt_vals_t {f : Nat → Nat} {u : Nat} {s : Bool} {q : Nat} (tgt_eq : tgt true f u s = some q) :
233 q = 17 ∨ q = 9 ∨ q = 16 ∨ q = 12 := by
234 unfold tgt at tgt_eq
235 revert tgt_eq
236 cases s <;> simp only [ite_true] <;> (repeat' split) <;> intro tgt_eq <;>
237 simp only [Option.some.injEq, reduceCtorEq] at tgt_eq <;> omega
239/-- For `ω = false` the map names only junctions 21, 16 and 17. -/
240theorem tgt_vals_f {f : Nat → Nat} {u : Nat} {s : Bool} {q : Nat} (tgt_eq : tgt false f u s = some q) :
241 q = 21 ∨ q = 16 ∨ q = 17 := by
242 unfold tgt at tgt_eq
243 revert tgt_eq
244 cases s <;> simp only [Bool.false_eq_true, ite_false] <;> (repeat' split) <;> intro tgt_eq <;>
245 simp only [Option.some.injEq, reduceCtorEq] at tgt_eq <;> omega
247/-- **The first step**: one level up, every port of `N_b` reaches a hook inside side 2, 3 or 4 of `N_{b+1}` (if
248`ω_b = true`, that is `b` even) or inside side 4 or 5 (if `ω_b = false`). Inside side 2, the hook is the one at
249junction 9. -/
250theorem first {b : Nat} (b_pos : 1 ≤ b) {x : Port} (x_port : (N b).IsPort x) :
251 ∃ J, Reach (b + 1) J (upPort b 1 x) ∧ (ori b = true → J = 2 ∨ J = 3 ∨ J = 4) ∧
252 (ori b = false → J = 4 ∨ J = 5) ∧
253 (J = 2 → (N (b + 1)).Linked (upPort b 1 x) ((N (b + 1)).bport (ori (b + 1)) (jpos (Lk b .Delta) 9, true))) := by
254 -- `N_b` has the signature
255 have good_b := good b .Delta b_pos
256 -- following the ribbon from `x` leaves `N_b` at a port `r`
257 obtain ⟨r, follows⟩ := good_b.sig.noClosed x x_port
258 obtain ⟨nothing_across, r_tile, r_vertex⟩ := Patch.Follow.end_ good_b.sig follows x_port.1 x_port.2
259 -- `r` is port `s` at a rim vertex `u`
260 obtain ⟨u, s, hu, rfl⟩ := Patch.rim_port good_b.sig r_tile r_vertex nothing_across
261 -- the rim of `N_b`
262 have rim_len := E_N b_pos
263 unfold N at rim_len
264 rw [rim_len] at hu
265 -- one level up, `x` is on the strand of that rim port
266 have lifted := lift_nest b_pos (.of_follow follows) x_port
267 -- and is a port of `N_{b+1}`
268 have x_up_port := isPort_up b_pos x_port
269 cases tgt_eq : tgt (ori b) (Lk b .Delta 1) u s with
270 | none =>
271 -- strictly inside child 1's side 2: the rim port is a hook of `N_{b+1}`, inside its side 4
272 obtain ⟨after_two, before_three⟩ := tgt_none tgt_eq
273 refine ⟨4, ⟨x_up_port, _, inside_stp b_pos after_two before_three, lifted.trans ?_⟩, fun _ => by omega,
274 fun _ => by omega, fun wrong => absurd wrong (by decide)⟩
275 -- the rim port of `N_b`, one level up, is a rim port of `N_{b+1}`
276 have same_port := stretch_eq b_pos after_two before_three s
277 rw [show N b = super b .Delta from rfl] at same_port
278 rw [same_port]
279 -- inside side 4 of `N_{b+1}`
280 have stp_inside := inside_stp b_pos after_two before_three
281 cases s
282 · exact .refl
283 · exact hook (by omega) (inside_bounds (by omega) stp_inside).1 (inside_bounds (by omega) stp_inside).2
284 | some q =>
285 -- one level up, the strand runs on to the hook at junction `q`
286 have to_junction := lifted.trans (step_tile b_pos hu tgt_eq)
287 cases orient : ori b
288 · rw [orient] at tgt_eq
289 rcases tgt_vals_f tgt_eq with rfl | rfl | rfl
290 · exact ⟨5, reach_of x_up_port (inside_21 b_pos) to_junction, fun wrong => by simp at wrong, fun _ => by omega,
291 fun wrong => absurd wrong (by decide)⟩
292 · exact ⟨4, reach_of x_up_port (inside_16 b_pos) to_junction, fun wrong => by simp at wrong, fun _ => by omega,
293 fun wrong => absurd wrong (by decide)⟩
294 · exact ⟨4, reach_of x_up_port (inside_17 b_pos) to_junction, fun wrong => by simp at wrong, fun _ => by omega,
295 fun wrong => absurd wrong (by decide)⟩
296 · rw [orient] at tgt_eq
297 rcases tgt_vals_t tgt_eq with rfl | rfl | rfl | rfl
298 · exact ⟨4, reach_of x_up_port (inside_17 b_pos) to_junction, fun _ => by omega, fun wrong => by simp at wrong,
299 fun wrong => absurd wrong (by decide)⟩
300 · exact ⟨2, reach_of x_up_port (inside_9 b_pos) to_junction, fun _ => by omega, fun wrong => by simp at wrong,
301 fun _ => to_junction⟩
302 · exact ⟨4, reach_of x_up_port (inside_16 b_pos) to_junction, fun _ => by omega, fun wrong => by simp at wrong,
303 fun wrong => absurd wrong (by decide)⟩
304 · exact ⟨3, reach_of x_up_port (inside_12 b_pos) to_junction, fun _ => by omega, fun wrong => by simp at wrong,
305 fun wrong => absurd wrong (by decide)⟩
307/-! ### The chain -/
309/-- The hook at junction 12 of `N_{n+1}`, where every strand of the block three or four levels down ends up. -/
310def Zp (n : Nat) : Port := (N (n + 1)).bport (ori (n + 1)) (jpos (Lk n .Delta) 12, true)
312/-- Even levels have `ω = true`. -/
313theorem ori_even {n : Nat} (even : n % 2 = 0) : ori n = true := by simp [ori, even]
314/-- Odd levels have `ω = false`. -/
315theorem ori_odd {n : Nat} (odd : n % 2 = 1) : ori n = false := by simp [ori, odd]
In the paper Theorem 9.1 Merging, Theorem B The Ariadne Theorem
317/-- **Even `b`**: every port of `N_b` lies, in `N_{b+3}`, on the strand of the hook at junction 12. -/
318theorem chain_even {b : Nat} (b_pos : 1 ≤ b) (even : b % 2 = 0) {x : Port} (x_port : (N b).IsPort x) :
319 (N (b + 3)).Linked (upPort b 3 x) (Zp (b + 2)) := by
320 -- level `b` is even
321 have ori_b := ori_even even
322 -- level `b + 1` odd
323 have ori_b1 : ori (b + 1) = false := ori_odd (by omega)
324 -- and level `b + 2` even
325 have ori_b2 : ori (b + 2) = true := ori_even (by omega)
326 -- one level up: inside side 2, 3 or 4
327 obtain ⟨J, reach_J, sides_even, _, _⟩ := first b_pos x_port
328 -- two levels up: inside side 4
329 have reach_four : Reach (b + 2) 4 (upPort (b + 1) 1 (upPort b 1 x)) := by
330 -- the port, one level up, is a port of `N_{b+1}`
331 have up_port := isPort_up (show 1 ≤ b + 1 by omega) reach_J.1
332 rcases sides_even ori_b with rfl | rfl | rfl
333 · exact reach_none (by omega) reach_J
334 · exact reach_of up_port (inside_16 (by omega)) (reach_some (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
335 · exact reach_of up_port (inside_16 (by omega)) (reach_some (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
336 -- three levels up: the hook at junction 12
337 exact reach_some (n := b + 2) (by omega) (by omega) reach_four (by rw [ori_b2]; rfl)
In the paper Theorem 9.1 Merging, Theorem B The Ariadne Theorem
339/-- **Odd `b`**: every port of `N_b` lies, in `N_{b+4}`, on the strand of the hook at junction 12. -/
340theorem chain_odd {b : Nat} (b_pos : 1 ≤ b) (odd : b % 2 = 1) {x : Port} (x_port : (N b).IsPort x) :
341 (N (b + 4)).Linked (upPort b 4 x) (Zp (b + 3)) := by
342 -- level `b` is odd
343 have ori_b := ori_odd odd
344 -- level `b + 1` even
345 have ori_b1 : ori (b + 1) = true := ori_even (by omega)
346 -- level `b + 2` odd
347 have ori_b2 : ori (b + 2) = false := ori_odd (by omega)
348 -- and level `b + 3` even
349 have ori_b3 : ori (b + 3) = true := ori_even (by omega)
350 -- one level up: inside side 4 or 5
351 obtain ⟨J, reach_J, _, sides_odd, _⟩ := first b_pos x_port
352 -- the port, one level up, is a port of `N_{b+1}`
353 have up_port := isPort_up (show 1 ≤ b + 1 by omega) reach_J.1
354 -- three levels up: inside side 4
355 have reach_four : Reach (b + 3) 4 (upPort (b + 2) 1 (upPort (b + 1) 1 (upPort b 1 x))) := by
356 -- the port, two levels up, is a port of `N_{b+2}`
357 have up_port2 := isPort_up (show 1 ≤ b + 2 by omega) up_port
358 rcases sides_odd ori_b with rfl | rfl
359 · -- from side 4
360 -- two levels up, inside side 3
361 have reach_three : Reach (b + 2) 3 (upPort (b + 1) 1 (upPort b 1 x)) :=
362 reach_of up_port (inside_12 (by omega)) (reach_some (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
363 exact reach_of up_port2 (inside_16 (by omega))
364 (reach_some (by omega) (by omega) reach_three (by rw [ori_b2]; rfl))
365 · -- from side 5
366 -- two levels up, inside side 2
367 have reach_two : Reach (b + 2) 2 (upPort (b + 1) 1 (upPort b 1 x)) :=
368 reach_of up_port (inside_9 (by omega)) (reach_some (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
369 exact reach_none (by omega) reach_two
370 -- four levels up: the hook at junction 12
371 exact reach_some (n := b + 3) (by omega) (by omega) reach_four (by rw [ori_b3]; rfl)
373/-- Any number of levels up, a port of `N_b` is still a port. -/
374theorem isPort_upk {b : Nat} (b_pos : 1 ≤ b) {x : Port} (x_port : (N b).IsPort x) :
375 ∀ k, (N (b + k)).IsPort (upPort b k x)
376 | 0 => x_port
377 | k + 1 => by rw [upPort_succ]; exact isPort_up (m := b + k) (by omega) (isPort_upk b_pos x_port k)
In the paper Theorem 9.1 Merging, Theorem B The Ariadne Theorem
379/-- **Theorem B with the paper's bound.** -/
381 intro b p q b_pos hp hq
382 rcases Nat.mod_two_eq_zero_or_one b with even | odd
383 · -- even `b`
384 -- both ports reach the hook at junction 12 of `N_{b+3}`, so they lie on one strand there
385 have linked3 : (N (b + 3)).Linked (upPort b 3 p) (upPort b 3 q) :=
386 (chain_even b_pos even hp).trans
387 (linked_symm (m := b + 3) (by omega) (chain_even b_pos even hq) (isPort_upk b_pos hq 3))
388 refine ⟨?_, fun _ => linked3⟩
389 -- and one level further up, in `N_{b+4}`
390 have linked4 := lift_nest (m := b + 3) (by omega) linked3 (isPort_upk b_pos hp 3)
391 rw [← upPort_succ, ← upPort_succ] at linked4
392 exact linked4
393 · -- odd `b`: both ports reach the hook at junction 12 of `N_{b+4}`
394 exact ⟨(chain_odd b_pos odd hp).trans
395 (linked_symm (m := b + 4) (by omega) (chain_odd b_pos odd hq) (isPort_upk b_pos hq 4)),
396 fun is_even => absurd is_even (by omega)⟩
398/-! ### No boundary -/
400/-- An edge glued in `N_m` stays glued in `N_{m+1}`. -/
401theorem glue_up {m : Nat} (m_pos : 1 ≤ m) {t i : Nat} (ht : t < (N m).tiles) {e : Nat × Nat}
402 (glued : (N m).glue t i = some e) : ∃ e', (N (m + 1)).glue (up m 1 t) i = some e' := by
403 rw [N_succ m_pos]
404 -- the children of `N_{m+1}`
405 have kids := KD m_pos
406 -- the same gluing, in child 1
407 have glued_child : (kidsD m 1).glue t i = some e := glued
408 show ∃ e', (Par m).glue (t + offC (kidsD m) 1) i = some e'
409 rw [kids.glue_shift (c := 1) (by decide) ht]
410 unfold glueAt
411 rw [glued_child]
412 exact ⟨_, rfl⟩
414/-- Child 1's sides other than side 2 are glued to siblings. -/
415theorem mate_some {n : Nat} (n_pos : 1 ≤ n) {p j : Nat} (hj : j < 6) (not_two : j ≠ 2)
416 (after_start : pos (Lk n .Delta 1) j ≤ p) (before_end : p < pos (Lk n .Delta 1) (j + 1)) :
417 ∃ e, (Comp.ofLens .Delta (Lk n .Delta) (dOff n) (ori n)).toGluing.mate 1 p = some e := by
418 -- side `j` has `L 1 j` edges
419 have side_len := pos_succ (Lk n .Delta 1) j
420 obtain ⟨o, rfl⟩ : ∃ o, p = pos (Lk n .Delta 1) j + o := ⟨p - pos (Lk n .Delta 1) j, by omega⟩
421 show ∃ e, (Comp.ofLens .Delta (Lk n .Delta) (dOff n) (ori n)).mate 1 (pos (Lk n .Delta 1) j + o) = some e
422 rw [ofLens_mate (fun c _ j _ => by
423 -- every side has an edge
424 have := len5 n_pos c j
425 omega) (by decide) hj (by omega)]
426 cases adj : adjAt .Delta 1 j with
427 | none => exact absurd (adj_one_none j hj adj) not_two
428 | some _ => exact ⟨_, rfl⟩
In the paper Lemma 8.3 Grandparent Lemma
430/-- **No boundary** (Lemma 8.3(b)): every edge of `N_b` is glued in `N_{b+2}`. -/
431theorem no_boundary {b : Nat} (b_pos : 1 ≤ b) {t i : Nat} (ht : t < (N b).tiles) (hi : i < 14) :
432 ((N (b + 2)).glue (up b 2 t) i).isSome := by
433 -- `N_b` has the signature
434 have good_b := good b .Delta b_pos
435 -- so does `N_{b+1}`, of level at least 1
436 have b1_pos : 1 ≤ b + 1 := by omega
437 -- the tile, one level up, is a tile of `N_{b+1}`
438 have t_up : up b 1 t < (N (b + 1)).tiles := (isPort_up b_pos (x := (t, i, true)) ⟨ht, hi⟩).1
439 -- an edge glued in `N_{b+1}` is glued in `N_{b+2}`
440 have glued_up : ∀ e, (N (b + 1)).glue (up b 1 t) i = some e → ((N (b + 2)).glue (up b 2 t) i).isSome := by
441 intro e glued
442 obtain ⟨e', glued'⟩ := glue_up b1_pos t_up glued
443 rw [show up b 2 t = up (b + 1) 1 (up b 1 t) from rfl, glued']; rfl
444 cases glued_b : (N b).glue t i with
445 | some e =>
446 -- glued in `N_b`, so in `N_{b+1}`
447 obtain ⟨e', glued'⟩ := glue_up b_pos ht glued_b
448 exact glued_up e' glued'
449 | none =>
450 -- a rim edge of `N_b`, at rim position `k`
451 obtain ⟨k, hk, at_k⟩ := good_b.sig.rim_all t i ht hi glued_b
452 -- the children of `N_{b+1}`
453 have kids := KD b_pos
454 -- the rim of `N_b`
455 have rim_len := E_N b_pos
456 unfold N at rim_len
457 -- so `k` is a rim position of child 1
458 have k_lt : k < pos (Lk b .Delta 1) 6 := by rw [← rim_len]; exact hk
459 -- `N_{b+1}` glues the edge as the gluing's `mate` says
460 have formula := kids.glue_rimEdge (c := 1) (by decide) hk
461 -- the edge, as rim edge `k` of child 1
462 have at_k' : (kidsD b 1).edgeAt k = (t, i) := at_k
463 rw [at_k'] at formula
464 -- its side `j` and offset `o`
465 obtain ⟨j, o, hj, ho, k_eq⟩ := decomp (Lk b .Delta 1) 6 (Nat.le_refl _) k k_lt
466 -- side `j` has `L 1 j` edges
467 have side_len := pos_succ (Lk b .Delta 1) j
468 by_cases side_two : j = 2
469 · -- on child 1's side 2: a rim edge of `N_{b+1}`, on its side 4
470 subst side_two
471 -- side 2 of child 1 lies on the parent's rim
472 have on_rim : (Comp.ofLens .Delta (Lk b .Delta) (dOff b) (ori b)).toGluing.mate 1 k = none := by
473 rw [k_eq]
474 exact ofLens_mate_none (fun c j => by
475 -- every side has an edge
476 have := len5 b_pos c j
477 omega) (by decide) (by omega) ho rfl
478 -- so the edge is the parent's rim edge at some position `p`
479 obtain ⟨p, hp, own_p⟩ := own_surj (d := dOff b) (ω := ori b) kids.len_pos (by decide) k_lt on_rim
480 -- piece 17 starts where piece 16 ends
481 have piece17 := jpos17 (Lk b .Delta)
482 -- and the rim ends at least 25 edges later
483 have to_end := jpos_le (Lk b .Delta) (len5 b_pos) (q := 17) (q' := 22) (by omega) (by omega)
484 -- where the pieces end
485 have pieces_end := jpos_full (Lk b .Delta)
486 -- `p` is on piece 16, child 1's side 2
487 have p_eq : p = jpos (Lk b .Delta) 16 + (Lk b .Delta 1 2 - 1 - o) := by
488 apply own_inj kids.len_pos hp (by omega)
489 rw [own_p, ownGo16 _ (by omega), k_eq]
490 -- the same edge of child 1
491 have edge_eq : pos (Lk b .Delta 1) 2 + Lk b .Delta 1 2 - 1 - (Lk b .Delta 1 2 - 1 - o) =
492 pos (Lk b .Delta 1) 2 + o := by omega
493 rw [edge_eq]
494 -- the edge at rim position `p` of `N_{b+1}` is `(up b 1 t, i)`
495 have edge_p : (kidsD (b + 1) 1).edgeAt p = (up b 1 t, i) := by
496 show (N (b + 1)).edgeAt p = _
497 rw [N_succ b_pos, rim_edgeAt kids.shape hp, own_p, at_k']
498 rfl
499 -- the children of `N_{b+2}`
500 have kids' := KD b1_pos
501 -- `p` is a rim position of `N_{b+1}`, child 1 of `N_{b+2}`
502 have p_lt : p < (kidsD (b + 1) 1).E := by
503 show p < (N (b + 1)).E
504 rw [N_succ b_pos, compose_E kids.shape]; exact hp
505 -- `N_{b+2}` glues it as `mate` says
506 have formula' := kids'.glue_rimEdge (c := 1) (by decide) p_lt
507 rw [edge_p] at formula'
508 -- side 4 of `N_{b+1}` starts at piece 14
509 have side4_start := pos_up b_pos (J := 4) (by omega)
510 -- and side 5 at piece 19
511 have side5_start := pos_up b_pos (J := 5) (by omega)
512 -- piece 16 starts at least 10 edges after piece 14
513 have from14 := jpos_le (Lk b .Delta) (len5 b_pos) (q := 14) (q' := 16) (by omega) (by omega)
514 -- and piece 19 at least 10 edges after piece 17
515 have to19 := jpos_le (Lk b .Delta) (len5 b_pos) (q := 17) (q' := 19) (by omega) (by omega)
516 -- side 4 of child 1 of `N_{b+2}` is glued to a sibling
517 obtain ⟨e, mated⟩ := mate_some b1_pos (j := 4) (p := p) (by omega) (by omega)
518 (by rw [side4_start]; show jpos (Lk b .Delta) 14 ≤ p; omega)
519 (by rw [side5_start]; show p < jpos (Lk b .Delta) 19; omega)
520 rw [mated] at formula'
521 rw [N_succ (show 1 ≤ b + 1 by omega)]
522 show ((Par (b + 1)).glue (up b 1 t + offC (kidsD (b + 1)) 1) i).isSome
523 rw [formula']; rfl
524 · -- on another side: glued to a sibling in `N_{b+1}`
525 obtain ⟨e, mated⟩ := mate_some b_pos (j := j) (p := k) hj side_two (by omega) (by omega)
526 rw [mated, Option.map_some] at formula
527 exact glued_up _ (by rw [N_succ b_pos]; exact formula)
529/-! ### Theorem B -/
In the paper Theorem 9.1 Merging, Theorem B The Ariadne Theorem
531/-- **Theorem B** (as stated in `Statement.lean`). -/
532theorem theoremB : TheoremB := by
533 refine ⟨fun b b_pos t i ht hi => no_boundary b_pos ht hi, fun b => theoremA b .Delta, ?_⟩
534 intro b p q hp hq
535 rcases Nat.eq_zero_or_pos b with rfl | b_pos
536 · -- `N_0` is one tile, tile 1 of `N_1`
537 -- `N_1` has nine tiles
538 have nine : (N 1).tiles = 9 := by decide
539 -- `p` is on the one tile of `N_0`
540 have p_tile : p.1 < 1 := hp.1
541 -- and so is `q`
542 have q_tile : q.1 < 1 := hq.1
543 -- one level up, `p` is a port of `N_1`
544 have p_up : (N 1).IsPort (upPort 0 1 p) := ⟨show p.1 + 1 < (N 1).tiles by omega, hp.2⟩
545 -- and so is `q`
546 have q_up : (N 1).IsPort (upPort 0 1 q) := ⟨show q.1 + 1 < (N 1).tiles by omega, hq.2⟩
547 exact ⟨5, (theoremB_sharp 1 _ _ (Nat.le_refl _) p_up q_up).1⟩
548 · exact ⟨4, (theoremB_sharp b p q b_pos hp hq).1⟩
550end SpectreKnot.Statement

← SpectreKnot/ProofA.leanSpectreKnot/ProofStrand.lean →