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

lean/SpectreKnot/Lens.lean

183 lines · 22 declarations, each with its own page · on GitHub ·

Compositions with given side lengths (Comp.ofLens): positions, the side containing an edge, and the gluing formula. Used by the parity lemma (Parity.lean).

← SpectreKnot/Subdivide.leanSpectreKnot/Move.lean →

All 39 files, and the declarations of this one
1/-
2Compositions with given side lengths (`Comp.ofLens`): positions, the side containing an edge, and the gluing formula.
3Used by the parity lemma (`Parity.lean`).
4-/
7
8namespace SpectreKnot.Compose
9
10open Gluing Pattern
12/-! ### Positions -/
14/-- `pos f j = f 0 + … + f (j-1)`: where side `j` begins, for side lengths `f`. -/
15def pos (f : Nat → Nat) : Nat → Nat
16 | 0 => 0
17 | j + 1 => pos f j + f j
19/-- Side `j + 1` begins where side `j` begins, plus the length of side `j`. -/
20theorem pos_succ (f : Nat → Nat) (j : Nat) : pos f (j + 1) = pos f j + f j := rfl
22/-- Later sides begin later: `pos f` is monotone. -/
23theorem pos_mono (f : Nat → Nat) {a b : Nat} (a_le_b : a ≤ b) : pos f a ≤ pos f b := by
24 induction b with
25 | zero =>
26 -- only side 0 begins at or before side 0
27 have a_zero : a = 0 := by omega
28 subst a_zero; exact Nat.le_refl _
29 | succ b ih =>
30 by_cases a_eq : a = b + 1
31 · subst a_eq; exact Nat.le_refl _
32 · have := ih (by omega) -- side `a` begins no later than side `b`, which begins before side `b + 1`
33 rw [pos_succ]; omega
35/-- Side `a` ends no later than any later side `b` begins. -/
36theorem pos_lt_of_pos (f : Nat → Nat) (len_pos : ∀ i, i < 6 → 1 ≤ f i) {a b : Nat} (a_lt_b : a < b) (b_le : b ≤ 6) :
37 pos f a + f a ≤ pos f b := by
38 rw [← pos_succ]; exact pos_mono f a_lt_b
40/-- The six side lengths, as an explicit list. -/
41theorem range6_map (f : Nat → Nat) : (List.range 6).map f = [f 0, f 1, f 2, f 3, f 4, f 5] := rfl
43/-- The prefix sums of the list of six side lengths, read at `j ≤ 6`, are `pos f j`: the list form of a child
44(`mkKidL`) puts side `j` where `pos` does. -/
45theorem prefixSums_getD (f : Nat → Nat) {j : Nat} (j_le : j ≤ 6) :
46 (prefixSums ((List.range 6).map f) 0).getD j 0 = pos f j := by
48 rcases (show j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3 ∨ j = 4 ∨ j = 5 ∨ j = 6 by omega) with
49 rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> rfl
51/-- Entry `j < 6` of the list of six side lengths is `f j`. -/
52theorem len_getD (f : Nat → Nat) {j : Nat} (j_lt : j < 6) : ((List.range 6).map f).getD j 0 = f j := by
54 rcases (show j = 0 ∨ j = 1 ∨ j = 2 ∨ j = 3 ∨ j = 4 ∨ j = 5 by omega) with rfl | rfl | rfl | rfl | rfl | rfl <;> rfl
56/-- Every position `k` of a rim with side lengths `f` (all positive) lies in exactly one side `j`, at offset `o`. -/
57theorem decomp (f : Nat → Nat) : ∀ i, i ≤ 6 → ∀ k, k < pos f i → ∃ j o, j < i ∧ o < f j ∧ k = pos f j + o := by
58 intro i
59 induction i with
60 | zero => intro _ k k_lt; simp [pos] at k_lt
61 | succ i ih =>
62 intro i_le k k_lt
63 by_cases before : k < pos f i
64 · obtain ⟨j, o, j_lt, o_lt, rfl⟩ := ih (by omega) k before
65 exact ⟨j, o, by omega, o_lt, rfl⟩
66 · rw [pos_succ] at k_lt
67 exact ⟨i, k - pos f i, by omega, by omega, by omega⟩
69/-- The side lookup `Comp.sideIdx` finds the side: at offset `o < f j` in side `j`, it returns `j`. -/
70theorem sideIdx_eq (f : Nat → Nat) (len_pos : ∀ i, i < 6 → 1 ≤ f i) {j o : Nat} (j_lt : j < 6) (o_lt : o < f j) :
71 Comp.sideIdx (prefixSums ((List.range 6).map f) 0) (pos f j + o) 5 = j := by
72 -- searching down from any side `i ≥ j` finds side `j`
73 have search : ∀ i, i ≤ 5 → j ≤ i →
74 Comp.sideIdx (prefixSums ((List.range 6).map f) 0) (pos f j + o) i = j := by
75 intro i
76 induction i with
77 | zero =>
78 intro _ j_le
79 -- only side 0 is left
80 have j_zero : j = 0 := by omega
81 subst j_zero; rfl
82 | succ i ih =>
83 intro i_le j_le
84 simp only [Comp.sideIdx]
85 rw [prefixSums_getD f (by omega)]
86 by_cases at_j : j = i + 1
87 · subst at_j; rw [ite_eq_left (by omega)]
88 -- side `j` ends before side `i + 1` begins
89 · have ends_before := pos_lt_of_pos f len_pos (show j < i + 1 by omega) (by omega)
90 rw [ite_eq_right (by omega)]
91 exact ih (by omega) (by omega)
92 exact search 5 (by omega) (by omega)
94/-! ### The children of `ofLens` -/
96variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
98/-- The number of children. -/
99abbrev nk (T : Kind) : Nat := (Pattern.kids T).length
101/-- The composition `ofLens` has the kind's children. -/
102theorem ofLens_n : (Comp.ofLens T L d ω).toGluing.n = nk T := by
105/-- Child `c` of `ofLens` is the child built from its kind and its side lengths `L c`. -/
106theorem ofLens_kid {c : Nat} (c_lt : c < nk T) :
107 (Comp.ofLens T L d ω).kid c = mkKidL (kidAt T c) ((List.range 6).map (L c)) d ω := by
108 simp [Comp.ofLens, Comp.kid, List.getD_eq_getElem?_getD, c_lt]
110/-- The rim of child `c` has `pos (L c) 6` edges: the sum of its six side lengths. -/
111theorem ofLens_E {c : Nat} (c_lt : c < nk T) : (Comp.ofLens T L d ω).toGluing.E c = pos (L c) 6 := by
112 simp only [Comp.toGluing, ofLens_kid c_lt, mkKidL]; exact prefixSums_getD _ (by omega)
114/-- Side `j` of child `c` begins at `pos (L c) j`. -/
115theorem ofLens_U {c j : Nat} (c_lt : c < nk T) (j_le : j ≤ 6) :
116 ((Comp.ofLens T L d ω).kid c).U.getD j 0 = pos (L c) j := by
117 simp only [ofLens_kid c_lt, mkKidL]; exact prefixSums_getD _ j_le
119/-- Side `j` of child `c` has length `L c j`. -/
120theorem ofLens_len {c j : Nat} (c_lt : c < nk T) (j_lt : j < 6) :
121 ((Comp.ofLens T L d ω).kid c).len.getD j 0 = L c j := by
122 simp only [ofLens_kid c_lt, mkKidL]; exact len_getD _ j_lt
124/-- The corner `A` of child `c`: vertex 0, or for the Σ child the point `d` along its side 5. -/
125theorem ofLens_A {c : Nat} (c_lt : c < nk T) :
126 (Comp.ofLens T L d ω).toGluing.A c = if kidAt T c = .Sigma then pos (L c) 5 + d else 0 := by
127 simp only [Comp.toGluing, ofLens_kid c_lt, mkKidL, prefixSums_getD _ (show 5 ≤ 6 by omega)]
129/-- The corner `B` of child `c`: the vertex after `A` if `ω`, the vertex before it otherwise. -/
130theorem ofLens_B {c : Nat} (c_lt : c < nk T) :
131 (Comp.ofLens T L d ω).toGluing.B c =
132 if ω then nxt (pos (L c) 6) ((Comp.ofLens T L d ω).toGluing.A c)
133 else prv (pos (L c) 6) ((Comp.ofLens T L d ω).toGluing.A c) := by
134 rw [ofLens_A c_lt]
135 simp only [Comp.toGluing, ofLens_kid c_lt, mkKidL, prefixSums_getD _ (show 5 ≤ 6 by omega),
136 prefixSums_getD _ (show 6 ≤ 6 by omega)]
138/-! ### The tables, as facts -/
140/-- Table 2 entry `adj T c j`. -/
141abbrev adjAt (T : Kind) (c j : Nat) : Option (Nat × Nat) := ((adj T).getD c []).getD j none
143/-- Table 2 is consistent at `(c, j)`: a glued side is glued back, to a side of a different child. -/
144def adjOk (T : Kind) (c j : Nat) : Bool :=
145 match adjAt T c j with
146 | none => true
147 | some (c', j') => decide (c' < nk T) && decide (j' < 6) && c' != c && adjAt T c' j' == some (c, j)
149/-- Table 2 is consistent at every side of every child of every kind (checked by `decide`). -/
150theorem adj_ok : ∀ T : Kind, ∀ c, c < nk T → ∀ j, j < 6 → adjOk T c j = true := by
151 intro T; cases T <;> decide
153/-- A side glued by Table 2 is glued to a side of a different child, which is glued back to it. -/
154theorem adj_valid {T : Kind} {c j c' j' : Nat} (c_lt : c < nk T) (j_lt : j < 6)
155 (glued : adjAt T c j = some (c', j')) : c' < nk T ∧ j' < 6 ∧ c' ≠ c ∧ adjAt T c' j' = some (c, j) := by
156 -- the table check at `(c, j)`
157 have table := adj_ok T c c_lt j j_lt
158 simp only [adjOk, glued, Bool.and_eq_true, decide_eq_true_eq, bne_iff_ne, ne_eq, beq_iff_eq] at table
159 exact ⟨table.1.1.1, table.1.1.2, table.1.2, table.2⟩
161/-! ### The gluing formula -/
163/-- Edge `pos j + o` of child `c` (offset `o` in side `j`) is glued as Table 2 says: to the edge of side `j'` of child
164`c'` that is `o` edges from its end. -/
165theorem ofLens_mate (len_pos : ∀ c, c < nk T → ∀ j, j < 6 → 1 ≤ L c j) {c j o : Nat} (c_lt : c < nk T) (j_lt : j < 6)
166 (o_lt : o < L c j) :
167 (Comp.ofLens T L d ω).mate c (pos (L c) j + o) =
168 (adjAt T c j).map fun (c', j') => (c', pos (L c') j' + L c' j' - 1 - o) := by
170 rw [ofLens_kid c_lt]
171 simp only [mkKidL]
172 rw [sideIdx_eq (L c) (len_pos c c_lt) j_lt o_lt, prefixSums_getD _ (by omega),
173 show pos (L c) j + o - pos (L c) j = o by omega]
174 show (match adjAt T c j with
175 | none => none
176 | some (c', j') =>
177 some (c', ((Comp.ofLens T L d ω).kid c').U.getD j' 0 + ((Comp.ofLens T L d ω).kid c').len.getD j' 0 - 1 - o)) = _
178 cases glued : adjAt T c j with
179 | none => rfl
180 | some p =>
181 obtain ⟨c', j'⟩ := p
182 obtain ⟨c'_lt, j'_lt, _, _⟩ := adj_valid c_lt j_lt glued
183 simp only [Option.map_some, ofLens_U c'_lt (by omega : j' ≤ 6), ofLens_len c'_lt j'_lt]

← SpectreKnot/Subdivide.leanSpectreKnot/Move.lean →