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

lean/SpectreKnot/ProofA.lean

248 lines · 18 declarations, each with its own page · on GitHub ·

Theorem A (theoremA): no supertile of any level or kind contains a closed strand.

← Axioms.leanSpectreKnot/ProofB.lean →

All 39 files, and the declarations of this one
1/-
2**Theorem A** (`theoremA`): no supertile of any level or kind contains a closed strand.
3
4The induction of Thm 7.6, at tile level: every level-`m` supertile (`m ≥ 1`) has the signature, with its corners
5`A`, `B` at the positions `aPos m K`, `bPos m K` and its vertices where the side lengths ℓ_m put them (`Good m K`).
6Level 1 is the kernel's check of the nine clusters (`good_one`, Computation 7.5). From level `m` to `m + 1`: the
7children have the signature, the composition has it by Prop 7.4 (`prop_7_4`), so the parent has it (`Kids.parent_sig`),
8with its corners where Table 3 puts the Γ child's corners (`aPos_succ`, `bPos_succ`). Level 0 is a tile, which has the
9signature (`tile_hasSig`, Lemma 4.4).
11On the way, two statements in the paper's terms: side `j` of `super m K` has `ℓ_m(K, j)` edges (`super_side_length`,
12Prop 6.1 for the supertiles themselves), and the corner `A` of a supertile is that of its Γ child (`cornerA_succ`, the
13paper's definition of `A`, §2.3).
14-/
17namespace SpectreKnot.Statement
19open Pattern Compose Gluing
21/-- `pos f J` depends only on the side lengths before `J`. -/
22theorem pos_congr {f g : Nat → Nat} : ∀ J, (∀ i, i < J → f i = g i) → pos f J = pos g J
23 | 0, _ => rfl
24 | J + 1, agree => by rw [pos_succ, pos_succ, pos_congr J (fun i i_lt => agree i (by omega)), agree J (by omega)]
26/-- `totL` is the sum of the side lengths of the pieces. -/
27theorem totL_eq (L : Nat → Nat → Nat) : ∀ l : List (Nat × Nat), totL L l = (l.map fun p => L p.1 p.2).sum
28 | [] => rfl
29 | (c, j) :: rest => by simp only [totL, List.map_cons, List.sum_cons, totL_eq L rest]
31/-- The side lengths of the children in a composition of level-`m` supertiles. -/
32abbrev Lk (m : Nat) (T : Kind) (c j : Nat) : Nat := letterLen m (letterOf (kidAt T c) j)
34/-- The parent's sides have the lengths ℓ_{m+1} (Prop 2.4(c) with Prop 6.1). -/
35theorem parentLen_eq {m : Nat} (m_pos : 1 ≤ m) (T : Kind) {J : Nat} (J_lt : J < 6) :
36 parentLen T (Lk m T) J = lenAt (m + 1) T J := by
37 obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
38 rw [lenAt, ← sideLen_eq_letterLen (m' + 2) (by omega) T J J_lt]
39 simp only [sideLen, parentLen, totL_eq]
40 congr 1
41 apply List.map_congr_left
42 intro p mem
43 rw [sideLen_eq_letterLen (m' + 1) (by omega) _ _ (pieces_valid T J J_lt p mem)]
45/-- The parent's vertices sit where the lengths ℓ_{m+1} put them. -/
46theorem vpos_eq {m : Nat} (m_pos : 1 ≤ m) (T : Kind) {J : Nat} (J_le : J ≤ 6) :
47 vpos (m + 1) T J = pos (parentLen T (Lk m T)) J :=
48 pos_congr J (fun i i_lt => (parentLen_eq m_pos T (by omega)).symm)
50/-! ### The induction -/
52/-- The children of a composition of level-`m` supertiles satisfy the bridge's hypotheses. -/
53theorem kids_at {m : Nat} (m_pos : 1 ≤ m) (T : Kind) (good_m : ∀ K, Good m K) :
54 Kids T (fun c => super m (kidAt T c)) (Lk m T) (dOff m) (ori m) (ori m) where
55 len_pos c j := by
56 -- every side is at least 5 long (Lemma 6.5)
57 have := (bounds m m_pos).1 (letterOf (kidAt T c) j)
58 simp only [Lk]; omega
59 pair c c_lt j j_lt c' j' adj_eq := by simp only [Lk, pair_letter c_lt j_lt adj_eq]
60 shape c _ := ⟨(good_m (kidAt T c)).vtx, (good_m (kidAt T c)).len⟩
61 sig c c_lt := by
62 -- the child has the signature at `aPos`, `bPos`
63 have has_sig := (good_m (kidAt T c)).sig
64 -- which is where the composition puts its corner `A`
65 have A_eq : (Comp.ofLens T (Lk m T) (dOff m) (ori m)).toGluing.A c = aPos m (kidAt T c) := by
66 rw [ofLens_A c_lt]; rfl
67 -- and its corner `B`
68 have B_eq : (Comp.ofLens T (Lk m T) (dOff m) (ori m)).toGluing.B c = bPos m (kidAt T c) := by
69 rw [ofLens_B c_lt, A_eq]; rfl
70 rw [A_eq, B_eq]; exact has_sig
71 csig := prop_7_4 m m_pos T (ori m)
73/-- The orientation flips from each level to the next. -/
74theorem ori_succ (m : Nat) : ori (m + 1) = !ori m := by
75 simp only [ori]
76 rcases Nat.mod_two_eq_zero_or_one m with even | odd
77 · have succ_odd : (m + 1) % 2 = 1 := by omega -- `m` even, so `m + 1` odd
78 simp [even, succ_odd]
79 · have succ_even : (m + 1) % 2 = 0 := by omega -- `m` odd, so `m + 1` even
80 simp [odd, succ_even]
82/-- **The parent's corner `A`**: where the induction puts it (`aPos`, Lemma 6.4) is the rim position `cA` of its Γ
83child's corner `A` (Table 3). For a Σ parent, `d_{m+1}` is the length of the pieces `0.2`, `0.1`, `7.0`. -/
84theorem aPos_succ {m : Nat} (m_pos : 1 ≤ m) (T : Kind) : aPos (m + 1) T = cA T (Lk m T) := by
85 obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
86 by_cases is_sigma : T = .Sigma
87 · subst is_sigma
88 -- `d_{m+1}` is the length of the first three pieces of side 5
89 have dOff_eq :
90 dOff (m' + 2) = Lk (m' + 1) .Sigma 0 2 + Lk (m' + 1) .Sigma 0 1 + Lk (m' + 1) .Sigma 7 0 := by
91 simp only [dOff, sigma_side5_start.1, List.map_cons, List.map_nil, List.sum_cons, List.sum_nil, Lk]
92 rw [sideLen_eq_letterLen _ (by omega) _ 2 (by omega), sideLen_eq_letterLen _ (by omega) _ 1 (by omega),
93 sideLen_eq_letterLen _ (by omega) _ 0 (by omega)]
94 omega
95 simp only [aPos, cA]
96 rw [vpos_eq m_pos _ (by omega), ← totL_take _ _ 5 (by omega), preS_eq, totL_append, dOff_eq]
97 simp [totL]; omega
98 · simp only [aPos, cA, ite_eq_right is_sigma]
100/-- **The parent's corner `B`**: where the induction puts it (`bPos`, `B = A + ω_{m+1}`) is the rim position `cB`
101of its Γ child's corner `B`. -/
102theorem bPos_succ {m : Nat} (m_pos : 1 ≤ m) (T : Kind) : bPos (m + 1) T = cB T (Lk m T) (ori m) := by
103 simp only [bPos, cB, aPos_succ m_pos T, ori_succ]
104 rw [vpos_eq m_pos T (Nat.le_refl _), ← rimN_eq]
106/-- **The induction step**: if every level-`m` supertile has the signature, so does every level-`(m+1)` one. -/
107theorem good_succ {m : Nat} (m_pos : 1 ≤ m) (good_m : ∀ K, Good m K) (T : Kind) : Good (m + 1) T := by
108 obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
109 -- the children satisfy the bridge's hypotheses
110 have kids := kids_at m_pos T good_m
111 -- the parent is the composition of its children
112 have super_eq : super (m' + 1 + 1) T = compose T fun c => super (m' + 1) (kidAt T c) := rfl
113 -- the parent's rim length is where its vertex 6 sits
114 have rim_len : rimN T (Lk (m' + 1) T) = vpos (m' + 1 + 1) T 6 := by
115 rw [rimN_eq, vpos_eq m_pos T (Nat.le_refl _)]
116 -- the parent's vertices sit where the lengths ℓ_{m+1} put them
117 have vtx_eq :
118 (compose T fun c => super (m' + 1) (kidAt T c)).vtx = (List.range 7).map (vpos (m' + 1 + 1) T) := by
119 rw [parent_vtx kids.shape]
120 apply List.map_congr_left
121 intro J J_mem
122 rw [vpos_eq m_pos T (by rw [List.mem_range] at J_mem; omega)]
123 -- the parent's rim length
124 have len_eq : (compose T fun c => super (m' + 1) (kidAt T c)).E = vpos (m' + 1 + 1) T 6 := by
125 rw [compose_E kids.shape, rim_len]
126 refine ⟨?_, by rw [super_eq]; exact vtx_eq, by rw [super_eq]; exact len_eq⟩
127 -- the parent has the signature at its Γ child's corners, which are where the induction puts them
128 rw [super_eq, ori_succ, bPos_succ m_pos T, aPos_succ m_pos T]
129 exact kids.parent_sig
In the paper Theorem 7.6 Signature Theorem
131/-- **Thm 7.6, at tile level**: every supertile of level `m ≥ 1` has the signature. -/
132theorem good : ∀ m K, 1 ≤ m → Good m K := by
133 intro m
134 induction m with
135 | zero => intro K one_le_zero; omega
136 | succ m ih =>
137 intro K _
138 rcases Nat.eq_zero_or_pos m with rfl | m_pos
139 · exact good_one K
140 · exact good_succ m_pos (fun K' => ih K' m_pos) K
In the paper Proposition 6.1 Lengths by letter
142/-- **Prop 6.1 for the supertiles themselves** (`m ≥ 1`): side `j` of `super m K` has `ℓ_m(K, j)` edges, the length
143`letterLen m` of its letter (Table 4); this is also `sideLen m K j`, the count by Table 3 (`sideLen_eq_letterLen`). -/
144theorem super_side_length {m : Nat} (m_pos : 1 ≤ m) (K : Kind) {j : Nat} (j_lt : j < 6) :
145 ((super m K).side j).length = letterLen m (letterOf K j) ∧ letterLen m (letterOf K j) = sideLen m K j :=
146 ⟨side_length (good m K m_pos).vtx (good m K m_pos).len j_lt, (sideLen_eq_letterLen m m_pos K j j_lt).symm⟩
In the paper Lemma 6.4 Position of A
148/-- The claim's corner `A` (`cornerA`, placed by position as in Lemma 6.4) is the induction's (`aPos`), since
149`d_m = 2 F_{3m+1}`. -/
150theorem cornerA_eq_aPos {m : Nat} (m_pos : 1 ≤ m) (K : Kind) : cornerA m K = aPos m K := by
151 -- vertex 5 lies where the side lengths put it
152 have vtx5 : (super m K).vtx.getD 5 0 = vpos m K 5 := by rw [(good m K m_pos).vtx]; rfl
154 rw [vtx5, (dOff_fib m m_pos).1]
In the paper Theorem 7.6 Signature Theorem
156/-- **The corner `A` of a supertile is that of its Γ child** (the paper's recursive definition of `A`, §2.3): for
157`m ≥ 1`, the port `L` of `super (m + 1) T` at its corner `A` is the port `R` of its Γ child, the last child, at the
158child's own corner `A`, with the child's tiles numbered as in the parent. (Parent and child are oriented oppositely, so
159`R` and `L` swap.) -/
160theorem cornerA_succ {m : Nat} (m_pos : 1 ≤ m) (T : Kind) :
161 (super (m + 1) T).bport (ori (m + 1)) (cornerA (m + 1) T, false) =
162 shiftP (fun c => super m (kidAt T c)) (nk T - 1) ((super m .Gamma).bport (ori m) (cornerA m .Gamma, true)) := by
163 -- the children have the signature, with the side lengths of the composition
164 have kids := kids_at m_pos T (fun K => good m K m_pos)
165 obtain ⟨m', rfl⟩ : ∃ m', m = m' + 1 := ⟨m - 1, by omega⟩
166 -- the parent is the composition of its children
167 have super_eq : super (m' + 1 + 1) T = compose T fun c => super (m' + 1) (kidAt T c) := rfl
168 -- the Γ child's corner `A` is its vertex 0
169 have gamma_A : aPos (m' + 1) .Gamma = 0 := rfl
170 -- the claim's corners are the induction's; the parent's is where Table 3 puts the Γ child's corner `A`
171 rw [cornerA_eq_aPos (by omega) T, aPos_succ m_pos T, cornerA_eq_aPos m_pos .Gamma, gamma_A, super_eq, ori_succ,
172 kids.bport_L kids.csig.cA_lt, kids.csig.at_A, gA_last (Nat.sub_lt (last_lt T) Nat.one_pos)]
173 show shiftP _ _ ((super (m' + 1) (kidAt T (nk T - 1))).bport _ _) = _
174 rw [kid_last T]
In the paper Lemma 4.2 Gluing
176/-- **`compose` never falls back on a default** in the supertiles of the statement. Let `m ≥ 1` and let `(t, i)` be an
177unglued edge of child `c` of `super (m + 1) T`. Then `compose` finds the edge on the child's rim list, at the one
178position `k` that holds it, so `findIdx?`'s default is not used; and a side of the child that Table 2 glues to a side
179of a sibling has as many edges as that side, so the lookup of the edge across stays inside it. (`glue_rim` says more:
180across the edge, `compose` glues exactly what the abstract composition says.) -/
181theorem compose_no_default {m : Nat} (m_pos : 1 ≤ m) (T : Kind) {c t i : Nat} (c_lt : c < nk T)
182 (ht : t < (super m (kidAt T c)).tiles) (hi : i < 14) (unglued : (super m (kidAt T c)).glue t i = none) :
183 (∃ k, (super m (kidAt T c)).rim.findIdx? (· == (t, i)) = some k ∧ (super m (kidAt T c)).edgeAt k = (t, i)) ∧
184 ∀ j c' j', j < 6 → adjAt T c j = some (c', j') →
185 ((super m (kidAt T c')).side j').length = ((super m (kidAt T c)).side j).length := by
186 -- the children have the signature, with the side lengths of the composition
187 have kids := kids_at m_pos T (fun K => good m K m_pos)
188 -- in particular child `c`: its rim lists every unglued edge, each once
189 have sig := (good m (kidAt T c) m_pos).sig
190 refine ⟨?_, fun j c' j' j_lt glued => ?_⟩
191 · obtain ⟨k, k_lt, at_k⟩ := sig.rim_all t i ht hi unglued
192 -- the rim list's entries are the edges `edgeAt` gives
193 have entry_eq : ∀ k', (k'_lt : k' < (super m (kidAt T c)).rim.length) →
194 (super m (kidAt T c)).rim[k'] = (super m (kidAt T c)).edgeAt k' := fun k' k'_lt => by
195 simp only [Patch.edgeAt, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem k'_lt, Option.getD_some]
196 refine ⟨k, List.findIdx?_eq_some_iff_getElem.mpr ⟨k_lt, ?_, ?_⟩, at_k⟩
197 · rw [entry_eq, at_k]; simp
198 · intro j j_lt same_edge
199 rw [entry_eq, beq_iff_eq] at same_edge
200 -- an earlier position holding the edge would be `k` itself
201 have := sig.rim_inj j k (by omega) k_lt (same_edge.trans at_k.symm)
202 omega
203 · -- the two sides have the lengths of their letters, which Table 2 pairs equally
204 obtain ⟨c'_lt, j'_lt, _, _⟩ := adj_valid c_lt j_lt glued
205 obtain ⟨vtx_eq, len_eq⟩ : (super m (kidAt T c)).vtx = (List.range 7).map (pos (Lk m T c)) ∧
206 (super m (kidAt T c)).E = pos (Lk m T c) 6 := kids.shape c c_lt
207 obtain ⟨vtx_eq', len_eq'⟩ : (super m (kidAt T c')).vtx = (List.range 7).map (pos (Lk m T c')) ∧
208 (super m (kidAt T c')).E = pos (Lk m T c') 6 := kids.shape c' c'_lt
209 rw [side_length vtx_eq' len_eq' j'_lt, side_length vtx_eq len_eq j_lt]
210 exact kids.pair c c_lt j j_lt c' j' glued
In the paper Theorem 7.6 Signature Theorem
212/-- **Theorem A** (as stated in `Statement.lean`): for every level `m` and every kind `K`, the supertile
213`super m K` contains no closed strand. -/
214theorem theoremA : TheoremA := by
215 intro m K
216 rcases Nat.eq_zero_or_pos m with rfl | m_pos
217 · exact tile_hasSig.noClosed
218 · exact (good m K m_pos).sig.noClosed
220/-! ### A negative control -/
222/-- A one-tile patch with a made-up gluing (not a real one) that traps a ribbon: edges `e_5` and `e_3` are both glued
223to `e_4`. -/
224def loopPatch : Patch := ⟨1, fun _ i => if i = 5 ∨ i = 3 then some (0, 4) else none, [], []⟩
226/-- **Negative control**: `NoClosedStrand` can fail, so `TheoremA` is not true by definition. In `loopPatch` the ribbon
227from `L(v_5)` goes round `v_5` to `R(v_5)`, across `e_5` to `R(v_4)`, round `v_4` to `L(v_4)`, and across `e_3` back to
228`L(v_5)`, for ever. -/
229theorem loopPatch_closed : ¬ loopPatch.NoClosedStrand := by
230 intro no_closed
231 obtain ⟨r, follow⟩ := no_closed (0, 5, false) ⟨by decide, by decide⟩
232 -- no finite walk starts at `L(v_5)` or `R(v_4)`: each only leads on to the other
233 have key : ∀ p r, loopPatch.Follow p r → p ≠ (0, 5, false) ∧ p ≠ (0, 4, true) := by
234 intro p r follow_pr
235 induction follow_pr with
236 | @leave p leaves =>
237 constructor <;> rintro rfl <;> simp [loopPatch, Patch.across, straightThrough, pieceEnd] at leaves
238 | @next p q r crosses _ ih =>
239 constructor <;> rintro rfl
240 · have q_eq : q = (0, 4, true) := by -- from `L(v_5)` the walk goes on to `R(v_4)`
241 simp [loopPatch, Patch.across, straightThrough, pieceEnd] at crosses; exact crosses.symm
242 exact ih.2 q_eq
243 · have q_eq : q = (0, 5, false) := by -- from `R(v_4)` the walk goes on to `L(v_5)`
244 simp [loopPatch, Patch.across, straightThrough, pieceEnd] at crosses; exact crosses.symm
245 exact ih.1 q_eq
246 exact (key _ _ follow).1 rfl
248end SpectreKnot.Statement

← Axioms.leanSpectreKnot/ProofB.lean →