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

lean/SpectreKnot/ProofGrand.lean

475 lines · 27 declarations, each with its own page · on GitHub ·

The Grandparent Lemma (grandparent, the paper's Lemma 8.3(a), at the vertices of tiles): for b ≥ 1, every vertex of every tile of N_b is surrounded by tiles of N_{b+2}.

← SpectreKnot/ProofExact.leanSpectreKnot/Basic.lean →

All 39 files, and the declarations of this one
1/-
2**The Grandparent Lemma** (`grandparent`, the paper's Lemma 8.3(a), at the vertices of tiles): for `b ≥ 1`, every
3vertex of every tile of `N_b` is surrounded by tiles of `N_{b+2}`.
4
5Every supertile is a disc at its rim (`chains_super`: the nine level-1 clusters by a kernel check, then
6`Kids.rimChains` level by level). A vertex of a tile of `N_b` is surrounded in `N_b`, or lies on the chain about a rim
7vertex `u` of `N_b` (`surrounded_or_chain`). Then the paper's argument on the tables (its proof of Lemma 8.3), at the
8vertices of tiles:
9* `u` not on the closed side 2 of `N_b`, which is child 1 of `N_{b+1}`: turning about vertex `u` of child 1 of the Δ
10 composition comes round, in two steps inside a side (`side_cycle`), in three at a vertex (Table 2:
11 `delta_cycles`); so the vertex is surrounded in `N_{b+1}` (`surrounded_off_side2`);
12* `u` on the closed side 2: in `N_{b+1}` the vertex lies on the chain about a rim vertex well inside side 4 of
13 `N_{b+1}` (child 1's side 2 is piece 16 of the rim, inside side 4, and its ends are junctions 16 and 17:
14 `chain_stretch`, `chain_j16`, `chain_j17`); side 4 of child 1 of `N_{b+2}` is glued to child 3, so turning about that
15 vertex comes round in two steps (`surrounded_side4`).
16-/
20namespace SpectreKnot.Statement
22open Pattern Compose Gluing
24/-! ### Every supertile is a disc at its rim -/
26/-- The chain check, as a computation: from the start of the chain about each rim vertex, turning reaches its end
27within `f` turns. -/
28def Patch.chainCheck (P : Patch) (o : Bool) (f : Nat) : Bool :=
29 (List.range P.E).all fun k => (List.range f).any fun n => P.turns n (P.sC o k) == some (P.fC o k)
31/-- The chain check is sound. -/
32theorem Patch.chainCheck_sound {P : Patch} {o : Bool} {f : Nat} (check : P.chainCheck o f = true) :
33 P.RimChains o := by
34 intro k k_lt
35 simp only [Patch.chainCheck, List.all_eq_true, List.mem_range, List.any_eq_true, beq_iff_eq] at check
36 obtain ⟨n, _, found⟩ := check k k_lt
37 exact ⟨n, found⟩
39/-- The kernel's check passes for the nine level-1 supertiles. -/
40theorem level1Chains : ∀ K, (level1 K).chainCheck (ori 1) 8 = true := by
41 intro K; cases K <;> decide +kernel
In the paper Lemma 8.3 Grandparent Lemma
43/-- **Every supertile of level `m ≥ 1` is a disc at its rim.** -/
44theorem chains_super : ∀ m K, 1 ≤ m → (super m K).RimChains (ori m) := by
45 intro m
46 induction m with
47 | zero => intro K one_le_zero; omega
48 | succ m ih =>
49 intro K _
50 rcases Nat.eq_zero_or_pos m with rfl | m_pos
52 · obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
53 -- the children satisfy the bridge's hypotheses
54 have kids := kids_at m_pos K (fun K' => good (m' + 1) K' m_pos)
56 exact kids.rimChains (fun c _ => ih (kidAt K c) m_pos)
58/-! ### Turning about a child vertex by the tables -/
60/-- One step of turning about vertex `j` of child `c` by Table 2 alone, in the sense of `bstep`: for clockwise
61children, across the side that starts at the vertex, to the vertex of the sibling where that side ends; for
62counter-clockwise children, across the side that ends at the vertex, to the vertex of the sibling where it starts. -/
63def tstep (T : Kind) (o : Bool) (x : Nat × Nat) : Option (Nat × Nat) :=
64 if o then adjAt T x.1 ((x.2 + 5) % 6) else (adjAt T x.1 x.2).map fun e => (e.1, (e.2 + 1) % 6)
66/-- `n` such steps. -/
67def tsteps (T : Kind) (o : Bool) : Nat → Nat × Nat → Option (Nat × Nat)
68 | 0, x => some x
69 | n + 1, x => (tstep T o x).bind (tsteps T o n)
In the paper Lemma 8.3 Grandparent Lemma
71/-- In the Δ composition, turning by Table 2 about vertex 0, 1, 4 or 5 of child 1 comes round in three steps, for
72either orientation of the children. -/
73theorem delta_cycles : ∀ o, ∀ j ∈ [0, 1, 4, 5], tsteps .Delta o 3 (1, j) = some (1, j) := by decide
75section Lens
77variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
79/-- The gluing's `mate` at offset `r` in side `j` of child `c`, as Table 2 gives it. -/
80theorem gmate (len_pos : ∀ c j, 1 ≤ L c j) {c j r c' j' : Nat} (c_lt : c < nk T) (j_lt : j < 6) (r_lt : r < L c j)
81 (adj_eq : adjAt T c j = some (c', j')) :
82 (Comp.ofLens T L d ω).toGluing.mate c (pos (L c) j + r) = some (c', pos (L c') j' + L c' j' - 1 - r) := by
83 show (Comp.ofLens T L d ω).mate c (pos (L c) j + r) = _
84 rw [ofLens_mate (fun c _ j _ => len_pos c j) c_lt j_lt r_lt, adj_eq]; rfl
86/-- A side ends no later than the rim. -/
87theorem side_end_le (f : Nat → Nat) {j : Nat} (j_lt : j < 6) : pos f j + f j ≤ pos f 6 := by
88 rw [← pos_succ]; exact pos_mono f (by omega)
90/-- A step by Table 2 is a step of the gluing, at the children's vertices. -/
91theorem tstep_sound (len_pos : ∀ c j, 1 ≤ L c j)
92 (pair : ∀ c, c < nk T → ∀ j, j < 6 → ∀ c' j', adjAt T c j = some (c', j') → L c' j' = L c j) {o : Bool}
93 {c j c' j' : Nat} (c_lt : c < nk T) (j_lt : j < 6) (stepped : tstep T o (c, j) = some (c', j')) :
94 c' < nk T ∧ j' < 6 ∧ bstep (Comp.ofLens T L d ω).toGluing o (c, pos (L c) j) = some (c', pos (L c') j') := by
95 cases o
96 · -- clockwise: across the first edge of side `j`, to the end of the side across
97 simp only [tstep, Bool.false_eq_true, ite_false] at stepped
98 cases adj_eq : adjAt T c j with
99 | none => rw [adj_eq] at stepped; contradiction
100 | some e =>
101 rw [adj_eq] at stepped
102 simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at stepped
103 obtain ⟨rfl, rfl⟩ := stepped
104 obtain ⟨e_lt, e_side_lt, _, _⟩ := adj_valid c_lt j_lt adj_eq
105 refine ⟨e_lt, Nat.mod_lt _ (by omega), ?_⟩
106 -- the first edge of side `j` is glued to the last edge of the side across
107 have mate_eq := gmate (d := d) (ω := ω) len_pos c_lt j_lt (len_pos c j) adj_eq
108 rw [Nat.add_zero, Nat.sub_zero] at mate_eq
109 simp only [bstep, Bool.false_eq_true, ite_false, mate_eq, Option.map_some, ofLens_E e_lt,
110 nxt_last (len_pos e.1) e_side_lt]
111 · -- counter-clockwise: across the last edge of side `j - 1`, to the start of the side across
112 simp only [tstep, ite_true] at stepped
113 -- the side before vertex `j`
114 have prev_lt : (j + 5) % 6 < 6 := Nat.mod_lt _ (by omega)
115 obtain ⟨c'_lt, j'_lt, _, _⟩ := adj_valid c_lt prev_lt stepped
116 refine ⟨c'_lt, j'_lt, ?_⟩
117 -- the side before vertex `j` has an edge
118 have prev_len := len_pos c ((j + 5) % 6)
119 -- the edge before vertex `j` is the last edge of side `j - 1`
120 have before : prv (pos (L c) 6) (pos (L c) j) = pos (L c) ((j + 5) % 6) + (L c ((j + 5) % 6) - 1) := by
121 rcases Nat.eq_zero_or_pos j with rfl | j_pos
122 · -- vertex 0: the edge before it is the last edge of side 5
123 show prv (pos (L c) 6) 0 = pos (L c) 5 + (L c 5 - 1)
124 -- the rim ends where side 5 does
125 have last : pos (L c) 6 = pos (L c) 5 + L c 5 := pos_succ (L c) 5
126 -- side 5 has an edge
127 have len5' := len_pos c 5
128 simp only [prv, ite_true]; omega
129 · -- vertex `j ≥ 1`: the edge before it is the last edge of side `j - 1`
130 obtain ⟨j₀, rfl⟩ : ∃ j₀, j = j₀ + 1 := ⟨j - 1, by omega⟩
131 rw [show (j₀ + 1 + 5) % 6 = j₀ by omega] at prev_len ⊢
132 -- side `j₀` ends at vertex `j₀ + 1`
133 have side_end := pos_succ (L c) j₀
134 simp only [prv]; rw [ite_eq_right (by omega)]; omega
135 -- which is glued to the first edge of the side across
136 have mate_eq := gmate (d := d) (ω := ω) len_pos c_lt prev_lt (r := L c ((j + 5) % 6) - 1) (by omega) stepped
137 rw [pair c c_lt _ prev_lt _ _ stepped] at mate_eq
138 simp only [bstep, ite_true, ofLens_E c_lt, before, mate_eq, Option.some.injEq, Prod.mk.injEq, true_and]
139 omega
141/-- Steps by Table 2 are steps of the gluing, at the children's vertices. -/
142theorem tsteps_sound (len_pos : ∀ c j, 1 ≤ L c j)
143 (pair : ∀ c, c < nk T → ∀ j, j < 6 → ∀ c' j', adjAt T c j = some (c', j') → L c' j' = L c j) {o : Bool} :
144 ∀ n {c j c' j' : Nat}, c < nk T → j < 6 → tsteps T o n (c, j) = some (c', j') →
145 bsteps (Comp.ofLens T L d ω).toGluing o n (c, pos (L c) j) = some (c', pos (L c') j') := by
146 intro n
147 induction n with
148 | zero => intro c j c' j' _ _ stepped; cases stepped; rfl
149 | succ n ih =>
150 intro c j c' j' c_lt j_lt stepped
151 simp only [tsteps] at stepped
152 cases step_eq : tstep T o (c, j) with
153 | none => rw [step_eq] at stepped; contradiction
154 | some y =>
155 rw [step_eq] at stepped
156 obtain ⟨c₁, j₁⟩ := y
157 obtain ⟨c₁_lt, j₁_lt, first⟩ := tstep_sound (d := d) (ω := ω) len_pos pair c_lt j_lt step_eq
158 simp only [bsteps, first, Option.bind_some]
159 exact ih c₁_lt j₁_lt stepped
161/-- **Inside a side, turning comes round in two steps**: about a vertex of child `c` strictly inside a side `j` that
162is glued to a sibling, the gluing turns into the sibling and straight back. -/
163theorem side_cycle (len_pos : ∀ c j, 1 ≤ L c j)
164 (pair : ∀ c, c < nk T → ∀ j, j < 6 → ∀ c' j', adjAt T c j = some (c', j') → L c' j' = L c j) {o : Bool}
165 {c j c' j' r : Nat} (c_lt : c < nk T) (j_lt : j < 6) (adj_eq : adjAt T c j = some (c', j')) (r_pos : 0 < r)
166 (r_lt : r < L c j) :
167 bsteps (Comp.ofLens T L d ω).toGluing o 2 (c, pos (L c) j + r) = some (c, pos (L c) j + r) := by
168 -- the side across has the same length
169 have same_len := pair c c_lt j j_lt c' j' adj_eq
170 obtain ⟨c'_lt, j'_lt, _, back⟩ := adj_valid c_lt j_lt adj_eq
171 -- side `j` ends no later than the rim
172 have end_c := side_end_le (L c) j_lt
173 -- and so does the side across
174 have end_c' := side_end_le (L c') j'_lt
175 cases o
176 · -- clockwise: across the edge leaving the vertex, and back across the edge leaving the next
177 -- the edge leaving the vertex is glued to the side across, `r` edges from its end
178 have first := gmate (d := d) (ω := ω) len_pos c_lt j_lt r_lt adj_eq
179 -- the edge leaving the vertex reached is glued back
180 have second := gmate (d := d) (ω := ω) len_pos c'_lt j'_lt (r := L c j - r) (by omega) back
181 -- the vertex reached
182 have next1 : nxt (pos (L c') 6) (pos (L c') j' + L c' j' - 1 - r) = pos (L c') j' + (L c j - r) := by
183 unfold nxt; rw [ite_eq_right (by omega)]; omega
184 -- and the vertex reached back
185 have next2 : nxt (pos (L c) 6) (pos (L c) j + L c j - 1 - (L c j - r)) = pos (L c) j + r := by
186 unfold nxt; rw [ite_eq_right (by omega)]; omega
187 simp only [bsteps, bstep, Bool.false_eq_true, ite_false, first, Option.map_some, Option.bind_some,
188 ofLens_E c'_lt, next1, second, ofLens_E c_lt, next2]
189 · -- counter-clockwise: across the edge arriving at the vertex, and back across the edge arriving at the next
190 -- the edge before the vertex
191 have prev0 : prv (pos (L c) 6) (pos (L c) j + r) = pos (L c) j + (r - 1) := by
192 unfold prv; rw [ite_eq_right (by omega)]; omega
193 -- is glued to the side across, `r - 1` edges from its end
194 have first := gmate (d := d) (ω := ω) len_pos c_lt j_lt (r := r - 1) (by omega) adj_eq
195 -- the edge before the vertex reached
196 have prev1 : prv (pos (L c') 6) (pos (L c') j' + L c' j' - 1 - (r - 1)) = pos (L c') j' + (L c j - r - 1) := by
197 unfold prv; rw [ite_eq_right (by omega)]; omega
198 -- is glued back
199 have second := gmate (d := d) (ω := ω) len_pos c'_lt j'_lt (r := L c j - r - 1) (by omega) back
200 -- to the edge before the start vertex
201 have back_eq : pos (L c) j + L c j - 1 - (L c j - r - 1) = pos (L c) j + r := by omega
202 simp only [bsteps, bstep, ite_true, ofLens_E c_lt, prev0, first, Option.bind_some, ofLens_E c'_lt, prev1, second,
203 back_eq]
205end Lens
207/-- **About a vertex of child 1 of the Δ composition off its side 2, turning comes round**: in two steps inside a
208side, in three at a vertex (`delta_cycles`). -/
209theorem child1_cycle {L : Nat → Nat → Nat} {d : Nat} {ω o : Bool} (len_pos : ∀ c j, 1 ≤ L c j)
210 (pair : ∀ c, c < nk .Delta → ∀ j, j < 6 → ∀ c' j', adjAt .Delta c j = some (c', j') → L c' j' = L c j)
211 {u : Nat} (u_lt : u < pos (L 1) 6) (off_side2 : u < pos (L 1) 2 ∨ pos (L 1) 3 < u) :
212 ∃ a, 0 < a ∧ bsteps (Comp.ofLens .Delta L d ω).toGluing o a (1, u) = some (1, u) := by
213 obtain ⟨j, r, j_lt, r_lt, rfl⟩ := decomp (L 1) 6 (Nat.le_refl _) u u_lt
214 -- side 2 ends where side 3 starts
215 have side2_end : pos (L 1) 3 = pos (L 1) 2 + L 1 2 := pos_succ (L 1) 2
216 rcases Nat.eq_zero_or_pos r with rfl | r_pos
217 · -- at vertex `j`, which is not 2 or 3 (the ends of side 2): three steps by Table 2
218 have j_mem : j ∈ [0, 1, 4, 5] := by
219 rcases off_side2 with before | after
220 · -- before side 2
221 have j_lt2 : j < 2 := by
222 refine Nat.lt_of_not_le fun two_le => ?_
223 -- vertex `j` is at or after vertex 2
224 have later := pos_mono (L 1) two_le
225 omega
226 simp only [List.mem_cons, List.not_mem_nil, or_false]; omega
227 · -- after side 2
228 have three_lt : 3 < j := by
229 refine Nat.lt_of_not_le fun le_three => ?_
230 -- vertex `j` is at or before vertex 3
231 have earlier := pos_mono (L 1) le_three
232 omega
233 simp only [List.mem_cons, List.not_mem_nil, or_false]; omega
234 refine ⟨3, by omega, ?_⟩
235 rw [Nat.add_zero]
236 exact tsteps_sound len_pos pair 3 (by decide) j_lt (delta_cycles o j j_mem)
237 · -- inside side `j`, which is not side 2: two steps
238 have j_ne : j ≠ 2 := by
239 intro j_two; subst j_two; rcases off_side2 with before | after <;> omega
240 cases adj_eq : adjAt .Delta 1 j with
241 | none => exact absurd (adj_one_none j j_lt adj_eq) j_ne
242 | some e => exact ⟨2, by omega, side_cycle len_pos pair (by decide) j_lt adj_eq r_pos r_lt⟩
244/-- **Inside side 4 of child 1 of the Δ composition** (glued to child 3), turning comes round in two steps. -/
245theorem side4_cycle {L : Nat → Nat → Nat} {d : Nat} {ω o : Bool} (len_pos : ∀ c j, 1 ≤ L c j)
246 (pair : ∀ c, c < nk .Delta → ∀ j, j < 6 → ∀ c' j', adjAt .Delta c j = some (c', j') → L c' j' = L c j)
247 {v : Nat} (after_start : pos (L 1) 4 < v) (before_end : v < pos (L 1) 5) :
248 bsteps (Comp.ofLens .Delta L d ω).toGluing o 2 (1, v) = some (1, v) := by
249 obtain ⟨r, rfl⟩ : ∃ r, v = pos (L 1) 4 + r := ⟨v - pos (L 1) 4, by omega⟩
250 -- side 4 ends where side 5 starts
251 have side4_end : pos (L 1) 5 = pos (L 1) 4 + L 1 4 := pos_succ (L 1) 4
252 exact side_cycle len_pos pair (c' := 3) (j' := 0) (by decide) (by omega) (by decide) (by omega) (by omega)
254/-! ### The nest -/
256/-- The children of `N_{m+1}` are discs at their rims. -/
257theorem kidsD_chains {m : Nat} (m_pos : 1 ≤ m) : ∀ c, c < nk .Delta → (kidsD m c).RimChains (ori m) :=
258 fun c _ => chains_super m (kidAt .Delta c) m_pos
260/-- Corner `x` of `N_m`, as a corner of `N_{m+1}`. -/
261abbrev upC (m : Nat) (x : Nat × Nat) : Nat × Nat := (up m 1 x.1, x.2)
263/-- Turning in `N_m` is turning in `N_{m+1}`. -/
264theorem turns_up {m : Nat} (m_pos : 1 ≤ m) (n : Nat) {x y : Nat × Nat} (x_tile : x.1 < (N m).tiles)
265 (turned : (N m).turns n x = some y) : (N (m + 1)).turns n (upC m x) = some (upC m y) := by
266 rw [N_succ m_pos]
267 exact (KD m_pos).turns_lift (c := 1) (by decide) n x_tile turned
269/-- A vertex surrounded in `N_m` is surrounded in `N_{m+1}`. -/
270theorem surrounded_up {m : Nat} (m_pos : 1 ≤ m) {t i : Nat} (t_lt : t < (N m).tiles)
271 (surrounded : (N m).Surrounded t i) : (N (m + 1)).Surrounded (up m 1 t) i := by
272 obtain ⟨n, n_pos, round⟩ := surrounded
273 exact ⟨n, n_pos, turns_up m_pos n (x := (t, i)) t_lt round⟩
275/-- **Off its side 2, `N_m` lies inside `N_{m+1}`**: a corner on the chain about a rim vertex of `N_m` that is not on
276the closed side 2 is surrounded in `N_{m+1}`. -/
277theorem surrounded_off_side2 {m : Nat} (m_pos : 1 ≤ m) {u n : Nat} {x : Nat × Nat} (u_lt : u < (N m).E)
278 (off_side2 : u < pos (Lk m .Delta 1) 2 ∨ pos (Lk m .Delta 1) 3 < u)
279 (on_chain : (N m).turns n ((N m).sC (ori m) u) = some x) : (N (m + 1)).Surrounded (up m 1 x.1) x.2 := by
280 -- the children of `N_{m+1}`
281 have kids := KD m_pos
282 -- the rim of `N_m`
283 have rim_len := E_N m_pos
284 obtain ⟨a, a_pos, cycle⟩ := child1_cycle (d := dOff m) (ω := ori m) (o := ori m) kids.len_pos kids.pair
285 (by rw [← rim_len]; exact u_lt) off_side2
286 rw [N_succ m_pos]
287 exact kids.surrounded_of_cycle (kidsD_chains m_pos) (c := 1) (by decide) u_lt a_pos cycle on_chain
289/-- **Around side 4 of `N_m`, `N_m` lies inside `N_{m+1}`**: a corner on the chain about a rim vertex well inside
290side 4 of `N_m` (which child 1's side 4, glued to child 3, is) is surrounded in `N_{m+1}`. -/
291theorem surrounded_side4 {m : Nat} (m_pos : 1 ≤ m) {v n : Nat} {x : Nat × Nat} (inside : Inside m 4 v)
292 (on_chain : (N m).turns n ((N m).sC (ori m) v) = some x) : (N (m + 1)).Surrounded (up m 1 x.1) x.2 := by
293 -- the children of `N_{m+1}`
294 have kids := KD m_pos
295 -- the rim of `N_m`
296 have rim_len := E_N m_pos
297 -- `v` lies two edges inside side 4
298 have after_start := inside.1
299 -- and two before its end
300 have before_end : v + 2 ≤ pos (Lk m .Delta 1) 5 := inside.2
301 -- which is no later than the rim
302 have five_le := pos_mono (Lk m .Delta 1) (show 5 ≤ 6 by omega)
303 -- turning about `v` comes round in two steps
304 have cycle := side4_cycle (d := dOff m) (ω := ori m) (o := ori m) kids.len_pos kids.pair (v := v) (by omega)
305 (by omega)
306 rw [N_succ m_pos]
307 exact kids.surrounded_of_cycle (kidsD_chains m_pos) (c := 1) (by decide)
308 (show v < (N m).E by rw [rim_len]; omega) (by omega) cycle on_chain
310/-- **Strictly inside side 2 of `N_m`** (on the rim of `N_{m+1}`): the chain about rim vertex `u` of `N_m` is, one
311level up, the chain about rim vertex `stp u` of `N_{m+1}`, or its start. -/
312theorem chain_stretch {m : Nat} (m_pos : 1 ≤ m) {u n : Nat} {x : Nat × Nat} (after_two : pos (Lk m .Delta 1) 2 < u)
313 (before_three : u < pos (Lk m .Delta 1) 3) (on_chain : (N m).turns n ((N m).sC (ori m) u) = some x) :
314 (N (m + 1)).turns n ((N (m + 1)).sC (ori (m + 1)) (stp (Lk m .Delta) u)) = some (upC m x) := by
315 -- the rim of `N_m`
316 have rim_len := E_N m_pos
317 -- vertex 3 is no later than the rim
318 have three_le := pos_mono (Lk m .Delta 1) (show 3 ≤ 6 by omega)
319 -- the start of the chain, one level up
320 have start : (N (m + 1)).sC (ori (m + 1)) (stp (Lk m .Delta) u) = upC m ((N m).sC (ori m) u) := by
321 -- the rim port of `N_m` there is, one level up, the rim port of `N_{m+1}`
322 have same_port := stretch_eq m_pos after_two before_three (ori m)
323 rw [← ori_succ] at same_port
324 show Patch.corner ((N (m + 1)).bport (ori (m + 1)) (stp (Lk m .Delta) u, ori (m + 1))) = _
325 rw [← same_port]; rfl
326 rw [start]
327 exact turns_up m_pos n (Patch.sC_valid (good m .Delta m_pos).sig (show u < (N m).E by rw [rim_len]; omega)).1
328 on_chain
330/-- Junction `q` of `N_{m+1}` is a rim position. -/
331theorem junction_lt {m q : Nat} (m_pos : 1 ≤ m) (q_lt : q < 22) : jpos (Lk m .Delta) q < rimN .Delta (Lk m .Delta) := by
332 -- the pieces from `q` to the end
333 have spread := jpos_le (Lk m .Delta) (len5 m_pos) (q := q) (q' := 22) (by omega) (Nat.le_refl _)
334 rw [jpos_full] at spread
335 omega
337/-- **At vertex 3 of `N_m`**, an end of its side 2: a corner on the chain about it is, one level up, on the chain
338about junction 16 of `N_{m+1}`. -/
339theorem chain_j16 {m : Nat} (m_pos : 1 ≤ m) {n : Nat} {x : Nat × Nat}
340 (on_chain : (N m).turns n ((N m).sC (ori m) (pos (Lk m .Delta 1) 3)) = some x) :
341 ∃ n', (N (m + 1)).turns n' ((N (m + 1)).sC (ori (m + 1)) (jpos (Lk m .Delta) 16)) = some (upC m x) := by
342 -- the children of `N_{m+1}`
343 have kids := KD m_pos
344 -- the parent's chain starts at vertex 1 of child 2, or at vertex 3 of child 1
345 have start : vS .Delta (Lk m .Delta) (dOff m) (ori m) (ori m) (jpos (Lk m .Delta) 16) =
346 if ori m then (2, pos (Lk m .Delta 2) 1) else (1, pos (Lk m .Delta 1) 3) := by
347 simp only [vS, gR_jpos m_pos (show 16 < 22 by omega), gL_jpos m_pos (show 1 ≤ 16 by omega) (show 16 < 22 by omega)]
348 rfl
349 -- from there, the gluing reaches vertex 3 of child 1 in at most one step
350 have path : ∃ a, bsteps (Comp.ofLens .Delta (Lk m .Delta) (dOff m) (ori m)).toGluing (ori m) a
351 (vS .Delta (Lk m .Delta) (dOff m) (ori m) (ori m) (jpos (Lk m .Delta) 16)) = some (1, pos (Lk m .Delta 1) 3) := by
352 rw [start]
353 cases ori m
354 · exact ⟨0, rfl⟩
355 · exact ⟨1, tsteps_sound kids.len_pos kids.pair 1 (by decide) (by decide) (by decide)⟩
356 obtain ⟨a, path⟩ := path
357 rw [N_succ m_pos, ori_succ]
358 exact kids.on_parent_chain (kidsD_chains m_pos) (junction_lt m_pos (by omega)) path on_chain
360/-- **At vertex 2 of `N_m`**, the other end of its side 2: a corner on the chain about it is, one level up, on the chain
361about junction 17 of `N_{m+1}`. -/
362theorem chain_j17 {m : Nat} (m_pos : 1 ≤ m) {n : Nat} {x : Nat × Nat}
363 (on_chain : (N m).turns n ((N m).sC (ori m) (pos (Lk m .Delta 1) 2)) = some x) :
364 ∃ n', (N (m + 1)).turns n' ((N (m + 1)).sC (ori (m + 1)) (jpos (Lk m .Delta) 17)) = some (upC m x) := by
365 -- the children of `N_{m+1}`
366 have kids := KD m_pos
367 -- the parent's chain starts at vertex 2 of child 1, or at vertex 5 of child 0
368 have start : vS .Delta (Lk m .Delta) (dOff m) (ori m) (ori m) (jpos (Lk m .Delta) 17) =
369 if ori m then (1, pos (Lk m .Delta 1) 2) else (0, pos (Lk m .Delta 0) 5) := by
370 simp only [vS, gR_jpos m_pos (show 17 < 22 by omega), gL_jpos m_pos (show 1 ≤ 17 by omega) (show 17 < 22 by omega)]
371 rfl
372 -- from there, the gluing reaches vertex 2 of child 1 in at most one step
373 have path : ∃ a, bsteps (Comp.ofLens .Delta (Lk m .Delta) (dOff m) (ori m)).toGluing (ori m) a
374 (vS .Delta (Lk m .Delta) (dOff m) (ori m) (ori m) (jpos (Lk m .Delta) 17)) = some (1, pos (Lk m .Delta 1) 2) := by
375 rw [start]
376 cases ori m
377 · exact ⟨1, tsteps_sound kids.len_pos kids.pair 1 (by decide) (by decide) (by decide)⟩
378 · exact ⟨0, rfl⟩
379 obtain ⟨a, path⟩ := path
380 rw [N_succ m_pos, ori_succ]
381 exact kids.on_parent_chain (kidsD_chains m_pos) (junction_lt m_pos (by omega)) path on_chain
383/-! ### A negative control -/
385/-- **Negative control**: in a patch with the signature, no vertex on the rim is surrounded (the corner where the chain
386about a rim vertex ends looks across a rim edge). So "surrounded" is not built into the definitions. -/
387theorem rim_not_surrounded {P : Patch} {o : Bool} {A B : Nat} (sig : P.HasSig o A B) {k : Nat} (k_lt : k < P.E) :
388 ¬ P.Surrounded (P.fC o k).1 (P.fC o k).2 := by
389 rintro ⟨n, n_pos, round⟩
390 obtain ⟨n', rfl⟩ : ∃ n', n = n' + 1 := ⟨n - 1, by omega⟩
391 -- the corner looks across a rim edge
392 have on_rim : P.turn ((P.fC o k).1, (P.fC o k).2) = none := by
393 cases o
394 · -- clockwise: across rim edge `k`
395 obtain ⟨_, i_lt, unglued⟩ := sig.rim_ok k k_lt
396 show P.glue (P.edgeAt k).1 ((((P.edgeAt k).2 + 1) % 14 + 13) % 14) = none
397 rw [mod14 i_lt]; exact unglued
398 · -- counter-clockwise: across rim edge `k - 1`
399 obtain ⟨_, i_lt, unglued⟩ := sig.rim_ok _ (prv_lt k_lt)
400 show P.glue (P.edgeAt (prv P.E k)).1 ((((P.edgeAt (prv P.E k)).2 + 1) % 14 + 13) % 14) = none
401 rw [mod14 i_lt]; exact unglued
402 simp only [Patch.turns, on_rim, Option.bind_none, reduceCtorEq] at round
404/-! ### The theorem -/
In the paper Lemma 8.3 Grandparent Lemma
406/-- **The Grandparent Lemma** (as stated in `Statement.lean`). -/
407theorem grandparent : Grandparent := by
408 intro b b_pos t i t_lt i_lt
409 -- `N_b` has the signature
410 have good_b := good b .Delta b_pos
411 -- one level up, the tile is a tile of `N_{b+1}`
412 have t_up : up b 1 t < (N (b + 1)).tiles := (isPort_up b_pos (x := (t, i, true)) ⟨t_lt, i_lt⟩).1
413 rw [show up b 2 t = up (b + 1) 1 (up b 1 t) from up_succ 1 b t]
414 rcases Patch.surrounded_or_chain good_b.sig (super_glueSymm b .Delta) t_lt i_lt with
415 surrounded | ⟨u, u_lt, n, on_chain⟩
416 · -- surrounded in `N_b` already
417 exact surrounded_up (by omega) t_up (surrounded_up b_pos t_lt surrounded)
418 · -- on the chain about rim vertex `u` of `N_b`
419 -- side 2 ends where side 3 starts
420 have side2_end : pos (Lk b .Delta 1) 3 = pos (Lk b .Delta 1) 2 + Lk b .Delta 1 2 := pos_succ (Lk b .Delta 1) 2
421 by_cases off_side2 : u < pos (Lk b .Delta 1) 2 ∨ pos (Lk b .Delta 1) 3 < u
422 · -- off the closed side 2: surrounded in `N_{b+1}`
423 exact surrounded_up (by omega) t_up (surrounded_off_side2 b_pos u_lt off_side2 on_chain)
424 · -- on the closed side 2: on a chain of `N_{b+1}` about a vertex well inside its side 4
425 rcases (show u = pos (Lk b .Delta 1) 2 ∨ (pos (Lk b .Delta 1) 2 < u ∧ u < pos (Lk b .Delta 1) 3) ∨
426 u = pos (Lk b .Delta 1) 3 by omega) with at_two | inside | at_three
427 · -- vertex 2: junction 17 of `N_{b+1}`
428 subst at_two
429 obtain ⟨n', up_chain⟩ := chain_j17 b_pos on_chain
430 exact surrounded_side4 (by omega) (inside_17 b_pos) up_chain
431 · -- strictly inside: the rim vertex `stp u` of `N_{b+1}`
432 exact surrounded_side4 (by omega) (inside_stp b_pos inside.1 inside.2)
433 (chain_stretch b_pos inside.1 inside.2 on_chain)
434 · -- vertex 3: junction 16 of `N_{b+1}`
435 subst at_three
436 obtain ⟨n', up_chain⟩ := chain_j16 b_pos on_chain
437 exact surrounded_side4 (by omega) (inside_16 b_pos) up_chain
439/-! ### The Signature Theorem -/
In the paper Theorem 7.6 Signature Theorem
441/-- **The Signature Theorem** (the claim `SignatureTheorem` of `Statement.lean`, the paper's Thm 7.6): the induction's
442conclusion `good` and `chains_super`, with the corners written out as the claim writes them. -/
444 intro m K m_pos
445 -- the induction's conclusion at level `m`
446 have good_m := good m K m_pos
447 -- the claim's `A` is the induction's: d_m = 2 F_{3m+1} (Lemma 6.4)
448 have a_eq := cornerA_eq_aPos m_pos K
449 -- and so is its `B`
450 have b_eq : cornerB m K = bPos m K := by
452 rw [a_eq, good_m.len]
453 by_cases even : m % 2 = 0 <;> simp [even]
454 -- vertex 6, the end of the rim, is one side 5 after vertex 5
455 have v6 : vpos m K 6 = vpos m K 5 + lenAt m K 5 := pos_succ (lenAt m K) 5
456 -- every side has at least 5 edges, and the Σ corner lies at least 4 edges before the end of side 5 (Lemma 6.5)
457 have bnd := bounds m m_pos
458 -- `A` is a rim vertex
459 have a_lt : aPos m K < (super m K).E := by
460 rw [good_m.len, v6]
461 unfold aPos
462 by_cases is_sigma : K = .Sigma
463 · subst is_sigma
464 -- side 5 of a Σ is a δ side
465 have side5 : lenAt m .Sigma 5 = letterLen m .delta := rfl
466 rw [ite_eq_left rfl, side5]
467 omega
468 · -- side 5 has at least 5 edges
469 have side5 : 5 ≤ lenAt m K 5 := bnd.1 (letterOf K 5)
470 rw [ite_eq_right is_sigma]
471 omega
472 rw [a_eq, b_eq]
473 exact ⟨a_lt, chains_super m K m_pos, good_m.sig⟩
475end SpectreKnot.Statement

← SpectreKnot/ProofExact.leanSpectreKnot/Basic.lean →