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

lean/SpectreKnot/StepMap.lean

615 lines · 31 declarations, each with its own page · on GitHub ·

The junction map of the nest (the paper's Computation 9.2 and Lemma 9.3), one level at a time. In the Δ composition, child 1 is the previous block of the nest. Every arc of child 1 lies on a parent hook at a junction, the vertex where piece q of Table 3 starts, and q depends only on where the arc is on child 1's rim and on the sign ω (tgt); the arcs on child 1's side 2, which lies on the parent's rim, are parent hooks themselves. StepOK states this; it is checked by the kernel at the level-1 lengths (step_base, Computation 9.2), is kept by the moves of Lemma 7.2(b) (StepOK.move), and so holds at every level (step_level, by adm_induct, as in the paper).

← SpectreKnot/NewWalk.leanSpectreKnot/Linked.lean →

All 39 files, and the declarations of this one
1/-
2**The junction map of the nest** (the paper's Computation 9.2 and Lemma 9.3), one level at a time. In the Δ
3composition, child 1 is the previous block of the nest. Every arc of child 1 lies on a parent hook at a *junction*, the
4vertex where piece `q` of Table 3 starts, and `q` depends only on where the arc is on child 1's rim and on the sign `ω`
5(`tgt`); the arcs on child 1's side 2, which lies on the parent's rim, are parent hooks themselves. `StepOK` states
6this; it is checked by the kernel at the level-1 lengths (`step_base`, Computation 9.2), is kept by the moves of
7Lemma 7.2(b) (`StepOK.move`), and so holds at every level (`step_level`, by `adm_induct`, as in the paper).
8-/
12namespace SpectreKnot.Statement
14open Pattern Compose Gluing
16/-! ### The map -/
18/-- Piece `q` of the Δ-supertile's rim (Table 3, flattened). -/
19abbrev pieceD (q : Nat) : Nat × Nat := (pcs .Delta).getD q (0, 0)
21/-- The port `R` of the parent hook at the start of piece `q`, as a port of the composition: the child vertex where
22piece `q`'s side ends, in the children's sense (port `L` there). -/
23def jR (L : Nat → Nat → Nat) (q : Nat) : GPort :=
24 ((pieceD q).1, pos (L (pieceD q).1) (((pieceD q).2 + 1) % 6), false)
26/-- The port `L` of the same parent hook: the child vertex where piece `q - 1`'s side begins (port `R` there). -/
27def jL (L : Nat → Nat → Nat) (q : Nat) : GPort :=
28 ((pieceD (q - 1)).1, pos (L (pieceD (q - 1)).1) (pieceD (q - 1)).2, true)
30/-- Where an arc of child 1 goes: the junction (a piece number) of the parent hook it lies on, for the port `s` at
31rim vertex `u` of child 1 (side lengths `f`); `none` for a vertex inside side 2 (a parent hook itself). Child 1's
32corners are `A = 0` and `B = 1` (`ω`) or `B = E - 1` (not `ω`); their arcs are the crossover arcs. -/
33def tgt (ω : Bool) (f : Nat → Nat) (u : Nat) (s : Bool) : Option Nat :=
34 if ω then
35 if u = 0 ∨ u = 1 then some (if s then 17 else 9)
36 else if u ≤ pos f 2 then some 17 else if u < pos f 3 then none else if u < pos f 4 then some 16
37 else if u < pos f 5 then some 12 else some 9
38 else
39 if u = 0 ∨ u = pos f 6 - 1 then some (if s then 21 else 16)
40 else if u ≤ pos f 1 then some 21 else if u ≤ pos f 2 then some 17 else if u < pos f 3 then none else some 16
42/-- The junction for a vertex well inside side `j` of child 1. -/
43def sideTgt (ω : Bool) (j : Nat) : Option Nat :=
44 if ω then (if j ≤ 1 then some 17 else if j = 2 then none else if j = 3 then some 16 else if j = 4 then some 12
45 else some 9)
46 else (if j = 0 then some 21 else if j = 1 then some 17 else if j = 2 then none else some 16)
48/-- **The junction map holds**: the walk from every port of child 1 (outside side 2) ends at a port of the parent hook
49at the junction `tgt` names. -/
50def StepOK (L : Nat → Nat → Nat) (d : Nat) (ω : Bool) : Prop :=
51 ∀ u, u < pos (L 1) 6 → ∀ s q, tgt ω (L 1) u s = some q →
52 ∃ r, (Comp.ofLens .Delta L d ω).toGluing.FullReach (1, u, s) r ∧ (r = jR L q ∨ r = jL L q)
54/-- Well inside side `j`, the map depends only on `j`: at a vertex `u` at least two edges from both ends of side `j`
55of child 1 (side lengths `f`), `tgt` is `sideTgt ω j`, for either port `s`. -/
56theorem tgt_side {ω : Bool} {f : Nat → Nat} {j u : Nat} (s : Bool) (hj : j < 6) (after_start : pos f j + 2 ≤ u)
57 (before_end : u + 2 ≤ pos f (j + 1)) : tgt ω f u s = sideTgt ω j := by
58 -- the sides start in order round the rim
59 have mono : ∀ a b, a ≤ b → pos f a ≤ pos f b := fun a b a_le_b => pos_mono f a_le_b
60 -- side 0 starts at vertex 0
61 have p0 : pos f 0 = 0 := rfl
62 -- side `j` ends before the rim does
63 have end_le := mono (j + 1) 6 (by omega)
64 -- the starts of sides 1 to 5, in order
65 have order : pos f 1 ≤ pos f 2 ∧ pos f 2 ≤ pos f 3 ∧ pos f 3 ≤ pos f 4 ∧ pos f 4 ≤ pos f 5 :=
66 ⟨mono 1 2 (by omega), mono 2 3 (by omega), mono 3 4 (by omega), mono 4 5 (by omega)⟩
67 rcases (show j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3 ∨ j = 4 ∨ j = 5 by omega) with rfl | rfl | rfl | rfl | rfl | rfl
68 · have before_end : u + 2 ≤ pos f 1 := before_end -- side 0 ends where side 1 starts
69 cases ω <;> simp only [tgt, sideTgt, Bool.false_eq_true, ite_false, ite_true] <;>
70 rw [ite_eq_right (by omega), ite_eq_left (by omega)] <;> simp
71 · have before_end : u + 2 ≤ pos f 2 := before_end -- side 1 ends where side 2 starts
72 cases ω <;> simp only [tgt, sideTgt, Bool.false_eq_true, ite_false, ite_true]
73 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_left (by omega)]; simp
74 · rw [ite_eq_right (by omega), ite_eq_left (by omega)]; simp
75 · have before_end : u + 2 ≤ pos f 3 := before_end -- side 2 ends where side 3 starts
76 cases ω <;> simp only [tgt, sideTgt, Bool.false_eq_true, ite_false, ite_true]
77 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_left (by omega)]; simp
78 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_left (by omega)]; simp
79 · have before_end : u + 2 ≤ pos f 4 := before_end -- side 3 ends where side 4 starts
80 cases ω <;> simp only [tgt, sideTgt, Bool.false_eq_true, ite_false, ite_true]
81 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega)]; simp
82 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_left (by omega)]; simp
83 · have before_end : u + 2 ≤ pos f 5 := before_end -- side 4 ends where side 5 starts
84 cases ω <;> simp only [tgt, sideTgt, Bool.false_eq_true, ite_false, ite_true]
85 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega)]; simp
86 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega),
87 ite_eq_left (by omega)]; simp
88 · have before_end : u + 2 ≤ pos f 6 := before_end -- side 5 ends where the rim ends
89 cases ω <;> simp only [tgt, sideTgt, Bool.false_eq_true, ite_false, ite_true]
90 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega)]; simp
91 · rw [ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega), ite_eq_right (by omega),
92 ite_eq_right (by omega)]; simp
94/-! ### The base case: the kernel's check at the level-1 lengths -/
96/-- The checks of `StepOK` at `(ℓ₁, d₁)`. -/
97def stepCheck (ω : Bool) : Bool :=
98 let C := Comp.ofLens .Delta (L₁ .Delta) (dOff 1) ω
99 (List.range (pos (L₁ .Delta 1) 6)).all fun u => [true, false].all fun s =>
100 match tgt ω (L₁ .Delta 1) u s with
101 | none => true
102 | some q =>
103 C.toGluing.fullWalk C.fuel (1, u, s) == some (jR (L₁ .Delta) q) ||
104 C.toGluing.fullWalk C.fuel (1, u, s) == some (jL (L₁ .Delta) q)
106/-- The kernel's check passes at the level-1 lengths for `ω = true`. -/
107theorem stepCheck_true : stepCheck true = true := by decide +kernel
108/-- The kernel's check passes at the level-1 lengths for `ω = false`. -/
109theorem stepCheck_false : stepCheck false = true := by decide +kernel
111/-- The check is sound: if it passes, the junction map holds at `(ℓ₁, d₁)`. -/
112theorem stepCheck_sound {ω : Bool} (check : stepCheck ω = true) : StepOK (L₁ .Delta) (dOff 1) ω := by
113 intro u hu s q tgt_eq
114 simp only [stepCheck, List.all_eq_true, List.mem_range] at check
115 -- the check at vertex `u` and port `s`
116 have at_port := check u hu s (by cases s <;> simp)
117 rw [tgt_eq] at at_port
118 simp only [Bool.or_eq_true, beq_iff_eq] at at_port
119 rcases at_port with walk_R | walk_L
120 · exact ⟨_, fullWalk_sound _ walk_R, Or.inl rfl⟩
121 · exact ⟨_, fullWalk_sound _ walk_L, Or.inr rfl⟩
In the paper Computation 9.2 The junction map at the level-1 lengths
123/-- **The base case**: the junction map holds at the level-1 lengths `(ℓ₁, d₁)`, for both signs. -/
124theorem step_base (ω : Bool) : StepOK (L₁ .Delta) (dOff 1) ω := by
125 cases ω
129end SpectreKnot.Statement
131/-! ### Positions under a move -/
133namespace SpectreKnot.Gluing.Cut.OK
135-- `ok`: the cut `κ` can be made in `G`
136variable {G : Gluing} {κ : Cut} (ok : κ.OK G)
138include ok
140/-- A cut keeps the order of positions on a child's rim. -/
141theorem sh_lt_sh {c u v : Nat} (u_lt_v : u < v) : κ.sh c u < κ.sh c v := by
142 rcases ok.sh_cases c u with ⟨u_stays, u_before₀, u_before₁⟩ | ⟨u_moves, u_after⟩ <;>
143 rcases ok.sh_cases c v with ⟨v_stays, v_before₀, v_before₁⟩ | ⟨v_moves, v_after⟩
144 · omega
145 · omega
146 · -- `u` moves on, so it lies after the cut; then so does `v`, which cannot stay
147 rcases u_after with ⟨on_c₀, past_e₀⟩ | ⟨shared, on_c₁, past_e₁⟩
148 · have := v_before₀ on_c₀ -- `v` stays, so it is not past the cut on `c₀`
149 omega
150 · have := v_before₁ ⟨shared, on_c₁⟩ -- `v` stays, so it is not past the cut on `c₁`
151 omega
152 · omega
154/-- A cut keeps strict order both ways. -/
155theorem sh_lt_iff {c u v : Nat} : κ.sh c u < κ.sh c v ↔ u < v := by
156 constructor
157 · intro sh_lt
158 rcases Nat.lt_or_ge u v with u_lt_v | v_le_u
159 · exact u_lt_v
160 · rcases Nat.eq_or_lt_of_le v_le_u with same | v_lt_u
161 · subst same; omega
162 · have := ok.sh_lt_sh (c := c) v_lt_u -- `v < u` would put the moved positions the other way round
163 omega
164 · exact ok.sh_lt_sh
166end SpectreKnot.Gluing.Cut.OK
168namespace SpectreKnot.Compose.Move.OK
170open Gluing Pattern
172set_option linter.unusedSectionVars false
174-- `ok`: the move `μ` can be made at `(L, d)`
175variable {T : Kind} {μ : Move} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool} (ok : μ.OK T L d ω)
177include ok
179/-- The vertices of the children stay put under a move: the cut takes the start of side `v` of child `c` to the
180start of side `v` with the new lengths. -/
181theorem shpos {c v : Nat} (hc : c < nk T) (hv : v ≤ 6) :
182 (μ.cut T L).sh c (pos (L c) v) = pos (μ.lens T L c) v := by
183 -- the cut edge is not the last edge of side `j₀`
184 have cut_before_end := ok.r₀'
185 -- nor its first
186 have cut_after_start := ok.r₀
187 -- `j₀` is a side
188 have j₀_lt := ok.j₀
189 by_cases on_c₀ : c = μ.c₀
190 · subst on_c₀
191 rw [ok.pos_c₀]
192 by_cases after_j₀ : μ.j₀ < v
193 · -- side `v` starts after the cut:
194 -- side `j₀` ends no later than side `v` starts
195 have j₀_end_le := pos_mono (L μ.c₀) (show μ.j₀ + 1 ≤ v by omega)
196 rw [pos_succ] at j₀_end_le
197 rw [ite_eq_left after_j₀, ok.sh₀_gt (by omega)]
198 · -- side `v` starts before the cut:
199 -- side `v` starts no later than side `j₀`
200 have := pos_mono (L μ.c₀) (show v ≤ μ.j₀ by omega)
201 rw [ite_eq_right after_j₀, ok.sh₀_le (by omega), Nat.add_zero]
202 · by_cases on_c₁ : μ.two T = true ∧ c = μ.c₁ T
203 · obtain ⟨shared, rfl⟩ := on_c₁
204 -- the sibling's side `j₁` is as long as side `j₀`
205 have same_len := ok.L₁ shared
206 -- and `j₁` is a side
207 have j₁_lt := (ok.sib shared).2.1
208 rw [ok.pos_c₁ shared]
209 by_cases after_j₁ : μ.j₁ T < v
210 · -- side `v` starts after the cut:
211 -- side `j₁` ends no later than side `v` starts
212 have j₁_end_le := pos_mono (L (μ.c₁ T)) (show μ.j₁ T + 1 ≤ v by omega)
213 rw [pos_succ] at j₁_end_le
214 rw [ite_eq_left after_j₁, ok.sh₁_gt shared (by simp only [Move.r₁]; omega)]
215 · -- side `v` starts before the cut:
216 -- side `v` starts no later than side `j₁`
217 have := pos_mono (L (μ.c₁ T)) (show v ≤ μ.j₁ T by omega)
218 rw [ite_eq_right after_j₁, ok.sh₁_le shared (by simp only [Move.r₁]; omega), Nat.add_zero]
219 · rw [ok.sh_oth on_c₀ on_c₁, ok.pos_other on_c₀ on_c₁]
221/-- Vertex 1 stays put (the cut edge is never the first edge of a child). -/
222theorem sh_one (c : Nat) : (μ.cut T L).sh c 1 = 1 := by
223 -- the cut edge is not the first edge of its side
224 have cut_after_start := ok.r₀
225 -- nor its last
226 have cut_before_end := ok.r₀'
227 unfold Cut.sh
228 rw [ite_eq_right (by simp only [Move.cut]; omega), ite_eq_right (by simp only [Move.cut, Move.r₁]; omega)]
230/-- The last vertex of a child moves with the end of its rim. -/
231theorem sh_last {c : Nat} (hc : c < nk T) :
232 (μ.cut T L).sh c (pos (L c) 6 - 1) = pos (μ.lens T L c) 6 - 1 := by
233 -- the last side has an edge, after the move
234 have last_pos := ok.lens_pos_len c hc 5 (by omega)
235 -- and before
236 have last_pos' := ok.pos_len c hc 5 (by omega)
237 -- so the rim has an edge
238 have rim_pos : 1 ≤ pos (L c) 6 := by rw [pos_succ]; omega
239 -- the end of the rim moves to the new end
240 have rim_end := ok.shpos hc (show 6 ≤ 6 by omega)
241 rcases ok.cutOK.sh_cases c (pos (L c) 6 - 1) with ⟨last_stays, last_before₀, last_before₁⟩ | ⟨last_moves, last_after⟩
242 · rcases ok.cutOK.sh_cases c (pos (L c) 6) with ⟨end_stays, _, _⟩ | ⟨end_moves, end_after⟩
243 · rw [last_stays]; rw [end_stays] at rim_end; omega
244 · -- the end moves on but the last vertex does not: then the cut edge would be the last edge
245 rcases end_after with ⟨on_c₀, past_e₀⟩ | ⟨shared, on_c₁, past_e₁⟩
246 · have last_le := last_before₀ on_c₀ -- the last vertex is not past the cut
247 -- the cut edge is not the last edge of `c₀`
248 have cut_lt := ok.cutOK.e₀
249 rw [← on_c₀, ofLens_E hc] at cut_lt
250 omega
251 · have last_le := last_before₁ ⟨shared, on_c₁⟩ -- the last vertex is not past the cut
252 -- the cut edge is not the last edge of `c₁`
253 have cut_lt := ok.cutOK.e₁ shared
254 rw [← on_c₁, ofLens_E hc] at cut_lt
255 omega
256 · rcases ok.cutOK.sh_cases c (pos (L c) 6) with ⟨end_stays, end_before₀, end_before₁⟩ | ⟨end_moves, _⟩
257 · -- the last vertex moves on but the end does not: impossible, the end comes after it
258 rcases last_after with ⟨on_c₀, past_e₀⟩ | ⟨shared, on_c₁, past_e₁⟩
259 · have := end_before₀ on_c₀ -- the end is not past the cut on `c₀`
260 omega
261 · have := end_before₁ ⟨shared, on_c₁⟩ -- the end is not past the cut on `c₁`
262 omega
263 · rw [last_moves]; rw [end_moves] at rim_end; omega
265end SpectreKnot.Compose.Move.OK
267namespace SpectreKnot.Statement
269open Pattern Compose Gluing
271/-! ### The map under a move -/
273/-- The junctions the map names are pieces `1 … 21`. -/
274theorem tgt_lt {ω : Bool} {f : Nat → Nat} {u : Nat} {s : Bool} {q : Nat} (tgt_eq : tgt ω f u s = some q) :
275 1 ≤ q ∧ q < 22 := by
276 unfold tgt at tgt_eq
277 revert tgt_eq
278 cases ω <;> cases s <;> simp only [Bool.false_eq_true, ite_false, ite_true] <;> (repeat' split) <;> intro tgt_eq <;>
279 simp only [Option.some.injEq, reduceCtorEq] at tgt_eq <;> omega
281/-- Each of the Δ supertile's 22 rim pieces is a side of an actual child. -/
282theorem piece_ok : ∀ q, q < 22 → (pieceD q).1 < nk .Delta ∧ (pieceD q).2 < 6 := by decide
284/-- Child 1 of Δ has only one side on the parent's rim: side 2. -/
285theorem adj_one_none : ∀ j, j < 6 → adjAt .Delta 1 j = none → j = 2 := by decide
287/-- Child 1's corners are `0` and `1` or `E - 1`: a vertex `x` with `2 ≤ x ≤ E - 2` is not a corner. -/
288theorem corner_one {L : Nat → Nat → Nat} {d : Nat} {ω : Bool} {x : Nat} (two_le_x : 2 ≤ x)
289 (x_le : x + 2 ≤ pos (L 1) 6) : (Comp.ofLens .Delta L d ω).toGluing.corner 1 x = false := by
290 -- child 1 is an actual child
291 have one_lt : 1 < nk .Delta := by decide
292 simp only [Gluing.corner, Bool.or_eq_false_iff, beq_eq_false_iff_ne, ne_eq]
293 rw [ofLens_B one_lt, ofLens_A one_lt, ite_eq_right (by decide)]
294 cases ω <;> simp only [ite_true, ite_false, Bool.false_eq_true, nxt, prv] <;> constructor <;> (try split) <;> omega
296/-- The map, read through a renumbering `φ` of child 1's rim that keeps the order, the first two vertices, the last
297vertex and the six corners (from side lengths `f` to `f'`). -/
298theorem tgt_map {ω : Bool} {f f' φ : Nat → Nat} (keeps_lt : ∀ a b, φ a < φ b ↔ a < b) (fixes_zero : φ 0 = 0)
299 (fixes_one : φ 1 = 1) (maps_last : φ (pos f 6 - 1) = pos f' 6 - 1)
300 (maps_corners : ∀ k, k ≤ 6 → φ (pos f k) = pos f' k) (u : Nat) (s : Bool) :
301 tgt ω f' (φ u) s = tgt ω f u s := by
302 -- `φ` is one to one
303 have keeps_eq : ∀ a b, φ a = φ b ↔ a = b := fun a b => by
304 constructor
305 · intro same
306 rcases Nat.lt_trichotomy a b with a_lt_b | a_eq_b | b_lt_a
307 · have := (keeps_lt a b).mpr a_lt_b -- `φ` keeps the strict order
308 omega
309 · exact a_eq_b
310 · have := (keeps_lt b a).mpr b_lt_a -- `φ` keeps the strict order
311 omega
312 · intro same; rw [same]
313 -- `φ` keeps `≤`
314 have keeps_le : ∀ a b, φ a ≤ φ b ↔ a ≤ b := fun a b => by
315 rw [← Nat.not_lt, ← Nat.not_lt, keeps_lt]
316 -- each test in `tgt` gives the same answer after the renumbering: the test `u = 0`
317 have is_zero : (φ u = 0) = (u = 0) := propext (by
318 -- `φ u = φ 0` exactly when `u = 0`
319 have at_zero := keeps_eq u 0
320 rwa [fixes_zero] at at_zero)
321 -- the test `u = 1`
322 have is_one : (φ u = 1) = (u = 1) := propext (by
323 -- `φ u = φ 1` exactly when `u = 1`
324 have at_one := keeps_eq u 1
325 rwa [fixes_one] at at_one)
326 -- the test for the last vertex
327 have is_last : (φ u = pos f' 6 - 1) = (u = pos f 6 - 1) := propext (by
328 -- `φ u` is the last vertex exactly when `u` is
329 have at_last := keeps_eq u (pos f 6 - 1)
330 rwa [maps_last] at at_last)
331 -- the tests `u ≤` a corner
332 have le_corner : ∀ k, k ≤ 6 → (φ u ≤ pos f' k) = (u ≤ pos f k) := fun k hk =>
333 propext (by
334 -- `φ u` is at most corner `k` exactly when `u` is
335 have at_corner := keeps_le u (pos f k)
336 rwa [maps_corners k hk] at at_corner)
337 -- the tests `u <` a corner
338 have lt_corner : ∀ k, k ≤ 6 → (φ u < pos f' k) = (u < pos f k) := fun k hk =>
339 propext (by
340 -- `φ u` is before corner `k` exactly when `u` is
341 have at_corner := keeps_lt u (pos f k)
342 rwa [maps_corners k hk] at at_corner)
343 simp only [tgt, is_zero, is_one, is_last, le_corner 1 (by omega), le_corner 2 (by omega), lt_corner 3 (by omega),
344 lt_corner 4 (by omega), lt_corner 5 (by omega)]
346section
347-- `ok`: the move `μ` can be made in the Δ composition at `(L, d)`
348variable {L : Nat → Nat → Nat} {d : Nat} {ω : Bool} {μ : Move} (ok : μ.OK .Delta L d ω)
349include ok
351set_option quotPrecheck false
352local notation "G₀" => (Comp.ofLens .Delta L d ω).toGluing
353local notation "G₁" => (Comp.ofLens .Delta (μ.lens .Delta L) (μ.d' .Delta L d) ω).toGluing
354local notation "Gs" => subdiv (Comp.ofLens .Delta L d ω).toGluing (μ.cut .Delta L)
355local notation "κ" => μ.cut .Delta L
358/-- A move takes port `R` of the hook at junction `q` (as `jR` reads it) to the same port with the new lengths. -/
359theorem port_jR {q : Nat} (hq : q < 22) : (κ).port (jR L q) = jR (μ.lens .Delta L) q := by
360 -- piece `q` is a side of an actual child
361 obtain ⟨child_lt, _⟩ := piece_ok q hq
362 show ((pieceD q).1, (κ).sh (pieceD q).1 (pos (L (pieceD q).1) (((pieceD q).2 + 1) % 6)), false) = _
363 rw [ok.shpos child_lt (by omega)]; rfl
365/-- A move takes port `L` of the hook at junction `q` (as `jL` reads it) to the same port with the new lengths. -/
366theorem port_jL {q : Nat} (q_pos : 1 ≤ q) (hq : q < 22) : (κ).port (jL L q) = jL (μ.lens .Delta L) q := by
367 -- piece `q - 1` is a side of an actual child
368 obtain ⟨child_lt, side_lt⟩ := piece_ok (q - 1) (by omega)
369 show ((pieceD (q - 1)).1, (κ).sh (pieceD (q - 1)).1 (pos (L (pieceD (q - 1)).1) (pieceD (q - 1)).2), true) = _
370 rw [ok.shpos child_lt (by omega)]; rfl
372/-- Vertex 0 of child 1 stays put under a move. -/
373theorem sh_zero : (κ).sh 1 0 = 0 := by
374 rcases ok.cutOK.sh_cases 1 0 with ⟨stays, _⟩ | ⟨_, after_cut⟩
375 · exact stays
376 · rcases after_cut with ⟨_, past_cut⟩ | ⟨_, _, past_cut⟩ <;> omega
In the paper Lemma 9.3 The junction map
378/-- **The map survives a move** whose cut, if on child 1, is at least two edges from either end of its side. -/
379theorem StepOK.move (clear₀ : μ.c₀ = 1 → 2 ≤ μ.r₀ ∧ μ.r₀ + 3 ≤ L 1 μ.j₀)
380 (clear₁ : μ.two .Delta = true → μ.c₁ .Delta = 1 → 2 ≤ μ.r₁ L ∧ μ.r₁ L + 3 ≤ L 1 (μ.j₁ .Delta))
381 (old_map : StepOK L d ω) : StepOK (μ.lens .Delta L) (μ.d' .Delta L d) ω := by
382 intro u' hu' s q tgt_eq
383 -- the cut can be made
384 have cut_ok := ok.cutOK
385 -- and the cut gluing is well formed
386 have wf_cut := cut_ok.wf_subdiv
387 -- child 1 is an actual child
388 have one_lt : 1 < nk .Delta := by decide
389 -- child 1's rim, before the move
390 have rim_old : (G₀).E 1 = pos (L 1) 6 := ofLens_E one_lt
391 -- and after the cut
392 have rim_cut : (Gs).E 1 = pos (μ.lens .Delta L 1) 6 := by rw [← ok.E_eq one_lt, ofLens_E one_lt]
393 -- the junction is one of the pieces `1 … 21`
394 obtain ⟨q_pos, q_lt⟩ := tgt_lt tgt_eq
395 -- the end: from the subdivided gluing to the new composition
396 have to_new : ∀ r, (Gs).FullReach (1, u', s) ((κ).port r) → (r = jR L q ∨ r = jL L q) →
397 ∃ r', (G₁).FullReach (1, u', s) r' ∧ (r' = jR (μ.lens .Delta L) q ∨ r' = jL (μ.lens .Delta L) q) := by
398 intro r cut_walk at_junction
399 refine ⟨_, ok.equiv.symm.fullReach wf_cut ⟨?_, ?_⟩ cut_walk, ?_⟩
400 · show 1 < (G₀).n
401 rw [ofLens_n]; exact one_lt
402 · show u' < (Gs).E 1
403 rw [rim_cut]; exact hu'
404 · rcases at_junction with rfl | rfl
405 · exact Or.inl (port_jR ok q_lt)
406 · exact Or.inr (port_jL ok q_pos q_lt)
407 by_cases new₀ : 1 = (κ).c₀ ∧ (κ).e₀ < u' ∧ u' ≤ (κ).e₀ + 2
408 · -- a new vertex of child `c₀ = 1`
409 obtain ⟨is_c₀, after_cut, within_cut⟩ := new₀
410 -- the move is on child 1
411 have μ_c₀ : μ.c₀ = 1 := is_c₀.symm
412 -- and so is the cut
413 have κ_c₀ : (κ).c₀ = 1 := is_c₀.symm
414 -- the cut is two edges clear of both ends of side `j₀`
415 obtain ⟨clear_start, clear_end⟩ := clear₀ μ_c₀
416 -- `j₀` is a side
417 have j₀_lt := ok.j₀
418 -- side `j₀` starts where it did
419 have start_j₀ := ok.pos_c₀ μ.j₀
420 -- and ends two edges later
421 have end_j₀ := ok.pos_c₀ (μ.j₀ + 1)
422 rw [μ_c₀] at start_j₀ end_j₀
423 rw [ite_eq_right (by omega)] at start_j₀
424 rw [ite_eq_left (by omega)] at end_j₀
425 -- side `j₀` has `L 1 j₀` edges
426 have side_len := pos_succ (L 1) μ.j₀
427 -- and lies within the rim
428 have side_in_rim := pos_mono (L 1) (show μ.j₀ + 1 ≤ 6 by omega)
429 -- where the cut edge is
430 have cut_at : (κ).e₀ = pos (L 1) μ.j₀ + μ.r₀ := by show pos (L μ.c₀) μ.j₀ + μ.r₀ = _; rw [μ_c₀]
431 -- the new vertex is well inside side `j₀`
432 rw [tgt_side s j₀_lt (by omega) (by omega)] at tgt_eq
433 cases glued : μ.two .Delta
434 · -- a rim side: it is side 2, where the map is not defined
435 -- the only rim side of child 1 is side 2
436 have side_two : μ.j₀ = 2 := by
437 apply adj_one_none _ j₀_lt
438 -- side `j₀` of child 1 has no sibling
439 have no_sib : (adjAt .Delta μ.c₀ μ.j₀).isSome = false := glued
440 rw [μ_c₀] at no_sib
441 cases adj : adjAt .Delta 1 μ.j₀ with
442 | none => rfl
443 | some _ => rw [adj] at no_sib; contradiction
444 rw [side_two] at tgt_eq; simp [sideTgt] at tgt_eq
445 · have cut_shared : (κ).two = true := glued -- the cut edge is shared with a sibling
446 -- the old vertices next to the cut lie well inside side `j₀` too, with the same junction
447 have old_tgt : ∀ x, x = (κ).e₀ ∨ x = (κ).e₀ + 1 → tgt ω (L 1) x s = some q := by
448 intro x next_to_cut
449 rw [tgt_side s j₀_lt (by omega) (by omega)]; exact tgt_eq
450 rcases (show u' = (κ).e₀ + 1 ∨ u' = (κ).e₀ + 2 by omega) with rfl | rfl
451 · -- new vertex `e₀ + 1` follows the old `e₀ + 1`
452 obtain ⟨r, old_walk, at_junction⟩ := old_map _ (by omega) s q (old_tgt _ (Or.inr rfl))
453 refine to_new r ?_ at_junction
454 cases s
455 · -- port `L`
456 -- in the cut gluing, the walk from the new vertex ends where the old walk did
457 have new_walk := cut_ok.nw0_1F cut_shared (r := r) (by rw [κ_c₀]; exact old_walk)
458 rw [κ_c₀] at new_walk; exact new_walk
459 · -- port `R`
460 -- in the cut gluing, the walk from the new vertex ends where the old walk did
461 have new_walk := cut_ok.nw0_1T cut_shared (by rw [κ_c₀]; exact corner_one (by omega) (by omega)) (r := r)
462 (by rw [κ_c₀]; exact old_walk)
463 rw [κ_c₀] at new_walk; exact new_walk
464 · -- new vertex `e₀ + 2` follows the old `e₀`
465 obtain ⟨r, old_walk, at_junction⟩ := old_map _ (by omega) s q (old_tgt _ (Or.inl rfl))
466 refine to_new r ?_ at_junction
467 cases s
468 · -- port `L`
469 -- in the cut gluing, the walk from the new vertex ends where the old walk did
470 have new_walk := cut_ok.nw0_2F cut_shared (by rw [κ_c₀]; exact corner_one (by omega) (by omega)) (r := r)
471 (by rw [κ_c₀]; exact old_walk)
472 rw [κ_c₀] at new_walk; exact new_walk
473 · -- port `R`
474 -- in the cut gluing, the walk from the new vertex ends where the old walk did
475 have new_walk := cut_ok.nw0_2T cut_shared (r := r) (by rw [κ_c₀]; exact old_walk)
476 rw [κ_c₀] at new_walk; exact new_walk
477 · by_cases new₁ : (κ).two = true ∧ 1 = (κ).c₁ ∧ (κ).e₁ < u' ∧ u' ≤ (κ).e₁ + 2
478 · -- a new vertex of child `c₁ = 1`
479 obtain ⟨cut_shared, is_c₁, after_cut, within_cut⟩ := new₁
480 -- the side cut is glued to a sibling
481 have shared : μ.two .Delta = true := cut_shared
482 -- the sibling is child 1
483 have μ_c₁ : μ.c₁ .Delta = 1 := is_c₁.symm
484 -- and so is the cut's second child
485 have κ_c₁ : (κ).c₁ = 1 := is_c₁.symm
486 -- the cut is two edges clear of both ends of side `j₁`
487 obtain ⟨clear_start, clear_end⟩ := clear₁ shared μ_c₁
488 -- `j₁` is a side
489 have j₁_lt := (ok.sib shared).2.1
490 -- side `j₁` is as long as side `j₀`
491 have same_len := ok.L₁ shared
492 -- the cut edge is not the last edge of side `j₁`
493 have r₁_le := ok.r₁_le
494 -- side `j₁` starts where it did
495 have start_j₁ := ok.pos_c₁ shared (μ.j₁ .Delta)
496 -- and ends two edges later
497 have end_j₁ := ok.pos_c₁ shared (μ.j₁ .Delta + 1)
498 rw [μ_c₁] at start_j₁ end_j₁ same_len
499 rw [ite_eq_right (by omega)] at start_j₁
500 rw [ite_eq_left (by omega)] at end_j₁
501 -- side `j₁` has `L 1 j₁` edges
502 have side_len := pos_succ (L 1) (μ.j₁ .Delta)
503 -- and lies within the rim
504 have side_in_rim := pos_mono (L 1) (show μ.j₁ .Delta + 1 ≤ 6 by omega)
505 -- where the cut edge is
506 have cut_at : (κ).e₁ = pos (L 1) (μ.j₁ .Delta) + μ.r₁ L := by
507 show pos (L (μ.c₁ .Delta)) (μ.j₁ .Delta) + μ.r₁ L = _; rw [μ_c₁]
508 -- the new vertex is well inside side `j₁`
509 rw [tgt_side s j₁_lt (by omega) (by omega)] at tgt_eq
510 -- the old vertices next to the cut lie well inside side `j₁` too, with the same junction
511 have old_tgt : ∀ x, x = (κ).e₁ ∨ x = (κ).e₁ + 1 → tgt ω (L 1) x s = some q := by
512 intro x next_to_cut
513 rw [tgt_side s j₁_lt (by omega) (by omega)]; exact tgt_eq
514 rcases (show u' = (κ).e₁ + 1 ∨ u' = (κ).e₁ + 2 by omega) with rfl | rfl
515 · -- new vertex `e₁ + 1` follows the old `e₁ + 1`
516 obtain ⟨r, old_walk, at_junction⟩ := old_map _ (by omega) s q (old_tgt _ (Or.inr rfl))
517 refine to_new r ?_ at_junction
518 cases s
519 · -- port `L`
520 -- in the cut gluing, the walk from the new vertex ends where the old walk did
521 have new_walk := cut_ok.nw1_1F cut_shared (r := r) (by rw [κ_c₁]; exact old_walk)
522 rw [κ_c₁] at new_walk; exact new_walk
523 · -- port `R`
524 -- in the cut gluing, the walk from the new vertex ends where the old walk did
525 have new_walk := cut_ok.nw1_1T cut_shared (by rw [κ_c₁]; exact corner_one (by omega) (by omega)) (r := r)
526 (by rw [κ_c₁]; exact old_walk)
527 rw [κ_c₁] at new_walk; exact new_walk
528 · -- new vertex `e₁ + 2` follows the old `e₁`
529 obtain ⟨r, old_walk, at_junction⟩ := old_map _ (by omega) s q (old_tgt _ (Or.inl rfl))
530 refine to_new r ?_ at_junction
531 cases s
532 · -- port `L`
533 -- in the cut gluing, the walk from the new vertex ends where the old walk did
534 have new_walk := cut_ok.nw1_2F cut_shared (by rw [κ_c₁]; exact corner_one (by omega) (by omega)) (r := r)
535 (by rw [κ_c₁]; exact old_walk)
536 rw [κ_c₁] at new_walk; exact new_walk
537 · -- port `R`
538 -- in the cut gluing, the walk from the new vertex ends where the old walk did
539 have new_walk := cut_ok.nw1_2T cut_shared (r := r) (by rw [κ_c₁]; exact old_walk)
540 rw [κ_c₁] at new_walk; exact new_walk
541 · -- an old vertex
542 obtain ⟨u, hu, rfl⟩ := cut_ok.preimage (c := 1) (by rw [rim_cut]; exact hu') new₀ new₁
543 rw [tgt_map (fun a b => cut_ok.sh_lt_iff) (sh_zero ok) (ok.sh_one 1) (ok.sh_last one_lt)
544 (fun k hk => ok.shpos one_lt hk)] at tgt_eq
545 obtain ⟨r, old_walk, at_junction⟩ := old_map u (by rw [← rim_old]; exact hu) s q tgt_eq
546 exact to_new r (cut_ok.port_reach ⟨by rw [ofLens_n]; exact one_lt, hu⟩ old_walk) at_junction
548end
550/-! ### Every level -/
552/-- The map depends on the side lengths only through the positions of the corners. -/
553theorem tgt_congr {ω : Bool} {f f' : Nat → Nat} (same_pos : ∀ k, k ≤ 6 → pos f k = pos f' k) (u : Nat) (s : Bool) :
554 tgt ω f' u s = tgt ω f u s :=
555 tgt_map (φ := fun x => x) (fun _ _ => Iff.rfl) rfl rfl (by rw [same_pos 6 (by omega)]) same_pos u s
557/-- The junction map depends only on the lengths of actual sides (and on `d` only through the Σ child). -/
558theorem StepOK.congr {L L' : Nat → Nat → Nat} {d d' : Nat} {ω : Bool}
559 (same_len : ∀ c, c < nk .Delta → ∀ j, j < 6 → L c j = L' c j)
560 (same_d : ∀ c, c < nk .Delta → kidAt .Delta c = .Sigma → d = d') (holds' : StepOK L' d' ω) : StepOK L d ω := by
561 -- the corners are in the same places
562 have same_pos : ∀ c, c < nk .Delta → ∀ v, v ≤ 6 → pos (L c) v = pos (L' c) v :=
563 fun c hc v _ => pos_congr v (fun i hi => same_len c hc i (by omega))
564 -- child 1 is an actual child
565 have one_lt : 1 < nk .Delta := by decide
566 intro u hu s q tgt_eq
567 -- the junction is one of the pieces `1 … 21`
568 obtain ⟨q_pos, q_lt⟩ := tgt_lt tgt_eq
569 rw [tgt_congr (f := L' 1) (fun k hk => (same_pos 1 one_lt k hk).symm)] at tgt_eq
570 obtain ⟨r, walk, at_junction⟩ := holds' u (by rw [← same_pos 1 one_lt 6 (by omega)]; exact hu) s q tgt_eq
571 refine ⟨r, by rw [ofLens_congr same_len same_d]; exact walk, ?_⟩
572 -- pieces `q` and `q - 1` are sides of actual children
573 obtain ⟨child_lt, side_lt⟩ := piece_ok q q_lt
574 obtain ⟨child_lt', side_lt'⟩ := piece_ok (q - 1) (by omega)
575 -- so the junction's port `R` is the same with either lengths
576 have same_jR : jR L q = jR L' q := by
577 simp only [jR, same_pos _ child_lt _ (show ((pieceD q).2 + 1) % 6 ≤ 6 by omega)]
578 -- and so is its port `L`
579 have same_jL : jL L q = jL L' q := by
580 simp only [jL, same_pos _ child_lt' _ (show (pieceD (q - 1)).2 ≤ 6 by omega)]
581 rw [same_jR, same_jL]; exact at_junction
583/-- Child 1 of Δ is not a Σ. -/
584theorem kid_one : kidAt .Delta 1 ≠ .Sigma := by decide
586/-- The sibling glued to side 5 of Δ's Σ child is not child 1. -/
587theorem sig_partner : ∀ c, c < nk .Delta → kidAt .Delta c = .Sigma → ((adjAt .Delta c 5).getD (0, 0)).1 ≠ 1 := by
588 decide
In the paper Lemma 9.3 The junction map
590/-- **The junction map at every level** `m ≥ 1`. -/
591theorem step_level (m : Nat) (m_pos : 1 ≤ m) (ω : Bool) : StepOK (Lk m .Delta) (dOff m) ω := by
592 refine adm_induct .Delta ω (fun L d => StepOK L d ω)
593 (fun L L' d d' same_len same_d holds' => StepOK.congr same_len same_d holds')
594 (step_base ω) ?_ _ _ (adm_level .Delta m m_pos)
595 intro μ L d move_ok clear old_map
596 refine StepOK.move move_ok ?_ ?_ old_map
597 · -- a cut on child 1 is two edges clear of the ends of its side (child 1 is not a Σ)
598 intro on_child_one
599 rcases clear with ⟨clear_start, clear_end⟩ | ⟨is_sigma, _⟩
600 · rw [on_child_one] at clear_end; exact ⟨clear_start, clear_end⟩
601 · rw [on_child_one] at is_sigma; exact absurd is_sigma kid_one
602 · -- and so is the same cut seen from the sibling, if that is child 1
603 intro shared sib_child_one
604 rcases clear with ⟨clear_start, clear_end⟩ | ⟨is_sigma, side_five⟩
605 · have same_len := move_ok.L₁ shared -- the sibling's side is as long as side `j₀`
606 rw [sib_child_one] at same_len
607 simp only [Move.r₁]
608 omega
609 · exfalso
610 -- the sibling glued to the Σ child's side 5 is not child 1
611 have not_one := sig_partner _ move_ok.c₀ is_sigma
612 rw [← side_five] at not_one
613 exact not_one sib_child_one
615end SpectreKnot.Statement

← SpectreKnot/NewWalk.leanSpectreKnot/Linked.lean →