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

lean/SpectreKnot/ParentRim.lean

516 lines · 34 declarations, each with its own page · on GitHub ·

The parent's rim, read from Table 3: position p of the rim of compose T child is edge k of child c's rim (ownGo). Its properties, for any side lengths: the positions are distinct edges, they are exactly the children's rim edges that the composition leaves unglued, and consecutive positions meet at a parent rim vertex in the sense of Gluing.Rot (a table check, consec_ok).

← SpectreKnot/ComposeTiles.leanSpectreKnot/Reverse.lean →

All 39 files, and the declarations of this one
1/-
2The parent's rim, read from Table 3: position `p` of the rim of `compose T child` is edge `k` of child `c`'s rim
3(`ownGo`). Its properties, for any side lengths: the positions are distinct edges, they are exactly the children's
4rim edges that the composition leaves unglued, and consecutive positions meet at a parent rim vertex in the sense of
5`Gluing.Rot` (a table check, `consec_ok`).
6-/
9
10namespace SpectreKnot.Statement
12open Pattern Compose Gluing
14/-! ### Rims made of pieces -/
16section Own
18variable (L : Nat → Nat → Nat)
20/-- The total length of the pieces. -/
21def totL : List (Nat × Nat) → Nat
22 | [] => 0
23 | (c, j) :: rest => L c j + totL rest
25/-- Position `p` of a rim made of the pieces `pcs`, each a side `j` of a child `c` traversed backwards: the edge
26`(c, k)` of the child there. -/
27def ownGo : List (Nat × Nat) → Nat → Nat × Nat
28 | [], _ => (0, 0)
29 | (c, j) :: rest, p => if p < L c j then (c, pos (L c) j + L c j - 1 - p) else ownGo rest (p - L c j)
31/-- `Consec pcs a b`: the piece `b` comes right after the piece `a` in `pcs`. -/
32inductive Consec : List (Nat × Nat) → Nat × Nat → Nat × Nat → Prop
33 | here {a b : Nat × Nat} {rest : List (Nat × Nat)} : Consec (a :: b :: rest) a b
34 | there {x a b : Nat × Nat} {rest : List (Nat × Nat)} : Consec rest a b → Consec (x :: rest) a b
36variable {L}
38/-- Both pieces of a consecutive pair are in the list. -/
39theorem Consec.mem {l : List (Nat × Nat)} {a b : Nat × Nat} (consec : Consec l a b) : a ∈ l ∧ b ∈ l := by
40 induction consec with
41 | here => exact ⟨List.mem_cons_self, List.mem_cons_of_mem _ List.mem_cons_self⟩
42 | there _ ih => exact ⟨List.mem_cons_of_mem _ ih.1, List.mem_cons_of_mem _ ih.2⟩
44/-- Two lists of pieces, one after the other, have the sum of their lengths. -/
45theorem totL_append (l₁ l₂ : List (Nat × Nat)) : totL L (l₁ ++ l₂) = totL L l₁ + totL L l₂ := by
46 induction l₁ with
47 | nil => simp [totL]
48 | cons x l ih => obtain ⟨c, j⟩ := x; simp only [List.cons_append, totL, ih]; omega
50/-- A position in two lists of pieces, one after the other: in the first list if it is below the first's length,
51otherwise in the second, counted from the second's start. -/
52theorem ownGo_append (l₁ l₂ : List (Nat × Nat)) (p : Nat) :
53 ownGo L (l₁ ++ l₂) p = if p < totL L l₁ then ownGo L l₁ p else ownGo L l₂ (p - totL L l₁) := by
54 induction l₁ generalizing p with
55 | nil => simp [totL]
56 | cons x l ih =>
57 obtain ⟨c, j⟩ := x
58 simp only [List.cons_append, ownGo, totL]
59 by_cases in_head : p < L c j
60 · have in_l₁ : p < L c j + totL L l := by omega -- in the first piece, so within `l₁`
61 simp [in_head, in_l₁]
62 · rw [ih]
63 by_cases in_rest : p - L c j < totL L l
64 · have in_l₁ : p < L c j + totL L l := by omega -- past the first piece, but within `l₁`
65 simp [in_head, in_rest, in_l₁]
66 · have past_l₁ : ¬ p < L c j + totL L l := by omega -- past the whole of `l₁`
67 simp only [in_head, in_rest, past_l₁, ite_false]
68 congr 1; omega
70/-- Every position below the total length is an edge `pos j + o` of a listed side `(c, j)`, with `o` inside the
71side. -/
72theorem ownGo_mem : ∀ (pcs : List (Nat × Nat)) (p : Nat), p < totL L pcs →
73 ∃ c j o, (c, j) ∈ pcs ∧ o < L c j ∧ ownGo L pcs p = (c, pos (L c) j + o) := by
74 intro pcs
75 induction pcs with
76 | nil => intro p p_lt; simp [totL] at p_lt
77 | cons x rest ih =>
78 obtain ⟨c, j⟩ := x
79 intro p p_lt
80 simp only [totL] at p_lt
81 simp only [ownGo]
82 by_cases in_head : p < L c j
83 · -- in the first piece, counted from the end of its side
84 rw [ite_eq_left in_head]
85 exact ⟨c, j, L c j - 1 - p, List.mem_cons_self, by omega, by congr 1; omega⟩
86 · -- in a later piece
87 rw [ite_eq_right in_head]
88 obtain ⟨c', j', o, mem, o_lt, at_p⟩ := ih (p - L c j) (by omega)
89 exact ⟨c', j', o, List.mem_cons_of_mem _ mem, o_lt, at_p⟩
91/-- Every edge of every listed side is at some position. -/
92theorem ownGo_surj : ∀ (pcs : List (Nat × Nat)) {c j o : Nat}, (c, j) ∈ pcs → o < L c j →
93 ∃ p, p < totL L pcs ∧ ownGo L pcs p = (c, pos (L c) j + o) := by
94 intro pcs
95 induction pcs with
96 | nil => intro c j o mem; simp at mem
97 | cons x rest ih =>
98 obtain ⟨c', j'⟩ := x
99 intro c j o mem o_lt
100 rcases List.mem_cons.mp mem with is_head | in_rest
101 · -- the first piece: counted from the end of its side
102 simp only [Prod.mk.injEq] at is_head
103 obtain ⟨rfl, rfl⟩ := is_head
104 refine ⟨L c j - 1 - o, by simp only [totL]; omega, ?_⟩
105 simp only [ownGo]
106 rw [ite_eq_left (by omega)]
107 congr 1; omega
108 · -- a later piece: after the first
109 obtain ⟨p, p_lt, at_p⟩ := ih in_rest o_lt
110 refine ⟨L c' j' + p, by simp only [totL]; omega, ?_⟩
111 simp only [ownGo]
112 rw [ite_eq_right (by omega), Nat.add_sub_cancel_left]
113 exact at_p
115/-- Positions in a side are distinct from those in another side of the same child. -/
116theorem side_pos_inj {f : Nat → Nat} (len_pos : ∀ i, i < 6 → 1 ≤ f i) {j j' o o' : Nat} (j_lt : j < 6)
117 (j_lt' : j' < 6) (o_lt : o < f j) (o_lt' : o' < f j') (same_pos : pos f j + o = pos f j' + o') :
118 j = j' ∧ o = o' := by
119 -- the side lookup at the position finds `j`
120 have side_j := sideIdx_eq f len_pos j_lt o_lt
121 -- and at the same position it finds `j'`
122 have side_j' := sideIdx_eq f len_pos j_lt' o_lt'
123 rw [same_pos] at side_j
124 rw [side_j] at side_j'
125 subst side_j'
126 exact ⟨rfl, by omega⟩
128/-- On a list of distinct sides, different positions are different edges. -/
129theorem ownGo_inj (len_pos : ∀ c j, j < 6 → 1 ≤ L c j) : ∀ (pcs : List (Nat × Nat)), pcs.Nodup →
130 (∀ x ∈ pcs, x.2 < 6) → ∀ p p', p < totL L pcs → p' < totL L pcs → ownGo L pcs p = ownGo L pcs p' → p = p' := by
131 intro pcs
132 induction pcs with
133 | nil => intro _ _ p p' p_lt; simp [totL] at p_lt
134 | cons x rest ih =>
135 obtain ⟨c, j⟩ := x
136 intro nodup sides_lt p p' p_lt p_lt' same_edge
137 rw [List.nodup_cons] at nodup
138 simp only [totL] at p_lt p_lt'
139 simp only [ownGo] at same_edge
140 -- the first piece is an actual side
141 have j_lt : j < 6 := sides_lt (c, j) List.mem_cons_self
142 -- and so are the later pieces
143 have rest_lt : ∀ x ∈ rest, x.2 < 6 := fun x mem => sides_lt x (List.mem_cons_of_mem _ mem)
144 -- an edge of the first piece is not an edge of a later piece
145 have sep : ∀ q q', q < L c j → q' < totL L rest → (c, pos (L c) j + L c j - 1 - q) ≠ ownGo L rest q' := by
146 intro q q' q_lt q_lt' same
147 obtain ⟨c₂, j₂, o₂, mem, o₂_lt, at_q'⟩ := ownGo_mem rest q' q_lt'
148 rw [at_q'] at same
149 simp only [Prod.mk.injEq] at same
150 obtain ⟨rfl, same_pos⟩ := same
151 -- the same edge of the same child: the same side, which the list would then hold twice
152 have same_side := side_pos_inj (len_pos c) j_lt (rest_lt _ mem) (show L c j - 1 - q < L c j by omega) o₂_lt
153 (by rw [← same_pos]; omega)
154 exact nodup.1 (same_side.1 ▸ mem)
155 by_cases in_head : p < L c j <;> by_cases in_head' : p' < L c j
156 · -- both in the first piece
157 rw [ite_eq_left in_head, ite_eq_left in_head'] at same_edge
158 simp only [Prod.mk.injEq] at same_edge
159 omega
160 · rw [ite_eq_left in_head, ite_eq_right in_head'] at same_edge
161 exact absurd same_edge (sep p (p' - L c j) in_head (by omega))
162 · rw [ite_eq_right in_head, ite_eq_left in_head'] at same_edge
163 exact absurd same_edge.symm (sep p' (p - L c j) in_head' (by omega))
164 · rw [ite_eq_right in_head, ite_eq_right in_head'] at same_edge
165 -- both in later pieces: by induction
166 have := ih nodup.2 rest_lt (p - L c j) (p' - L c j) (by omega) (by omega) same_edge
167 omega
169/-- Position 0 is the last edge of the first piece's side (sides are traversed backwards). -/
170theorem ownGo_zero {c j : Nat} {rest : List (Nat × Nat)} (len_pos : 1 ≤ L c j) :
171 ownGo L ((c, j) :: rest) 0 = (c, pos (L c) j + L c j - 1) := by
172 simp only [ownGo]; rw [ite_eq_left (show 0 < L c j by omega)]; rfl
174/-- The last position is the first edge of the last piece's side. -/
175theorem ownGo_last {c j : Nat} (len_pos : 1 ≤ L c j) : ∀ (pcs : List (Nat × Nat)),
176 ownGo L (pcs ++ [(c, j)]) (totL L (pcs ++ [(c, j)]) - 1) = (c, pos (L c) j) := by
177 intro pcs
178 -- the last piece adds its side's length
179 have total : totL L (pcs ++ [(c, j)]) = totL L pcs + L c j := by rw [totL_append]; simp [totL]
180 rw [ownGo_append, total, ite_eq_right (show ¬ (totL L pcs + L c j - 1 < totL L pcs) by omega),
181 show totL L pcs + L c j - 1 - totL L pcs = L c j - 1 by omega]
182 simp only [ownGo]
183 rw [ite_eq_left (show L c j - 1 < L c j by omega)]
184 congr 1; omega
186/-- Going back one position: inside a piece, the next edge of the same side (in the children's sense); at the start
187of a piece, the first edge of the previous piece. -/
188theorem ownGo_pred (len_pos : ∀ c j, 1 ≤ L c j) : ∀ (pcs : List (Nat × Nat)) (p : Nat), 0 < p → p < totL L pcs →
189 (∃ c j o, (c, j) ∈ pcs ∧ o + 1 < L c j ∧ ownGo L pcs p = (c, pos (L c) j + o) ∧
190 ownGo L pcs (p - 1) = (c, pos (L c) j + o + 1)) ∨
191 (∃ c j c' j', Consec pcs (c', j') (c, j) ∧ ownGo L pcs p = (c, pos (L c) j + L c j - 1) ∧
192 ownGo L pcs (p - 1) = (c', pos (L c') j')) := by
193 intro pcs
194 induction pcs with
195 | nil => intro p _ p_lt; simp [totL] at p_lt
196 | cons x rest ih =>
197 obtain ⟨c, j⟩ := x
198 intro p p_pos p_lt
199 simp only [totL] at p_lt
200 by_cases in_head : p < L c j
201 · -- inside the first piece
202 left
203 refine ⟨c, j, L c j - 1 - p, List.mem_cons_self, by omega, ?_, ?_⟩
204 · simp only [ownGo]; rw [ite_eq_left in_head]; congr 1; omega
205 · simp only [ownGo]; rw [ite_eq_left (by omega)]; congr 1; omega
206 · by_cases at_start : p = L c j
207 · -- at the start of the second piece: the step back is into the first
208 right
209 subst at_start
210 cases rest with
211 | nil => simp [totL] at p_lt
212 | cons y rest' =>
213 obtain ⟨c₂, j₂⟩ := y
214 refine ⟨c₂, j₂, c, j, .here, ?_, ?_⟩
215 · simp only [ownGo]
216 rw [ite_eq_right (show ¬ (L c j < L c j) by omega), Nat.sub_self,
217 ite_eq_left (show 0 < L c₂ j₂ from len_pos c₂ j₂)]
218 rfl
219 · simp only [ownGo]; rw [ite_eq_left (by omega)]; congr 1; omega
220 · -- further on: by induction, in the rest of the list
221 -- a positive position in the rest of the list
222 have past_pos : 0 < p - L c j := by omega
223 rcases ih (p - L c j) past_pos (by omega) with
224 ⟨c', j', o, mem, o_lt, at_p, at_prev⟩ | ⟨c', j', c'', j'', consec, at_p, at_prev⟩
225 · left
226 refine ⟨c', j', o, List.mem_cons_of_mem _ mem, o_lt, ?_, ?_⟩
227 · simp only [ownGo]; rw [ite_eq_right in_head]; exact at_p
228 · simp only [ownGo]; rw [ite_eq_right (by omega), show p - 1 - L c j = p - L c j - 1 by omega]; exact at_prev
229 · right
230 refine ⟨c', j', c'', j'', .there consec, ?_, ?_⟩
231 · simp only [ownGo]; rw [ite_eq_right in_head]; exact at_p
232 · simp only [ownGo]; rw [ite_eq_right (by omega), show p - 1 - L c j = p - L c j - 1 by omega]; exact at_prev
234end Own
236/-! ### Table 3 as a rim, and Table 2 at the vertices -/
238/-- The parent's rim pieces, in order (Table 3 flattened). -/
239def pcs (T : Kind) : List (Nat × Nat) := (pside T).flatMap id
241/-- Turning about vertex `v` of child `c` by Table 2 alone: while the side starting at the vertex is glued to side
242`j₂` of a sibling `c₂`, go on to the vertex where that side ends, vertex `j₂ + 1` of `c₂`. -/
243def tabRot (T : Kind) : Nat → Nat × Nat → Option (Nat × Nat)
244 | 0, _ => none
245 | f + 1, (c, v) =>
246 match adjAt T c v with
247 | none => some (c, v)
248 | some (c₂, j₂) => tabRot T f (c₂, (j₂ + 1) % 6)
250/-- Consecutive pieces `a`, `b` of the parent's rim meet at a parent rim vertex: turning about the vertex where side
251`b` ends (in the children's sense, where the parent's side runs into piece `a`) reaches the vertex where side `a`
252begins. -/
253def consecOk (T : Kind) : List (Nat × Nat) → Bool
254 | a :: b :: rest => tabRot T 30 (b.1, (b.2 + 1) % 6) == some a && consecOk T (b :: rest)
255 | _ => true
257/-- The checks on Tables 2 and 3 that make Table 3 the rim of the glued children. -/
258def rimTablesOk (T : Kind) : Bool :=
259 ((pcs T).all fun x => decide (x.1 < nk T) && decide (x.2 < 6) && (adjAt T x.1 x.2).isNone) &&
260 decide (pcs T).Nodup &&
261 ((List.range (nk T)).all fun c => (List.range 6).all fun j => (adjAt T c j).isSome || (pcs T).contains (c, j)) &&
262 consecOk T (pcs T) &&
263 match (pcs T).head?, (pcs T).getLast? with
264 | some a, some b => tabRot T 30 (a.1, (a.2 + 1) % 6) == some b
265 | _, _ => false
267/-- The table checks pass for all nine kinds. -/
268theorem rimTablesOk_all : ∀ T, rimTablesOk T = true := by intro T; cases T <;> decide
270/-- The check `consecOk` is sound: for consecutive pieces `a`, `b` of a checked list, turning about the vertex where
271side `b` ends reaches the vertex where side `a` begins. -/
272theorem consecOk_sound {T : Kind} : ∀ {l : List (Nat × Nat)} {a b : Nat × Nat}, consecOk T l = true →
273 Consec l a b → tabRot T 30 (b.1, (b.2 + 1) % 6) = some a := by
274 intro l a b ok consec
275 induction consec with
276 | here => simp only [consecOk, Bool.and_eq_true, beq_iff_eq] at ok; exact ok.1
277 | @there x a b rest rest_consec ih =>
278 apply ih
279 cases rest with
280 | nil => cases rest_consec
281 | cons y rest => simp only [consecOk, Bool.and_eq_true] at ok; exact ok.2
283section Facts
285variable (T : Kind)
287/-- Each piece of Table 3 is a side of an actual child, and Table 2 puts that side on the parent's rim. -/
288theorem pcs_valid : ∀ x ∈ pcs T, x.1 < nk T ∧ x.2 < 6 ∧ adjAt T x.1 x.2 = none := by
289 intro x mem
290 -- the table checks for this kind
291 have ok := rimTablesOk_all T
292 simp only [rimTablesOk, Bool.and_eq_true, List.all_eq_true, decide_eq_true_eq, Option.isNone_iff_eq_none] at ok
293 exact ⟨(ok.1.1.1.1 x mem).1.1, (ok.1.1.1.1 x mem).1.2, (ok.1.1.1.1 x mem).2⟩
295/-- Table 3 lists no side twice. -/
296theorem pcs_nodup : (pcs T).Nodup := by
297 -- the table checks for this kind
298 have ok := rimTablesOk_all T
299 simp only [rimTablesOk, Bool.and_eq_true, decide_eq_true_eq] at ok
300 exact ok.1.1.1.2
302/-- Every side of a child that Table 2 puts on the parent's rim is listed in Table 3. -/
303theorem pcs_cover {c j : Nat} (c_lt : c < nk T) (j_lt : j < 6) (on_rim : adjAt T c j = none) : (c, j) ∈ pcs T := by
304 -- the table checks for this kind
305 have ok := rimTablesOk_all T
306 simp only [rimTablesOk, Bool.and_eq_true, List.all_eq_true, List.mem_range, Bool.or_eq_true,
307 Option.isSome_iff_exists, List.contains_iff_mem] at ok
308 rcases ok.1.1.2 c c_lt j j_lt with ⟨x, glued⟩ | mem
309 · rw [on_rim] at glued; contradiction
310 · exact mem
312/-- Consecutive pieces of Table 3 meet at a vertex: turning about the vertex where side `b` ends reaches the vertex
313where side `a` begins. -/
314theorem pcs_consec {a b : Nat × Nat} (consec : Consec (pcs T) a b) : tabRot T 30 (b.1, (b.2 + 1) % 6) = some a := by
315 -- the table checks for this kind
316 have ok := rimTablesOk_all T
317 simp only [rimTablesOk, Bool.and_eq_true] at ok
318 exact consecOk_sound ok.1.2 consec
320/-- Table 3 is not empty. -/
321theorem pcs_ne : pcs T ≠ [] := by cases T <;> decide
323/-- The parent's rim closes up: the last piece of Table 3 meets the first, as consecutive pieces do. -/
324theorem pcs_wrap : tabRot T 30 (((pcs T).head (pcs_ne T)).1, (((pcs T).head (pcs_ne T)).2 + 1) % 6) =
325 some ((pcs T).getLast (pcs_ne T)) := by
326 -- the table checks for this kind
327 have ok := rimTablesOk_all T
328 simp only [rimTablesOk, Bool.and_eq_true] at ok
329 -- the last check: the wrap-around, in terms of `head?` and `getLast?`
330 have wrap_ok := ok.2
331 rw [List.head?_eq_some_head (pcs_ne T), List.getLast?_eq_some_getLast (pcs_ne T)] at wrap_ok
332 simpa using wrap_ok
334end Facts
336/-! ### The rim of the composition `Comp.ofLens` -/
338section Rot
340variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
342/-- With positive side lengths `f`, the position after the last edge of side `j` is vertex `j + 1` (vertex 0 after
343side 5). -/
344theorem nxt_last {f : Nat → Nat} (len_pos : ∀ i, 1 ≤ f i) {j : Nat} (j_lt : j < 6) :
345 nxt (pos f 6) (pos f j + f j - 1) = pos f ((j + 1) % 6) := by
346 -- side `j` has an edge
347 have len_j := len_pos j
348 rcases (show j = 5 ∨ j < 5 by omega) with rfl | j_lt5
349 · -- the last side
350 -- its last edge is the last on the rim, so the next position wraps round to 0
351 have wraps : pos f 5 + f 5 - 1 + 1 = pos f 6 := by
352 rw [show pos f 6 = pos f 5 + f 5 from pos_succ f 5]; omega
353 simp only [nxt]; rw [ite_eq_left wraps]; rfl
354 · -- an earlier side: no wrap-around
355 -- vertex `j + 1` is before the end of the rim
356 have before_end := pos_lt_of_pos f (fun i _ => len_pos i) (show j + 1 < 6 by omega) (Nat.le_refl 6)
357 -- and is where side `j` ends
358 have pos_next : pos f (j + 1) = pos f j + f j := pos_succ f j
359 -- side `j + 1` has an edge
360 have len_next := len_pos (j + 1)
361 simp only [nxt]
362 rw [ite_eq_right (show ¬ (pos f j + f j - 1 + 1 = pos f 6) by omega), Nat.mod_eq_of_lt (show j + 1 < 6 by omega)]
363 omega
365/-- An edge of a side that Table 2 puts on the parent's rim is unglued in the composition. -/
366theorem ofLens_mate_none (len_pos : ∀ c j, 1 ≤ L c j) {c j o : Nat} (c_lt : c < nk T) (j_lt : j < 6)
367 (o_lt : o < L c j) (on_rim : adjAt T c j = none) :
368 (Comp.ofLens T L d ω).toGluing.mate c (pos (L c) j + o) = none := by
369 show (Comp.ofLens T L d ω).mate c (pos (L c) j + o) = none
370 rw [ofLens_mate (fun c _ j _ => len_pos c j) c_lt j_lt o_lt, on_rim]; rfl
372/-- Turning about a vertex of a child, in the composition, follows Table 2. -/
373theorem rot_tab (len_pos : ∀ c j, 1 ≤ L c j) : ∀ f c v c' v', tabRot T f (c, v) = some (c', v') → c < nk T → v < 6 →
374 (Comp.ofLens T L d ω).toGluing.Rot (c, pos (L c) v) (c', pos (L c') v') := by
375 intro f
376 induction f with
377 | zero => intro c v c' v' found; simp [tabRot] at found
378 | succ f ih =>
379 intro c v c' v' found c_lt v_lt
380 simp only [tabRot] at found
381 cases adj_eq : adjAt T c v with
382 | none =>
383 -- side `v` is on the parent's rim: turning stops here
384 rw [adj_eq] at found
385 simp only [Option.some.injEq, Prod.mk.injEq] at found
386 obtain ⟨rfl, rfl⟩ := found
387 -- the first edge of the side is unglued
388 have unglued := ofLens_mate_none (d := d) (ω := ω) len_pos c_lt v_lt (show 0 < L c v from len_pos c v) adj_eq
389 rw [Nat.add_zero] at unglued
390 exact .stop unglued
391 | some p =>
392 -- side `v` is glued to side `j₂` of `c₂`: turn on from the end of that side
393 obtain ⟨c₂, j₂⟩ := p
394 rw [adj_eq] at found
395 obtain ⟨c₂_lt, j₂_lt, _, _⟩ := adj_valid c_lt v_lt adj_eq
396 -- the first edge of side `v` is glued to the last edge of side `j₂` of `c₂`
397 have mate_eq : (Comp.ofLens T L d ω).toGluing.mate c (pos (L c) v) =
398 some (c₂, pos (L c₂) j₂ + L c₂ j₂ - 1) := by
399 show (Comp.ofLens T L d ω).mate c (pos (L c) v) = _
400 -- Table 2's gluing, at offset 0
401 have mate_formula :=
402 ofLens_mate (d := d) (ω := ω) (fun c _ j _ => len_pos c j) c_lt v_lt (show 0 < L c v from len_pos c v)
403 rw [Nat.add_zero, adj_eq] at mate_formula
404 rw [mate_formula]; rfl
405 refine .step mate_eq ?_
406 rw [ofLens_E c₂_lt, nxt_last (len_pos c₂) j₂_lt]
407 exact ih _ _ _ _ found c₂_lt (Nat.mod_lt _ (by omega))
409variable (T L)
411/-- The parent's rim length. -/
412abbrev rimN : Nat := totL L (pcs T)
414variable {T L}
416/-- Each parent rim position is an edge of a listed side, which Table 2 puts on the parent's rim. -/
417theorem own_valid {p : Nat} (p_lt : p < rimN T L) :
418 ∃ c j o, (c, j) ∈ pcs T ∧ c < nk T ∧ j < 6 ∧ adjAt T c j = none ∧ o < L c j ∧
419 ownGo L (pcs T) p = (c, pos (L c) j + o) := by
420 obtain ⟨c, j, o, mem, o_lt, at_p⟩ := ownGo_mem (pcs T) p p_lt
421 obtain ⟨c_lt, j_lt, on_rim⟩ := pcs_valid T _ mem
422 exact ⟨c, j, o, mem, c_lt, j_lt, on_rim, o_lt, at_p⟩
424/-- Every parent rim position is a rim edge of the composition. -/
425theorem own_mate (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
426 (ownGo L (pcs T) p).1 < nk T ∧ (ownGo L (pcs T) p).2 < pos (L (ownGo L (pcs T) p).1) 6 ∧
427 (Comp.ofLens T L d ω).toGluing.mate (ownGo L (pcs T) p).1 (ownGo L (pcs T) p).2 = none := by
428 obtain ⟨c, j, o, _, c_lt, j_lt, on_rim, o_lt, at_p⟩ := own_valid p_lt
429 rw [at_p]
430 dsimp only
431 refine ⟨c_lt, ?_, ofLens_mate_none len_pos c_lt j_lt o_lt on_rim⟩
432 -- side `j` ends where side `j + 1` starts
433 have := pos_lt_of_pos (L c) (fun i _ => len_pos c i) (show j < j + 1 by omega) (show j + 1 ≤ 6 by omega)
434 -- and ends no later than the rim
435 have side_end := pos_mono (L c) (show j + 1 ≤ 6 by omega)
436 rw [pos_succ] at side_end; omega
438/-- Every rim edge of the composition is a parent rim position. -/
439theorem own_surj (len_pos : ∀ c j, 1 ≤ L c j) {c k : Nat} (c_lt : c < nk T) (k_lt : k < pos (L c) 6)
440 (unglued : (Comp.ofLens T L d ω).toGluing.mate c k = none) :
441 ∃ p, p < rimN T L ∧ ownGo L (pcs T) p = (c, k) := by
442 obtain ⟨j, o, j_lt, o_lt, rfl⟩ := decomp (L c) 6 (Nat.le_refl _) k k_lt
443 -- an unglued edge lies on a side that Table 2 puts on the parent's rim
444 have on_rim : adjAt T c j = none := by
445 -- Table 2's gluing at this edge
446 have mate_formula := ofLens_mate (d := d) (ω := ω) (fun c _ j _ => len_pos c j) c_lt j_lt o_lt
447 cases adj_eq : adjAt T c j with
448 | none => rfl
449 | some q => rw [adj_eq] at mate_formula; exact absurd (unglued.symm.trans mate_formula) (by simp)
450 exact ownGo_surj (pcs T) (pcs_cover T c_lt j_lt on_rim) o_lt
452/-- Different parent rim positions are different edges. -/
453theorem own_inj (len_pos : ∀ c j, 1 ≤ L c j) {p p' : Nat} (p_lt : p < rimN T L) (p_lt' : p' < rimN T L)
454 (same_edge : ownGo L (pcs T) p = ownGo L (pcs T) p') : p = p' :=
455 ownGo_inj (fun c j _ => len_pos c j) (pcs T) (pcs_nodup T) (fun x mem => (pcs_valid T x mem).2.1) p p' p_lt p_lt'
456 same_edge
458/-- **The parent's rim, read from Table 3, is consistent with turning about its vertices**: from the end of the edge
459at position `p` (in the children's sense), turning about the vertex reaches the edge at position `p - 1`. -/
460theorem own_rot (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
461 (Comp.ofLens T L d ω).toGluing.Rot ((ownGo L (pcs T) p).1,
462 nxt ((Comp.ofLens T L d ω).toGluing.E (ownGo L (pcs T) p).1) (ownGo L (pcs T) p).2)
463 (ownGo L (pcs T) (prv (rimN T L) p)) := by
464 by_cases p_zero : p = 0
465 · -- position 0: the step back wraps round to the last position, and Table 3's wrap check applies
466 subst p_zero
467 -- Table 3 is not empty
468 have nonempty := pcs_ne T
469 -- Table 3 is its last piece after the others
470 have split_last := List.dropLast_concat_getLast nonempty
471 obtain ⟨c_lt, j_lt, _⟩ := pcs_valid T _ (List.head_mem nonempty)
472 obtain ⟨c_lt_last, j_lt_last, _⟩ := pcs_valid T _ (List.getLast_mem nonempty)
473 -- position 0 is the last edge of the first piece's side
474 have at_zero : ownGo L (pcs T) 0 = (((pcs T).head nonempty).1,
475 pos (L ((pcs T).head nonempty).1) ((pcs T).head nonempty).2 +
476 L ((pcs T).head nonempty).1 ((pcs T).head nonempty).2 - 1) := by
477 conv => lhs; rw [← List.cons_head_tail nonempty]
478 exact ownGo_zero (len_pos _ _)
479 -- the last position is the first edge of the last piece's side
480 have at_last : ownGo L (pcs T) (prv (rimN T L) 0) = (((pcs T).getLast nonempty).1,
481 pos (L ((pcs T).getLast nonempty).1) ((pcs T).getLast nonempty).2) := by
482 simp only [prv, rimN, ite_true]
483 conv => lhs; rw [← split_last]
484 exact ownGo_last (len_pos _ _) _
485 rw [at_zero, at_last, ofLens_E c_lt, nxt_last (len_pos _) j_lt]
486 exact rot_tab len_pos 30 _ _ _ _ (pcs_wrap T) c_lt (Nat.mod_lt _ (by omega))
487 · -- a later position
488 -- the step back is to `p - 1`
489 have prv_eq : prv (rimN T L) p = p - 1 := by simp only [prv]; rw [ite_eq_right p_zero]
490 rw [prv_eq]
491 rcases ownGo_pred len_pos (pcs T) p (by omega) p_lt with
492 ⟨c, j, o, mem, o_lt, at_p, at_prev⟩ | ⟨c, j, c', j', consec, at_p, at_prev⟩
493 · -- inside a piece: the next edge of the same side, and that side is on the parent's rim
494 obtain ⟨c_lt, j_lt, on_rim⟩ := pcs_valid T _ mem
495 rw [at_p, at_prev, ofLens_E c_lt]
496 -- side `j` ends no later than the rim
497 have side_end := pos_mono (L c) (show j + 1 ≤ 6 by omega)
498 rw [pos_succ] at side_end
499 -- so the next position does not wrap round
500 have nxt_eq : nxt (pos (L c) 6) (pos (L c) j + o) = pos (L c) j + (o + 1) := by
501 simp only [nxt]; rw [ite_eq_right (by omega)]; omega
502 rw [nxt_eq, ← Nat.add_assoc]
503 -- the next edge is unglued, so turning stops at once
504 have unglued := ofLens_mate_none (d := d) (ω := ω) len_pos c_lt j_lt o_lt on_rim
505 rw [← Nat.add_assoc] at unglued
506 exact .stop unglued
507 · -- at the start of a piece: turning about the vertex leads to the previous piece, by Table 3's check
508 -- the piece is in Table 3
509 have mem : (c, j) ∈ pcs T := (Consec.mem consec).2
510 obtain ⟨c_lt, j_lt, _⟩ := pcs_valid T _ mem
511 rw [at_p, at_prev, ofLens_E c_lt, nxt_last (len_pos _) j_lt]
512 exact rot_tab len_pos 30 _ _ _ _ (pcs_consec T consec) c_lt (Nat.mod_lt _ (by omega))
514end Rot
516end SpectreKnot.Statement

← SpectreKnot/ComposeTiles.leanSpectreKnot/Reverse.lean →