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

lean/SpectreKnot/Move.lean

710 lines · 49 declarations, each with its own page · on GitHub ·

A move: lengthen side j₀ of child c₀ by 2, together with the side of the sibling glued to it (Table 2), or alone if it lies on the parent's rim. The composition with the longer sides is (equivalent to) the old one with one edge cut into three (Move.OK.equiv), so by Subdivide and Signature it has the signature if the old one has (Lemma 7.1: Move.OK.keep, in Parity.lean).

← SpectreKnot/Lens.leanSpectreKnot/Signature.lean →

All 39 files, and the declarations of this one
1/-
2A *move*: lengthen side `j₀` of child `c₀` by 2, together with the side of the sibling glued to it (Table 2), or
3alone if it lies on the parent's rim. The composition with the longer sides is (equivalent to) the old one with one
4edge cut into three (`Move.OK.equiv`), so by `Subdivide` and `Signature` it has the signature if the old one has
5(Lemma 7.1: `Move.OK.keep`, in `Parity.lean`).
6-/
8
9namespace SpectreKnot.Compose
11open Gluing Pattern
13/-- A move: cut the edge at offset `r₀` of side `j₀` of child `c₀` (and the same edge seen from the sibling). -/
14structure Move where
15 c₀ : Nat
16 j₀ : Nat
17 r₀ : Nat
19namespace Move
21variable (T : Kind) (μ : Move)
23/-- Is side `j₀` of child `c₀` glued to a sibling? -/
24def two : Bool := (adjAt T μ.c₀ μ.j₀).isSome
26/-- The sibling and its side (meaningful when `two`). -/
27def c₁ : Nat := ((adjAt T μ.c₀ μ.j₀).getD (0, 0)).1
28def j₁ : Nat := ((adjAt T μ.c₀ μ.j₀).getD (0, 0)).2
30/-- Side `j` of child `c` is one of the sides lengthened. -/
31def Hit (c j : Nat) : Prop := (c = μ.c₀ ∧ j = μ.j₀) ∨ (μ.two T = true ∧ c = μ.c₁ T ∧ j = μ.j₁ T)
33instance (c j : Nat) : Decidable (μ.Hit T c j) := by unfold Hit; infer_instance
35/-- The new side lengths. -/
36def lens (L : Nat → Nat → Nat) (c j : Nat) : Nat := L c j + if μ.Hit T c j then 2 else 0
38/-- The offset of the cut edge in the sibling's side. -/
39def r₁ (L : Nat → Nat → Nat) : Nat := L μ.c₀ μ.j₀ - 1 - μ.r₀
41/-- The cut, in the positions of the old composition. -/
42def cut (L : Nat → Nat → Nat) : Cut :=
43 ⟨μ.c₀, pos (L μ.c₀) μ.j₀ + μ.r₀, μ.c₁ T, pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L, μ.two T⟩
45/-- The new Σ offset: the corner moves on by 2 if the edge cut lies before it on the Σ child's side 5. -/
46def d' (L : Nat → Nat → Nat) (d : Nat) : Nat :=
47 d + (if kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5 ∧ μ.r₀ + 2 ≤ d then 2 else 0)
48 + (if μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma ∧ μ.j₁ T = 5 ∧ μ.r₁ L + 2 ≤ d then 2 else 0)
50/-- When a move can be made. -/
51structure OK (L : Nat → Nat → Nat) (d : Nat) (ω : Bool) : Prop where
52 /-- the old composition is well formed -/
53 wf : (Comp.ofLens T L d ω).toGluing.WF
54 /-- every side has an edge -/
55 pos_len : ∀ c, c < nk T → ∀ j, j < 6 → 1 ≤ L c j
56 /-- glued sides have the same length -/
57 pair : ∀ c, c < nk T → ∀ j, j < 6 → ∀ c' j', adjAt T c j = some (c', j') → L c' j' = L c j
58 /-- the child cut is a child -/
59 c₀ : μ.c₀ < nk T
60 /-- the side cut is one of its six sides -/
61 j₀ : μ.j₀ < 6
62 /-- the cut edge is not the first edge of its side -/
63 r₀ : 1 ≤ μ.r₀
64 /-- nor the last -/
65 r₀' : μ.r₀ + 2 ≤ L μ.c₀ μ.j₀
66 /-- the Σ corner and its neighbours lie inside side 5 of the Σ child -/
67 sig : ∀ c, c < nk T → kidAt T c = .Sigma → 2 ≤ d ∧ d + 2 ≤ L c 5
68 /-- there is only one Σ child -/
69 sig1 : ∀ c c', c < nk T → c' < nk T → kidAt T c = .Sigma → kidAt T c' = .Sigma → c = c'
70 /-- a cut on the Σ child's side 5 is clear of its corners -/
71 cut₀ : kidAt T μ.c₀ = .Sigma → μ.j₀ = 5 → d + 1 ≤ μ.r₀ ∨ μ.r₀ + 2 ≤ d
72 /-- the same, seen from the sibling -/
73 cut₁ : μ.two T = true → kidAt T (μ.c₁ T) = .Sigma → μ.j₁ T = 5 → d + 1 ≤ μ.r₁ L ∨ μ.r₁ L + 2 ≤ d
75variable {T} {μ} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
77/-- Side `j₀` of `c₀` is glued to side `j₁` of the sibling `c₁` if `two`, and lies on the parent's rim otherwise. -/
78theorem adj₀ : adjAt T μ.c₀ μ.j₀ = if μ.two T = true then some (μ.c₁ T, μ.j₁ T) else none := by
79 unfold two c₁ j₁
80 cases adjAt T μ.c₀ μ.j₀ <;> rfl
82/-! #### The new Σ offset -/
84/-- If neither side lengthened is side 5 of the Σ child, the Σ offset does not change. -/
85theorem d'_eq (not_sigma₀ : ¬ (kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5))
86 (not_sigma₁ : ¬ (μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma ∧ μ.j₁ T = 5)) : μ.d' T L d = d := by
87 unfold d'
88 rw [ite_eq_right (show ¬ (kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5 ∧ μ.r₀ + 2 ≤ d) from
89 fun ⟨is_sigma, is_5, _⟩ => not_sigma₀ ⟨is_sigma, is_5⟩),
90 ite_eq_right (show ¬ (μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma ∧ μ.j₁ T = 5 ∧ μ.r₁ L + 2 ≤ d) from
91 fun ⟨side_glued, is_sigma, is_5, _⟩ => not_sigma₁ ⟨side_glued, is_sigma, is_5⟩)]
92 rfl
94/-- If side `j₀` of `c₀` is side 5 of the Σ child, the Σ offset moves on by 2 exactly when the cut lies before the
95corner. -/
96theorem d'_c₀ (is_sigma : kidAt T μ.c₀ = .Sigma) (is_5 : μ.j₀ = 5)
97 (not_sigma₁ : ¬ (μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma ∧ μ.j₁ T = 5)) :
98 μ.d' T L d = d + if μ.r₀ + 2 ≤ d then 2 else 0 := by
99 unfold d'
100 rw [ite_eq_right (show ¬ (μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma ∧ μ.j₁ T = 5 ∧ μ.r₁ L + 2 ≤ d) from
101 fun ⟨side_glued, sib_sigma, sib_5, _⟩ => not_sigma₁ ⟨side_glued, sib_sigma, sib_5⟩), Nat.add_zero]
102 by_cases before : μ.r₀ + 2 ≤ d
103 · rw [ite_eq_left ⟨is_sigma, is_5, before⟩, ite_eq_left before]
104 · rw [ite_eq_right (fun ⟨_, _, before'⟩ => before before'), ite_eq_right before]
106/-- If the sibling's side `j₁` is side 5 of the Σ child, the Σ offset moves on by 2 exactly when the cut lies before
107the corner. -/
108theorem d'_c₁ (side_glued : μ.two T = true) (is_sigma : kidAt T (μ.c₁ T) = .Sigma) (is_5 : μ.j₁ T = 5)
109 (not_sigma₀ : ¬ (kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5)) :
110 μ.d' T L d = d + if μ.r₁ L + 2 ≤ d then 2 else 0 := by
111 unfold d'
112 rw [ite_eq_right (show ¬ (kidAt T μ.c₀ = .Sigma ∧ μ.j₀ = 5 ∧ μ.r₀ + 2 ≤ d) from
113 fun ⟨c₀_sigma, c₀_5, _⟩ => not_sigma₀ ⟨c₀_sigma, c₀_5⟩), Nat.add_zero]
114 by_cases before : μ.r₁ L + 2 ≤ d
115 · rw [ite_eq_left ⟨side_glued, is_sigma, is_5, before⟩, ite_eq_left before]
116 · rw [ite_eq_right (fun ⟨_, _, _, before'⟩ => before before'), ite_eq_right before]
118namespace OK
120variable (move_ok : μ.OK T L d ω)
122include move_ok
124set_option linter.unusedSectionVars false
126/-- If side `j₀` of `c₀` is glued, the sibling `c₁` is a different child, and its side `j₁` is glued back. -/
127theorem sib (side_glued : μ.two T = true) :
128 μ.c₁ T < nk T ∧ μ.j₁ T < 6 ∧ μ.c₁ T ≠ μ.c₀ ∧ adjAt T (μ.c₁ T) (μ.j₁ T) = some (μ.c₀, μ.j₀) := by
129 -- Table 2 glues side `j₀` of `c₀` to side `j₁` of `c₁`
130 have glued := adj₀ (T := T) (μ := μ)
131 rw [ite_eq_left side_glued] at glued
132 exact adj_valid move_ok.c₀ move_ok.j₀ glued
134/-- The sibling's side `j₁` is as long as side `j₀` of `c₀`. -/
135theorem L₁ (side_glued : μ.two T = true) : L (μ.c₁ T) (μ.j₁ T) = L μ.c₀ μ.j₀ := by
136 -- Table 2 glues side `j₀` of `c₀` to side `j₁` of `c₁`
137 have glued := adj₀ (T := T) (μ := μ)
138 rw [ite_eq_left side_glued] at glued
139 exact move_ok.pair _ move_ok.c₀ _ move_ok.j₀ _ _ glued
141/-- Only one side of each child is hit: of `c₀`, side `j₀`. -/
142theorem hit_c₀ {j : Nat} : μ.Hit T μ.c₀ j ↔ j = μ.j₀ := by
143 unfold Hit
144 constructor
145 · rintro (⟨_, is_j₀⟩ | ⟨side_glued, same, _⟩)
146 · exact is_j₀
147 · exact absurd same.symm (move_ok.sib side_glued).2.2.1
148 · intro is_j₀; exact Or.inl ⟨rfl, is_j₀⟩
150/-- Of the sibling `c₁`, only side `j₁` is hit. -/
151theorem hit_c₁ (side_glued : μ.two T = true) {j : Nat} : μ.Hit T (μ.c₁ T) j ↔ j = μ.j₁ T := by
152 unfold Hit
153 constructor
154 · rintro (⟨same, _⟩ | ⟨_, _, is_j₁⟩)
155 · exact absurd same (move_ok.sib side_glued).2.2.1
156 · exact is_j₁
157 · intro is_j₁; exact Or.inr ⟨side_glued, rfl, is_j₁⟩
159/-- No side of any other child is hit. -/
160theorem hit_other {c j : Nat} (not_c₀ : c ≠ μ.c₀) (not_c₁ : ¬ (μ.two T = true ∧ c = μ.c₁ T)) : ¬ μ.Hit T c j := by
161 rintro (⟨is_c₀, _⟩ | ⟨side_glued, is_c₁, _⟩)
162 · exact not_c₀ is_c₀
163 · exact not_c₁ ⟨side_glued, is_c₁⟩
165/-- Positions of the new composition, on `c₀`: the sides after `j₀` begin two edges later. -/
166theorem pos_c₀ (j : Nat) : pos (μ.lens T L μ.c₀) j = pos (L μ.c₀) j + if μ.j₀ < j then 2 else 0 := by
167 induction j with
168 | zero => simp [pos]
169 | succ j ih =>
171 simp only [lens]
172 by_cases is_j₀ : j = μ.j₀
173 · rw [ite_eq_left (move_ok.hit_c₀.mpr is_j₀), ite_eq_right (by omega), ite_eq_left (by omega)]; omega
174 · rw [ite_eq_right (fun hit => is_j₀ (move_ok.hit_c₀.mp hit))]
175 by_cases after : μ.j₀ < j
176 · rw [ite_eq_left after, ite_eq_left (by omega)]; omega
177 · rw [ite_eq_right after, ite_eq_right (by omega)]; omega
179/-- Positions of the new composition, on the sibling `c₁`: the sides after `j₁` begin two edges later. -/
180theorem pos_c₁ (side_glued : μ.two T = true) (j : Nat) :
181 pos (μ.lens T L (μ.c₁ T)) j = pos (L (μ.c₁ T)) j + if μ.j₁ T < j then 2 else 0 := by
182 induction j with
183 | zero => simp [pos]
184 | succ j ih =>
186 simp only [lens]
187 by_cases is_j₁ : j = μ.j₁ T
188 · rw [ite_eq_left ((move_ok.hit_c₁ side_glued).mpr is_j₁), ite_eq_right (by omega), ite_eq_left (by omega)]; omega
189 · rw [ite_eq_right (fun hit => is_j₁ ((move_ok.hit_c₁ side_glued).mp hit))]
190 by_cases after : μ.j₁ T < j
191 · rw [ite_eq_left after, ite_eq_left (by omega)]; omega
192 · rw [ite_eq_right after, ite_eq_right (by omega)]; omega
194/-- Positions of the new composition, on every other child: unchanged. -/
195theorem pos_other {c : Nat} (not_c₀ : c ≠ μ.c₀) (not_c₁ : ¬ (μ.two T = true ∧ c = μ.c₁ T)) (j : Nat) :
196 pos (μ.lens T L c) j = pos (L c) j := by
197 induction j with
198 | zero => rfl
199 | succ j ih =>
200 rw [pos_succ, pos_succ, ih]; simp only [lens]; rw [ite_eq_right (move_ok.hit_other not_c₀ not_c₁)]; omega
202/-- After the move every side still has an edge. -/
203theorem lens_pos_len : ∀ c, c < nk T → ∀ j, j < 6 → 1 ≤ μ.lens T L c j := by
204 intro c c_lt j j_lt
205 -- every side had an edge before
206 have := move_ok.pos_len c c_lt j j_lt
207 simp only [lens]; omega
209/-- The cut can be made. -/
210theorem cutOK : (μ.cut T L).OK (Comp.ofLens T L d ω).toGluing where
211 wf := move_ok.wf
212 c₀ := by simp only [cut]; rw [ofLens_n]; exact move_ok.c₀
213 e₀ := by
214 show pos (L μ.c₀) μ.j₀ + μ.r₀ + 1 < (Comp.ofLens T L d ω).toGluing.E μ.c₀
215 rw [ofLens_E move_ok.c₀]
216 -- side `j₀` is one of the six sides
217 have j₀_lt := move_ok.j₀
218 -- side `j₀` ends where side `j₀ + 1` begins
219 have side_end := pos_lt_of_pos (L μ.c₀) (move_ok.pos_len _ move_ok.c₀) (show μ.j₀ < μ.j₀ + 1 by omega)
220 (by omega)
221 -- side `j₀ + 1` begins no later than the end of the rim
222 have next_le := pos_mono (L μ.c₀) (show μ.j₀ + 1 ≤ 6 by omega)
223 -- the cut edge is at least two edges from the end of side `j₀`
224 have r₀_le := move_ok.r₀'
225 rw [pos_succ] at next_le; omega
226 mate := by
227 show (Comp.ofLens T L d ω).mate μ.c₀ (pos (L μ.c₀) μ.j₀ + μ.r₀) =
228 if μ.two T = true then some (μ.c₁ T, pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L) else none
229 -- the cut edge lies inside side `j₀`
230 have r₀_le := move_ok.r₀'
231 rw [ofLens_mate move_ok.pos_len move_ok.c₀ move_ok.j₀ (by omega), adj₀]
232 by_cases side_glued : μ.two T = true
233 · rw [ite_eq_left side_glued, ite_eq_left side_glued]
234 simp only [Option.map_some, move_ok.L₁ side_glued, r₁]
235 congr 2; omega
236 · rw [ite_eq_right side_glued, ite_eq_right side_glued]; rfl
237 ne side_glued := (move_ok.sib side_glued).2.2.1
238 e₁ side_glued := by
239 obtain ⟨c₁_lt, j₁_lt, _, _⟩ := move_ok.sib side_glued
240 show pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L + 1 < (Comp.ofLens T L d ω).toGluing.E (μ.c₁ T)
241 rw [ofLens_E c₁_lt]
242 -- side `j₁ + 1` begins no later than the end of the rim
243 have next_le := pos_mono (L (μ.c₁ T)) (show μ.j₁ T + 1 ≤ 6 by omega)
244 -- the cut edge is at least two edges from the end of side `j₀`
245 have r₀_le := move_ok.r₀'
246 -- and at least one edge from its start
247 have r₀_ge := move_ok.r₀
248 -- the two glued sides have the same length
249 have same_len := move_ok.L₁ side_glued
250 simp only [r₁]; rw [pos_succ] at next_le; omega
252/-! #### Positions under the cut -/
254/-- On `c₀`, positions up to the cut edge stay put. -/
255theorem sh₀_le {p : Nat} (p_le : p ≤ pos (L μ.c₀) μ.j₀ + μ.r₀) : (μ.cut T L).sh μ.c₀ p = p :=
256 move_ok.cutOK.sh_c₀_le (G := (Comp.ofLens T L d ω).toGluing) p_le
258/-- On `c₀`, positions after the cut edge move on by 2. -/
259theorem sh₀_gt {p : Nat} (p_gt : pos (L μ.c₀) μ.j₀ + μ.r₀ < p) : (μ.cut T L).sh μ.c₀ p = p + 2 :=
260 move_ok.cutOK.sh_c₀_gt (G := (Comp.ofLens T L d ω).toGluing) p_gt
262/-- On the sibling, positions up to its cut edge stay put. -/
263theorem sh₁_le (side_glued : μ.two T = true) {p : Nat} (p_le : p ≤ pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L) :
264 (μ.cut T L).sh (μ.c₁ T) p = p :=
265 move_ok.cutOK.sh_c₁_le (G := (Comp.ofLens T L d ω).toGluing) side_glued p_le
267/-- On the sibling, positions after its cut edge move on by 2. -/
268theorem sh₁_gt (side_glued : μ.two T = true) {p : Nat} (p_gt : pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L < p) :
269 (μ.cut T L).sh (μ.c₁ T) p = p + 2 :=
270 move_ok.cutOK.sh_c₁_gt (G := (Comp.ofLens T L d ω).toGluing) side_glued p_gt
272/-- On every other child, positions stay put. -/
273theorem sh_oth {c p : Nat} (not_c₀ : c ≠ μ.c₀) (not_c₁ : ¬ (μ.two T = true ∧ c = μ.c₁ T)) :
274 (μ.cut T L).sh c p = p :=
275 move_ok.cutOK.sh_other (G := (Comp.ofLens T L d ω).toGluing) not_c₀ not_c₁
277/-- Positions in a side that is not lengthened move with the sides before it. -/
278theorem sh_side {c j q : Nat} (c_lt : c < nk T) (j_lt : j < 6) (q_lt : q < L c j) (not_hit : ¬ μ.Hit T c j) :
279 (μ.cut T L).sh c (pos (L c) j + q) = pos (μ.lens T L c) j + q := by
280 -- the cut edge is at least two edges from the end of side `j₀`
281 have r₀_le := move_ok.r₀'
282 by_cases is_c₀ : c = μ.c₀
283 · subst is_c₀
284 -- side `j` is not the side cut
285 have not_j₀ : j ≠ μ.j₀ := fun is_j₀ => not_hit (move_ok.hit_c₀.mpr is_j₀)
286 rw [move_ok.pos_c₀]
287 by_cases before : j < μ.j₀
288 -- side `j` ends no later than side `j₀` begins
289 · have side_ends := pos_mono (L μ.c₀) (show j + 1 ≤ μ.j₀ by omega)
290 rw [pos_succ] at side_ends
291 rw [move_ok.sh₀_le (by omega), ite_eq_right (by omega)]; omega
292 -- side `j` begins no earlier than side `j₀` ends
293 · have side_begins := pos_mono (L μ.c₀) (show μ.j₀ + 1 ≤ j by omega)
294 rw [pos_succ] at side_begins
295 rw [move_ok.sh₀_gt (by omega), ite_eq_left (by omega)]; omega
296 · by_cases is_c₁ : μ.two T = true ∧ c = μ.c₁ T
297 · obtain ⟨side_glued, rfl⟩ := is_c₁
298 -- side `j` is not the sibling's side cut
299 have not_j₁ : j ≠ μ.j₁ T := fun is_j₁ => not_hit ((move_ok.hit_c₁ side_glued).mpr is_j₁)
300 -- the two glued sides have the same length
301 have same_len := move_ok.L₁ side_glued
302 rw [move_ok.pos_c₁ side_glued]
303 by_cases before : j < μ.j₁ T
304 -- side `j` ends no later than side `j₁` begins
305 · have side_ends := pos_mono (L (μ.c₁ T)) (show j + 1 ≤ μ.j₁ T by omega)
306 rw [pos_succ] at side_ends
307 rw [move_ok.sh₁_le side_glued (by simp only [r₁]; omega), ite_eq_right (by omega)]; omega
308 -- side `j` begins no earlier than side `j₁` ends
309 · have side_begins := pos_mono (L (μ.c₁ T)) (show μ.j₁ T + 1 ≤ j by omega)
310 rw [pos_succ] at side_begins
311 rw [move_ok.sh₁_gt side_glued (by simp only [r₁]; omega), ite_eq_left (by omega)]; omega
312 · rw [move_ok.sh_oth is_c₀ is_c₁, move_ok.pos_other is_c₀ is_c₁]
314/-- A position determines its side and offset. -/
315theorem side_unique {c j j' o o' : Nat} (c_lt : c < nk T) (j_lt : j < 6) (j'_lt : j' < 6) (o_lt : o < L c j)
316 (o'_lt : o' < L c j') (same : pos (L c) j + o = pos (L c) j' + o') : j = j' := by
317 -- the side lookup finds side `j` at the first position
318 have finds_j := sideIdx_eq (L c) (move_ok.pos_len c c_lt) j_lt o_lt
319 -- and side `j'` at the second
320 have finds_j' := sideIdx_eq (L c) (move_ok.pos_len c c_lt) j'_lt o'_lt
321 rw [same] at finds_j
322 rw [finds_j] at finds_j'; exact finds_j'
324/-- The partner of a side that is not lengthened is not lengthened either. -/
325theorem not_hit_partner {c j c' j' : Nat} (c_lt : c < nk T) (j_lt : j < 6) (glued : adjAt T c j = some (c', j'))
326 (not_hit : ¬ μ.Hit T c j) : ¬ μ.Hit T c' j' := by
327 obtain ⟨c'_lt, j'_lt, c'_ne, glued_back⟩ := adj_valid c_lt j_lt glued
328 rintro (⟨rfl, rfl⟩ | ⟨side_glued, rfl, rfl⟩)
329 -- (c', j') = (c₀, j₀): then (c, j) is the partner of (c₀, j₀), which is hit
330 · have partner := adj₀ (T := T) (μ := μ)
331 rw [glued_back] at partner
332 by_cases side_glued : μ.two T = true
333 · rw [ite_eq_left side_glued] at partner
334 simp only [Option.some.injEq, Prod.mk.injEq] at partner
335 exact not_hit (Or.inr ⟨side_glued, partner.1, partner.2⟩)
336 · rw [ite_eq_right side_glued] at partner; contradiction
337 -- (c', j') = (c₁, j₁): then (c, j) is the partner of (c₁, j₁), that is (c₀, j₀)
338 · have partner := (move_ok.sib side_glued).2.2.2
339 rw [glued_back] at partner
340 simp only [Option.some.injEq, Prod.mk.injEq] at partner
341 exact not_hit (Or.inl ⟨partner.1, partner.2⟩)
343/-! #### The subdivided gluing, in the move's terms -/
345set_option quotPrecheck false
346local notation "G₀" => (Comp.ofLens T L d ω).toGluing
347local notation "G₁" => (Comp.ofLens T (μ.lens T L) (μ.d' T L d) ω).toGluing
348local notation "Gs" => subdiv (Comp.ofLens T L d ω).toGluing (μ.cut T L)
350/-- In the subdivided gluing, `c₀` has two more edges. -/
351theorem sE₀ : (Gs).E μ.c₀ = (G₀).E μ.c₀ + 2 := move_ok.cutOK.E_c₀
353/-- In the subdivided gluing, the sibling has two more edges. -/
354theorem sE₁ (side_glued : μ.two T = true) : (Gs).E (μ.c₁ T) = (G₀).E (μ.c₁ T) + 2 := move_ok.cutOK.E_c₁ side_glued
356/-- In the subdivided gluing, every other child keeps its rim length. -/
357theorem sE_oth {c : Nat} (not_c₀ : c ≠ μ.c₀) (not_c₁ : ¬ (μ.two T = true ∧ c = μ.c₁ T)) : (Gs).E c = (G₀).E c :=
358 move_ok.cutOK.E_other not_c₀ not_c₁
360/-- In the subdivided gluing, an edge that is not cut is glued as before (with positions moved on). -/
361theorem smate_old {c k : Nat} (not_cut₀ : ¬ (c = μ.c₀ ∧ k = pos (L μ.c₀) μ.j₀ + μ.r₀))
362 (not_cut₁ : ¬ (μ.two T = true ∧ c = μ.c₁ T ∧ k = pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L)) :
363 (Gs).mate c ((μ.cut T L).sh c k) = ((G₀).mate c k).map fun (c₂, k₂) => (c₂, (μ.cut T L).sh c₂ k₂) :=
364 move_ok.cutOK.mate_old not_cut₀ not_cut₁
366/-- In the subdivided gluing, the three new edges of `c₀` are glued, in reverse order, to the sibling's (or lie on the
367rim). -/
368theorem smate_new₀ {i : Nat} (i_le : i ≤ 2) :
369 (Gs).mate μ.c₀ (pos (L μ.c₀) μ.j₀ + μ.r₀ + i) =
370 if μ.two T = true then some (μ.c₁ T, pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L + 2 - i) else none :=
371 move_ok.cutOK.mate_new₀ i_le
373/-- In the subdivided gluing, the three new edges of the sibling are glued, in reverse order, to those of `c₀`. -/
374theorem smate_new₁ (side_glued : μ.two T = true) {i : Nat} (i_le : i ≤ 2) :
375 (Gs).mate (μ.c₁ T) (pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L + i) = some (μ.c₀, pos (L μ.c₀) μ.j₀ + μ.r₀ + 2 - i) :=
376 move_ok.cutOK.mate_new₁ side_glued i_le
378/-- Rim lengths agree. -/
379theorem E_eq {c : Nat} (c_lt : c < nk T) : (G₁).E c = (Gs).E c := by
380 rw [ofLens_E c_lt]
381 -- side `j₀` is one of the six sides
382 have j₀_lt := move_ok.j₀
383 by_cases is_c₀ : c = μ.c₀
384 · subst is_c₀; rw [move_ok.pos_c₀, ite_eq_left (by omega), move_ok.sE₀, ofLens_E c_lt]
385 · by_cases is_c₁ : μ.two T = true ∧ c = μ.c₁ T
386 · obtain ⟨side_glued, rfl⟩ := is_c₁
387 rw [move_ok.pos_c₁ side_glued, ite_eq_left (move_ok.sib side_glued).2.1, move_ok.sE₁ side_glued, ofLens_E c_lt]
388 · rw [move_ok.pos_other is_c₀ is_c₁, move_ok.sE_oth is_c₀ is_c₁, ofLens_E c_lt]
390/-- Corners agree. -/
391theorem A_eq {c : Nat} (c_lt : c < nk T) : (G₁).A c = (μ.cut T L).sh c ((G₀).A c) := by
392 rw [ofLens_A c_lt, ofLens_A c_lt]
393 -- the cut edge is at least two edges from the end of side `j₀`
394 have r₀_le := move_ok.r₀'
395 -- and at least one edge from its start
396 have r₀_ge := move_ok.r₀
397 -- side `j₀` is one of the six sides
398 have j₀_lt := move_ok.j₀
399 by_cases is_sigma : kidAt T c = .Sigma
400 · rw [ite_eq_left is_sigma, ite_eq_left is_sigma]
401 obtain ⟨d_ge, d_le⟩ := move_ok.sig c c_lt is_sigma
402 by_cases is_c₀ : c = μ.c₀
403 · subst is_c₀
404 -- the sibling is not the Σ child as well
405 have sib_not_sigma : ¬ (μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma) := fun ⟨side_glued, sib_sigma⟩ =>
406 (move_ok.sib side_glued).2.2.1 (move_ok.sig1 _ _ (move_ok.sib side_glued).1 c_lt sib_sigma is_sigma)
407 rw [move_ok.pos_c₀]
408 by_cases is_5 : μ.j₀ = 5
409 · rw [ite_eq_right (by omega)]
410 -- side `j₀` is side 5
411 have pos_5 : pos (L μ.c₀) μ.j₀ = pos (L μ.c₀) 5 := by rw [is_5]
412 rw [d'_c₀ is_sigma is_5 (fun ⟨side_glued, sib_sigma, _⟩ => sib_not_sigma ⟨side_glued, sib_sigma⟩)]
413 rcases move_ok.cut₀ is_sigma is_5 with cut_after | cut_before
414 · rw [ite_eq_right (show ¬ μ.r₀ + 2 ≤ d by omega), move_ok.sh₀_le (by omega)]; omega
415 · rw [ite_eq_left cut_before, move_ok.sh₀_gt (by omega)]; omega
416 · rw [ite_eq_left (by omega), d'_eq (fun ⟨_, is_5'⟩ => is_5 is_5')
417 (fun ⟨side_glued, sib_sigma, _⟩ => sib_not_sigma ⟨side_glued, sib_sigma⟩)]
418 -- side `j₀` ends before side 5 begins
419 have side_ends := pos_mono (L μ.c₀) (show μ.j₀ + 1 ≤ 5 by omega)
420 rw [pos_succ] at side_ends
421 rw [move_ok.sh₀_gt (by omega)]; omega
422 · by_cases is_c₁ : μ.two T = true ∧ c = μ.c₁ T
423 · obtain ⟨side_glued, rfl⟩ := is_c₁
424 -- `c₀` is not the Σ child, since the sibling is
425 have c₀_not_sigma : kidAt T μ.c₀ ≠ .Sigma :=
426 fun c₀_sigma => is_c₀ (move_ok.sig1 _ _ c_lt move_ok.c₀ is_sigma c₀_sigma)
427 -- the two glued sides have the same length
428 have same_len := move_ok.L₁ side_glued
429 rw [move_ok.pos_c₁ side_glued]
430 by_cases is_5 : μ.j₁ T = 5
431 · rw [ite_eq_right (by omega)]
432 -- side `j₁` is side 5
433 have pos_5 : pos (L (μ.c₁ T)) (μ.j₁ T) = pos (L (μ.c₁ T)) 5 := by rw [is_5]
434 rw [d'_c₁ side_glued is_sigma is_5 (fun ⟨c₀_sigma, _⟩ => c₀_not_sigma c₀_sigma)]
435 rcases move_ok.cut₁ side_glued is_sigma is_5 with cut_after | cut_before
436 · rw [ite_eq_right (show ¬ μ.r₁ L + 2 ≤ d by omega), move_ok.sh₁_le side_glued (by omega)]; omega
437 · rw [ite_eq_left cut_before, move_ok.sh₁_gt side_glued (by omega)]; omega
438 -- side `j₁` is one of the six sides, and not side 5
439 · have j₁_lt := (move_ok.sib side_glued).2.1
440 rw [ite_eq_left (by omega)]
441 rw [d'_eq (fun ⟨c₀_sigma, _⟩ => c₀_not_sigma c₀_sigma) (fun ⟨_, _, is_5'⟩ => is_5 is_5')]
442 -- side `j₁` ends before side 5 begins
443 have side_ends := pos_mono (L (μ.c₁ T)) (show μ.j₁ T + 1 ≤ 5 by omega)
444 rw [pos_succ] at side_ends
445 rw [move_ok.sh₁_gt side_glued (by simp only [r₁]; omega)]; omega
446 -- the Σ child is neither `c₀` nor the sibling
447 · have c₀_not_sigma : kidAt T μ.c₀ ≠ .Sigma :=
448 fun c₀_sigma => is_c₀ (move_ok.sig1 _ _ c_lt move_ok.c₀ is_sigma c₀_sigma)
449 -- the sibling is not the Σ child
450 have sib_not_sigma : ¬ (μ.two T = true ∧ kidAt T (μ.c₁ T) = .Sigma) := fun ⟨side_glued, sib_sigma⟩ =>
451 is_c₁ ⟨side_glued, move_ok.sig1 _ _ c_lt (move_ok.sib side_glued).1 is_sigma sib_sigma⟩
452 rw [move_ok.pos_other is_c₀ is_c₁, d'_eq (fun ⟨c₀_sigma, _⟩ => c₀_not_sigma c₀_sigma)
453 (fun ⟨side_glued, sib_sigma, _⟩ => sib_not_sigma ⟨side_glued, sib_sigma⟩), move_ok.sh_oth is_c₀ is_c₁]
454 · rw [ite_eq_right is_sigma, ite_eq_right is_sigma]
455 by_cases is_c₀ : c = μ.c₀
456 · subst is_c₀; rw [move_ok.sh₀_le (by omega)]
457 · by_cases is_c₁ : μ.two T = true ∧ c = μ.c₁ T
458 · obtain ⟨side_glued, rfl⟩ := is_c₁; rw [move_ok.sh₁_le side_glued (by omega)]
459 · rw [move_ok.sh_oth is_c₀ is_c₁]
461/-- The corner `A` is not at either end of a cut edge (cuts avoid the first and last edge of every side, and the Σ
462corner). -/
463theorem A_clear₀ {c : Nat} (c_lt : c < nk T) (is_c₀ : c = μ.c₀) :
464 (G₀).A c ≠ pos (L μ.c₀) μ.j₀ + μ.r₀ ∧ (G₀).A c ≠ pos (L μ.c₀) μ.j₀ + μ.r₀ + 1 := by
465 subst is_c₀
466 rw [ofLens_A c_lt]
467 -- the cut edge is at least two edges from the end of side `j₀`
468 have r₀_le := move_ok.r₀'
469 -- and at least one edge from its start
470 have r₀_ge := move_ok.r₀
471 -- side `j₀` is one of the six sides
472 have j₀_lt := move_ok.j₀
473 by_cases is_sigma : kidAt T μ.c₀ = .Sigma
474 · rw [ite_eq_left is_sigma]
475 obtain ⟨d_ge, d_le⟩ := move_ok.sig _ c_lt is_sigma
476 by_cases is_5 : μ.j₀ = 5
477 -- side `j₀` is side 5, and the cut is clear of the corner
478 · have pos_5 : pos (L μ.c₀) μ.j₀ = pos (L μ.c₀) 5 := by rw [is_5]
479 rcases move_ok.cut₀ is_sigma is_5 with cut_after | cut_before <;> omega
480 -- side `j₀` ends before side 5 begins
481 · have side_ends := pos_mono (L μ.c₀) (show μ.j₀ + 1 ≤ 5 by omega)
482 rw [pos_succ] at side_ends; omega
483 · rw [ite_eq_right is_sigma]; omega
485/-- The cut edge is not the first edge of the sibling's side. -/
486theorem r₁_ge : 1 ≤ μ.r₁ L := by
487 -- the cut edge is not the last edge of side `j₀`
488 have := move_ok.r₀'
489 simp only [r₁]; omega
491/-- Nor the last. -/
492theorem r₁_le : μ.r₁ L + 2 ≤ L μ.c₀ μ.j₀ := by
493 -- the cut edge is not the first edge of side `j₀`
494 have := move_ok.r₀
495 -- nor the last
496 have := move_ok.r₀'
497 simp only [r₁]; omega
499/-- The sibling's corner `A` is not at either end of its cut edge. -/
500theorem A_clear₁ (side_glued : μ.two T = true) {c : Nat} (c_lt : c < nk T) (is_c₁ : c = μ.c₁ T) :
501 (G₀).A c ≠ pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L ∧ (G₀).A c ≠ pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L + 1 := by
502 subst is_c₁
503 rw [ofLens_A c_lt]
504 -- the cut edge is not the last edge of the sibling's side
505 have r₁_le := move_ok.r₁_le
506 -- nor the first
507 have r₁_ge := move_ok.r₁_ge
508 -- the two glued sides have the same length
509 have same_len := move_ok.L₁ side_glued
510 -- side `j₁` is one of the six sides
511 have j₁_lt := (move_ok.sib side_glued).2.1
512 by_cases is_sigma : kidAt T (μ.c₁ T) = .Sigma
513 · rw [ite_eq_left is_sigma]
514 obtain ⟨d_ge, d_le⟩ := move_ok.sig _ c_lt is_sigma
515 by_cases is_5 : μ.j₁ T = 5
516 -- side `j₁` is side 5, and the cut is clear of the corner
517 · have pos_5 : pos (L (μ.c₁ T)) (μ.j₁ T) = pos (L (μ.c₁ T)) 5 := by rw [is_5]
518 rcases move_ok.cut₁ side_glued is_sigma is_5 with cut_after | cut_before <;> omega
519 -- side `j₁` ends before side 5 begins
520 · have side_ends := pos_mono (L (μ.c₁ T)) (show μ.j₁ T + 1 ≤ 5 by omega)
521 rw [pos_succ] at side_ends; omega
522 · rw [ite_eq_right is_sigma]; omega
524/-- Second corners agree. -/
525theorem B_eq {c : Nat} (c_lt : c < nk T) : (G₁).B c = (μ.cut T L).sh c ((G₀).B c) := by
526 -- the corner `A` is a vertex of the child
527 have A_lt := move_ok.wf.A_lt c (by rw [ofLens_n]; exact c_lt)
528 rw [ofLens_B (L := μ.lens T L) (d := μ.d' T L d) c_lt, ofLens_B (L := L) (d := d) c_lt,
529 ← ofLens_E (L := μ.lens T L) (d := μ.d' T L d) (ω := ω) c_lt, ← ofLens_E (L := L) (d := d) (ω := ω) c_lt,
530 move_ok.E_eq c_lt, move_ok.A_eq c_lt]
531 -- `A` is at neither end of the cut edge of `c₀`
532 have not_cut₀ : ∀ i, i ≤ 1 → ¬ (c = (μ.cut T L).c₀ ∧ (G₀).A c = (μ.cut T L).e₀ + i) := by
533 rintro i i_le ⟨is_c₀, at_cut⟩
534 -- the corner is clear of both ends of the cut edge
535 have clear := move_ok.A_clear₀ c_lt is_c₀
536 rcases (show i = 0 ∨ i = 1 by omega) with rfl | rfl
537 · exact clear.1 at_cut
538 · exact clear.2 at_cut
539 -- nor at either end of the sibling's cut edge
540 have not_cut₁ : ∀ i, i ≤ 1 →
541 ¬ ((μ.cut T L).two = true ∧ c = (μ.cut T L).c₁ ∧ (G₀).A c = (μ.cut T L).e₁ + i) := by
542 rintro i i_le ⟨side_glued, is_c₁, at_cut⟩
543 -- the corner is clear of both ends of the cut edge
544 have clear := move_ok.A_clear₁ side_glued c_lt is_c₁
545 rcases (show i = 0 ∨ i = 1 by omega) with rfl | rfl
546 · exact clear.1 at_cut
547 · exact clear.2 at_cut
548 by_cases B_after_A : ω = true
549 · rw [ite_eq_left B_after_A, ite_eq_left B_after_A]
550 exact move_ok.cutOK.nxt_sh A_lt (not_cut₀ 0 (by omega)) (not_cut₁ 0 (by omega))
551 · rw [ite_eq_right B_after_A, ite_eq_right B_after_A]
552 exact move_ok.cutOK.prv_sh A_lt (not_cut₀ 1 (by omega)) (not_cut₁ 1 (by omega))
554/-- The gluing along the lengthened side `j₀` of `c₀`. -/
555theorem mate_hit₀ {o : Nat} (o_lt : o < L μ.c₀ μ.j₀ + 2) :
556 (adjAt T μ.c₀ μ.j₀).map (fun (c', j') => (c', pos (μ.lens T L c') j' + μ.lens T L c' j' - 1 - o)) =
557 (Gs).mate μ.c₀ (pos (μ.lens T L μ.c₀) μ.j₀ + o) := by
558 -- the cut edge is at least two edges from the end of side `j₀`
559 have r₀_le := move_ok.r₀'
560 -- and at least one edge from its start
561 have r₀_ge := move_ok.r₀
562 rw [move_ok.pos_c₀, ite_eq_right (Nat.lt_irrefl _), Nat.add_zero]
563 -- `c₀` is not the sibling, so none of its edges is the sibling's cut edge
564 have not_cut₁ : ∀ k, ¬ (μ.two T = true ∧ μ.c₀ = μ.c₁ T ∧ k = pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L) :=
565 fun _ ⟨side_glued, same, _⟩ => (move_ok.sib side_glued).2.2.1 same.symm
566 -- an old edge of side `j₀` other than the cut edge is glued as Table 2 says, with positions moved on
567 have old : ∀ q, q < L μ.c₀ μ.j₀ → q ≠ μ.r₀ →
568 (Gs).mate μ.c₀ ((μ.cut T L).sh μ.c₀ (pos (L μ.c₀) μ.j₀ + q)) =
569 if μ.two T = true then
570 some (μ.c₁ T, (μ.cut T L).sh (μ.c₁ T) (pos (L (μ.c₁ T)) (μ.j₁ T) + L μ.c₀ μ.j₀ - 1 - q))
571 else none := by
572 intro q q_lt not_r₀
573 rw [move_ok.smate_old (fun ⟨_, same⟩ => not_r₀ (by omega)) (not_cut₁ _)]
574 show ((Comp.ofLens T L d ω).mate μ.c₀ (pos (L μ.c₀) μ.j₀ + q)).map _ = _
575 rw [ofLens_mate move_ok.pos_len move_ok.c₀ move_ok.j₀ q_lt, adj₀]
576 by_cases side_glued : μ.two T = true
577 · rw [ite_eq_left side_glued, ite_eq_left side_glued]; simp only [Option.map_some, move_ok.L₁ side_glued]
578 · rw [ite_eq_right side_glued, ite_eq_right side_glued]; rfl
579 rw [adj₀]
580 rcases (show o < μ.r₀ ∨ (μ.r₀ ≤ o ∧ o ≤ μ.r₀ + 2) ∨ μ.r₀ + 2 < o by omega) with before | at_cut | after
581 · rw [← move_ok.sh₀_le (p := pos (L μ.c₀) μ.j₀ + o) (by omega), old o (by omega) (by omega)]
582 by_cases side_glued : μ.two T = true
583 · rw [ite_eq_left side_glued, ite_eq_left side_glued]; simp only [Option.map_some]
584 rw [move_ok.pos_c₁ side_glued, ite_eq_right (Nat.lt_irrefl _), Nat.add_zero, lens,
585 ite_eq_left ((move_ok.hit_c₁ side_glued).mpr rfl), move_ok.L₁ side_glued,
586 move_ok.sh₁_gt side_glued (by simp only [r₁]; omega)]
587 congr 2; omega
588 · rw [ite_eq_right side_glued, ite_eq_right side_glued]; rfl
589 · obtain ⟨i, i_le, rfl⟩ : ∃ i, i ≤ 2 ∧ o = μ.r₀ + i := ⟨o - μ.r₀, by omega, by omega⟩
590 rw [show pos (L μ.c₀) μ.j₀ + (μ.r₀ + i) = pos (L μ.c₀) μ.j₀ + μ.r₀ + i by omega, move_ok.smate_new₀ i_le]
591 by_cases side_glued : μ.two T = true
592 · rw [ite_eq_left side_glued, ite_eq_left side_glued]; simp only [Option.map_some]
593 rw [move_ok.pos_c₁ side_glued, ite_eq_right (Nat.lt_irrefl _), Nat.add_zero, lens,
594 ite_eq_left ((move_ok.hit_c₁ side_glued).mpr rfl), move_ok.L₁ side_glued]
595 simp only [r₁]; congr 2; omega
596 · rw [ite_eq_right side_glued, ite_eq_right side_glued]; rfl
597 · rw [show pos (L μ.c₀) μ.j₀ + o = pos (L μ.c₀) μ.j₀ + (o - 2) + 2 by omega,
598 ← move_ok.sh₀_gt (p := pos (L μ.c₀) μ.j₀ + (o - 2)) (by omega), old (o - 2) (by omega) (by omega)]
599 by_cases side_glued : μ.two T = true
600 · rw [ite_eq_left side_glued, ite_eq_left side_glued]; simp only [Option.map_some]
601 rw [move_ok.pos_c₁ side_glued, ite_eq_right (Nat.lt_irrefl _), Nat.add_zero, lens,
602 ite_eq_left ((move_ok.hit_c₁ side_glued).mpr rfl), move_ok.L₁ side_glued,
603 move_ok.sh₁_le side_glued (by simp only [r₁]; omega)]
604 congr 2; omega
605 · rw [ite_eq_right side_glued, ite_eq_right side_glued]; rfl
607/-- The gluing along the lengthened side `j₁` of the sibling `c₁`. -/
608theorem mate_hit₁ (side_glued : μ.two T = true) {o : Nat} (o_lt : o < L μ.c₀ μ.j₀ + 2) :
609 (adjAt T (μ.c₁ T) (μ.j₁ T)).map (fun (c', j') => (c', pos (μ.lens T L c') j' + μ.lens T L c' j' - 1 - o)) =
610 (Gs).mate (μ.c₁ T) (pos (μ.lens T L (μ.c₁ T)) (μ.j₁ T) + o) := by
611 -- the cut edge is at least two edges from the end of side `j₀`
612 have r₀_le := move_ok.r₀'
613 -- and at least one edge from its start
614 have r₀_ge := move_ok.r₀
615 -- the two glued sides have the same length
616 have same_len := move_ok.L₁ side_glued
617 -- the offset of the cut edge in the sibling's side
618 have r₁_eq : μ.r₁ L = L μ.c₀ μ.j₀ - 1 - μ.r₀ := rfl
619 obtain ⟨c₁_lt, j₁_lt, c₁_ne, glued_back⟩ := move_ok.sib side_glued
620 rw [move_ok.pos_c₁ side_glued, ite_eq_right (Nat.lt_irrefl _), Nat.add_zero, glued_back]; simp only [Option.map_some]
621 rw [move_ok.pos_c₀, ite_eq_right (Nat.lt_irrefl _), Nat.add_zero, lens, ite_eq_left (move_ok.hit_c₀.mpr rfl)]
622 -- the sibling is not `c₀`, so none of its edges is the cut edge of `c₀`
623 have not_cut₀ : ∀ k, ¬ (μ.c₁ T = μ.c₀ ∧ k = pos (L μ.c₀) μ.j₀ + μ.r₀) := fun _ ⟨same, _⟩ => c₁_ne same
624 -- an old edge of side `j₁` other than the cut edge is glued as Table 2 says, with positions moved on
625 have old : ∀ q, q < L μ.c₀ μ.j₀ → q ≠ μ.r₁ L →
626 (Gs).mate (μ.c₁ T) ((μ.cut T L).sh (μ.c₁ T) (pos (L (μ.c₁ T)) (μ.j₁ T) + q)) =
627 some (μ.c₀, (μ.cut T L).sh μ.c₀ (pos (L μ.c₀) μ.j₀ + L μ.c₀ μ.j₀ - 1 - q)) := by
628 intro q q_lt not_r₁
629 rw [move_ok.smate_old (not_cut₀ _) (fun ⟨_, _, same⟩ => not_r₁ (by omega))]
630 show ((Comp.ofLens T L d ω).mate (μ.c₁ T) (pos (L (μ.c₁ T)) (μ.j₁ T) + q)).map _ = _
631 rw [ofLens_mate move_ok.pos_len c₁_lt j₁_lt (by omega), glued_back]; simp only [Option.map_some]
632 rcases (show o < μ.r₁ L ∨ (μ.r₁ L ≤ o ∧ o ≤ μ.r₁ L + 2) ∨ μ.r₁ L + 2 < o by omega) with before | at_cut | after
633 · rw [← move_ok.sh₁_le side_glued (p := pos (L (μ.c₁ T)) (μ.j₁ T) + o) (by omega),
634 old o (by simp only [r₁] at before; omega) (by omega), move_ok.sh₀_gt (by simp only [r₁] at before; omega)]
635 congr 2; omega
636 · obtain ⟨i, i_le, rfl⟩ : ∃ i, i ≤ 2 ∧ o = μ.r₁ L + i := ⟨o - μ.r₁ L, by omega, by omega⟩
637 rw [show pos (L (μ.c₁ T)) (μ.j₁ T) + (μ.r₁ L + i) = pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L + i by omega,
638 move_ok.smate_new₁ side_glued i_le]
639 simp only [r₁]; congr 2; omega
640 · rw [show pos (L (μ.c₁ T)) (μ.j₁ T) + o = pos (L (μ.c₁ T)) (μ.j₁ T) + (o - 2) + 2 by omega,
641 ← move_ok.sh₁_gt side_glued (p := pos (L (μ.c₁ T)) (μ.j₁ T) + (o - 2)) (by omega),
642 old (o - 2) (by simp only [r₁] at after; omega) (by omega),
643 move_ok.sh₀_le (by simp only [r₁] at after; omega)]
644 congr 2; omega
646/-- The gluings agree. -/
647theorem mate_eq {c k : Nat} (c_lt : c < nk T) (k_lt : k < (G₁).E c) : (G₁).mate c k = (Gs).mate c k := by
648 rw [ofLens_E c_lt] at k_lt
649 obtain ⟨j, o, j_lt, o_lt, rfl⟩ := decomp (μ.lens T L c) 6 (Nat.le_refl _) k k_lt
650 show (Comp.ofLens T (μ.lens T L) (μ.d' T L d) ω).mate c (pos (μ.lens T L c) j + o) = _
651 rw [ofLens_mate move_ok.lens_pos_len c_lt j_lt o_lt]
652 by_cases side_hit : μ.Hit T c j
653 -- a lengthened side: the offset, against the old length plus 2
654 · have o_lt_old := o_lt
655 simp only [lens, ite_eq_left side_hit] at o_lt_old
656 rcases side_hit with ⟨rfl, rfl⟩ | ⟨side_glued, rfl, rfl⟩
657 · exact move_ok.mate_hit₀ o_lt_old
658 · rw [move_ok.L₁ side_glued] at o_lt_old; exact move_ok.mate_hit₁ side_glued o_lt_old
659 -- a side that is not lengthened keeps its length
660 · have unchanged : ∀ c j, ¬ μ.Hit T c j → μ.lens T L c j = L c j := fun c j not_hit => by
661 simp only [lens]; rw [ite_eq_right not_hit, Nat.add_zero]
662 rw [unchanged c j side_hit] at o_lt
663 rw [← move_ok.sh_side c_lt j_lt o_lt side_hit]
664 -- the edge is not the cut edge of `c₀`, which lies in a lengthened side
665 have not_cut₀ : ¬ (c = μ.c₀ ∧ pos (L c) j + o = pos (L μ.c₀) μ.j₀ + μ.r₀) := by
666 rintro ⟨rfl, same⟩
667 -- the cut edge lies inside side `j₀`
668 have r₀_le := move_ok.r₀'
669 exact side_hit (Or.inl ⟨rfl, move_ok.side_unique c_lt j_lt move_ok.j₀ o_lt (by omega) same⟩)
670 -- nor the sibling's cut edge
671 have not_cut₁ : ¬ (μ.two T = true ∧ c = μ.c₁ T ∧ pos (L c) j + o = pos (L (μ.c₁ T)) (μ.j₁ T) + μ.r₁ L) := by
672 rintro ⟨side_glued, rfl, same⟩
673 -- the cut edge lies inside the sibling's side `j₁`
674 have r₁_le := move_ok.r₁_le
675 -- the two glued sides have the same length
676 have same_len := move_ok.L₁ side_glued
677 exact side_hit (Or.inr ⟨side_glued, rfl,
678 move_ok.side_unique c_lt j_lt (move_ok.sib side_glued).2.1 o_lt (by omega) same⟩)
679 rw [move_ok.smate_old not_cut₀ not_cut₁]
680 show _ = ((Comp.ofLens T L d ω).mate c (pos (L c) j + o)).map _
681 rw [ofLens_mate move_ok.pos_len c_lt j_lt o_lt]
682 cases glued : adjAt T c j with
683 | none => rfl
684 | some p =>
685 obtain ⟨c', j'⟩ := p
686 obtain ⟨c'_lt, j'_lt, _, _⟩ := adj_valid c_lt j_lt glued
687 -- the partner side is not lengthened either
688 have partner_not_hit := move_ok.not_hit_partner c_lt j_lt glued side_hit
689 -- and it has the same length
690 have same_len := move_ok.pair c c_lt j j_lt c' j' glued
691 simp only [Option.map_some]
692 rw [unchanged c' j' partner_not_hit,
693 show pos (L c') j' + L c' j' - 1 - o = pos (L c') j' + (L c' j' - 1 - o) by omega,
694 move_ok.sh_side c'_lt j'_lt (by omega) partner_not_hit]
695 congr 2; omega
In the paper Lemma 7.1 Lengthening
697/-- **Lengthening is subdividing**: the composition with the lengthened sides is equivalent to the old one with the
698edge cut. -/
699theorem equiv : Gluing.Equiv (G₁) (Gs) where
700 n := by rw [ofLens_n]; show nk T = (Comp.ofLens T L d ω).toGluing.n; rw [ofLens_n]
701 E c c_lt := move_ok.E_eq (by rwa [ofLens_n] at c_lt)
702 A c c_lt := move_ok.A_eq (by rwa [ofLens_n] at c_lt)
703 B c c_lt := move_ok.B_eq (by rwa [ofLens_n] at c_lt)
704 mate c k c_lt k_lt := move_ok.mate_eq (by rwa [ofLens_n] at c_lt) k_lt
706end OK
708end Move
710end SpectreKnot.Compose

← SpectreKnot/Lens.leanSpectreKnot/Signature.lean →