lean/SpectreKnot/NewWalk.lean
362 lines · 20 declarations, each with its own page · on GitHub ·
Walks through the two new vertices of a cut edge (paper Lemma 7.1: a cut creates no closed strand; Lemma 9.3: the new vertices). When an edge shared by two children is cut into three, each child gets two new vertices on it. The ribbon from a port at a new vertex follows one of the two connections of the zigzag lemma along the new path, for one or two crossings, to a port at an old vertex next to the cut, and runs on from there (step0_2F, …). So a cut creates no closed strand (noLoops). And the strand through a new vertex's hook is the strand that, before the cut, ran through the hook at the old vertex next to it, the port of the same hand: e₀ + 2 follows the old e₀, and e₀ + 1 the old e₀ + 1 (and the same on the other side; nw0_2F, …). That carries the junction map (StepMap.lean) through moves.
← SpectreKnot/ParentSig.leanSpectreKnot/StepMap.lean →
All 39 files, and the declarations of this one
1/-
2Walks through the two new vertices of a cut edge (paper Lemma 7.1: a cut creates no closed strand; Lemma 9.3: the new
3vertices). When an edge shared by two children is cut into three, each child gets two new vertices on it. The ribbon
4from a port at a new vertex follows one of the two connections of the zigzag lemma along the new path, for one or two
5crossings, to a port at an old vertex next to the cut, and runs on from there (`step0_2F`, …). So a cut creates no
6closed strand (`noLoops`). And the strand through a new vertex's hook is the strand that, before the cut, ran through
7the hook at the old vertex next to it, the port of the same hand: `e₀ + 2` follows the old `e₀`, and `e₀ + 1` the old
8`e₀ + 1` (and the same on the other side; `nw0_2F`, …). That carries the junction map (`StepMap.lean`) through moves.
9-/
10import SpectreKnot.Subdivide
12namespace SpectreKnot.Gluing
14/-- The first step of a walk, then the rest: if from `x` the piece and then the crossing lead to `y`, and the walk
15from `y` ends at `r`, then the walk from `x` ends at `r`. -/
16theorem fullReach_step {G : Gluing} {x y r : GPort} (first_step : G.sigma (G.tau x) = some y)
17 (rest : G.FullReach y r) : G.FullReach x r := by
18 obtain ⟨k, rest_walk⟩ := rest
19 exact ⟨k + 1, .step first_step rest_walk⟩
21/-- A walk whose first step lands on `y` goes on from `y`: if the walk from `x` ends at `r`, so does the walk from
22`y`. -/
23theorem fullReach_first {G : Gluing} {x y r : GPort} (first_step : G.sigma (G.tau x) = some y)
24 (walk : G.FullReach x r) : G.FullReach y r := by
25 obtain ⟨k, walk_k⟩ := walk
26 cases walk_k with
27 | stop at_rim =>
28 -- the walk cannot stop at once: its first crossing exists
29 rw [first_step] at at_rim; contradiction
30 | step step_to rest_walk =>
31 -- the walk's first step is the same step, to `y`
32 rw [first_step] at step_to
33 simp only [Option.some.injEq] at step_to
34 subst step_to
35 exact ⟨_, rest_walk⟩
37namespace Cut.OK
39set_option linter.unusedSectionVars false
41-- `ok`: the cut `κ` can be made in `G`
44include ok
46/-- A walk of `G` from an actual port, carried into the cut gluing: it starts and ends at the same ports, with
47positions after the cut moved on by 2. -/
48theorem port_reach {x r : GPort} (x_valid : G.Valid x) (walk : G.FullReach x r) :
50 obtain ⟨k, walk_k⟩ := walk
53section
54-- `shared`: the cut edge is shared by two children, `c₀` and `c₁`
55variable (shared : κ.two = true)
56include shared
58/-! ### From a new port to an old one -/
60/-- New vertex `e₀ + 2` of `c₀`, port `L`: through the new hook and across new edge `e₀ + 2`, the ribbon reaches
61`R_{c₁}` at the old vertex `e₁`, and runs on from there. -/
64 -- the cut edge is not the last edge of `c₀`
65 have e₀_succ_lt := ok.e₀
67 refine fullReach_step ?_ walk
68 rw [ok.tau_new₀ (by omega) (by omega), Bool.not_false, sigmaR, ok.mate_new₀ (by omega), ite_eq_left shared]
69 simp
71/-- New vertex `e₀ + 2` of `c₀`, port `R`: across new edges `e₀ + 1` and `e₁ + 2`, through the new hook of `c₁` at
72`e₁ + 2`, the ribbon reaches `R_{c₀}` at the old vertex `e₀`, and runs on from there. -/
75 -- the cut edge is not the last edge of `c₀`
76 have e₀_succ_lt := ok.e₀
77 -- nor is its mate the last edge of `c₁`
78 have e₁_succ_lt := ok.e₁ shared
80 refine fullReach_step (y := (κ.c₁, κ.e₁ + 2, false)) ?_ (fullReach_step ?_ walk)
81 · rw [ok.tau_new₀ (by omega) (by omega), Bool.not_true, sigmaL, ok.E_c₀, show κ.e₀ + 2 = (κ.e₀ + 1) + 1 from rfl,
83 simp only [Option.map_some, show κ.e₁ + 2 - 1 = κ.e₁ + 1 by omega, ok.E_c₁ shared, nxt_of_lt' (show κ.e₁ + 1 + 1 <
84 (G.E κ.c₁ + 2) by omega)]
85 · rw [ok.tau_new₁ shared (by omega) (by omega), Bool.not_false, sigmaR, ok.mate_new₁ shared (by omega)]
86 simp
88/-- New vertex `e₀ + 1` of `c₀`, port `R`: through the new hook and across new edge `e₀`, the ribbon reaches `L_{c₁}`
89at the old vertex `e₁ + 1`, and runs on from there. -/
92 -- the cut edge is not the last edge of `c₀`
93 have e₀_succ_lt := ok.e₀
94 -- nor is its mate the last edge of `c₁`
95 have e₁_succ_lt := ok.e₁ shared
97 refine fullReach_step ?_ walk
98 rw [ok.tau_new₀ (by omega) (by omega), Bool.not_true, sigmaL, prv_succ', ok.mate_cut₀, ite_eq_left shared]
99 simp only [Option.map_some, ok.E_c₁ shared, nxt_of_lt' (show κ.e₁ + 2 + 1 < G.E κ.c₁ + 2 by omega)]
101/-- New vertex `e₀ + 1` of `c₀`, port `L`: across new edges `e₀ + 1` and `e₁`, through the new hook of `c₁` at
102`e₁ + 1`, the ribbon reaches `L_{c₀}` at the old vertex `e₀ + 1`, and runs on from there. -/
103theorem step0_1F {r : GPort} (walk : (subdiv G κ).FullReach (κ.port (κ.c₀, κ.e₀ + 1, false)) r) :
105 -- the cut edge is not the last edge of `c₀`
106 have e₀_succ_lt := ok.e₀
107 -- nor is its mate the last edge of `c₁`
108 have e₁_succ_lt := ok.e₁ shared
110 refine fullReach_step (y := (κ.c₁, κ.e₁ + 1, true)) ?_ (fullReach_step ?_ walk)
111 · rw [ok.tau_new₀ (by omega) (by omega), Bool.not_false, sigmaR, ok.mate_new₀ (by omega), ite_eq_left shared]
112 simp only [Option.map_some, show κ.e₁ + 2 - 1 = κ.e₁ + 1 by omega]
113 · rw [ok.tau_new₁ shared (by omega) (by omega), Bool.not_true, sigmaL, prv_succ', ok.mate_cut₁ shared]
114 simp only [Option.map_some, ok.E_c₀, nxt_of_lt' (show κ.e₀ + 2 + 1 < G.E κ.c₀ + 2 by omega)]
116/-- New vertex `e₁ + 2` of `c₁`, port `L`: through the new hook and across new edge `e₁ + 2`, the ribbon reaches
117`R_{c₀}` at the old vertex `e₀`, and runs on from there. -/
120 -- the cut edge is not the last edge of `c₀`
121 have e₀_succ_lt := ok.e₀
123 refine fullReach_step ?_ walk
124 rw [ok.tau_new₁ shared (by omega) (by omega), Bool.not_false, sigmaR, ok.mate_new₁ shared (by omega)]
125 simp
127/-- New vertex `e₁ + 2` of `c₁`, port `R`: across new edges `e₁ + 1` and `e₀ + 2`, through the new hook of `c₀` at
128`e₀ + 2`, the ribbon reaches `R_{c₁}` at the old vertex `e₁`, and runs on from there. -/
131 -- the cut edge is not the last edge of `c₀`
132 have e₀_succ_lt := ok.e₀
133 -- nor is its mate the last edge of `c₁`
134 have e₁_succ_lt := ok.e₁ shared
136 refine fullReach_step (y := (κ.c₀, κ.e₀ + 2, false)) ?_ (fullReach_step ?_ walk)
139 simp only [Option.map_some, show κ.e₀ + 2 - 1 = κ.e₀ + 1 by omega, ok.E_c₀,
140 nxt_of_lt' (show κ.e₀ + 1 + 1 < G.E κ.c₀ + 2 by omega)]
141 · rw [ok.tau_new₀ (by omega) (by omega), Bool.not_false, sigmaR, ok.mate_new₀ (by omega), ite_eq_left shared]
142 simp
144/-- New vertex `e₁ + 1` of `c₁`, port `R`: through the new hook and across new edge `e₁`, the ribbon reaches `L_{c₀}`
145at the old vertex `e₀ + 1`, and runs on from there. -/
146theorem step1_1T {r : GPort} (walk : (subdiv G κ).FullReach (κ.port (κ.c₀, κ.e₀ + 1, false)) r) :
148 -- the cut edge is not the last edge of `c₀`
149 have e₀_succ_lt := ok.e₀
150 -- nor is its mate the last edge of `c₁`
151 have e₁_succ_lt := ok.e₁ shared
153 refine fullReach_step ?_ walk
154 rw [ok.tau_new₁ shared (by omega) (by omega), Bool.not_true, sigmaL, prv_succ', ok.mate_cut₁ shared]
155 simp only [Option.map_some, ok.E_c₀, nxt_of_lt' (show κ.e₀ + 2 + 1 < G.E κ.c₀ + 2 by omega)]
157/-- New vertex `e₁ + 1` of `c₁`, port `L`: across new edges `e₁ + 1` and `e₀`, through the new hook of `c₀` at
158`e₀ + 1`, the ribbon reaches `L_{c₁}` at the old vertex `e₁ + 1`, and runs on from there. -/
159theorem step1_1F {r : GPort} (walk : (subdiv G κ).FullReach (κ.port (κ.c₁, κ.e₁ + 1, false)) r) :
161 -- the cut edge is not the last edge of `c₀`
162 have e₀_succ_lt := ok.e₀
163 -- nor is its mate the last edge of `c₁`
164 have e₁_succ_lt := ok.e₁ shared
166 refine fullReach_step (y := (κ.c₀, κ.e₀ + 1, true)) ?_ (fullReach_step ?_ walk)
167 · rw [ok.tau_new₁ shared (by omega) (by omega), Bool.not_false, sigmaR, ok.mate_new₁ shared (by omega)]
168 simp only [Option.map_some, show κ.e₀ + 2 - 1 = κ.e₀ + 1 by omega]
169 · rw [ok.tau_new₀ (by omega) (by omega), Bool.not_true, sigmaL, prv_succ', ok.mate_cut₀, ite_eq_left shared]
170 simp only [Option.map_some, ok.E_c₁ shared, nxt_of_lt' (show κ.e₁ + 2 + 1 < G.E κ.c₁ + 2 by omega)]
172/-! ### The same strand as before the cut (Lemma 9.3) -/
174/-- New vertex `e₀ + 2` of `c₀`, port `L`: the walk from `L(e₀ + 2)` in the cut gluing ends where the walk from the
175old `L(e₀)` ended in `G` (when `e₀` is not a corner of `c₀`). -/
176theorem nw0_2F (not_corner : G.corner κ.c₀ κ.e₀ = false) {r : GPort} (old_walk : G.FullReach (κ.c₀, κ.e₀, false) r) :
178 -- the mate of the cut edge is an actual edge of an actual child
179 obtain ⟨c₁_lt, e₁_lt, _⟩ := ok.two_mate shared
180 -- in `G`: through the hook at `e₀` to `R_{c₀}(e₀)`, then across the cut edge to `R_{c₁}(e₁)`
181 have first_step : G.sigma (G.tau (κ.c₀, κ.e₀, false)) = some (κ.c₁, κ.e₁, true) := by
182 rw [tau_of_not_corner not_corner, Bool.not_false, sigmaR]
183 -- the cut edge is edge `e₁` of `c₁`
184 have cut_mate := ok.mate
185 rw [ite_eq_left shared] at cut_mate
186 rw [cut_mate]; rfl
187 -- in the cut gluing, one step from `L(e₀ + 2)` reaches `R_{c₁}(e₁)` too; from there, the rest of the old walk
188 exact ok.step0_2F shared (ok.port_reach ⟨c₁_lt, e₁_lt⟩ (fullReach_first first_step old_walk))
190/-- New vertex `e₀ + 2` of `c₀`, port `R`: the walk from `R(e₀ + 2)` in the cut gluing ends where the walk from the
191old `R(e₀)` ended in `G`. -/
194 -- the cut edge is not the last edge of `c₀`
195 have e₀_succ_lt := ok.e₀
196 -- two steps from `R(e₀ + 2)` reach `R_{c₀}(e₀)`; from there, the old walk
197 exact ok.step0_2T shared (ok.port_reach ⟨ok.c₀, show κ.e₀ < G.E κ.c₀ by omega⟩ old_walk)
199/-- New vertex `e₀ + 1` of `c₀`, port `R`: the walk from `R(e₀ + 1)` in the cut gluing ends where the walk from the
200old `R(e₀ + 1)` ended in `G` (when the old `e₀ + 1` is not a corner of `c₀`). -/
202 (old_walk : G.FullReach (κ.c₀, κ.e₀ + 1, true) r) :
204 -- the mate of the cut edge is an actual edge of an actual child
205 obtain ⟨c₁_lt, e₁_lt, _⟩ := ok.two_mate shared
206 -- and not its last edge
207 have e₁_succ_lt := ok.e₁ shared
208 -- in `G`: through the hook at the old `e₀ + 1` to `L`, then across the cut edge to `L_{c₁}(e₁ + 1)`
209 have first_step : G.sigma (G.tau (κ.c₀, κ.e₀ + 1, true)) = some (κ.c₁, κ.e₁ + 1, false) := by
210 rw [tau_of_not_corner not_corner, Bool.not_true, sigmaL, prv_succ']
211 -- the cut edge is edge `e₁` of `c₁`
212 have cut_mate := ok.mate
213 rw [ite_eq_left shared] at cut_mate
214 rw [cut_mate]
215 simp only [Option.map_some, nxt_of_lt' e₁_succ_lt]
216 -- in the cut gluing, one step from `R(e₀ + 1)` reaches `L_{c₁}` at the old `e₁ + 1` too; then the rest of the old
217 -- walk
218 exact ok.step0_1T shared
219 (ok.port_reach ⟨c₁_lt, show κ.e₁ + 1 < G.E κ.c₁ by omega⟩ (fullReach_first first_step old_walk))
221/-- New vertex `e₀ + 1` of `c₀`, port `L`: the walk from `L(e₀ + 1)` in the cut gluing ends where the walk from the
222old `L(e₀ + 1)` ended in `G`. -/
225 -- the cut edge is not the last edge of `c₀`
226 have e₀_succ_lt := ok.e₀
227 -- two steps from `L(e₀ + 1)` reach `L_{c₀}` at the old `e₀ + 1`; from there, the old walk
228 exact ok.step0_1F shared (ok.port_reach ⟨ok.c₀, show κ.e₀ + 1 < G.E κ.c₀ by omega⟩ old_walk)
230/-- New vertex `e₁ + 2` of `c₁`, port `L`: the walk from `L(e₁ + 2)` in the cut gluing ends where the walk from the
231old `L(e₁)` ended in `G` (when `e₁` is not a corner of `c₁`). -/
232theorem nw1_2F (not_corner : G.corner κ.c₁ κ.e₁ = false) {r : GPort} (old_walk : G.FullReach (κ.c₁, κ.e₁, false) r) :
234 -- the cut edge is not the last edge of `c₀`
235 have e₀_succ_lt := ok.e₀
236 -- the cut edge's mate is glued back to it
237 obtain ⟨_, _, mate_back⟩ := ok.two_mate shared
238 -- in `G`: through the hook at `e₁` to `R_{c₁}(e₁)`, then across the cut edge to `R_{c₀}(e₀)`
239 have first_step : G.sigma (G.tau (κ.c₁, κ.e₁, false)) = some (κ.c₀, κ.e₀, true) := by
240 rw [tau_of_not_corner not_corner, Bool.not_false, sigmaR, mate_back]; rfl
241 -- in the cut gluing, one step from `L(e₁ + 2)` reaches `R_{c₀}(e₀)` too; from there, the rest of the old walk
242 exact ok.step1_2F shared
243 (ok.port_reach ⟨ok.c₀, show κ.e₀ < G.E κ.c₀ by omega⟩ (fullReach_first first_step old_walk))
245/-- New vertex `e₁ + 2` of `c₁`, port `R`: the walk from `R(e₁ + 2)` in the cut gluing ends where the walk from the
246old `R(e₁)` ended in `G`. -/
249 -- the mate of the cut edge is an actual edge of an actual child
250 obtain ⟨c₁_lt, e₁_lt, _⟩ := ok.two_mate shared
251 -- two steps from `R(e₁ + 2)` reach `R_{c₁}(e₁)`; from there, the old walk
252 exact ok.step1_2T shared (ok.port_reach ⟨c₁_lt, e₁_lt⟩ old_walk)
254/-- New vertex `e₁ + 1` of `c₁`, port `R`: the walk from `R(e₁ + 1)` in the cut gluing ends where the walk from the
255old `R(e₁ + 1)` ended in `G` (when the old `e₁ + 1` is not a corner of `c₁`). -/
257 (old_walk : G.FullReach (κ.c₁, κ.e₁ + 1, true) r) :
259 -- the cut edge is not the last edge of `c₀`
260 have e₀_succ_lt := ok.e₀
261 -- the cut edge's mate is glued back to it
262 obtain ⟨_, _, mate_back⟩ := ok.two_mate shared
263 -- in `G`: through the hook at the old `e₁ + 1` to `L`, then across the cut edge to `L_{c₀}(e₀ + 1)`
264 have first_step : G.sigma (G.tau (κ.c₁, κ.e₁ + 1, true)) = some (κ.c₀, κ.e₀ + 1, false) := by
265 rw [tau_of_not_corner not_corner, Bool.not_true, sigmaL, prv_succ', mate_back]
266 simp only [Option.map_some, nxt_of_lt' e₀_succ_lt]
267 -- in the cut gluing, one step from `R(e₁ + 1)` reaches `L_{c₀}` at the old `e₀ + 1` too; then the rest of the old
268 -- walk
269 exact ok.step1_1T shared
270 (ok.port_reach ⟨ok.c₀, show κ.e₀ + 1 < G.E κ.c₀ by omega⟩ (fullReach_first first_step old_walk))
272/-- New vertex `e₁ + 1` of `c₁`, port `L`: the walk from `L(e₁ + 1)` in the cut gluing ends where the walk from the
273old `L(e₁ + 1)` ended in `G`. -/
276 -- the mate of the cut edge is an actual edge of an actual child
277 obtain ⟨c₁_lt, _, _⟩ := ok.two_mate shared
278 -- and not its last edge
279 have e₁_succ_lt := ok.e₁ shared
280 -- two steps from `L(e₁ + 1)` reach `L_{c₁}` at the old `e₁ + 1`; from there, the old walk
281 exact ok.step1_1F shared (ok.port_reach ⟨c₁_lt, show κ.e₁ + 1 < G.E κ.c₁ by omega⟩ old_walk)
283end
285/-! ### A cut creates no closed strand (Lemma 7.1) -/
287/-- **A cut creates no closed strand** (the end of the proof of Lemma 7.1). If the walk of `G` from every port reaches
288the rim, so does the walk of the cut gluing from every port. From a port at an old vertex it is the image of a walk of
289`G` (`Sim.reach`). From a port at a new vertex it follows one of the two connections along the new path, for one or
290two crossings, to a port at an old vertex (`step0_2F`, …); or, if the cut edge lies on the rim, it leaves at once,
291through the new hook. -/
294 -- the cut edge is not the last edge of `c₀`
295 have e₀_lt := ok.e₀
296 -- from the image of a port of `G`: the image of its walk
298 obtain ⟨r, walk⟩ := no_loops y y_valid
299 exact ⟨κ.port r, ok.port_reach y_valid walk⟩
300 rintro ⟨c, v, s⟩ ⟨c_lt, v_lt⟩
301 by_cases new₀ : c = κ.c₀ ∧ κ.e₀ < v ∧ v ≤ κ.e₀ + 2
302 · obtain ⟨rfl, v_gt, v_le⟩ := new₀
303 obtain ⟨i, i_ge, i_le, rfl⟩ : ∃ i, 1 ≤ i ∧ i ≤ 2 ∧ v = κ.e₀ + i := ⟨v - κ.e₀, by omega, by omega, by omega⟩
304 by_cases shared : κ.two = true
305 · -- the mate of the cut edge is an actual edge of an actual child
306 obtain ⟨c₁_lt, e₁_lt, _⟩ := ok.two_mate shared
307 -- and not its last edge
308 have e₁_succ_lt := ok.e₁ shared
309 obtain rfl | rfl : i = 1 ∨ i = 2 := by omega
310 · cases s
311 · -- `L(e₀ + 1)`: to `L_{c₀}` at the old `e₀ + 1`
312 obtain ⟨r, walk⟩ := old (κ.c₀, κ.e₀ + 1, false) ⟨ok.c₀, e₀_lt⟩
313 exact ⟨r, ok.step0_1F shared walk⟩
314 · -- `R(e₀ + 1)`: to `L_{c₁}` at the old `e₁ + 1`
315 obtain ⟨r, walk⟩ := old (κ.c₁, κ.e₁ + 1, false) ⟨c₁_lt, e₁_succ_lt⟩
316 exact ⟨r, ok.step0_1T shared walk⟩
317 · cases s
318 · -- `L(e₀ + 2)`: to `R_{c₁}(e₁)`
319 obtain ⟨r, walk⟩ := old (κ.c₁, κ.e₁, true) ⟨c₁_lt, e₁_lt⟩
320 exact ⟨r, ok.step0_2F shared walk⟩
321 · -- `R(e₀ + 2)`: to `R_{c₀}(e₀)`
322 obtain ⟨r, walk⟩ := old (κ.c₀, κ.e₀, true) ⟨ok.c₀, show κ.e₀ < G.E κ.c₀ by omega⟩
323 exact ⟨r, ok.step0_2T shared walk⟩
324 · -- the cut edge lies on the rim: through the new hook, onto a new rim edge
326 rw [ok.tau_new₀ i_ge i_le]
327 cases s
328 · -- from `L` to `R`, on the new edge `e₀ + i`
330 · -- from `R` to `L`, on the new edge `e₀ + i - 1`
332 ok.mate_new₀ (by omega), ite_eq_right shared]; rfl
333 · by_cases new₁ : κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ < v ∧ v ≤ κ.e₁ + 2
334 · obtain ⟨shared, rfl, v_gt, v_le⟩ := new₁
335 -- the mate of the cut edge is an actual edge of an actual child
336 obtain ⟨c₁_lt, e₁_lt, _⟩ := ok.two_mate shared
337 -- and not its last edge
338 have e₁_succ_lt := ok.e₁ shared
339 obtain rfl | rfl : v = κ.e₁ + 1 ∨ v = κ.e₁ + 2 := by omega
340 · cases s
341 · -- `L(e₁ + 1)`: to `L_{c₁}` at the old `e₁ + 1`
342 obtain ⟨r, walk⟩ := old (κ.c₁, κ.e₁ + 1, false) ⟨c₁_lt, e₁_succ_lt⟩
343 exact ⟨r, ok.step1_1F shared walk⟩
344 · -- `R(e₁ + 1)`: to `L_{c₀}` at the old `e₀ + 1`
345 obtain ⟨r, walk⟩ := old (κ.c₀, κ.e₀ + 1, false) ⟨ok.c₀, e₀_lt⟩
346 exact ⟨r, ok.step1_1T shared walk⟩
347 · cases s
348 · -- `L(e₁ + 2)`: to `R_{c₀}(e₀)`
349 obtain ⟨r, walk⟩ := old (κ.c₀, κ.e₀, true) ⟨ok.c₀, show κ.e₀ < G.E κ.c₀ by omega⟩
350 exact ⟨r, ok.step1_2F shared walk⟩
351 · -- `R(e₁ + 2)`: to `R_{c₁}(e₁)`
352 obtain ⟨r, walk⟩ := old (κ.c₁, κ.e₁, true) ⟨c₁_lt, e₁_lt⟩
353 exact ⟨r, ok.step1_2T shared walk⟩
354 · -- an old vertex: the image of a port of `G`
355 obtain ⟨u, u_lt, shifted⟩ := ok.preimage v_lt new₀ new₁
356 obtain ⟨r, walk⟩ := old (c, u, s) ⟨c_lt, u_lt⟩
358 exact ⟨r, walk⟩
360end Cut.OK
362end SpectreKnot.Gluing