lean/SpectreKnot/ProofExact.lean
420 lines · 25 declarations, each with its own page · on GitHub ·
The bound is exact (theoremB_exact, the last two rows of the paper's Table 5): for b ≥ 1, the ports of N_b lie on exactly two strands of N_{b+2}, and, if b is odd, on exactly two strands of N_{b+3}.
← SpectreKnot/ProofChain.leanSpectreKnot/ProofGrand.lean →
All 39 files, and the declarations of this one
1/-
2**The bound is exact** (`theoremB_exact`, the last two rows of the paper's Table 5): for `b ≥ 1`, the ports of `N_b`
3lie on exactly two strands of `N_{b+2}`, and, if `b` is odd, on exactly two strands of `N_{b+3}`.
5The paper's argument (the end of its proof of Thm 9.1), at tile level. Following the junction map as `ProofB.lean`
6does, every strand of `N_b` reaches one of two hooks of `N_{b+2}` (and, for odd `b`, of `N_{b+3}`), and each of the two
7is reached, from a hook well inside one of two chosen sides of `N_b`. Hooks at different rim vertices lie on different
8strands (`hooks_apart`): along a strand its two ends on the rim stay the same (`Linked.ends`), and the ends of a hook's
9strand are the hook's own two ports.
10-/
11import SpectreKnot.ProofB
13namespace SpectreKnot.Statement
15open Pattern Compose Gluing
17/-! ### A strand is determined by its ends -/
19namespace Patch
23/-- Following a ribbon has one result. -/
24theorem Follow.unique {p r r' : Port} (follows : P.Follow p r) (follows' : P.Follow p r') : r = r' := by
25 induction follows generalizing r' with
26 | leave leaves =>
27 cases follows' with
28 | leave _ => rfl
29 | next crosses _ => rw [leaves] at crosses; contradiction
30 | next crosses _ ih =>
31 cases follows' with
32 | leave leaves => rw [crosses] at leaves; contradiction
33 | next crosses' rest' =>
34 rw [crosses] at crosses'
35 cases crosses'
36 exact ih rest'
38/-- **The two ends of the strand through port `q`**: following the ribbon from `q` (along its piece first) leaves the
39patch at `a`; going the other way (across `q`'s edge first) it leaves at `b`, which is `q` itself if `q` is on the
40rim. -/
42 P.Follow q a ∧ ((P.across q = none ∧ b = q) ∨ ∃ q', P.across q = some q' ∧ P.Follow q' b)
44/-- A port has one pair of ends. -/
45theorem Ends.unique {q a b a' b' : Port} (ends : P.Ends q a b) (ends' : P.Ends q a' b') : a = a' ∧ b = b' := by
46 refine ⟨ends.1.unique ends'.1, ?_⟩
47 rcases ends.2 with ⟨on_rim, rfl⟩ | ⟨q₁, crosses, follows⟩ <;>
48 rcases ends'.2 with ⟨on_rim', rfl⟩ | ⟨q₁', crosses', follows'⟩
49 · rfl
50 · rw [on_rim] at crosses'; contradiction
51 · rw [crosses] at on_rim'; contradiction
52 · rw [crosses] at crosses'
53 cases crosses'
54 exact follows.unique follows'
56/-- Seen from the other end of `q`'s piece, the ends are the same, the other way round. -/
57theorem Ends.piece {q a b : Port} (ends : P.Ends q a b) : P.Ends (pieceEnd q) b a := by
58 obtain ⟨follows, beyond⟩ := ends
59 refine ⟨?_, ?_⟩
60 · rcases beyond with ⟨on_rim, b_eq⟩ | ⟨q₁, crosses, follows₁⟩
61 · -- `q` is on the rim: from the other end, the ribbon runs along the piece and leaves at `q`
62 have leave := Follow.leave (P := P) (p := pieceEnd q) (by rw [pieceEnd_pieceEnd]; exact on_rim)
63 rw [b_eq]
64 rwa [pieceEnd_pieceEnd] at leave
65 · -- from the other end, the ribbon runs along the piece, across `q`'s edge, and on to `b`
66 exact .next (by rw [pieceEnd_pieceEnd]; exact crosses) follows₁
67 · -- across the edge at the other end is where following the ribbon from `q` goes
68 cases follows with
69 | leave leaves => exact .inl ⟨leaves, rfl⟩
70 | next crosses rest => exact .inr ⟨_, crosses, rest⟩
72/-- Seen from across `q`'s edge, the ends are the same, the other way round. -/
74 (back : P.across q' = some q) : P.Ends q' b a := by
75 obtain ⟨follows, beyond⟩ := ends
76 refine ⟨?_, .inr ⟨q, back, follows⟩⟩
77 rcases beyond with ⟨on_rim, _⟩ | ⟨q₁, crosses, follows₁⟩
78 · rw [across_eq] at on_rim; contradiction
79 · rw [across_eq] at crosses
80 cases crosses
81 exact follows₁
83/-- **Along a strand, its ends stay the same** (in a patch with the signature and symmetric gluing, where every move
84along a strand can be undone): if `q` is on the strand of `p`, the ends seen from `q` are those seen from `p`, one way
85round or the other. -/
86theorem Linked.ends {o : Bool} {A B : Nat} (sig : P.HasSig o A B) (symm : P.GlueSymm) {p q a b : Port}
87 (linked : P.Linked p q) (p_port : P.IsPort p) (ends : P.Ends p a b) : P.Ends q a b ∨ P.Ends q b a := by
88 induction linked with
89 | refl => exact .inl ends
90 | piece _ ih =>
91 rcases ih with same | swapped
92 · exact .inr same.piece
93 · exact .inl swapped.piece
94 | edge to_q across_eq ih =>
95 -- the edge can be crossed back
96 have back := across_symm sig symm (to_q.valid sig p_port) across_eq
97 rcases ih with same | swapped
98 · exact .inr (same.edge across_eq back)
99 · exact .inl (swapped.edge across_eq back)
101/-- Nothing lies across a rim port. -/
102theorem across_bport {o : Bool} {A B : Nat} (sig : P.HasSig o A B) {k : Nat} (k_lt : k < P.E) (s : Bool) :
103 P.across (P.bport o (k, s)) = none := by
104 cases s with
105 | true =>
106 obtain ⟨_, i_lt, unglued⟩ := sig.rim_ok k k_lt
107 cases o <;> simp only [bport, across, straightThrough, ite_true, ite_false, Bool.false_eq_true, mod14 i_lt, unglued,
108 Option.map_none]
109 | false =>
111 cases o <;> simp only [bport, across, straightThrough, ite_true, ite_false, Bool.false_eq_true, mod14 i_lt, unglued,
112 Option.map_none]
114/-- A rim port is a port of an actual tile. -/
115theorem bport_isPort {o : Bool} {A B : Nat} (sig : P.HasSig o A B) {k : Nat} (k_lt : k < P.E) (s : Bool) :
116 P.IsPort (P.bport o (k, s)) := by
117 cases s with
118 | true =>
119 obtain ⟨t_lt, i_lt, _⟩ := sig.rim_ok k k_lt
120 cases o <;> exact ⟨t_lt, by simp only [bport]; first | exact i_lt | exact Nat.mod_lt _ (by omega)⟩
121 | false =>
123 cases o <;> exact ⟨t_lt, by simp only [bport]; first | exact i_lt | exact Nat.mod_lt _ (by omega)⟩
125/-- Different rim ports are different ports. -/
126theorem bport_inj {o : Bool} {A B : Nat} (sig : P.HasSig o A B) {k k' : Nat} (k_lt : k < P.E) (k_lt' : k' < P.E)
127 {s s' : Bool} (same : P.bport o (k, s) = P.bport o (k', s')) : k = k' ∧ s = s' := by
128 -- the rim edges at the two positions are actual edges
129 obtain ⟨_, i_lt, _⟩ := sig.rim_ok k k_lt
130 -- (the second)
131 obtain ⟨_, i_lt', _⟩ := sig.rim_ok k' k_lt'
132 -- and so are those before them
134 -- (the second)
136 -- the same edge at two rim positions: the same position
137 have at_same : ∀ x y, x < P.E → y < P.E → (P.edgeAt x).1 = (P.edgeAt y).1 → (P.edgeAt x).2 = (P.edgeAt y).2 →
138 x = y := fun x y x_lt y_lt same_tile same_edge => sig.rim_inj x y x_lt y_lt (Prod.ext same_tile same_edge)
139 cases o <;> cases s <;> cases s' <;>
140 simp only [bport, ite_true, ite_false, Bool.false_eq_true, Prod.mk.injEq, reduceCtorEq, and_false,
141 and_true] at same ⊢
143 · exact at_same _ _ k_lt k_lt' same.1 (by omega)
145 · exact at_same _ _ k_lt k_lt' same.1 same.2
147end Patch
149/-! ### Hooks at different vertices lie on different strands -/
151/-- The port `R` at rim vertex `v` of `N_m`, a port of the hook there. -/
154/-- At a rim vertex of `N_m` other than the corners, the strand of the hook ends at the vertex's two ports. -/
155theorem hook_ends {m : Nat} (m_pos : 1 ≤ m) {v : Nat} (two_le_v : 2 ≤ v) (v_le : v + 2 ≤ pos (Lk m .Delta 1) 6) :
157 -- `N_m` has the signature
159 -- with corners `0` and `1` or `E - 1`
161 -- and its rim length
164 -- from `R(v)` the ribbon leads to the port the signature pairs it with
165 have follows := good_m.sig.sig v true (by rw [rim_len]; omega)
166 -- which is `L(v)`, since `v` is not a corner
169 rw [ite_eq_right (by omega), ite_eq_right (by omega)]; rfl
170 rw [paired] at follows
171 exact ⟨follows, .inl ⟨Patch.across_bport good_m.sig (by rw [rim_len]; omega) true, rfl⟩⟩
173/-- **Hooks at different rim vertices of `N_m` (other than the corners) lie on different strands.** -/
174theorem hooks_apart {m : Nat} (m_pos : 1 ≤ m) {v w : Nat} (two_le_v : 2 ≤ v) (v_le : v + 2 ≤ pos (Lk m .Delta 1) 6)
177 intro linked
178 -- `N_m` has the signature
180 -- and its rim length
183 -- seen from `R(w)`, the ends are those of the hook at `v`, one way round or the other
184 have ends_v := linked.ends good_m.sig (super_glueSymm m .Delta)
185 (Patch.bport_isPort good_m.sig (by rw [rim_len]; omega) true) (hook_ends m_pos two_le_v v_le)
186 -- but they are those of the hook at `w`
188 rcases ends_v with same | swapped
189 · -- the same way round: `R(v) = R(w)`
190 have equal := (same.unique ends_w).2
191 exact v_ne_w (Patch.bport_inj good_m.sig (by rw [rim_len]; omega) (by rw [rim_len]; omega) equal).1
192 · -- the other way round: `R(v) = L(w)`
193 have equal := (swapped.unique ends_w).1
194 exact absurd (Patch.bport_inj good_m.sig (by rw [rim_len]; omega) (by rw [rim_len]; omega) equal).2
195 (by decide)
197/-- **Two strands, from two hooks**: if every port of `N_b` lies, in `N_{b+k}`, on the strand of the hook at `vA` or
198of the hook at `vB` (two different rim vertices, not corners), and some port of `N_b` lies on each, then the ports of
199`N_b` lie on exactly two strands of `N_{b+k}`. -/
200theorem twoStrands_of {b k vA vB : Nat} (b_pos : 1 ≤ b) (two_le_vA : 2 ≤ vA)
201 (vA_le : vA + 2 ≤ pos (Lk (b + k) .Delta 1) 6) (two_le_vB : 2 ≤ vB) (vB_le : vB + 2 ≤ pos (Lk (b + k) .Delta 1) 6)
206 (N (b + k)).Linked (upPort b k x) (hookAt (b + k) vA) ∨ (N (b + k)).Linked (upPort b k x) (hookAt (b + k) vB)) :
207 TwoStrands b k := by
208 -- the level `b + k` is at least 1
209 have level_pos : 1 ≤ b + k := by omega
210 -- back from the hook at `vA` to `pA`
211 have from_A := linked_symm (m := b + k) level_pos to_A (isPort_upk b_pos pA_port k)
212 -- and from the hook at `vB` to `pB`
213 have from_B := linked_symm (m := b + k) level_pos to_B (isPort_upk b_pos pB_port k)
214 refine ⟨pA, pB, pA_port, pB_port, fun linked => ?_, fun x x_port => ?_⟩
215 · -- `pA` and `pB` on one strand would put the two hooks on one strand
216 exact hooks_apart level_pos two_le_vA vA_le two_le_vB vB_le vA_ne_vB (from_A.trans (linked.trans to_B))
217 · rcases to_either x x_port with to_vA | to_vB
218 · exact .inl (to_vA.trans from_A)
219 · exact .inr (to_vB.trans from_B)
221/-! ### Hooks well inside a side -/
223/-- A rim vertex well inside side `J` of `N_n`: two edges after the side's start. -/
224theorem inside_two {n J : Nat} (n_pos : 1 ≤ n) : Inside n J (pos (Lk n .Delta 1) J + 2) := by
225 -- side `J` has at least 5 edges
227 -- and ends where side `J + 1` starts
229 exact ⟨Nat.le_refl _, by omega⟩
231/-- The hook port at a vertex inside a side of `N_n` is a port of `N_n`. -/
232theorem hook_port {n J v : Nat} (n_pos : 1 ≤ n) (hJ : J < 6) (inside : Inside n J v) : (N n).IsPort (hookAt n v) := by
233 -- `v` is a rim vertex away from the corners
234 have bounds := inside_bounds hJ inside
235 -- of a rim of this length
238 exact Patch.bport_isPort (good n .Delta n_pos).sig (by rw [rim_len]; omega) true
240/-- The hook at a vertex `u` strictly inside child 1's side 2 lies at a different vertex of `N_{n+1}` from junction
24116 (where that side ends), and both lie well inside side 4 of `N_{n+1}`. -/
247 refine ⟨inside_bounds (by omega) (inside_16 n_pos),
248 inside_bounds (by omega) (inside_stp n_pos (by omega) (by omega)), ?_⟩
251/-! ### Even `b` -/
253/-- **Even `b`, two levels up**: every port of `N_b` lies, in `N_{b+2}`, on the strand of the hook at junction 16, or
254on that of the hook at junction 9 of `N_{b+1}`, which lies on the rim of `N_{b+2}`. -/
255theorem even_two {b : Nat} (b_pos : 1 ≤ b) (even : b % 2 = 0) {x : Port} (x_port : (N b).IsPort x) :
257 (N (b + 2)).Linked (upPort b 2 x) (hookAt (b + 2) (stp (Lk (b + 1) .Delta) (jpos (Lk b .Delta) 9))) := by
258 -- level `b` is even
260 -- level `b + 1` odd
262 -- one level up: inside side 2 (at junction 9), 3 or 4
263 obtain ⟨J, reach_J, sides_even, _, at_nine⟩ := first b_pos x_port
264 rw [show upPort b 2 x = upPort (b + 1) 1 (upPort b 1 x) from upPort_succ b 1 x]
265 rcases sides_even ori_b with rfl | rfl | rfl
266 · -- inside side 2, at junction 9: a hook of `N_{b+1}` on the rim of `N_{b+2}`
267 exact .inr ((lift_nest (m := b + 1) (by omega) (at_nine rfl) reach_J.1).trans (adv_none (by omega) (inside_9 b_pos)))
268 · -- inside side 3: on to junction 16
269 exact .inl (reach_some (q := 16) (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
270 · -- inside side 4: on to junction 16
271 exact .inl (reach_some (q := 16) (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
273/-- **Even `b`**: the ports of `N_b` lie on exactly two strands of `N_{b+2}`. -/
274theorem two_even {b : Nat} (b_pos : 1 ≤ b) (even : b % 2 = 0) : TwoStrands b 2 := by
275 -- level `b` is even
277 -- level `b + 1` odd
279 -- junction 9 of `N_{b+1}` lies well inside its side 2
281 -- (its end)
283 -- the two hooks of `N_{b+2}`: different, and away from the corners
284 obtain ⟨⟨two_le_A, A_le⟩, ⟨two_le_B, B_le⟩, A_ne_B⟩ := stp_apart (n := b + 1) (by omega) nine_start nine_end
285 -- a hook well inside side 4 of `N_b`
286 have inside_A := inside_two (n := b) (J := 4) b_pos
287 -- and one well inside side 5
288 have inside_B := inside_two (n := b) (J := 5) b_pos
289 -- one level up, the first reaches junction 12, inside side 3 of `N_{b+1}`
291 -- and the second junction 9, inside side 2
293 refine twoStrands_of b_pos two_le_A A_le two_le_B B_le A_ne_B (hook_port b_pos (by omega) inside_A)
295 · -- two levels up, the first reaches junction 16
296 rw [show upPort b 2 (hookAt b _) = upPort (b + 1) 1 (upPort b 1 (hookAt b _)) from upPort_succ b 1 _]
297 exact reach_some (q := 16) (by omega) (by omega)
298 ⟨isPort_up b_pos (hook_port b_pos (by omega) inside_A), _, inside_12 b_pos, A_one⟩ (by rw [ori_b1]; rfl)
299 · -- and the second the hook at junction 9 of `N_{b+1}`
300 rw [show upPort b 2 (hookAt b _) = upPort (b + 1) 1 (upPort b 1 (hookAt b _)) from upPort_succ b 1 _]
301 exact (lift_nest (m := b + 1) (by omega) B_one (isPort_up b_pos (hook_port b_pos (by omega) inside_B))).trans
304/-! ### Odd `b` -/
306/-- **Odd `b`, two levels up**: every port of `N_b` lies, in `N_{b+2}`, on the strand of the hook at junction 12 or
307of the hook at junction 9. -/
308theorem odd_two {b : Nat} (b_pos : 1 ≤ b) (odd : b % 2 = 1) {x : Port} (x_port : (N b).IsPort x) :
311 -- level `b` is odd
313 -- level `b + 1` even
315 -- one level up: inside side 4 or 5
316 obtain ⟨J, reach_J, _, sides_odd, _⟩ := first b_pos x_port
317 rw [show upPort b 2 x = upPort (b + 1) 1 (upPort b 1 x) from upPort_succ b 1 x]
318 rcases sides_odd ori_b with rfl | rfl
319 · -- inside side 4: on to junction 12
320 exact .inl (reach_some (q := 12) (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
321 · -- inside side 5: on to junction 9
322 exact .inr (reach_some (q := 9) (by omega) (by omega) reach_J (by rw [ori_b1]; rfl))
324/-- Odd `b`, from two levels up to three: the strand of the hook at junction 12 of `N_{b+2}` runs on to the hook at
325junction 16 of `N_{b+3}`. -/
326theorem odd_up_12 {b : Nat} (b_pos : 1 ≤ b) (odd : b % 2 = 1) {x : Port} (x_port : (N b).IsPort x)
329 -- level `b + 2` is odd
331 rw [show upPort b 3 x = upPort (b + 2) 1 (upPort b 2 x) from upPort_succ b 2 x]
332 exact reach_some (q := 16) (by omega) (by omega)
333 ⟨isPort_upk b_pos x_port 2, _, inside_12 (n := b + 1) (by omega), linked⟩ (by rw [ori_b2]; rfl)
335/-- Odd `b`, from two levels up to three: the hook at junction 9 of `N_{b+2}` lies on the rim of `N_{b+3}`, and its
336strand is a hook there. -/
339 (N (b + 3)).Linked (upPort b 3 x) (hookAt (b + 3) (stp (Lk (b + 2) .Delta) (jpos (Lk (b + 1) .Delta) 9))) := by
340 rw [show upPort b 3 x = upPort (b + 2) 1 (upPort b 2 x) from upPort_succ b 2 x]
341 exact (lift_nest (m := b + 2) (by omega) linked (isPort_upk b_pos x_port 2)).trans
344/-- The two witnesses for odd `b`: a hook well inside side 4 of `N_b` reaches junction 12 of `N_{b+2}`, and one well
345inside side 0 reaches junction 9. -/
346theorem odd_witnesses {b : Nat} (b_pos : 1 ≤ b) (odd : b % 2 = 1) :
351 -- level `b` is odd
353 -- level `b + 1` even
355 -- a hook well inside side 4 of `N_b`
356 have inside_A := inside_two (n := b) (J := 4) b_pos
357 -- and one well inside side 0
358 have inside_B := inside_two (n := b) (J := 0) b_pos
359 -- one level up, the first reaches junction 16, inside side 4 of `N_{b+1}`
361 -- and the second junction 21, inside side 5
367 exact ⟨reach_some (q := 12) (by omega) (by omega)
368 ⟨isPort_up b_pos (hook_port b_pos (by omega) inside_A), _, inside_16 b_pos, A_one⟩ (by rw [ori_b1]; rfl),
369 reach_some (q := 9) (by omega) (by omega)
370 ⟨isPort_up b_pos (hook_port b_pos (by omega) inside_B), _, inside_21 b_pos, B_one⟩ (by rw [ori_b1]; rfl)⟩
372/-- **Odd `b`**: the ports of `N_b` lie on exactly two strands of `N_{b+2}`. -/
373theorem two_odd {b : Nat} (b_pos : 1 ≤ b) (odd : b % 2 = 1) : TwoStrands b 2 := by
374 -- junction 9 lies well inside side 2 of `N_{b+2}`
375 have nine_end : jpos (Lk (b + 1) .Delta) 9 + 2 ≤ pos (Lk (b + 2) .Delta 1) 3 := (inside_9 (n := b + 1) (by omega)).2
376 -- and junction 12 well inside side 3
379 -- both away from the corners
380 obtain ⟨two_le_A, A_le⟩ := inside_bounds (by omega) (inside_12 (n := b + 1) (by omega))
381 -- (the second)
382 obtain ⟨two_le_B, B_le⟩ := inside_bounds (by omega) (inside_9 (n := b + 1) (by omega))
383 -- the two witnesses
384 obtain ⟨to_A, to_B⟩ := odd_witnesses b_pos odd
385 exact twoStrands_of b_pos two_le_A A_le two_le_B B_le (by omega)
386 (hook_port b_pos (by omega) (inside_two (n := b) (J := 4) b_pos))
387 (hook_port b_pos (by omega) (inside_two (n := b) (J := 0) b_pos)) to_A to_B
390/-- **Odd `b`**: the ports of `N_b` lie on exactly two strands of `N_{b+3}`. -/
391theorem three_odd {b : Nat} (b_pos : 1 ≤ b) (odd : b % 2 = 1) : TwoStrands b 3 := by
392 -- junction 9 of `N_{b+2}` lies well inside its side 2
395 -- (its end)
396 have nine_end : jpos (Lk (b + 1) .Delta) 9 + 2 ≤ pos (Lk (b + 2) .Delta 1) 3 := (inside_9 (n := b + 1) (by omega)).2
397 -- the two hooks of `N_{b+3}`: different, and away from the corners
398 obtain ⟨⟨two_le_A, A_le⟩, ⟨two_le_B, B_le⟩, A_ne_B⟩ := stp_apart (n := b + 2) (by omega) nine_start nine_end
399 -- the two witnesses, two levels up
400 obtain ⟨to_A, to_B⟩ := odd_witnesses b_pos odd
401 -- the first witness is a port of `N_b`
402 have pA_port := hook_port b_pos (by omega) (inside_two (n := b) (J := 4) b_pos)
403 -- and so is the second
404 have pB_port := hook_port b_pos (by omega) (inside_two (n := b) (J := 0) b_pos)
405 refine twoStrands_of b_pos two_le_A A_le two_le_B B_le A_ne_B pA_port pB_port
407 rcases odd_two b_pos odd x_port with to_12 | to_9
411/-! ### The theorem -/
413/-- **The bound is exact** (as stated in `Statement.lean`). -/
414theorem theoremB_exact : TheoremB_exact := by
415 intro b b_pos
416 rcases Nat.mod_two_eq_zero_or_one b with even | odd
420end SpectreKnot.Statement