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

lean/SpectreKnot/Subdivide.lean

893 lines · 59 declarations, each with its own page · on GitHub ·

Simulations between gluings, and subdivision of an edge (paper Lemma 7.1, lengthening: the engine of the parity lemma).

← SpectreKnot/CompFull.leanSpectreKnot/Lens.lean →

All 39 files, and the declarations of this one
1/-
2Simulations between gluings, and subdivision of an edge (paper Lemma 7.1, lengthening: the engine of the parity lemma).
3
4A *simulation* `Sim G G' φ` maps the ports of `G` into those of `G'` so that `τ` commutes with `φ`, rim ports go to
5rim ports, and each crossing `σ x = y` of `G` becomes a forced chain of crossings `Cross (φ x) (φ y)` in `G'` (one
6crossing, or several joined by `τ`). Then every walk of `G` maps to a walk of `G'` (`Sim.reach`).
7
8*Subdividing* an edge into three (`subdiv`) is a simulation: by the zigzag lemma with `n = 3` (`cross_three`), crossing
9the three short edges ends where crossing the long one did. Lengthening a side of a composition by 2 is such a
10subdivision, so the parity lemma follows by repeated subdivision from the level-1 lengths. That a cut creates no closed
11strand is `Cut.OK.noLoops`, in `NewWalk.lean`.
12-/
16namespace SpectreKnot.Gluing
18variable {G G' : Gluing}
20/-! ### Forced chains of crossings -/
22/-- `Cross p q`: from port `p`, crossing an edge (`σ`) and then, while not yet at `q`, going through a piece (`τ`) and
23crossing again, leads to `q`: a connection of the zigzag lemma (`Zigzag.Chain`) in the gluing. -/
24abbrev Cross (G : Gluing) : GPort → GPort → Prop := Zigzag.Chain G.sigma G.tau
26/-- A forced chain of crossings from `p` to `q` extends walks backwards: if the piece at `x` leads to `p`, and the walk
27from `q` ends at the rim port `r`, then so does the walk from `x`. -/
28theorem Cross.reach {p q : GPort} (cross : G.Cross p q) :
29 ∀ x r, G.tau x = p → G.FullReach q r → G.FullReach x r := by
30 induction cross with
31 | one crosses =>
32 intro x r tau_x reach_q
33 obtain ⟨k, walk⟩ := reach_q
34 exact ⟨k + 1, .step (by rw [tau_x]; exact crosses) walk⟩
35 | more crosses _ ih =>
36 intro x r tau_x reach_q
37 obtain ⟨k, walk⟩ := ih _ r rfl reach_q
38 exact ⟨k + 1, .step (by rw [tau_x]; exact crosses) walk⟩
40/-- In a well-formed gluing, crossing an edge from a valid port lands on a valid port. -/
41theorem sigma_valid (G_wf : G.WF) {x y : GPort} (x_valid : G.Valid x) (crosses : G.sigma x = some y) : G.Valid y := by
42 obtain ⟨c, u, s⟩ := x
43 obtain ⟨c_lt, u_lt⟩ := x_valid
44 cases s with
45 | true =>
46 simp only [sigma, Option.map_eq_some_iff] at crosses
47 obtain ⟨⟨c', k'⟩, glued, rfl⟩ := crosses
48 -- port `R`: across edge `u` itself, to edge `k'` of `c'`
49 obtain ⟨c'_lt, k'_lt, _⟩ := G_wf.mate_valid c u c' k' c_lt u_lt glued
50 exact ⟨c'_lt, k'_lt⟩
51 | false =>
52 simp only [sigma, Option.map_eq_some_iff] at crosses
53 obtain ⟨⟨c', k'⟩, glued, rfl⟩ := crosses
54 -- port `L`: across the edge before vertex `u`, to the vertex after edge `k'` of `c'`
55 obtain ⟨c'_lt, k'_lt, _⟩ := G_wf.mate_valid c _ c' k' c_lt (prv_lt u_lt) glued
56 exact ⟨c'_lt, nxt_lt k'_lt⟩
58/-! ### Simulations -/
60/-- `φ` simulates `G` in `G'`. -/
61structure Sim (G G' : Gluing) (φ : GPort → GPort) : Prop where
62 valid : ∀ x, G.Valid x → G'.Valid (φ x)
63 tau : ∀ x, G.Valid x → G'.tau (φ x) = φ (G.tau x)
64 rim : ∀ x, G.Valid x → G.sigma x = none → G'.sigma (φ x) = none
65 cross : ∀ x y, G.Valid x → G.sigma x = some y → G'.Cross (φ x) (φ y)
67/-- Along a simulation, every walk of `G` from a valid port maps to a walk of `G'` between the images of its ends. -/
68theorem Sim.reach (G_wf : G.WF) {φ : GPort → GPort} (sim : Sim G G' φ) :
69 ∀ k x r, G.Valid x → G.FReach k x r → G'.FullReach (φ x) (φ r) := by
70 intro k x r x_valid walk
71 induction walk with
72 | @stop x on_rim =>
73 -- the piece at `x` commutes with `φ`
74 have tau_comm := sim.tau x x_valid
75 refine ⟨0, ?_⟩
76 -- the image of the piece's other end is a rim port of `G'`, so the walk of `G'` stops there too
77 have stops := FReach.stop (G := G') (x := φ x)
78 (by rw [tau_comm]; exact sim.rim _ (tau_valid G_wf x_valid) on_rim)
79 rwa [tau_comm] at stops
80 | @step k x y r crosses _ ih =>
81 -- the port crossed to is valid, so the rest of the walk maps too
82 have y_valid := sigma_valid G_wf (tau_valid G_wf x_valid) crosses
83 exact Cross.reach (sim.cross _ _ (tau_valid G_wf x_valid) crosses) (φ x) (φ r) (sim.tau x x_valid) (ih y_valid)
85/-! ### Equivalent gluings -/
87/-- Two gluings that agree on their actual children: the same number of children, rim lengths, corners, and gluing
88of actual edges. (They may differ outside, where nothing is ever looked up.) -/
89structure Equiv (G G' : Gluing) : Prop where
90 n : G.n = G'.n
91 E : ∀ c, c < G.n → G.E c = G'.E c
92 A : ∀ c, c < G.n → G.A c = G'.A c
93 B : ∀ c, c < G.n → G.B c = G'.B c
94 mate : ∀ c k, c < G.n → k < G.E c → G.mate c k = G'.mate c k
96namespace Equiv
98variable (equiv : Equiv G G')
100include equiv
102/-- A valid port of `G'` is a valid port of an equivalent gluing `G`. -/
103theorem valid' {x : GPort} (x_valid : G'.Valid x) : G.Valid x := by
104 -- the port's child is a child of `G`
105 have c_lt : x.1 < G.n := equiv.n ▸ x_valid.1
106 exact ⟨c_lt, (equiv.E _ c_lt).symm ▸ x_valid.2⟩
108/-- Equivalent gluings have the same pieces at valid ports. -/
109theorem tau {x : GPort} (x_valid : G.Valid x) : G'.tau x = G.tau x := by
110 obtain ⟨c, u, s⟩ := x
111 simp only [Gluing.tau, equiv.A c x_valid.1, equiv.B c x_valid.1]
113/-- Equivalent gluings cross edges in the same way at valid ports. -/
114theorem sigma (G_wf : G.WF) {x : GPort} (x_valid : G.Valid x) : G'.sigma x = G.sigma x := by
115 obtain ⟨c, u, s⟩ := x
116 obtain ⟨c_lt, u_lt⟩ := x_valid
117 cases s with
118 | true => simp only [Gluing.sigma, equiv.mate c u c_lt u_lt]
119 | false =>
120 simp only [Gluing.sigma, ← equiv.E c c_lt, ← equiv.mate c _ c_lt (prv_lt u_lt)]
121 cases glued : G.mate c (prv (G.E c) u) with
122 | none => rfl
123 | some p =>
124 obtain ⟨c', k'⟩ := p
125 -- the child glued to is a child of `G`, so its rim length is the same in `G'`
126 obtain ⟨c'_lt, _, _⟩ := G_wf.mate_valid c _ c' k' c_lt (prv_lt u_lt) glued
127 simp [equiv.E c' c'_lt]
129/-- A gluing equivalent to a well-formed one is well formed. -/
130theorem wf (G_wf : G.WF) : G'.WF where
131 E_pos c c_lt := by rw [← equiv.E c (equiv.n ▸ c_lt)]; exact G_wf.E_pos c (equiv.n ▸ c_lt)
132 A_lt c c_lt := by
133 rw [← equiv.E c (equiv.n ▸ c_lt), ← equiv.A c (equiv.n ▸ c_lt)]; exact G_wf.A_lt c (equiv.n ▸ c_lt)
134 B_lt c c_lt := by
135 rw [← equiv.E c (equiv.n ▸ c_lt), ← equiv.B c (equiv.n ▸ c_lt)]; exact G_wf.B_lt c (equiv.n ▸ c_lt)
136 A_ne_B c c_lt := by
137 rw [← equiv.A c (equiv.n ▸ c_lt), ← equiv.B c (equiv.n ▸ c_lt)]; exact G_wf.A_ne_B c (equiv.n ▸ c_lt)
138 mate_valid c k c' k' c_lt k_lt glued := by
139 -- the child is a child of `G`
140 have c_lt_G : c < G.n := equiv.n ▸ c_lt
141 -- the edge is an edge of the child in `G`
142 have k_lt_G : k < G.E c := (equiv.E c c_lt_G) ▸ k_lt
143 rw [← equiv.mate c k c_lt_G k_lt_G] at glued
144 obtain ⟨c'_lt, k'_lt, glued_back⟩ := G_wf.mate_valid c k c' k' c_lt_G k_lt_G glued
145 exact ⟨equiv.n ▸ c'_lt, (equiv.E c' c'_lt) ▸ k'_lt, by rw [← equiv.mate c' k' c'_lt k'_lt]; exact glued_back⟩
147/-- Every walk of `G` from a valid port is a walk of an equivalent gluing `G'`. -/
148theorem freach (G_wf : G.WF) : ∀ k x r, G.Valid x → G.FReach k x r → G'.FReach k x r := by
149 intro k x r x_valid walk
150 induction walk with
151 | @stop x on_rim =>
152 -- the walk of `G'` stops at the same rim port
153 have stops := FReach.stop (G := G') (x := x)
154 (by rw [equiv.tau x_valid, equiv.sigma G_wf (tau_valid G_wf x_valid)]; exact on_rim)
155 rwa [equiv.tau x_valid] at stops
156 | @step k x y r crosses _ ih =>
157 exact .step (by rw [equiv.tau x_valid, equiv.sigma G_wf (tau_valid G_wf x_valid)]; exact crosses)
158 (ih (sigma_valid G_wf (tau_valid G_wf x_valid) crosses))
160/-- A walk of `G` from a valid port reaches the same rim port in an equivalent gluing `G'`. -/
161theorem fullReach (G_wf : G.WF) {x r : GPort} (x_valid : G.Valid x) (reach : G.FullReach x r) : G'.FullReach x r := by
162 obtain ⟨k, walk⟩ := reach
163 exact ⟨k, equiv.freach G_wf k x r x_valid walk⟩
165end Equiv
167/-- Equivalence of gluings is symmetric. -/
168theorem Equiv.symm (equiv : Equiv G G') : Equiv G' G where
169 n := equiv.n.symm
170 E c c_lt := (equiv.E c (equiv.n ▸ c_lt)).symm
171 A c c_lt := (equiv.A c (equiv.n ▸ c_lt)).symm
172 B c c_lt := (equiv.B c (equiv.n ▸ c_lt)).symm
173 mate c k c_lt k_lt := (equiv.mate c k (equiv.n ▸ c_lt) ((equiv.E c (equiv.n ▸ c_lt)) ▸ k_lt)).symm
175/-! ### Subdivision of an edge -/
177/-- A cut: edge `e₀` of child `c₀` is cut into three edges. If `two`, it is glued to edge `e₁` of child `c₁`, which is
178cut too (the same physical edge); otherwise it lies on the parent's rim. -/
179structure Cut where
180 c₀ : Nat
181 e₀ : Nat
182 c₁ : Nat
183 e₁ : Nat
184 two : Bool
186namespace Cut
188variable (κ : Cut)
190/-- Where vertex `p` (or edge `p`) of child `c` goes: positions after the cut move on by 2. -/
191def sh (c p : Nat) : Nat :=
192 if c = κ.c₀ ∧ κ.e₀ < p then p + 2 else if κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ < p then p + 2 else p
194/-- Back from the subdivided numbering (for positions that are not new). -/
195def unsh (c k : Nat) : Nat :=
196 if c = κ.c₀ ∧ κ.e₀ + 2 < k then k - 2 else if κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ + 2 < k then k - 2 else k
198/-- A port of the old gluing, in the subdivided one. -/
199def port (x : GPort) : GPort := (x.1, κ.sh x.1 x.2.1, x.2.2)
201end Cut
203/-- `G` with the cut `κ` made: the cut edge becomes three edges, and positions after it move on by 2. -/
204def subdiv (G : Gluing) (κ : Cut) : Gluing where
205 n := G.n
206 E c := G.E c + (if c = κ.c₀ then 2 else 0) + (if κ.two = true ∧ c = κ.c₁ then 2 else 0)
207 A c := κ.sh c (G.A c)
208 B c := κ.sh c (G.B c)
209 mate c k :=
210 if c = κ.c₀ ∧ κ.e₀ ≤ k ∧ k ≤ κ.e₀ + 2 then
211 (if κ.two = true then some (κ.c₁, κ.e₁ + 2 - (k - κ.e₀)) else none)
212 else if κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ ≤ k ∧ k ≤ κ.e₁ + 2 then some (κ.c₀, κ.e₀ + 2 - (k - κ.e₁))
213 else (G.mate c (κ.unsh c k)).map fun (c₂, k₂) => (c₂, κ.sh c₂ k₂)
215/-- When a cut can be made: the cut edge is not the last edge of its child (so nothing wraps round), and it is glued
216to an edge of a different child, also not the last, or lies on the rim. -/
217structure Cut.OK (G : Gluing) (κ : Cut) : Prop where
218 wf : G.WF
219 c₀ : κ.c₀ < G.n
220 e₀ : κ.e₀ + 1 < G.E κ.c₀
221 mate : G.mate κ.c₀ κ.e₀ = if κ.two = true then some (κ.c₁, κ.e₁) else none
222 ne : κ.two = true → κ.c₁ ≠ κ.c₀
223 e₁ : κ.two = true → κ.e₁ + 1 < G.E κ.c₁
225/-- Crossing from port `R` at vertex `u`: across edge `u` itself, to port `R` at the vertex where the edge glued to it
226starts. -/
227theorem sigmaR (G : Gluing) (c u : Nat) :
228 G.sigma (c, u, true) = (G.mate c u).map fun (c', k') => (c', k', true) := rfl
230/-- Crossing from port `L` at vertex `u`: across the edge before `u`, to port `L` at the vertex after the edge glued to
231it. -/
232theorem sigmaL (G : Gluing) (c u : Nat) :
233 G.sigma (c, u, false) = (G.mate c (prv (G.E c) u)).map fun (c', k') => (c', nxt (G.E c') k', false) := rfl
235/-- The vertex before `q + 1` is `q`. -/
236theorem prv_succ' (E q : Nat) : prv E (q + 1) = q := by simp [prv]
238/-- The vertex after `q` is `q + 1` when that is not the end of the rim. -/
239theorem nxt_of_lt' {E q : Nat} (succ_lt : q + 1 < E) : nxt E q = q + 1 := by simp [nxt]; omega
241/-! ### A shared path of three edges -/
243/-- The ports along a path of three edges `ea, ea + 1, ea + 2` of child `a`, glued to edges `eb + 2, eb + 1, eb` of
244child `b`: `u_k` is vertex `ea + k` of `a`, which is vertex `eb + 3 - k` of `b`. -/
245def pathPort (a ea b eb : Nat) : Strip → GPort
246 | .c hand k => (a, ea + k, hand.isR)
247 | .d hand k => (b, eb + 3 - k, hand.isR)
In the paper Lemma 5.1 Zigzag Lemma, Lemma 7.1 Lengthening
249/-- **A shared path of three edges, by the zigzag lemma (Lemma 5.1 with `n = 3`).** Let edges `ea, ea + 1, ea + 2` of
250child `a` be glued, in reverse order, to edges `eb + 2, eb + 1, eb` of child `b`, with hooks at the inner vertices
251`ea + 1, ea + 2` of `a` and `eb + 1, eb + 2` of `b`. Then the crossings from `R_a(ea)` are forced along the path to
252`R_b(eb)`, and those from `L_b(eb + 3)` to `L_a(ea + 3)`: the two connections for odd `n`. -/
253theorem cross_three {G : Gluing} {a ea b eb : Nat} (a_room : ea + 3 < G.E a)
254 (glued_a : ∀ i, i ≤ 2 → G.mate a (ea + i) = some (b, eb + 2 - i))
255 (glued_b : ∀ i, i ≤ 2 → G.mate b (eb + i) = some (a, ea + 2 - i))
256 (hook_a : ∀ i, 1 ≤ i → i ≤ 2 → G.corner a (ea + i) = false)
257 (hook_b : ∀ i, 1 ≤ i → i ≤ 2 → G.corner b (eb + i) = false) :
258 G.Cross (a, ea, true) (b, eb, true) ∧ G.Cross (b, eb + 3, false) (a, ea + 3, false) := by
259 obtain ⟨from_R, from_L, _⟩ := Zigzag.zigzag G.sigma G.tau (pathPort a ea b eb) 3 (by omega)
260 (fun k k_lt => by
261 -- across edge `ea + k` of `a`, to `R_b` at vertex `eb + 2 - k`, where that edge of `b` starts
262 simp only [pathPort, Hand.isR, sigmaR, glued_a k (by omega), Option.map_some, Option.some.injEq,
263 Prod.mk.injEq, true_and, and_true]
264 omega)
265 (fun k k_lt => by
266 -- across the edge of `b` before its vertex `eb + 3 - k`, edge `eb + 2 - k`, to `L_a` after edge `ea + k`
267 simp only [pathPort, Hand.isR, sigmaL]
268 rw [show eb + 3 - k = (eb + (2 - k)) + 1 by omega, prv_succ', glued_b (2 - k) (by omega)]
269 simp only [Option.map_some, show ea + 2 - (2 - k) = ea + k by omega,
270 nxt_of_lt' (show ea + k + 1 < G.E a by omega), Nat.add_assoc])
271 (fun k k_pos k_lt => by
272 -- the hook of `a` at its inner vertex `ea + k`
273 simp only [pathPort, Hand.isR]
274 rw [tau_of_not_corner (hook_a k k_pos (by omega))]; rfl)
275 (fun k k_pos k_lt => by
276 -- the hook of `b` at its inner vertex `eb + 3 - k`
277 simp only [pathPort, Hand.isR]
278 rw [show eb + 3 - k = eb + (3 - k) by omega, tau_of_not_corner (hook_b (3 - k) (by omega) (by omega))]; rfl)
279 simp only [pathPort, Hand.isR, Nat.add_zero, show 3 % 2 = 1 by rfl, Nat.one_ne_zero, ite_false,
280 show eb + 3 - 3 = eb by omega, show eb + 3 - 0 = eb + 3 by omega] at from_R from_L
281 exact ⟨from_R, from_L⟩
283namespace Cut.OK
285set_option linter.unusedSectionVars false
287variable {G : Gluing} {κ : Cut} (cut_ok : κ.OK G)
289include cut_ok
291/-- If the cut edge is glued (`two`), its partner is an edge of `c₁`, glued back to it. -/
292theorem two_mate (cut_glued : κ.two = true) :
293 κ.c₁ < G.n ∧ κ.e₁ < G.E κ.c₁ ∧ G.mate κ.c₁ κ.e₁ = some (κ.c₀, κ.e₀) := by
294 -- the cut edge is glued to edge `e₁` of `c₁`
295 have glued := cut_ok.mate
296 rw [ite_eq_left cut_glued] at glued
297 -- the cut edge is not the last edge of `c₀`
298 have e₀_lt := cut_ok.e₀
299 exact cut_ok.wf.mate_valid _ _ _ _ cut_ok.c₀ (by omega) glued
301/-- On `c₀`, positions up to the cut edge stay put. -/
302theorem sh_c₀_le {p : Nat} (p_le : p ≤ κ.e₀) : κ.sh κ.c₀ p = p := by
303 unfold Cut.sh
304 -- `c₀` is not the partner child `c₁`
305 have not_c₁ : ¬ (κ.two = true ∧ κ.c₀ = κ.c₁ ∧ κ.e₁ < p) :=
306 fun ⟨cut_glued, same, _⟩ => cut_ok.ne cut_glued same.symm
307 rw [ite_eq_right (by omega), ite_eq_right not_c₁]
309/-- On `c₀`, positions after the cut edge move on by 2. -/
310theorem sh_c₀_gt {p : Nat} (p_gt : κ.e₀ < p) : κ.sh κ.c₀ p = p + 2 := by
311 unfold Cut.sh; rw [ite_eq_left ⟨rfl, p_gt⟩]
313/-- On `c₁` (when the cut edge is glued), positions up to the partner edge stay put. -/
314theorem sh_c₁_le (cut_glued : κ.two = true) {p : Nat} (p_le : p ≤ κ.e₁) : κ.sh κ.c₁ p = p := by
315 unfold Cut.sh
316 rw [ite_eq_right (fun ⟨same, _⟩ => cut_ok.ne cut_glued same), ite_eq_right (by omega)]
318/-- On `c₁` (when the cut edge is glued), positions after the partner edge move on by 2. -/
319theorem sh_c₁_gt (cut_glued : κ.two = true) {p : Nat} (p_gt : κ.e₁ < p) : κ.sh κ.c₁ p = p + 2 := by
320 unfold Cut.sh
321 rw [ite_eq_right (fun ⟨same, _⟩ => cut_ok.ne cut_glued same), ite_eq_left ⟨cut_glued, rfl, p_gt⟩]
323/-- On every other child, positions stay put. -/
324theorem sh_other {c p : Nat} (not_c₀ : c ≠ κ.c₀) (not_c₁ : ¬ (κ.two = true ∧ c = κ.c₁)) : κ.sh c p = p := by
325 unfold Cut.sh
326 rw [ite_eq_right (fun ⟨is_c₀, _⟩ => not_c₀ is_c₀),
327 ite_eq_right (fun ⟨cut_glued, is_c₁, _⟩ => not_c₁ ⟨cut_glued, is_c₁⟩)]
329/-- The cut child `c₀` has two more edges after the cut. -/
330theorem E_c₀ : (subdiv G κ).E κ.c₀ = G.E κ.c₀ + 2 := by
331 dsimp only [subdiv]
332 rw [ite_eq_left rfl, ite_eq_right (fun ⟨cut_glued, same⟩ => cut_ok.ne cut_glued same.symm)]
334/-- The partner child `c₁` (when the cut edge is glued) has two more edges after the cut. -/
335theorem E_c₁ (cut_glued : κ.two = true) : (subdiv G κ).E κ.c₁ = G.E κ.c₁ + 2 := by
336 dsimp only [subdiv]
337 rw [ite_eq_right (cut_ok.ne cut_glued), ite_eq_left ⟨cut_glued, rfl⟩]
339/-- Every other child keeps its rim length. -/
340theorem E_other {c : Nat} (not_c₀ : c ≠ κ.c₀) (not_c₁ : ¬ (κ.two = true ∧ c = κ.c₁)) :
341 (subdiv G κ).E c = G.E c := by
342 dsimp only [subdiv]
343 rw [ite_eq_right not_c₀, ite_eq_right not_c₁]; simp
345/-- Positions move only forwards, and never onto the new vertices. -/
346theorem sh_cases (c p : Nat) :
347 (κ.sh c p = p ∧ (c = κ.c₀ → p ≤ κ.e₀) ∧ (κ.two = true ∧ c = κ.c₁ → p ≤ κ.e₁)) ∨
348 (κ.sh c p = p + 2 ∧ ((c = κ.c₀ ∧ κ.e₀ < p) ∨ (κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ < p))) := by
349 by_cases is_c₀ : c = κ.c₀
350 · subst is_c₀
351 by_cases after : κ.e₀ < p
352 · exact Or.inr ⟨cut_ok.sh_c₀_gt after, Or.inl ⟨rfl, after⟩⟩
353 · exact Or.inl ⟨cut_ok.sh_c₀_le (by omega), fun _ => by omega,
354 fun ⟨cut_glued, same⟩ => absurd same.symm (cut_ok.ne cut_glued)⟩
355 · by_cases is_c₁ : κ.two = true ∧ c = κ.c₁
356 · obtain ⟨cut_glued, rfl⟩ := is_c₁
357 by_cases after : κ.e₁ < p
358 · exact Or.inr ⟨cut_ok.sh_c₁_gt cut_glued after, Or.inr ⟨cut_glued, rfl, after⟩⟩
359 · exact Or.inl ⟨cut_ok.sh_c₁_le cut_glued (by omega), fun same => absurd same is_c₀, fun _ => by omega⟩
360 · exact Or.inl ⟨cut_ok.sh_other is_c₀ is_c₁, fun same => absurd same is_c₀, fun same => absurd same is_c₁⟩
362/-- The shift is one to one on each child. -/
363theorem sh_inj {c p q : Nat} (same : κ.sh c p = κ.sh c q) : p = q := by
364 rcases cut_ok.sh_cases c p with ⟨p_stays, p_le₀, p_le₁⟩ | ⟨p_moves, p_after⟩ <;>
365 rcases cut_ok.sh_cases c q with ⟨q_stays, q_le₀, q_le₁⟩ | ⟨q_moves, q_after⟩
366 · omega
367 · rw [p_stays, q_moves] at same
368 rcases q_after with ⟨rfl, q_gt⟩ | ⟨cut_glued, rfl, q_gt⟩
369 · have := p_le₀ rfl -- `p` is at most the cut edge, `q` past it
370 omega
371 · have := p_le₁ ⟨cut_glued, rfl⟩ -- `p` is at most the partner edge, `q` past it
372 omega
373 · rw [p_moves, q_stays] at same
374 rcases p_after with ⟨rfl, p_gt⟩ | ⟨cut_glued, rfl, p_gt⟩
375 · have := q_le₀ rfl -- `q` is at most the cut edge, `p` past it
376 omega
377 · have := q_le₁ ⟨cut_glued, rfl⟩ -- `q` is at most the partner edge, `p` past it
378 omega
379 · omega
381/-- A position of child `c` is still a position of `c` after the cut. -/
382theorem sh_lt {c p : Nat} (p_lt : p < G.E c) : κ.sh c p < (subdiv G κ).E c := by
383 rcases cut_ok.sh_cases c p with ⟨stays, _, _⟩ | ⟨moves, after⟩
384 · rw [stays]; dsimp only [subdiv]; omega
385 · rw [moves]
386 rcases after with ⟨rfl, _⟩ | ⟨cut_glued, rfl, _⟩
387 · rw [cut_ok.E_c₀]; omega
388 · rw [cut_ok.E_c₁ cut_glued]; omega
390/-- The three edges that the cut edge of `c₀` becomes: glued, in reverse order, to the three that the partner edge
391becomes, or on the parent's rim like the cut edge. -/
392theorem mate_new₀ {i : Nat} (i_le : i ≤ 2) :
393 (subdiv G κ).mate κ.c₀ (κ.e₀ + i) = if κ.two = true then some (κ.c₁, κ.e₁ + 2 - i) else none := by
394 dsimp only [subdiv]
395 rw [ite_eq_left ⟨rfl, by omega, by omega⟩, show κ.e₀ + i - κ.e₀ = i by omega]
397/-- The three edges that the partner edge of `c₁` becomes: glued, in reverse order, to the three new edges of `c₀`. -/
398theorem mate_new₁ (cut_glued : κ.two = true) {i : Nat} (i_le : i ≤ 2) :
399 (subdiv G κ).mate κ.c₁ (κ.e₁ + i) = some (κ.c₀, κ.e₀ + 2 - i) := by
400 dsimp only [subdiv]
401 rw [ite_eq_right (fun ⟨same, _⟩ => cut_ok.ne cut_glued same), ite_eq_left ⟨cut_glued, rfl, by omega, by omega⟩,
402 show κ.e₁ + i - κ.e₁ = i by omega]
404/-- An edge that is not cut is glued as before (with positions moved on). -/
405theorem mate_old {c k : Nat} (not_cut₀ : ¬ (c = κ.c₀ ∧ k = κ.e₀))
406 (not_cut₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ k = κ.e₁)) :
407 (subdiv G κ).mate c (κ.sh c k) = (G.mate c k).map fun (c₂, k₂) => (c₂, κ.sh c₂ k₂) := by
408 dsimp only [subdiv]
409 -- undoing the shift gives back `k`
410 have unshift : κ.unsh c (κ.sh c k) = k := by
411 unfold Cut.unsh
412 rcases cut_ok.sh_cases c k with ⟨stays, le₀, le₁⟩ | ⟨moves, after⟩
413 · rw [stays]
414 by_cases is_c₀ : c = κ.c₀
415 · have k_le := le₀ is_c₀ -- `k` is at most the cut edge
416 rw [ite_eq_right (by omega), ite_eq_right (fun ⟨cut_glued, is_c₁, _⟩ => cut_ok.ne cut_glued (is_c₁ ▸ is_c₀))]
417 · rw [ite_eq_right (fun ⟨on_c₀, _⟩ => is_c₀ on_c₀)]
418 by_cases is_c₁ : κ.two = true ∧ c = κ.c₁
419 · have k_le := le₁ is_c₁ -- `k` is at most the partner edge
420 rw [ite_eq_right (by omega)]
421 · rw [ite_eq_right (fun ⟨cut_glued, on_c₁, _⟩ => is_c₁ ⟨cut_glued, on_c₁⟩)]
422 · rw [moves]
423 rcases after with ⟨rfl, k_gt⟩ | ⟨cut_glued, rfl, k_gt⟩
424 · rw [ite_eq_left ⟨rfl, by omega⟩]; omega
425 · rw [ite_eq_right (fun ⟨same, _⟩ => cut_ok.ne cut_glued same), ite_eq_left ⟨cut_glued, rfl, by omega⟩]; omega
426 -- the shifted position is not one of the three new edges of `c₀`
427 have not_new₀ : ¬ (c = κ.c₀ ∧ κ.e₀ ≤ κ.sh c k ∧ κ.sh c k ≤ κ.e₀ + 2) := by
428 rintro ⟨rfl, ge_cut, le_cut⟩
429 rcases cut_ok.sh_cases κ.c₀ k with ⟨stays, le₀, _⟩ | ⟨moves, after⟩
430 · have k_le := le₀ rfl -- `k` is at most the cut edge, so it would be the cut edge
431 rw [stays] at ge_cut le_cut; exact not_cut₀ ⟨rfl, by omega⟩
432 · rw [moves] at ge_cut le_cut
433 rcases after with ⟨_, k_gt⟩ | ⟨cut_glued, same, _⟩
434 · omega
435 · exact cut_ok.ne cut_glued same.symm
436 -- the shifted position is not one of the three new edges of `c₁`
437 have not_new₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ ≤ κ.sh c k ∧ κ.sh c k ≤ κ.e₁ + 2) := by
438 rintro ⟨cut_glued, rfl, ge_cut, le_cut⟩
439 rcases cut_ok.sh_cases κ.c₁ k with ⟨stays, _, le₁⟩ | ⟨moves, after⟩
440 · have k_le := le₁ ⟨cut_glued, rfl⟩ -- `k` is at most the partner edge, so it would be the partner edge
441 rw [stays] at ge_cut le_cut; exact not_cut₁ ⟨cut_glued, rfl, by omega⟩
442 · rw [moves] at ge_cut le_cut
443 rcases after with ⟨same, _⟩ | ⟨_, _, k_gt⟩
444 · exact cut_ok.ne cut_glued same
445 · omega
446 rw [ite_eq_right not_new₀, ite_eq_right not_new₁, unshift]
448/-- Going back one vertex commutes with the shift, except at the old vertex just after a cut edge. -/
449theorem prv_sh {c p : Nat} (p_lt : p < G.E c) (not_after₀ : ¬ (c = κ.c₀ ∧ p = κ.e₀ + 1))
450 (not_after₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ p = κ.e₁ + 1)) :
451 prv ((subdiv G κ).E c) (κ.sh c p) = κ.sh c (prv (G.E c) p) := by
452 -- the cut edge is not the last edge of `c₀`
453 have e₀_lt := cut_ok.e₀
454 -- going back from vertex 0 wraps round to the last vertex
455 have prv_zero : ∀ E, prv E 0 = E - 1 := fun E => by simp [prv]
456 -- going back from any other vertex subtracts one
457 have prv_pos : ∀ E q, 0 < q → prv E q = q - 1 := fun E q q_pos => by simp [prv]; omega
458 by_cases is_c₀ : c = κ.c₀
459 · subst is_c₀
460 rw [cut_ok.E_c₀]
461 by_cases at_zero : p = 0
462 · subst at_zero; rw [cut_ok.sh_c₀_le (by omega), prv_zero, prv_zero, cut_ok.sh_c₀_gt (by omega)]; omega
463 · rw [prv_pos _ p (by omega)]
464 by_cases before : p ≤ κ.e₀
465 · rw [cut_ok.sh_c₀_le before, cut_ok.sh_c₀_le (by omega), prv_pos _ p (by omega)]
466 -- `p` is past the vertex just after the cut edge
467 · have p_gt : κ.e₀ + 1 < p := by
468 -- by assumption, `p` is not the vertex just after the cut edge
469 have not_next : ¬ p = κ.e₀ + 1 := fun same => not_after₀ ⟨rfl, same⟩
470 omega
471 rw [cut_ok.sh_c₀_gt (p := p) (by omega), cut_ok.sh_c₀_gt (p := p - 1) (by omega),
472 prv_pos _ (p + 2) (by omega)]
473 omega
474 · by_cases is_c₁ : κ.two = true ∧ c = κ.c₁
475 · obtain ⟨cut_glued, rfl⟩ := is_c₁
476 -- the partner edge is not the last edge of `c₁`
477 have e₁_lt := cut_ok.e₁ cut_glued
478 rw [cut_ok.E_c₁ cut_glued]
479 by_cases at_zero : p = 0
480 · subst at_zero
481 rw [cut_ok.sh_c₁_le cut_glued (by omega), prv_zero, prv_zero, cut_ok.sh_c₁_gt cut_glued (by omega)]; omega
482 · rw [prv_pos _ p (by omega)]
483 by_cases before : p ≤ κ.e₁
484 · rw [cut_ok.sh_c₁_le cut_glued before, cut_ok.sh_c₁_le cut_glued (by omega), prv_pos _ p (by omega)]
485 -- `p` is past the vertex just after the partner edge
486 · have p_gt : κ.e₁ + 1 < p := by
487 -- by assumption, `p` is not the vertex just after the partner edge
488 have not_next : ¬ p = κ.e₁ + 1 := fun same => not_after₁ ⟨cut_glued, rfl, same⟩
489 omega
490 rw [cut_ok.sh_c₁_gt cut_glued (p := p) (by omega), cut_ok.sh_c₁_gt cut_glued (p := p - 1) (by omega),
491 prv_pos _ (p + 2) (by omega)]
492 omega
493 · rw [cut_ok.E_other is_c₀ is_c₁, cut_ok.sh_other is_c₀ is_c₁, cut_ok.sh_other is_c₀ is_c₁]
495/-- Going forward one vertex from the start of an edge that is not cut commutes with the shift. -/
496theorem nxt_sh {c k : Nat} (k_lt : k < G.E c) (not_cut₀ : ¬ (c = κ.c₀ ∧ k = κ.e₀))
497 (not_cut₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ k = κ.e₁)) :
498 nxt ((subdiv G κ).E c) (κ.sh c k) = κ.sh c (nxt (G.E c) k) := by
499 -- the cut edge is not the last edge of `c₀`
500 have e₀_lt := cut_ok.e₀
501 by_cases is_c₀ : c = κ.c₀
502 · subst is_c₀
503 rw [cut_ok.E_c₀]
504 unfold nxt
505 by_cases before : k < κ.e₀
506 · rw [cut_ok.sh_c₀_le (p := k) (by omega), ite_eq_right (show ¬ (k + 1 = G.E κ.c₀ + 2) by omega),
507 ite_eq_right (show ¬ (k + 1 = G.E κ.c₀) by omega), cut_ok.sh_c₀_le (p := k + 1) (by omega)]
508 -- `k` is past the cut edge
509 · have k_gt : κ.e₀ < k := by
510 -- by assumption, `k` is not the cut edge
511 have not_cut : ¬ k = κ.e₀ := fun same => not_cut₀ ⟨rfl, same⟩
512 omega
513 rw [cut_ok.sh_c₀_gt k_gt]
514 by_cases at_end : k + 1 = G.E κ.c₀
515 · rw [ite_eq_left (show k + 2 + 1 = G.E κ.c₀ + 2 by omega), ite_eq_left at_end,
516 cut_ok.sh_c₀_le (p := 0) (by omega)]
517 · rw [ite_eq_right (show ¬ (k + 2 + 1 = G.E κ.c₀ + 2) by omega), ite_eq_right at_end,
518 cut_ok.sh_c₀_gt (p := k + 1) (by omega)]
519 · by_cases is_c₁ : κ.two = true ∧ c = κ.c₁
520 · obtain ⟨cut_glued, rfl⟩ := is_c₁
521 -- the partner edge is not the last edge of `c₁`
522 have e₁_lt := cut_ok.e₁ cut_glued
523 rw [cut_ok.E_c₁ cut_glued]
524 unfold nxt
525 by_cases before : k < κ.e₁
526 · rw [cut_ok.sh_c₁_le cut_glued (p := k) (by omega), ite_eq_right (show ¬ (k + 1 = G.E κ.c₁ + 2) by omega),
527 ite_eq_right (show ¬ (k + 1 = G.E κ.c₁) by omega), cut_ok.sh_c₁_le cut_glued (p := k + 1) (by omega)]
528 -- `k` is past the partner edge
529 · have k_gt : κ.e₁ < k := by
530 -- by assumption, `k` is not the partner edge
531 have not_cut : ¬ k = κ.e₁ := fun same => not_cut₁ ⟨cut_glued, rfl, same⟩
532 omega
533 rw [cut_ok.sh_c₁_gt cut_glued k_gt]
534 by_cases at_end : k + 1 = G.E κ.c₁
535 · rw [ite_eq_left (show k + 2 + 1 = G.E κ.c₁ + 2 by omega), ite_eq_left at_end,
536 cut_ok.sh_c₁_le cut_glued (p := 0) (by omega)]
537 · rw [ite_eq_right (show ¬ (k + 2 + 1 = G.E κ.c₁ + 2) by omega), ite_eq_right at_end,
538 cut_ok.sh_c₁_gt cut_glued (p := k + 1) (by omega)]
539 · rw [cut_ok.E_other is_c₀ is_c₁, cut_ok.sh_other is_c₀ is_c₁, cut_ok.sh_other is_c₀ is_c₁]
541/-- The other end of an edge that is not cut is not a cut edge either. -/
542theorem target_not_cut {c k c₂ k₂ : Nat} (c_lt : c < G.n) (k_lt : k < G.E c) (glued : G.mate c k = some (c₂, k₂))
543 (not_cut₀ : ¬ (c = κ.c₀ ∧ k = κ.e₀)) (not_cut₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ k = κ.e₁)) :
544 ¬ (c₂ = κ.c₀ ∧ k₂ = κ.e₀) ∧ ¬ (κ.two = true ∧ c₂ = κ.c₁ ∧ k₂ = κ.e₁) := by
545 obtain ⟨_, _, glued_back⟩ := cut_ok.wf.mate_valid c k c₂ k₂ c_lt k_lt glued
546 constructor
547 · rintro ⟨rfl, rfl⟩
548 -- the cut edge is glued back to edge `k` of `c`, so that is the partner edge
549 have cut_mate := cut_ok.mate
550 rw [glued_back] at cut_mate
551 by_cases cut_glued : κ.two = true
552 · rw [ite_eq_left cut_glued] at cut_mate
553 simp only [Option.some.injEq, Prod.mk.injEq] at cut_mate
554 exact not_cut₁ ⟨cut_glued, cut_mate.1, cut_mate.2⟩
555 · rw [ite_eq_right cut_glued] at cut_mate; contradiction
556 · rintro ⟨cut_glued, rfl, rfl⟩
557 rw [(cut_ok.two_mate cut_glued).2.2] at glued_back
558 simp only [Option.some.injEq, Prod.mk.injEq] at glued_back
559 exact not_cut₀ ⟨glued_back.1.symm, glued_back.2.symm⟩
561/-- `τ` commutes with the shift (corners go to corners, and the shift is one to one). -/
562theorem tau_port (x : GPort) : (subdiv G κ).tau (κ.port x) = κ.port (G.tau x) := by
563 obtain ⟨c, p, s⟩ := x
564 -- the piece of the subdivided gluing, at the shifted corners
565 have lhs : (subdiv G κ).tau (κ.port (c, p, s)) =
566 if κ.sh c p = κ.sh c (G.A c) then (c, κ.sh c (G.B c), s)
567 else if κ.sh c p = κ.sh c (G.B c) then (c, κ.sh c (G.A c), s) else (c, κ.sh c p, !s) := rfl
568 rw [lhs]
569 by_cases at_A : p = G.A c
570 -- at corner `A` the piece goes to corner `B`
571 · have tau_A : G.tau (c, p, s) = (c, G.B c, s) := by simp [Gluing.tau, at_A]
572 rw [tau_A, ite_eq_left (by rw [at_A])]; rfl
573 · rw [ite_eq_right (fun same => at_A (cut_ok.sh_inj same))]
574 by_cases at_B : p = G.B c
575 -- at corner `B` the piece goes to corner `A`
576 · have tau_B : G.tau (c, p, s) = (c, G.A c, s) := by simp [Gluing.tau, at_A, at_B]
577 rw [tau_B, ite_eq_left (by rw [at_B])]; rfl
578 -- elsewhere the piece goes to the other port at the same vertex
579 · have tau_other : G.tau (c, p, s) = (c, p, !s) := by simp [Gluing.tau, at_A, at_B]
580 rw [tau_other, ite_eq_right (fun same => at_B (cut_ok.sh_inj same))]; rfl
582/-- The new vertices of `c₀` are not corners. -/
583theorem corner_new₀ {i : Nat} (i_ge : 1 ≤ i) (i_le : i ≤ 2) : (subdiv G κ).corner κ.c₀ (κ.e₀ + i) = false := by
584 simp only [Gluing.corner, Bool.or_eq_false_iff, beq_eq_false_iff_ne, ne_eq]
585 dsimp only [subdiv]
586 constructor <;> intro at_corner <;>
587 · rcases cut_ok.sh_cases κ.c₀ _ with ⟨stays, le₀, _⟩ | ⟨moves, after⟩
588 · rw [stays] at at_corner
589 -- the corner is at most the cut edge, so it is not a new vertex
590 have := le₀ rfl
591 omega
592 · rw [moves] at at_corner
593 rcases after with ⟨_, _⟩ | ⟨cut_glued, same, _⟩
594 · omega
595 · exact cut_ok.ne cut_glued same.symm
597/-- The new vertices of `c₁` (when the cut edge is glued) are not corners. -/
598theorem corner_new₁ (cut_glued : κ.two = true) {i : Nat} (i_ge : 1 ≤ i) (i_le : i ≤ 2) :
599 (subdiv G κ).corner κ.c₁ (κ.e₁ + i) = false := by
600 simp only [Gluing.corner, Bool.or_eq_false_iff, beq_eq_false_iff_ne, ne_eq]
601 dsimp only [subdiv]
602 constructor <;> intro at_corner <;>
603 · rcases cut_ok.sh_cases κ.c₁ _ with ⟨stays, _, le₁⟩ | ⟨moves, after⟩
604 · rw [stays] at at_corner
605 -- the corner is at most the partner edge, so it is not a new vertex
606 have := le₁ ⟨cut_glued, rfl⟩
607 omega
608 · rw [moves] at at_corner
609 rcases after with ⟨same, _⟩ | ⟨_, _, _⟩
610 · exact cut_ok.ne cut_glued same
611 · omega
613/-- Every position of the subdivided child that is not new comes from an old one. -/
614theorem preimage {c k : Nat} (k_lt : k < (subdiv G κ).E c) (not_new₀ : ¬ (c = κ.c₀ ∧ κ.e₀ < k ∧ k ≤ κ.e₀ + 2))
615 (not_new₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ < k ∧ k ≤ κ.e₁ + 2)) : ∃ u, u < G.E c ∧ κ.sh c u = k := by
616 by_cases is_c₀ : c = κ.c₀
617 · subst is_c₀
618 rw [cut_ok.E_c₀] at k_lt
619 -- the cut edge is not the last edge of `c₀`
620 have e₀_lt := cut_ok.e₀
621 -- `k` is not one of the two new vertices of `c₀`
622 have not_new : ¬ (κ.e₀ < k ∧ k ≤ κ.e₀ + 2) := fun ⟨k_gt, k_le⟩ => not_new₀ ⟨rfl, k_gt, k_le⟩
623 by_cases before : k ≤ κ.e₀
624 · exact ⟨k, by omega, cut_ok.sh_c₀_le before⟩
625 · refine ⟨k - 2, by omega, ?_⟩
626 rw [cut_ok.sh_c₀_gt (by omega)]; omega
627 · by_cases is_c₁ : κ.two = true ∧ c = κ.c₁
628 · obtain ⟨cut_glued, rfl⟩ := is_c₁
629 rw [cut_ok.E_c₁ cut_glued] at k_lt
630 -- the partner edge is not the last edge of `c₁`
631 have e₁_lt := cut_ok.e₁ cut_glued
632 -- `k` is not one of the two new vertices of `c₁`
633 have not_new : ¬ (κ.e₁ < k ∧ k ≤ κ.e₁ + 2) := fun ⟨k_gt, k_le⟩ => not_new₁ ⟨cut_glued, rfl, k_gt, k_le⟩
634 by_cases before : k ≤ κ.e₁
635 · exact ⟨k, by omega, cut_ok.sh_c₁_le cut_glued before⟩
636 · refine ⟨k - 2, by omega, ?_⟩
637 rw [cut_ok.sh_c₁_gt cut_glued (by omega)]; omega
638 · rw [cut_ok.E_other is_c₀ is_c₁] at k_lt
639 exact ⟨k, k_lt, cut_ok.sh_other is_c₀ is_c₁⟩
641/-- If the cut edge lies on the parent's rim, only it is cut. -/
642theorem two_false (on_rim : G.mate κ.c₀ κ.e₀ = none) : κ.two = false := by
643 -- what `OK` says about the gluing of the cut edge
644 have cut_mate := cut_ok.mate
645 rw [on_rim] at cut_mate
646 cases cut_glued : κ.two
647 · rfl
648 · rw [cut_glued] at cut_mate; simp at cut_mate
650/-- If the cut edge is glued, its partner is cut too, and it is the edge it is glued to. -/
651theorem two_true {q : Nat × Nat} (glued : G.mate κ.c₀ κ.e₀ = some q) : κ.two = true ∧ q = (κ.c₁, κ.e₁) := by
652 -- what `OK` says about the gluing of the cut edge
653 have cut_mate := cut_ok.mate
654 rw [glued] at cut_mate
655 cases cut_glued : κ.two
656 · rw [cut_glued] at cut_mate; simp at cut_mate
657 · rw [cut_glued] at cut_mate; simp only [ite_true, Option.some.injEq] at cut_mate; exact ⟨rfl, cut_mate⟩
659/-- The first new edge of `c₀` (where the cut edge began) is glued to the last new edge of `c₁`, or lies on the rim. -/
660theorem mate_cut₀ : (subdiv G κ).mate κ.c₀ κ.e₀ = if κ.two = true then some (κ.c₁, κ.e₁ + 2) else none := by
661 -- `mate_new₀` at the first new edge
662 have first := cut_ok.mate_new₀ (i := 0) (by omega)
663 simpa using first
665/-- The first new edge of `c₁` (where the partner edge began) is glued to the last new edge of `c₀`. -/
666theorem mate_cut₁ (cut_glued : κ.two = true) : (subdiv G κ).mate κ.c₁ κ.e₁ = some (κ.c₀, κ.e₀ + 2) := by
667 -- `mate_new₁` at the first new edge
668 have first := cut_ok.mate_new₁ cut_glued (i := 0) (by omega)
669 simpa using first
671/-- At a new vertex of `c₀` the piece joins the two ports at that vertex. -/
672theorem tau_new₀ {i : Nat} (i_ge : 1 ≤ i) (i_le : i ≤ 2) (s : Bool) :
673 (subdiv G κ).tau (κ.c₀, κ.e₀ + i, s) = (κ.c₀, κ.e₀ + i, !s) := tau_of_not_corner (cut_ok.corner_new₀ i_ge i_le)
675/-- At a new vertex of `c₁` the piece joins the two ports at that vertex. -/
676theorem tau_new₁ (cut_glued : κ.two = true) {i : Nat} (i_ge : 1 ≤ i) (i_le : i ≤ 2) (s : Bool) :
677 (subdiv G κ).tau (κ.c₁, κ.e₁ + i, s) = (κ.c₁, κ.e₁ + i, !s) :=
678 tau_of_not_corner (cut_ok.corner_new₁ cut_glued i_ge i_le)
680/-- The vertex before an old vertex is the start of the cut edge only right after the cut edge. -/
681theorem prv_cut {c p : Nat} (p_lt : p < G.E c) (prev_cut : c = κ.c₀ ∧ prv (G.E c) p = κ.e₀) : p = κ.e₀ + 1 := by
682 obtain ⟨rfl, prev_eq⟩ := prev_cut
683 -- the cut edge is not the last edge of `c₀`
684 have := cut_ok.e₀
685 unfold prv at prev_eq; split at prev_eq <;> omega
687/-- The vertex before an old vertex is the start of the partner edge only right after the partner edge. -/
688theorem prv_cut₁ (cut_glued : κ.two = true) {c p : Nat} (p_lt : p < G.E c)
689 (prev_cut : c = κ.c₁ ∧ prv (G.E c) p = κ.e₁) : p = κ.e₁ + 1 := by
690 obtain ⟨rfl, prev_eq⟩ := prev_cut
691 -- the partner edge is not the last edge of `c₁`
692 have := cut_ok.e₁ cut_glued
693 unfold prv at prev_eq; split at prev_eq <;> omega
695/-- The new path of a glued cut edge, read from `c₀` (Lemma 7.1 with the zigzag lemma for `n = 3`): from `R_{c₀}(e₀)` to
696`R_{c₁}(e₁)`, and from `L_{c₁}(e₁ + 3)` to `L_{c₀}(e₀ + 3)`. -/
697theorem cross_cut₀ (cut_glued : κ.two = true) :
698 (subdiv G κ).Cross (κ.c₀, κ.e₀, true) (κ.c₁, κ.e₁, true) ∧
699 (subdiv G κ).Cross (κ.c₁, κ.e₁ + 3, false) (κ.c₀, κ.e₀ + 3, false) := by
700 -- the cut edge is not the last edge of `c₀`
701 have e₀_lt := cut_ok.e₀
702 exact cross_three (by rw [cut_ok.E_c₀]; omega)
703 (fun i i_le => by rw [cut_ok.mate_new₀ i_le, ite_eq_left cut_glued])
704 (fun i i_le => cut_ok.mate_new₁ cut_glued i_le)
705 (fun i i_ge i_le => cut_ok.corner_new₀ i_ge i_le)
706 (fun i i_ge i_le => cut_ok.corner_new₁ cut_glued i_ge i_le)
708/-- The new path of a glued cut edge, read from `c₁`: from `R_{c₁}(e₁)` to `R_{c₀}(e₀)`, and from `L_{c₀}(e₀ + 3)` to
709`L_{c₁}(e₁ + 3)`. -/
710theorem cross_cut₁ (cut_glued : κ.two = true) :
711 (subdiv G κ).Cross (κ.c₁, κ.e₁, true) (κ.c₀, κ.e₀, true) ∧
712 (subdiv G κ).Cross (κ.c₀, κ.e₀ + 3, false) (κ.c₁, κ.e₁ + 3, false) := by
713 -- the partner edge is not the last edge of `c₁`
714 have e₁_lt := cut_ok.e₁ cut_glued
715 exact cross_three (by rw [cut_ok.E_c₁ cut_glued]; omega)
716 (fun i i_le => cut_ok.mate_new₁ cut_glued i_le)
717 (fun i i_le => by rw [cut_ok.mate_new₀ i_le, ite_eq_left cut_glued])
718 (fun i i_ge i_le => cut_ok.corner_new₁ cut_glued i_ge i_le)
719 (fun i i_ge i_le => cut_ok.corner_new₀ i_ge i_le)
In the paper Lemma 7.1 Lengthening
721/-- **Subdividing an edge is a simulation.** -/
722theorem sim : Sim G (subdiv G κ) κ.port where
723 valid x x_valid := ⟨x_valid.1, cut_ok.sh_lt x_valid.2⟩
724 tau x _ := cut_ok.tau_port x
725 rim := by
726 rintro ⟨c, p, s⟩ ⟨c_lt, p_lt⟩ on_rim
727 -- the cut edge is not the last edge of `c₀`
728 have e₀_lt := cut_ok.e₀
729 cases s with
730 | true =>
731 simp only [Cut.port]
732 rw [sigmaR] at on_rim ⊢
733 rw [Option.map_eq_none_iff] at on_rim ⊢
734 by_cases is_cut₀ : c = κ.c₀ ∧ p = κ.e₀
735 · obtain ⟨rfl, rfl⟩ := is_cut₀
736 -- the cut edge is on the rim, so only it is cut
737 have cut_on_rim := cut_ok.two_false on_rim
738 rw [cut_ok.sh_c₀_le (Nat.le_refl _), cut_ok.mate_cut₀, cut_on_rim]; rfl
739 · by_cases is_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ p = κ.e₁
740 · obtain ⟨cut_glued, rfl, rfl⟩ := is_cut₁
741 rw [(cut_ok.two_mate cut_glued).2.2] at on_rim; contradiction
742 · rw [cut_ok.mate_old is_cut₀ is_cut₁, on_rim]; rfl
743 | false =>
744 simp only [Cut.port]
745 rw [sigmaL] at on_rim ⊢
746 rw [Option.map_eq_none_iff] at on_rim ⊢
747 by_cases after_cut₀ : c = κ.c₀ ∧ p = κ.e₀ + 1
748 · obtain ⟨rfl, rfl⟩ := after_cut₀
749 rw [prv_succ'] at on_rim
750 -- the cut edge is on the rim, so only it is cut
751 have cut_on_rim := cut_ok.two_false on_rim
752 rw [cut_ok.sh_c₀_gt (by omega), cut_ok.E_c₀, show κ.e₀ + 1 + 2 = (κ.e₀ + 2) + 1 by omega, prv_succ',
753 cut_ok.mate_new₀ (by omega), cut_on_rim]; rfl
754 · by_cases after_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ p = κ.e₁ + 1
755 · obtain ⟨cut_glued, rfl, rfl⟩ := after_cut₁
756 rw [prv_succ', (cut_ok.two_mate cut_glued).2.2] at on_rim; contradiction
757 · rw [cut_ok.prv_sh p_lt after_cut₀ after_cut₁]
758 -- the edge before `p` is not the cut edge
759 have not_cut₀ : ¬ (c = κ.c₀ ∧ prv (G.E c) p = κ.e₀) :=
760 fun prev_cut => after_cut₀ ⟨prev_cut.1, cut_ok.prv_cut p_lt prev_cut⟩
761 -- nor the partner edge
762 have not_cut₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ prv (G.E c) p = κ.e₁) := fun ⟨cut_glued, is_c₁, prev_eq⟩ =>
763 after_cut₁ ⟨cut_glued, is_c₁, cut_ok.prv_cut₁ cut_glued p_lt ⟨is_c₁, prev_eq⟩⟩
764 rw [cut_ok.mate_old not_cut₀ not_cut₁, on_rim]; rfl
765 cross := by
766 rintro ⟨c, p, s⟩ y ⟨c_lt, p_lt⟩ crosses
767 -- the cut edge is not the last edge of `c₀`
768 have e₀_lt := cut_ok.e₀
769 cases s with
770 | true =>
771 simp only [Cut.port]
772 rw [sigmaR] at crosses
773 rw [Option.map_eq_some_iff] at crosses
774 obtain ⟨⟨c', k'⟩, glued, rfl⟩ := crosses
775 by_cases is_cut₀ : c = κ.c₀ ∧ p = κ.e₀
776 · obtain ⟨rfl, rfl⟩ := is_cut₀
777 -- the cut edge: across the new path, from R(e₀) of c₀ to R(e₁) of c₁, by the zigzag lemma
778 obtain ⟨cut_glued, partner⟩ := cut_ok.two_true glued
779 simp only [Prod.mk.injEq] at partner
780 obtain ⟨rfl, rfl⟩ := partner
781 rw [cut_ok.sh_c₀_le (Nat.le_refl _), cut_ok.sh_c₁_le cut_glued (Nat.le_refl _)]
782 exact (cut_ok.cross_cut₀ cut_glued).1
783 · by_cases is_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ p = κ.e₁
784 · obtain ⟨cut_glued, rfl, rfl⟩ := is_cut₁
785 -- the partner of the cut edge: across the new path, from R(e₁) of c₁ to R(e₀) of c₀
786 rw [(cut_ok.two_mate cut_glued).2.2] at glued
787 simp only [Option.some.injEq, Prod.mk.injEq] at glued
788 obtain ⟨rfl, rfl⟩ := glued
789 rw [cut_ok.sh_c₁_le cut_glued (Nat.le_refl _), cut_ok.sh_c₀_le (Nat.le_refl _)]
790 exact (cut_ok.cross_cut₁ cut_glued).1
791 · refine .one ?_
792 rw [sigmaR, cut_ok.mate_old is_cut₀ is_cut₁, glued]; rfl
793 | false =>
794 simp only [Cut.port]
795 rw [sigmaL] at crosses
796 rw [Option.map_eq_some_iff] at crosses
797 obtain ⟨⟨c', k'⟩, glued, rfl⟩ := crosses
798 by_cases after_cut₀ : c = κ.c₀ ∧ p = κ.e₀ + 1
799 · obtain ⟨rfl, rfl⟩ := after_cut₀
800 rw [prv_succ'] at glued
801 obtain ⟨cut_glued, partner⟩ := cut_ok.two_true glued
802 simp only [Prod.mk.injEq] at partner
803 obtain ⟨rfl, rfl⟩ := partner
804 -- the partner edge is not the last edge of `c₁`
805 have e₁_lt := cut_ok.e₁ cut_glued
806 -- across the new path, from L(e₀+3) of c₀ to L(e₁+3) of c₁, by the zigzag lemma
807 rw [cut_ok.sh_c₀_gt (by omega)]
808 simp only
809 rw [nxt_of_lt' e₁_lt, cut_ok.sh_c₁_gt cut_glued (by omega)]
810 exact (cut_ok.cross_cut₁ cut_glued).2
811 · by_cases after_cut₁ : κ.two = true ∧ c = κ.c₁ ∧ p = κ.e₁ + 1
812 · obtain ⟨cut_glued, rfl, rfl⟩ := after_cut₁
813 rw [prv_succ', (cut_ok.two_mate cut_glued).2.2] at glued
814 simp only [Option.some.injEq, Prod.mk.injEq] at glued
815 obtain ⟨rfl, rfl⟩ := glued
816 -- across the new path, from L(e₁+3) of c₁ to L(e₀+3) of c₀, by the zigzag lemma
817 rw [cut_ok.sh_c₁_gt cut_glued (by omega)]
818 simp only
819 rw [nxt_of_lt' e₀_lt, cut_ok.sh_c₀_gt (by omega)]
820 exact (cut_ok.cross_cut₀ cut_glued).2
821 · refine .one ?_
822 -- the edge before `p` is not the cut edge
823 have not_cut₀ : ¬ (c = κ.c₀ ∧ prv (G.E c) p = κ.e₀) :=
824 fun prev_cut => after_cut₀ ⟨prev_cut.1, cut_ok.prv_cut p_lt prev_cut⟩
825 -- nor the partner edge
826 have not_cut₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ prv (G.E c) p = κ.e₁) := fun ⟨cut_glued, is_c₁, prev_eq⟩ =>
827 after_cut₁ ⟨cut_glued, is_c₁, cut_ok.prv_cut₁ cut_glued p_lt ⟨is_c₁, prev_eq⟩⟩
828 -- the edge before `p` is an edge of `c`
829 have prev_lt : prv (G.E c) p < G.E c := prv_lt p_lt
830 obtain ⟨c'_lt, k'_lt, _⟩ := cut_ok.wf.mate_valid c _ c' k' c_lt prev_lt glued
831 obtain ⟨mate_not_cut₀, mate_not_cut₁⟩ := cut_ok.target_not_cut c_lt prev_lt glued not_cut₀ not_cut₁
832 rw [sigmaL, cut_ok.prv_sh p_lt after_cut₀ after_cut₁, cut_ok.mate_old not_cut₀ not_cut₁, glued]
833 simp only [Option.map_some]
834 rw [cut_ok.nxt_sh k'_lt mate_not_cut₀ mate_not_cut₁]
836/-- The subdivided gluing is well formed. -/
837theorem wf_subdiv : (subdiv G κ).WF where
838 E_pos c c_lt := by
839 -- every child had an edge before the cut
840 have := cut_ok.wf.E_pos c c_lt
841 dsimp only [subdiv]; omega
842 A_lt c c_lt := cut_ok.sh_lt (cut_ok.wf.A_lt c c_lt)
843 B_lt c c_lt := cut_ok.sh_lt (cut_ok.wf.B_lt c c_lt)
844 A_ne_B c c_lt same := cut_ok.wf.A_ne_B c c_lt (cut_ok.sh_inj same)
845 mate_valid := by
846 intro c k c' k' c_lt k_lt glued
847 -- the cut edge is not the last edge of `c₀`
848 have e₀_lt := cut_ok.e₀
849 by_cases new₀ : c = κ.c₀ ∧ κ.e₀ ≤ k ∧ k ≤ κ.e₀ + 2
850 · obtain ⟨rfl, k_ge, k_le⟩ := new₀
851 rw [show k = κ.e₀ + (k - κ.e₀) by omega, cut_ok.mate_new₀ (by omega)] at glued
852 by_cases cut_glued : κ.two = true
853 · rw [ite_eq_left cut_glued] at glued
854 simp only [Option.some.injEq, Prod.mk.injEq] at glued
855 obtain ⟨rfl, rfl⟩ := glued
856 -- the partner edge is not the last edge of `c₁`
857 have e₁_lt := cut_ok.e₁ cut_glued
858 refine ⟨(cut_ok.two_mate cut_glued).1, by rw [cut_ok.E_c₁ cut_glued]; omega, ?_⟩
859 rw [show κ.e₁ + 2 - (k - κ.e₀) = κ.e₁ + (2 - (k - κ.e₀)) by omega, cut_ok.mate_new₁ cut_glued (by omega)]
860 congr 2; omega
861 · rw [ite_eq_right cut_glued] at glued; contradiction
862 · by_cases new₁ : κ.two = true ∧ c = κ.c₁ ∧ κ.e₁ ≤ k ∧ k ≤ κ.e₁ + 2
863 · obtain ⟨cut_glued, rfl, k_ge, k_le⟩ := new₁
864 rw [show k = κ.e₁ + (k - κ.e₁) by omega, cut_ok.mate_new₁ cut_glued (by omega)] at glued
865 simp only [Option.some.injEq, Prod.mk.injEq] at glued
866 obtain ⟨rfl, rfl⟩ := glued
867 refine ⟨cut_ok.c₀, by rw [cut_ok.E_c₀]; omega, ?_⟩
868 rw [show κ.e₀ + 2 - (k - κ.e₁) = κ.e₀ + (2 - (k - κ.e₁)) by omega, cut_ok.mate_new₀ (by omega),
869 ite_eq_left cut_glued]
870 congr 2; omega
871 · obtain ⟨u, u_lt, rfl⟩ := cut_ok.preimage k_lt (fun ⟨is_c₀, k_gt, k_le⟩ => new₀ ⟨is_c₀, by omega, k_le⟩)
872 (fun ⟨cut_glued, is_c₁, k_gt, k_le⟩ => new₁ ⟨cut_glued, is_c₁, by omega, k_le⟩)
873 -- the edge is not the cut edge (whose position would be a new edge)
874 have not_cut₀ : ¬ (c = κ.c₀ ∧ u = κ.e₀) := by
875 rintro ⟨rfl, rfl⟩; exact new₀ ⟨rfl, by rw [cut_ok.sh_c₀_le (Nat.le_refl _)]; omega,
876 by rw [cut_ok.sh_c₀_le (Nat.le_refl _)]; omega⟩
877 -- nor the partner edge
878 have not_cut₁ : ¬ (κ.two = true ∧ c = κ.c₁ ∧ u = κ.e₁) := by
879 rintro ⟨cut_glued, rfl, rfl⟩
880 exact new₁ ⟨cut_glued, rfl, by rw [cut_ok.sh_c₁_le cut_glued (Nat.le_refl _)]; omega,
881 by rw [cut_ok.sh_c₁_le cut_glued (Nat.le_refl _)]; omega⟩
882 rw [cut_ok.mate_old not_cut₀ not_cut₁, Option.map_eq_some_iff] at glued
883 obtain ⟨⟨c₂, u₂⟩, glued_old, shifted⟩ := glued
884 simp only [Prod.mk.injEq] at shifted
885 obtain ⟨rfl, rfl⟩ := shifted
886 obtain ⟨c₂_lt, u₂_lt, glued_back⟩ := cut_ok.wf.mate_valid c u c₂ u₂ c_lt u_lt glued_old
887 obtain ⟨mate_not_cut₀, mate_not_cut₁⟩ := cut_ok.target_not_cut c_lt u_lt glued_old not_cut₀ not_cut₁
888 refine ⟨c₂_lt, cut_ok.sh_lt u₂_lt, ?_⟩
889 rw [cut_ok.mate_old mate_not_cut₀ mate_not_cut₁, glued_back]; rfl
891end Cut.OK
893end SpectreKnot.Gluing

← SpectreKnot/CompFull.leanSpectreKnot/Lens.lean →