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

lean/SpectreKnot/ComposeTiles.lean

277 lines · 17 declarations, each with its own page · on GitHub ·

compose (the statement file's supertile construction) read in terms of the abstract composition Comp.ofLens: which child a tile belongs to, what is glued across a child's rim edge (glue_rim: exactly what Comp.mate says), and the parent's rim as a list of children's rim edges (rim_edgeAt, via ownGo).

← SpectreKnot/PatchSig.leanSpectreKnot/ParentRim.lean →

All 39 files, and the declarations of this one
1/-
2`compose` (the statement file's supertile construction) read in terms of the abstract composition `Comp.ofLens`:
3which child a tile belongs to, what is glued across a child's rim edge (`glue_rim`: exactly what `Comp.mate`
4says), and the parent's rim as a list of children's rim edges (`rim_edgeAt`, via `ownGo`).
5-/
8
9namespace SpectreKnot.Statement
11open Pattern Compose
13/-! ### Counting the entries of a strictly increasing sequence below a bound -/
15/-- A sequence that increases at every step below `n` is monotone on `0 … n`. -/
16theorem mono_of_succ {f : Nat → Nat} {n : Nat} (step_lt : ∀ a, a < n → f a < f (a + 1)) :
17 ∀ a b, a ≤ b → b ≤ n → f a ≤ f b := by
18 intro a b a_le b_le
19 induction b with
20 | zero =>
21 -- `a ≤ 0`, so `a = 0`
22 have a_zero : a = 0 := by omega
23 subst a_zero; exact Nat.le_refl _
24 | succ b ih =>
25 by_cases a_eq : a = b + 1
26 · subst a_eq; exact Nat.le_refl _
27 · have le_b := ih (by omega) (by omega) -- up to `b` by induction
28 -- and one step more
29 have step := step_lt b (by omega)
30 omega
32/-- If, below `n`, `f a ≤ x` holds exactly when `a ≤ c`, then `min n (c + 1)` of the entries `f 0 … f (n-1)` are at
33most `x`. -/
34theorem count_min {f : Nat → Nat} {x : Nat} :
35 ∀ n c, (∀ a, a < n → (f a ≤ x ↔ a ≤ c)) →
36 ((List.range n).filter fun a => decide (f a ≤ x)).length = min n (c + 1) := by
37 intro n
38 induction n with
39 | zero => intro c _; simp
40 | succ n ih =>
41 intro c at_most_iff
42 rw [List.range_succ, List.filter_append, List.length_append, ih c (fun a a_lt => at_most_iff a (by omega))]
43 by_cases n_le : n ≤ c
44 · have counted : f n ≤ x := (at_most_iff n (by omega)).mpr n_le -- entry `n` is counted
45 simp [counted]; omega
46 · have not_counted : ¬ f n ≤ x := -- entry `n` is not counted
47 fun at_most => n_le ((at_most_iff n (by omega)).mp at_most)
48 simp [not_counted]; omega
50/-- In a strictly increasing sequence, the number of entries `f 0 … f (n-1)` at most `x`, less one, is the index
51`c` with `f c ≤ x < f (c + 1)`. -/
52theorem count_eq {f : Nat → Nat} {n c x : Nat} (step_lt : ∀ a, a < n → f a < f (a + 1)) (c_lt : c < n)
53 (at_c : f c ≤ x) (below_next : x < f (c + 1)) :
54 ((List.range n).filter fun a => decide (f a ≤ x)).length - 1 = c := by
55 -- the sequence is monotone
56 have mono := mono_of_succ step_lt
57 rw [count_min n c (fun a a_lt => ⟨fun at_most => ?_, fun a_le => ?_⟩)]
58 · omega
59 · by_cases a_le : a ≤ c
60 · exact a_le
61 · have := mono (c + 1) a (by omega) (by omega) -- past `c`, the entries exceed `x`
62 omega
63 · have := mono a c a_le (by omega) -- up to `c`, the entries are at most `f c ≤ x`
64 omega
66/-! ### Lists of seven positions -/
68/-- Entry `j` (for `j < 7`) of the list `g 0, …, g 6` is `g j`. -/
69theorem range7_getD (g : Nat → Nat) {j : Nat} (j_lt : j < 7) : ((List.range 7).map g).getD j 0 = g j := by
70 rcases (show j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3 ∨ j = 4 ∨ j = 5 ∨ j = 6 by omega) with
71 rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> rfl
73/-! ### Sides of a patch with its vertices at `pos f` -/
75section Side
77variable {P : Patch} {f : Nat → Nat}
79/-- If a patch's vertices sit where the side lengths `f` put them, side `j` has `f j` edges. -/
80theorem side_length (vtx_eq : P.vtx = (List.range 7).map (pos f)) (len_eq : P.E = pos f 6) {j : Nat}
81 (j_lt : j < 6) : (P.side j).length = f j := by
82 simp only [Patch.side, vtx_eq, range7_getD _ (show j < 7 by omega), range7_getD _ (show j + 1 < 7 by omega),
83 List.length_take, List.length_drop, pos_succ]
84 -- the rim has `pos f 6` edges
85 have rim_len : P.rim.length = pos f 6 := len_eq
86 -- side `j` ends no later than the rim
87 have side_end := pos_mono f (show j + 1 ≤ 6 by omega)
88 rw [pos_succ] at side_end
89 omega
91/-- If a patch's vertices sit where the side lengths `f` put them, edge `r` of side `j` is rim edge `pos f j + r`. -/
92theorem side_getElem? (vtx_eq : P.vtx = (List.range 7).map (pos f)) (len_eq : P.E = pos f 6) {j r : Nat}
93 (j_lt : j < 6) (r_lt : r < f j) : (P.side j)[r]? = some (P.edgeAt (pos f j + r)) := by
94 simp only [Patch.side, vtx_eq, range7_getD _ (show j < 7 by omega), range7_getD _ (show j + 1 < 7 by omega),
96 rw [List.getElem?_take_of_lt (by omega), List.getElem?_drop]
97 -- side `j` ends no later than the rim
98 have side_end := pos_mono f (show j + 1 ≤ 6 by omega)
99 rw [pos_succ] at side_end
100 -- so the position is on the rim
101 have in_rim : pos f j + r < P.rim.length := by rw [show P.rim.length = P.E from rfl, len_eq]; omega
102 simp only [Patch.edgeAt, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem in_rim, Option.getD_some]
104end Side
106/-! ### The children's tiles in the parent -/
108/-- The number of the first tile of child `c` in the parent. -/
109def offC (child : Nat → Patch) (c : Nat) : Nat := ((List.range c).map fun c' => (child c').tiles).sum
111/-- Child `c + 1` starts right after the tiles of child `c`. -/
112theorem offC_succ (child : Nat → Patch) (c : Nat) : offC child (c + 1) = offC child c + (child c).tiles := by
113 simp [offC, List.range_succ, List.map_append, List.sum_append]
115/-- Every tile of the parent belongs to a child: it lies between that child's first tile and the next child's.
116(`owner_unique`: to only one.) -/
117theorem owner_exists (child : Nat → Patch) : ∀ n t, t < offC child n → ∃ c, c < n ∧ offC child c ≤ t ∧
118 t < offC child c + (child c).tiles := by
119 intro n
120 induction n with
121 | zero => intro t t_lt; simp [offC] at t_lt
122 | succ n ih =>
123 intro t t_lt
124 rw [offC_succ] at t_lt
125 by_cases before_n : t < offC child n
126 · -- a tile of one of the first `n` children
127 obtain ⟨c, c_lt, start_le, lt_end⟩ := ih t before_n
128 exact ⟨c, by omega, start_le, lt_end⟩
129 · -- a tile of child `n`
130 exact ⟨n, by omega, by omega, t_lt⟩
132/-- Tile numbers of the parent do not overlap: tile `t` of child `c` and tile `t'` of child `c'` have the same number
133only if `c = c'` and `t = t'`. -/
134theorem owner_unique (child : Nat → Patch) {c c' t t' : Nat} (t_lt : t < (child c).tiles)
135 (t_lt' : t' < (child c').tiles) (same_num : offC child c + t = offC child c' + t') : c = c' ∧ t = t' := by
136 -- later children start later
137 have mono : ∀ a b, a ≤ b → offC child a ≤ offC child b := by
138 intro a b a_le
139 induction b with
140 | zero =>
141 -- `a ≤ 0`, so `a = 0`
142 have a_zero : a = 0 := by omega
143 subst a_zero; exact Nat.le_refl _
144 | succ b ih =>
145 by_cases a_eq : a = b + 1
146 · subst a_eq; exact Nat.le_refl _
147 · have := ih (by omega) -- up to `b` by induction
148 rw [offC_succ]; omega
149 rcases Nat.lt_trichotomy c c' with c_lt | rfl | c_gt
150 · have c'_after := mono (c + 1) c' c_lt -- child `c'` starts after child `c` ends
151 rw [offC_succ] at c'_after; omega
152 · exact ⟨rfl, by omega⟩
153 · have c_after := mono (c' + 1) c c_gt -- child `c` starts after child `c'` ends
154 rw [offC_succ] at c_after; omega
156section Compose
158variable {T : Kind} {child : Nat → Patch}
160/-- The child that tile `t` of the parent belongs to (as `compose` computes it). -/
161def ownerC (T : Kind) (child : Nat → Patch) (t : Nat) : Nat :=
162 ((List.range (Pattern.kids T).length).filter fun c => decide (offC child c ≤ t)).length - 1
164/-- What `compose` glues across edge `e_i` of tile `t` of child `c`. -/
165def glueAt (T : Kind) (child : Nat → Patch) (c t i : Nat) : Option (Nat × Nat) :=
166 match (child c).glue t i with
167 | some e => some (e.1 + offC child c, e.2)
168 | none =>
169 let pos := ((child c).rim.findIdx? (· == (t, i))).getD 0
170 let j := ((List.range 6).filter fun j => (child c).vtx.getD j 0 ≤ pos).length - 1
171 let o := pos - (child c).vtx.getD j 0
172 match ((Pattern.adj T).getD c []).getD j none with
173 | none => none
174 | some (c', j') =>
175 let s := (child c').side j'
176 (s[s.length - 1 - o]?).map fun e => (e.1 + offC child c', e.2)
178/-- `compose`'s gluing, unfolded: find the tile's child, then glue as `glueAt` says. -/
179theorem compose_glue_def (t i : Nat) :
180 (compose T child).glue t i = glueAt T child (ownerC T child t) (t - offC child (ownerC T child t)) i := rfl
182/-- If every child has a tile, `compose` finds the right child for tile `t` of child `c`. -/
183theorem ownerC_eq (tiles_pos : ∀ c, c < nk T → 0 < (child c).tiles) {c t : Nat} (c_lt : c < nk T)
184 (t_lt : t < (child c).tiles) : ownerC T child (offC child c + t) = c :=
185 count_eq (f := offC child)
186 (fun a a_lt => by
188 -- child `a` has a tile, so child `a + 1` starts later
189 have := tiles_pos a a_lt
190 omega)
191 c_lt (by omega) (by rw [offC_succ]; omega)
193/-- What is glued across edge `e_i` of tile `t` of child `c`, in the parent. -/
194theorem compose_glue (tiles_pos : ∀ c, c < nk T → 0 < (child c).tiles) {c t : Nat} (c_lt : c < nk T)
195 (t_lt : t < (child c).tiles) (i : Nat) :
196 (compose T child).glue (offC child c + t) i = glueAt T child c t i := by
197 rw [compose_glue_def, ownerC_eq tiles_pos c_lt t_lt, Nat.add_sub_cancel_left]
199end Compose
201/-! ### Across a child's rim edge -/
203/-- On a rim that lists no edge twice, looking up rim edge `k` finds position `k`. -/
204theorem findIdx_rim {P : Patch} {k : Nat} (k_lt : k < P.E)
205 (rim_inj : ∀ k', k' < P.E → P.edgeAt k' = P.edgeAt k → k' = k) :
206 (P.rim.findIdx? (· == ((P.edgeAt k).1, (P.edgeAt k).2))).getD 0 = k := by
207 -- `P.E` is the length of the rim list
208 have k_lt_len : k < P.rim.length := k_lt
209 -- on the rim, the list entry is the edge `edgeAt` gives
210 have entry_eq : ∀ k', (k'_lt : k' < P.rim.length) → P.rim[k'] = P.edgeAt k' := fun k' k'_lt => by
211 simp only [Patch.edgeAt, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem k'_lt, Option.getD_some]
212 rw [List.findIdx?_eq_some_iff_getElem.mpr ⟨k_lt_len, ?_, ?_⟩]
213 · rfl
214 · rw [entry_eq]; simp
215 · intro j j_lt same_edge
216 rw [entry_eq, beq_iff_eq] at same_edge
217 -- an earlier position with the same edge would be `k` itself
218 have := rim_inj j
219 (by
220 -- `k` is a rim position
221 have : k < P.E := k_lt
222 show j < P.rim.length; omega)
223 (by rw [same_edge])
224 omega
226section Rim
228variable {T : Kind} {child : Nat → Patch} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
In the paper Lemma 4.2 Gluing
230/-- **Across a child's rim edge, `compose` glues what `Comp.mate` says.** Edge `k` of child `c`'s rim (counted in
231its own orientation, from its vertex 0) is glued to edge `k'` of child `c'`'s rim exactly when the abstract
232composition with these side lengths says so. Here `L c j` is the length of side `j` of child `c`. -/
233theorem glue_rim (len_pos : ∀ c, c < nk T → ∀ j, j < 6 → 1 ≤ L c j)
234 (pair_len : ∀ c, c < nk T → ∀ j, j < 6 → ∀ c' j', adjAt T c j = some (c', j') → L c' j' = L c j)
235 (shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧ (child c).E = pos (L c) 6)
236 {c k : Nat} (c_lt : c < nk T) (k_lt : k < pos (L c) 6)
237 (unglued : (child c).glue ((child c).edgeAt k).1 ((child c).edgeAt k).2 = none)
238 (rim_inj : ∀ k', k' < (child c).E → (child c).edgeAt k' = (child c).edgeAt k → k' = k) :
239 glueAt T child c ((child c).edgeAt k).1 ((child c).edgeAt k).2 =
240 ((Comp.ofLens T L d ω).mate c k).map fun (c', k') =>
241 (((child c').edgeAt k').1 + offC child c', ((child c').edgeAt k').2) := by
242 obtain ⟨vtx_eq, len_eq⟩ := shape c c_lt
243 obtain ⟨j, o, j_lt, o_lt, rfl⟩ := decomp (L c) 6 (Nat.le_refl _) k k_lt
244 -- `compose` finds the edge at its own rim position
245 have found_at := findIdx_rim (P := child c) (k := pos (L c) j + o) (by rw [len_eq]; exact k_lt) rim_inj
246 -- and finds that it lies on side `j`
247 have side_eq :
248 ((List.range 6).filter fun a => decide ((child c).vtx.getD a 0 ≤ pos (L c) j + o)).length - 1 = j := by
249 refine count_eq (f := fun j => (child c).vtx.getD j 0) (fun a a_lt => ?_) j_lt ?_ ?_
250 · simp only [vtx_eq, range7_getD _ (show a < 7 by omega), range7_getD _ (show a + 1 < 7 by omega), pos_succ]
251 have := len_pos c c_lt a a_lt -- side `a` has an edge, so vertex `a + 1` comes after vertex `a`
252 omega
253 · simp only [vtx_eq, range7_getD _ (show j < 7 by omega)]; omega
254 · simp only [vtx_eq, range7_getD _ (show j + 1 < 7 by omega), pos_succ]; omega
255 unfold glueAt
256 rw [unglued]
257 simp only []
258 rw [found_at, side_eq, vtx_eq, range7_getD _ (show j < 7 by omega), ofLens_mate len_pos c_lt j_lt o_lt,
259 show pos (L c) j + o - pos (L c) j = o by omega]
260 simp only [adjAt]
261 cases adj_eq : ((Pattern.adj T).getD c []).getD j none with
262 | none => rfl
263 | some p =>
264 obtain ⟨c', j'⟩ := p
265 obtain ⟨c_lt', j_lt', _, _⟩ := adj_valid c_lt j_lt adj_eq
266 -- the two glued sides have the same length
267 have same_len := pair_len c c_lt j j_lt c' j' adj_eq
268 obtain ⟨vtx_eq', len_eq'⟩ := shape c' c_lt'
269 simp only [Option.map_some]
270 rw [side_length vtx_eq' len_eq' j_lt',
271 side_getElem? vtx_eq' len_eq' j_lt' (show L c' j' - 1 - o < L c' j' by omega),
272 show pos (L c') j' + L c' j' - 1 - o = pos (L c') j' + (L c' j' - 1 - o) by omega]
273 rfl
275end Rim
277end SpectreKnot.Statement

← SpectreKnot/PatchSig.leanSpectreKnot/ParentRim.lean →