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

lean/SpectreKnot/CompSig.lean

612 lines · 39 declarations, each with its own page · on GitHub ·

"A composition has the signature", as the paper's §7.1 words it, and Computation 7.3 in that form.

← SpectreKnot/Signature.leanSpectreKnot/Parity.lean →

All 39 files, and the declarations of this one
1/-
2**"A composition has the signature"**, as the paper's §7.1 words it, and Computation 7.3 in that form.
3
4The composition `Comp.ofLens T L d ω` has Table 3's rim: its rim vertex at position `p` (in the parent's own order)
5lies between the children's edges at positions `p - 1` and `p` (`ownGo`), with the ports `gR p` and `gL p`. The Γ
6child's corners `A` and `B` are the rim vertices at the adjacent positions `cA` and `cB` (`corners_at`). `CompSig`
7says that the composition has the signature: no closed strand, a hook at every other rim vertex, and the crossover at
8`A` and `B`.
9
10The kernel's check of Computation 7.3 (`Comp.check`) gives `Sig`, the form in which the proof of Lemma 7.1 carries the
11signature through cuts (`sig_of_check`); and `Sig` gives `CompSig` (`compSig_of_sig`). So Computation 7.3 holds as the
12paper words it (`Compose.comp_7_3`), and so, after the induction, does Prop 7.4 (`Compose.prop_7_4`, `Parity.lean`).
13-/
17namespace SpectreKnot.Statement
19open Pattern Compose Gluing
21/-- Stepping back one position round a rim of length `N` is one to one. -/
22theorem prv_inj {N p p' : Nat} (p_lt : p < N) (p_lt' : p' < N) (same : prv N p = prv N p') : p = p' := by
23 unfold prv at same; split at same <;> split at same <;> omega
25/-! ### The corners of a composition -/
27/-- The last child is the Γ child. -/
28theorem kid_last : ∀ T : Kind, kidAt T (nk T - 1) = .Gamma := by intro T; cases T <;> rfl
30/-- Every kind has a child. -/
31theorem last_lt : ∀ T : Kind, 0 < nk T := by intro T; cases T <;> decide
33/-- For every kind but Σ, the parent's rim begins with side 5 of the Γ child and ends with its side 0. -/
34theorem pcs_nonSigma : ∀ T : Kind, T ≠ .Sigma →
35 pcs T = (nk T - 1, 5) :: ((pcs T).drop 1).dropLast ++ [(nk T - 1, 0)] := by
36 intro T not_sigma; cases T <;> first | exact absurd rfl not_sigma | decide
38/-- The pieces of the Σ-supertile's rim before its crossover corner. -/
39def preS : List (Nat × Nat) :=
40 [(6, 3), (6, 2), (5, 4), (5, 3), (5, 2), (5, 1), (4, 2), (3, 4), (3, 3), (3, 2), (2, 4), (2, 3), (2, 2), (2, 1),
41 (1, 2), (0, 4), (0, 3), (0, 2), (0, 1)]
43/-- The Σ-supertile's rim: `preS`, then sides 0 and 5 of the Γ child (child 7), then side 4 of child 6. -/
44theorem pcs_sigma : pcs .Sigma = preS ++ [(7, 0), (7, 5), (6, 4)] := by decide
46/-- `preS` is the pieces of the Σ-supertile's sides 0–4, then the first two pieces of its side 5. -/
47theorem preS_eq : preS = ((pside .Sigma).take 5).flatMap id ++ [(0, 2), (0, 1)] := by decide
49section Corners
51variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
53/-- The Γ child's corner `A` is its vertex 0. -/
54theorem gA_last (last_lt' : nk T - 1 < nk T) : (Comp.ofLens T L d ω).toGluing.A (nk T - 1) = 0 := by
55 rw [ofLens_A last_lt', ite_eq_right (by rw [kid_last]; decide)]
57/-- With positive side lengths, a child's rim has at least two edges, and ends after its side 5. -/
58theorem pos6 (len_pos : ∀ c j, 1 ≤ L c j) (c : Nat) : 2 ≤ pos (L c) 6 ∧ pos (L c) 6 = pos (L c) 5 + L c 5 := by
59 -- sides 0 … 4 come before vertex 5
60 have before_5 := pos_lt_of_pos (L c) (fun i _ => len_pos c i) (show 0 < 5 by omega) (by omega)
61 -- side 5 has an edge
62 have len_5 := len_pos c 5
63 -- the rim ends after side 5
64 have pos_6 : pos (L c) 6 = pos (L c) 5 + L c 5 := pos_succ _ 5
65 -- the rim starts at vertex 0
66 have pos_0 : pos (L c) 0 = 0 := rfl
67 -- side 0 has an edge
68 have len_0 := len_pos c 0
69 exact ⟨by omega, pos_6⟩
71/-- The Γ child's corner `B` is its vertex 1 if `ω`, and its last rim vertex otherwise. -/
72theorem gB_last (len_pos : ∀ c j, 1 ≤ L c j) (last_lt' : nk T - 1 < nk T) :
73 (Comp.ofLens T L d ω).toGluing.B (nk T - 1) =
74 if ω then 1 else pos (L (nk T - 1)) 6 - 1 := by
75 -- the Γ child's rim has at least two edges
76 have rim_ge_two := (pos6 len_pos (nk T - 1)).1
77 rw [ofLens_B last_lt', gA_last last_lt']
78 cases ω with
79 | true => simp only [ite_true, nxt]; rw [ite_eq_right (by omega)]
80 | false => rfl
82/-- The corners of a non-Σ parent: `A` at its vertex 0, `B` next to it. -/
83theorem corners_nonSigma (not_sigma : T ≠ .Sigma) (len_pos : ∀ c j, 1 ≤ L c j)
84 (side0_ge_two : 2 ≤ L (nk T - 1) 0) :
85 0 < rimN T L ∧ (if !ω then nxt (rimN T L) 0 else prv (rimN T L) 0) < rimN T L ∧
86 0 ≠ (if !ω then nxt (rimN T L) 0 else prv (rimN T L) 0) ∧
87 ownGo L (pcs T) (prv (rimN T L) 0) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.A (nk T - 1)) ∧
88 ownGo L (pcs T) (prv (rimN T L) (if !ω then nxt (rimN T L) 0 else prv (rimN T L) 0)) =
89 (nk T - 1, (Comp.ofLens T L d ω).toGluing.B (nk T - 1)) := by
90 -- the Γ child is an actual child
91 have last_lt' : nk T - 1 < nk T := by
92 -- every kind has a child
93 have := last_lt T
94 omega
95 -- the parent's rim begins with the Γ child's side 5 and ends with its side 0
96 have pcs_shape := pcs_nonSigma T not_sigma
97 generalize ((pcs T).drop 1).dropLast = mid at pcs_shape
98 -- the last rim position is the Γ child's edge 0
99 have at_last : ownGo L (pcs T) (rimN T L - 1) = (nk T - 1, 0) := by
100 -- the last position of a list ending with side 0 of the Γ child
101 have last := ownGo_last (L := L) (c := nk T - 1) (j := 0) (len_pos _ 0) ((nk T - 1, 5) :: mid)
102 rw [← pcs_shape] at last
103 exact last
104 -- the first rim position is the Γ child's last edge
105 have at_zero : ownGo L (pcs T) 0 = (nk T - 1, pos (L (nk T - 1)) 6 - 1) := by
106 rw [pcs_shape, List.cons_append, ownGo_zero (len_pos _ 5), (pos6 len_pos _).2]
107 -- the rim length, with the last piece split off
108 have total : rimN T L = totL L ((nk T - 1, 5) :: mid) + L (nk T - 1) 0 := by
109 show totL L (pcs T) = _
110 rw [pcs_shape, totL_append]; simp only [totL]; omega
111 -- the second-last rim position is the Γ child's edge 1
112 have at_last2 : ownGo L (pcs T) (rimN T L - 2) = (nk T - 1, 1) := by
113 rw [total, pcs_shape, ownGo_append, ite_eq_right (by omega), show totL L ((nk T - 1, 5) :: mid) + L (nk T - 1) 0 -
114 2 - totL L ((nk T - 1, 5) :: mid) = L (nk T - 1) 0 - 2 by omega]
115 simp only [ownGo]
116 rw [ite_eq_left (by omega)]
117 simp only [pos]
118 congr 1; omega
119 -- the rim has at least two edges
120 have rim_ge_two : 2 ≤ rimN T L := by
121 rw [total]; simp only [totL]
122 -- the Γ child's side 5 has an edge
123 have := len_pos (nk T - 1) 5
124 omega
125 rw [gA_last last_lt', gB_last len_pos last_lt']
126 -- the step back from 0 wraps round to the last position
127 have prv_zero : prv (rimN T L) 0 = rimN T L - 1 := by simp [prv]
128 cases ω with
129 | true =>
130 -- two steps back from 0
131 have prv_prv : prv (rimN T L) (prv (rimN T L) 0) = rimN T L - 2 := by
132 rw [prv_zero]; simp only [prv]; rw [ite_eq_right (show ¬ (rimN T L - 1 = 0) by omega)]; omega
133 simp only [Bool.not_true, ite_false, Bool.false_eq_true, ite_true]
134 refine ⟨by omega, prv_lt (by omega), by rw [prv_zero]; omega, by rw [prv_zero, at_last], ?_⟩
135 rw [prv_prv, at_last2]
136 | false =>
137 -- one step forwards from 0
138 have nxt_zero : nxt (rimN T L) 0 = 1 := by simp only [nxt]; rw [ite_eq_right (show ¬ (0 + 1 = rimN T L) by omega)]
139 -- and back again
140 have prv_nxt_zero : prv (rimN T L) (nxt (rimN T L) 0) = 0 := by rw [nxt_zero]; rfl
141 simp only [Bool.not_false, ite_true, ite_false, Bool.false_eq_true]
142 refine ⟨by omega, by rw [nxt_zero]; omega, by rw [nxt_zero]; omega, by rw [prv_zero, at_last], ?_⟩
143 rw [prv_nxt_zero, at_zero]
145/-- The corners of a Σ parent: `A` on side 5, after the pieces `preS` and the Γ child's side 0. -/
146theorem corners_sigma (len_pos : ∀ c j, 1 ≤ L c j) (side0_ge_two : 2 ≤ L 7 0) :
147 totL L preS + L 7 0 < rimN .Sigma L ∧
148 (if !ω then nxt (rimN .Sigma L) (totL L preS + L 7 0) else prv (rimN .Sigma L) (totL L preS + L 7 0)) <
149 rimN .Sigma L ∧
150 totL L preS + L 7 0 ≠
151 (if !ω then nxt (rimN .Sigma L) (totL L preS + L 7 0) else prv (rimN .Sigma L) (totL L preS + L 7 0)) ∧
152 ownGo L (pcs .Sigma) (prv (rimN .Sigma L) (totL L preS + L 7 0)) =
153 (7, (Comp.ofLens .Sigma L d ω).toGluing.A 7) ∧
154 ownGo L (pcs .Sigma) (prv (rimN .Sigma L)
155 (if !ω then nxt (rimN .Sigma L) (totL L preS + L 7 0) else prv (rimN .Sigma L) (totL L preS + L 7 0))) =
156 (7, (Comp.ofLens .Sigma L d ω).toGluing.B 7) := by
157 -- the Γ child, child 7, is an actual child
158 have last_lt' : nk .Sigma - 1 < nk .Sigma := by decide
159 -- its corner `A` is its vertex 0
160 have A_zero : (Comp.ofLens .Sigma L d ω).toGluing.A 7 = 0 := gA_last last_lt'
161 -- and its corner `B` is vertex 1 or its last vertex
162 have B_eq : (Comp.ofLens .Sigma L d ω).toGluing.B 7 = if ω then 1 else pos (L 7) 6 - 1 := gB_last len_pos last_lt'
163 -- the rim length, piece by piece
164 have total : rimN .Sigma L = totL L preS + L 7 0 + L 7 5 + L 6 4 := by
165 show totL L (pcs .Sigma) = _
166 rw [pcs_sigma, totL_append]; simp only [totL]; omega
167 -- past `preS`, the rim is the last three pieces
168 have after_preS : ∀ q, ownGo L (pcs .Sigma) (totL L preS + q) = ownGo L [(7, 0), (7, 5), (6, 4)] q := by
169 intro q
170 rw [pcs_sigma, ownGo_append, ite_eq_right (show ¬ (totL L preS + q < totL L preS) by omega),
171 Nat.add_sub_cancel_left]
172 -- the Γ child's rim starts at vertex 0
173 have pos_zero : pos (L 7) 0 = 0 := rfl
174 -- the last position in the Γ child's side 0 is its edge 0
175 have at_edge0 : ownGo L (pcs .Sigma) (totL L preS + (L 7 0 - 1)) = (7, 0) := by
176 rw [after_preS]; simp only [ownGo]; rw [ite_eq_left (show L 7 0 - 1 < L 7 0 by omega), pos_zero,
177 show 0 + L 7 0 - 1 - (L 7 0 - 1) = 0 by omega]
178 -- the one before it is its edge 1
179 have at_edge1 : ownGo L (pcs .Sigma) (totL L preS + (L 7 0 - 2)) = (7, 1) := by
180 rw [after_preS]; simp only [ownGo]; rw [ite_eq_left (show L 7 0 - 2 < L 7 0 by omega), pos_zero,
181 show 0 + L 7 0 - 1 - (L 7 0 - 2) = 1 by omega]
182 -- the next position, the first of the piece `(7, 5)`, is the Γ child's last edge
183 have at_last : ownGo L (pcs .Sigma) (totL L preS + L 7 0) = (7, pos (L 7) 6 - 1) := by
184 rw [after_preS]; simp only [ownGo]
185 rw [ite_eq_right (show ¬ (L 7 0 < L 7 0) by omega), Nat.sub_self, ite_eq_left (show 0 < L 7 5 from len_pos 7 5),
186 (pos6 len_pos 7).2, Nat.sub_zero]
187 -- the Γ child's side 5 has an edge
188 have len_75 := len_pos 7 5
189 -- and so does child 6's side 4
190 have len_64 := len_pos 6 4
191 -- the step back from the corner position
192 have prv_corner : prv (rimN .Sigma L) (totL L preS + L 7 0) = totL L preS + (L 7 0 - 1) := by
193 simp only [prv]; rw [ite_eq_right (show ¬ (totL L preS + L 7 0 = 0) by omega)]; omega
194 rw [A_zero, B_eq]
195 cases ω with
196 | true =>
197 -- two steps back
198 have prv_prv : prv (rimN .Sigma L) (totL L preS + (L 7 0 - 1)) = totL L preS + (L 7 0 - 2) := by
199 simp only [prv]; rw [ite_eq_right (show ¬ (totL L preS + (L 7 0 - 1) = 0) by omega)]; omega
200 simp only [Bool.not_true, Bool.false_eq_true, ↓reduceIte]
201 refine ⟨by omega, by rw [prv_corner]; omega, by rw [prv_corner]; omega, by rw [prv_corner, at_edge0], ?_⟩
202 rw [prv_corner, prv_prv, at_edge1]
203 | false =>
204 -- one step forwards from the corner position
205 have nxt_corner : nxt (rimN .Sigma L) (totL L preS + L 7 0) = totL L preS + L 7 0 + 1 := by
206 simp only [nxt]; rw [ite_eq_right (show ¬ (totL L preS + L 7 0 + 1 = rimN .Sigma L) by omega)]
207 -- and back again
208 have prv_nxt_corner : prv (rimN .Sigma L) (totL L preS + L 7 0 + 1) = totL L preS + L 7 0 := by
209 simp only [prv]; rw [ite_eq_right (show ¬ (totL L preS + L 7 0 + 1 = 0) by omega)]; omega
210 simp only [Bool.not_false, Bool.false_eq_true, ↓reduceIte]
211 refine ⟨by omega, by rw [nxt_corner]; omega, by rw [nxt_corner]; omega, by rw [prv_corner, at_edge0], ?_⟩
212 rw [nxt_corner, prv_nxt_corner, at_last]
214end Corners
216/-! ### The rim vertices of a composition -/
218/-- The gluing's port at the parent's port `R(p)` (in the parent's orientation): the end of the child edge at rim
219position `p`, in the children's sense. -/
220def gR (T : Kind) (L : Nat → Nat → Nat) (d : Nat) (ω : Bool) (p : Nat) : GPort :=
221 ((ownGo L (pcs T) p).1, nxt ((Comp.ofLens T L d ω).toGluing.E (ownGo L (pcs T) p).1) (ownGo L (pcs T) p).2, false)
223/-- The gluing's port at the parent's port `L(p)`: the start of the child edge at rim position `p - 1`. -/
224def gL (T : Kind) (L : Nat → Nat → Nat) (p : Nat) : GPort :=
225 ((ownGo L (pcs T) (prv (rimN T L) p)).1, (ownGo L (pcs T) (prv (rimN T L) p)).2, true)
227section Ports
229variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
231/-- The vertex of `gR p` is a parent rim vertex reached along the rim: the edge before it is unglued. -/
232theorem gR_rimL (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
233 (Comp.ofLens T L d ω).toGluing.RimL (gR T L d ω p).1 (gR T L d ω p).2.1 := by
234 obtain ⟨c_lt, k_lt, unglued⟩ := own_mate (d := d) (ω := ω) len_pos p_lt
235 -- the edge is on the child's rim, in the composition's terms
236 have k_lt' : (ownGo L (pcs T) p).2 < (Comp.ofLens T L d ω).toGluing.E (ownGo L (pcs T) p).1 := by
237 rw [ofLens_E c_lt]; exact k_lt
238 exact ⟨by rw [ofLens_n]; exact c_lt, nxt_lt k_lt', by simp only [gR]; rw [prv_nxt k_lt']; exact unglued⟩
240/-- Turning about the vertex of `gR p` reaches the start of the child edge at position `p - 1`, the vertex of
241`gL p`. -/
242theorem gR_rot (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
243 (Comp.ofLens T L d ω).toGluing.Rot ((gR T L d ω p).1, (gR T L d ω p).2.1) (ownGo L (pcs T) (prv (rimN T L) p)) :=
244 own_rot len_pos p_lt
246/-- `gR p` is a port of an actual child, at an actual rim vertex. -/
247theorem gR_valid (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
248 (Comp.ofLens T L d ω).toGluing.Valid (gR T L d ω p) :=
249 ⟨(gR_rimL len_pos p_lt).1, (gR_rimL len_pos p_lt).2.1⟩
251/-- `gL p` is a port of an actual child, at an actual rim vertex. -/
252theorem gL_valid (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
253 (Comp.ofLens T L d ω).toGluing.Valid (gL T L p) := by
254 obtain ⟨c_lt, k_lt, _⟩ := own_mate (d := d) (ω := ω) len_pos (prv_lt p_lt)
255 refine ⟨?_, ?_⟩ <;> simp only [gL]
256 · rw [ofLens_n]; exact c_lt
257 · rw [ofLens_E c_lt]; exact k_lt
259/-- `gR p` is on the parent's rim: nothing lies across it. -/
260theorem gR_sigma (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
261 (Comp.ofLens T L d ω).toGluing.sigma (gR T L d ω p) = none := by
262 -- the edge before the vertex is unglued
263 have unglued := (gR_rimL (d := d) (ω := ω) len_pos p_lt).2.2
264 simp only [gR, Gluing.sigma] at unglued ⊢
265 rw [unglued]; rfl
267/-- `gL p` is on the parent's rim: nothing lies across it. -/
268theorem gL_sigma (len_pos : ∀ c j, 1 ≤ L c j) {p : Nat} (p_lt : p < rimN T L) :
269 (Comp.ofLens T L d ω).toGluing.sigma (gL T L p) = none := by
270 obtain ⟨_, _, unglued⟩ := own_mate (d := d) (ω := ω) len_pos (prv_lt p_lt)
271 simp only [gL, Gluing.sigma]
272 rw [unglued]; rfl
274end Ports
276/-! ### The corners of the composition, as rim positions -/
278/-- The parent rim position of the Γ child's corner `A`: position 0, or for a Σ parent the position after the pieces
279`preS` and the Γ child's side 0 (Table 3). -/
280def cA (T : Kind) (L : Nat → Nat → Nat) : Nat := if T = .Sigma then totL L preS + L 7 0 else 0
282/-- The parent rim position of the Γ child's corner `B`, next to `cA`: before it in the parent's own order if `ω`
283(that is, after it in the children's order), after it otherwise. -/
284def cB (T : Kind) (L : Nat → Nat → Nat) (ω : Bool) : Nat :=
285 if !ω then nxt (rimN T L) (cA T L) else prv (rimN T L) (cA T L)
287section CornersAt
289variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
291/-- **The Γ child's corners are adjacent rim vertices of the composition**, at the positions `cA` and `cB`: the
292child edge before position `cA` starts at `A`, the one before `cB` at `B`. -/
293theorem corners_at (len_pos : ∀ c j, 1 ≤ L c j) (side0_ge_two : 2 ≤ L (nk T - 1) 0) :
294 cA T L < rimN T L ∧ cB T L ω < rimN T L ∧ cA T L ≠ cB T L ω ∧
295 ownGo L (pcs T) (prv (rimN T L) (cA T L)) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.A (nk T - 1)) ∧
296 ownGo L (pcs T) (prv (rimN T L) (cB T L ω)) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.B (nk T - 1)) := by
297 by_cases is_sigma : T = .Sigma
298 · subst is_sigma
299 -- a Σ parent: `A` on its side 5
300 exact corners_sigma len_pos side0_ge_two
301 · -- any other parent: `A` at its vertex 0
302 simp only [cA, cB, ite_eq_right is_sigma]
303 exact corners_nonSigma is_sigma len_pos side0_ge_two
305end CornersAt
307/-! ### "Has the signature" -/
309/-- **The composition `C_T(L, d, ω)` has the signature**, as §7.1 words it: it is well formed; it has no closed strand;
310the Γ child's corners `A` and `B` are its rim vertices at the adjacent positions `cA` and `cB` of Table 3's rim; every
311other rim vertex `p` is a hook, its port `gR p` joined to its port `gL p`; and `A` and `B` carry the crossover,
312`R(A) ↔ R(B)` and `L(A) ↔ L(B)`. -/
313structure CompSig (T : Kind) (L : Nat → Nat → Nat) (d : Nat) (ω : Bool) : Prop where
314 wf : (Comp.ofLens T L d ω).toGluing.WF
315 noLoops : ∀ x, (Comp.ofLens T L d ω).toGluing.Valid x → ∃ r, (Comp.ofLens T L d ω).toGluing.FullReach x r
316 cA_lt : cA T L < rimN T L
317 cB_lt : cB T L ω < rimN T L
318 at_A : gL T L (cA T L) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.A (nk T - 1), true)
319 at_B : gL T L (cB T L ω) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.B (nk T - 1), true)
320 hooks : ∀ p, p < rimN T L → p ≠ cA T L → p ≠ cB T L ω →
321 (Comp.ofLens T L d ω).toGluing.FullReach (gR T L d ω p) (gL T L p)
322 crossR : (Comp.ofLens T L d ω).toGluing.FullReach (gL T L (cA T L)) (gL T L (cB T L ω))
323 crossL : (Comp.ofLens T L d ω).toGluing.FullReach (gR T L d ω (cA T L)) (gR T L d ω (cB T L ω))
325section FromSig
327variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
329/-- **`Sig` gives "has the signature"**: the turning form that the proof of Lemma 7.1 carries through cuts, read at
330Table 3's rim positions. A rim vertex found by turning is the one at a position (`own_rot`); it is a corner only at
331`cA` or `cB`, since different positions are different edges (`own_inj`); and the crossover walks start at the ports
332`gR` of the corners, since turning about a vertex is one to one on rim vertices (`Rot.inj`). -/
333theorem compSig_of_sig (len_pos : ∀ c j, 1 ≤ L c j) (side0_ge_two : 2 ≤ L (nk T - 1) 0)
334 (has_sig : Sig (Comp.ofLens T L d ω).toGluing (nk T - 1)) : CompSig T L d ω := by
335 obtain ⟨pA_lt, pB_lt, _, at_A, at_B⟩ := corners_at (d := d) (ω := ω) len_pos side0_ge_two
336 -- the composition is well formed
337 have wf := has_sig.wf
338 -- turning about the vertex of `gR cA` reaches the Γ child's corner `A`
339 have rot_A := gR_rot (d := d) (ω := ω) len_pos pA_lt
340 rw [at_A] at rot_A
341 -- and about that of `gR cB`, its corner `B`
342 have rot_B := gR_rot (d := d) (ω := ω) len_pos pB_lt
343 rw [at_B] at rot_B
344 -- `gL cA` is the port `R` at the Γ child's corner `A`
345 have gL_A : gL T L (cA T L) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.A (nk T - 1), true) := by
346 simp only [gL, at_A]
347 -- `gL cB` is the port `R` at its corner `B`
348 have gL_B : gL T L (cB T L ω) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.B (nk T - 1), true) := by
349 simp only [gL, at_B]
350 refine ⟨wf, has_sig.noLoops, pA_lt, pB_lt, gL_A, gL_B, fun p p_lt ne_A ne_B => ?_, ?_, ?_⟩
351 · -- a hook: turning about the vertex of `gR p` reaches that of `gL p`
352 obtain ⟨c₂, u₂, turn, corner_or_hook⟩ := has_sig.hooks _ _ (gR_rimL len_pos p_lt)
353 -- the vertex turned to is the start of the child edge at position `p - 1`
354 have same_vtx := Rot.unique turn (gR_rot len_pos p_lt)
355 -- it is not one of the Γ child's corners, since `p` is neither `cA` nor `cB`
356 have not_corner : ¬ (c₂ = nk T - 1 ∧ (u₂ = (Comp.ofLens T L d ω).toGluing.A (nk T - 1) ∨
357 u₂ = (Comp.ofLens T L d ω).toGluing.B (nk T - 1))) := by
358 rintro ⟨rfl, at_cA | at_cB⟩
359 · rw [at_cA, ← at_A] at same_vtx
360 exact ne_A (prv_inj p_lt pA_lt (own_inj len_pos (prv_lt pA_lt) (prv_lt p_lt) same_vtx).symm)
361 · rw [at_cB, ← at_B] at same_vtx
362 exact ne_B (prv_inj p_lt pB_lt (own_inj len_pos (prv_lt pB_lt) (prv_lt p_lt) same_vtx).symm)
363 rcases corner_or_hook with corner | hook
364 · exact absurd corner not_corner
365 · have gL_eq : gL T L p = (c₂, u₂, true) := by simp only [gL, ← same_vtx] -- `R` at the vertex turned to
366 rw [gL_eq]; exact hook
367 · -- `R(A) ↔ R(B)`: the crossover of `Sig`
368 rw [gL_A, gL_B]; exact has_sig.crossR
369 · -- `L(A) ↔ L(B)`: the vertices that turn to `A` and `B` are those of `gR cA` and `gR cB`
370 obtain ⟨cA', uA', cB', uB', rim_A, turn_A, rim_B, turn_B, reach⟩ := has_sig.crossL
371 -- the vertex turning to `A` is that of `gR cA`
372 have vtx_A := Rot.inj wf rim_A (gR_rimL len_pos pA_lt) turn_A rot_A
373 -- the vertex turning to `B` is that of `gR cB`
374 have vtx_B := Rot.inj wf rim_B (gR_rimL len_pos pB_lt) turn_B rot_B
375 -- so `gR cA` is the start of the crossover walk
376 have gR_A : gR T L d ω (cA T L) = (cA', uA', false) := by
377 rw [Prod.ext_iff] at vtx_A; exact Prod.ext vtx_A.1.symm (Prod.ext vtx_A.2.symm rfl)
378 -- and `gR cB` its end
379 have gR_B : gR T L d ω (cB T L ω) = (cB', uB', false) := by
380 rw [Prod.ext_iff] at vtx_B; exact Prod.ext vtx_B.1.symm (Prod.ext vtx_B.2.symm rfl)
381 rw [gR_A, gR_B]; exact reach
383end FromSig
385/-! ### Table 3's rim as `Comp.check` lists it -/
387section CheckRim
389/-- Table 3's rim as a list, in the parent's own order: the edges of each listed side, from its last edge to its
390first (as `ownGo` reads them). -/
391def ownList (L : Nat → Nat → Nat) (l : List (Nat × Nat)) : List (Nat × Nat) :=
392 l.flatMap fun x => (List.range (L x.1 x.2)).map fun i => (x.1, pos (L x.1) x.2 + L x.1 x.2 - 1 - i)
394/-- The list has the total length of its pieces. -/
395theorem ownList_length (L : Nat → Nat → Nat) : ∀ l, (ownList L l).length = totL L l
396 | [] => rfl
397 | (c, j) :: rest => by
398 simp only [ownList, List.flatMap_cons, List.length_append, List.length_map, List.length_range, totL]
399 rw [← ownList_length L rest]; rfl
401/-- Entry `p` of the list is the edge `ownGo` finds at position `p`. -/
402theorem ownList_getElem? (L : Nat → Nat → Nat) : ∀ l p, p < totL L l → (ownList L l)[p]? = some (ownGo L l p)
403 | [], p, p_lt => by simp [totL] at p_lt
404 | (c, j) :: rest, p, p_lt => by
405 simp only [totL] at p_lt
406 simp only [ownList, List.flatMap_cons]
407 by_cases in_head : p < L c j
408 · -- in the first piece
409 rw [List.getElem?_append_left (by simp only [List.length_map, List.length_range]; exact in_head),
410 List.getElem?_map, List.getElem?_range in_head]
411 simp only [ownGo, ite_eq_left in_head, Option.map_some]
412 · -- in a later piece: by induction
413 rw [List.getElem?_append_right (by simp only [List.length_map, List.length_range]; omega)]
414 simp only [List.length_map, List.length_range]
415 rw [show (rest.flatMap fun x => (List.range (L x.1 x.2)).map fun i => (x.1, pos (L x.1) x.2 + L x.1 x.2 - 1 - i))
416 = ownList L rest from rfl, ownList_getElem? L rest (p - L c j) (by omega)]
417 simp only [ownGo, ite_eq_right in_head]
419/-- Two functions that agree on a list give the same `flatMap` over it. -/
420theorem flatMap_congr_mem {α β : Type} {f g : α → List β} : ∀ (l : List α), (∀ x ∈ l, f x = g x) →
421 l.flatMap f = l.flatMap g
422 | [], _ => rfl
423 | x :: rest, agree => by
424 rw [List.flatMap_cons, List.flatMap_cons, agree x List.mem_cons_self,
425 flatMap_congr_mem rest (fun y mem => agree y (List.mem_cons_of_mem _ mem))]
427variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
429/-- `Comp.check` lists Table 3's rim (`rimEdges`, in the children's sense) as `ownList` backwards. -/
430theorem rimEdges_eq : (Comp.ofLens T L d ω).rimEdges = (ownList L (pcs T)).reverse := by
431 show (((pside T).flatMap id).flatMap fun (x : Nat × Nat) =>
432 (List.range (((Comp.ofLens T L d ω).kid x.1).len.getD x.2 0)).map fun i =>
433 (x.1, ((Comp.ofLens T L d ω).kid x.1).U.getD x.2 0 + ((Comp.ofLens T L d ω).kid x.1).len.getD x.2 0 - 1 -
434 i)).reverse = _
435 congr 1
437 intro x mem
438 -- the piece is a side of an actual child
439 obtain ⟨c_lt, j_lt, _⟩ := pcs_valid T x mem
440 rw [ofLens_len c_lt j_lt, ofLens_U c_lt (by omega)]
442/-- The rim that `Comp.check` reads has `rimN T L` vertices. -/
443theorem rimVertexPorts_length : (Comp.ofLens T L d ω).rimVertexPorts.length = rimN T L := by
444 simp only [Comp.rimVertexPorts, List.length_map, List.length_range, rimEdges_eq, List.length_reverse,
447/-- **The rim vertex that `Comp.check` numbers `t` is the one at position `N - 1 - t`** (the check counts in the
448children's sense, positions in the parent's own order): its ports are `gR` and `gL` there. -/
449theorem vtx_eq {t : Nat} (t_lt : t < rimN T L) :
450 (Comp.ofLens T L d ω).vtx t = (gR T L d ω (rimN T L - 1 - t), gL T L (rimN T L - 1 - t)) := by
451 -- entry `t` of the rim list, read backwards
452 have entry : ∀ s, s < rimN T L →
453 (Comp.ofLens T L d ω).rimEdges.getD s (0, 0) = ownGo L (pcs T) (rimN T L - 1 - s) := by
454 intro s s_lt
455 rw [List.getD_eq_getElem?_getD, rimEdges_eq, List.getElem?_reverse (by rw [ownList_length]; exact s_lt),
456 ownList_length, ownList_getElem? L _ _ (by show rimN T L - 1 - s < rimN T L; omega)]
457 rfl
458 -- the next entry, cyclically, is the edge at the position before
459 have next : (Comp.ofLens T L d ω).rimEdges.getD ((t + 1) % rimN T L) (0, 0) =
460 ownGo L (pcs T) (prv (rimN T L) (rimN T L - 1 - t)) := by
461 rw [entry _ (Nat.mod_lt _ (by omega))]
462 congr 1
463 simp only [prv]
464 by_cases at_end : t + 1 = rimN T L
465 · rw [at_end, Nat.mod_self, ite_eq_left (by omega)]; omega
466 · rw [Nat.mod_eq_of_lt (by omega), ite_eq_right (by omega)]; omega
468 rw [List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range (by
469 rw [rimEdges_eq, List.length_reverse, ownList_length]; exact t_lt)]
470 simp only [Option.map_some, Option.getD_some]
471 rw [show (Comp.ofLens T L d ω).rimEdges.length = rimN T L by rw [rimEdges_eq, List.length_reverse, ownList_length],
472 entry t t_lt, next]
473 rfl
475end CheckRim
477/-! ### `Comp.check` gives `Sig` -/
479section FromCheck
481variable {T : Kind} {L : Nat → Nat → Nat} {d : Nat} {ω : Bool}
483/-- The composition has the kind's children. -/
484theorem ofLens_kids_length : (Comp.ofLens T L d ω).kids.length = nk T := by
487/-- What `Comp.check`'s search for a corner found: if the index it returns is a rim vertex, that vertex's port `R` is
488the one searched for. -/
489theorem found_corner {C : Comp} {u t : Nat}
490 (t_eq : t = (C.rimVertexPorts.findIdx? fun (x : GPort × GPort) => x.2 == (C.kids.length - 1, u, true)).getD
491 C.rimVertexPorts.length)
492 (t_lt : t < C.rimVertexPorts.length) : (C.vtx t).2 = (C.kids.length - 1, u, true) := by
493 cases found : C.rimVertexPorts.findIdx? (fun (x : GPort × GPort) => x.2 == (C.kids.length - 1, u, true)) with
494 | none => rw [found, Option.getD_none] at t_eq; omega
495 | some i =>
496 rw [found, Option.getD_some] at t_eq
497 subst t_eq
498 obtain ⟨i_lt, pred_i, _⟩ := List.findIdx?_eq_some_iff_getElem.mp found
499 simp only [Comp.vtx, List.getD_eq_getElem?_getD, List.getElem?_eq_getElem i_lt, Option.getD_some]
500 simpa using pred_i
502/-- **Computation 7.3's check gives `Sig`**, the form in which the proof of Lemma 7.1 carries the signature through
503cuts: every rim vertex found by turning about a child's vertex is the check's rim vertex at some position
504(`own_surj`, `own_rot`, `vtx_eq`), so the check's hooks, corners and crossover are `Sig`'s. -/
505theorem sig_of_check (len_pos : ∀ c j, 1 ≤ L c j) (checked : (Comp.ofLens T L d ω).check ω = true) :
506 Sig (Comp.ofLens T L d ω).toGluing (nk T - 1) := by
507 obtain ⟨wf, no_loops, hooks, tA_lt, tB_lt, _, cross_R, cross_L⟩ := Comp.check_sound _ checked
508 -- what the searches for the corners found, at the check's indices `tA` and `tB`
509 have found_A := found_corner (C := Comp.ofLens T L d ω) (t := (Comp.ofLens T L d ω).tA) rfl tA_lt
510 -- (and for `B`)
511 have found_B := found_corner (C := Comp.ofLens T L d ω) (t := (Comp.ofLens T L d ω).tB) rfl tB_lt
512 rw [rimVertexPorts_length] at tA_lt tB_lt hooks
513 rw [ofLens_kids_length] at found_A found_B
514 -- the check's vertices at `tA` and `tB` are the rim vertices at the positions `N - 1 - tA` and `N - 1 - tB`
515 rw [vtx_eq tA_lt] at found_A cross_R cross_L
516 rw [vtx_eq tB_lt] at found_B cross_R cross_L
517 generalize pA_def : rimN T L - 1 - (Comp.ofLens T L d ω).tA = pA at found_A cross_R cross_L
518 generalize pB_def : rimN T L - 1 - (Comp.ofLens T L d ω).tB = pB at found_B cross_R cross_L
519 -- the positions are on the rim
520 have pA_lt : pA < rimN T L := by omega
521 -- (both of them)
522 have pB_lt : pB < rimN T L := by omega
523 -- the child edge before `pA` starts at the Γ child's corner `A`
524 have own_A : ownGo L (pcs T) (prv (rimN T L) pA) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.A (nk T - 1)) := by
525 simp only [gL, Prod.mk.injEq] at found_A
526 exact Prod.ext found_A.1 found_A.2.1
527 -- and the one before `pB` at its corner `B`
528 have own_B : ownGo L (pcs T) (prv (rimN T L) pB) = (nk T - 1, (Comp.ofLens T L d ω).toGluing.B (nk T - 1)) := by
529 simp only [gL, Prod.mk.injEq] at found_B
530 exact Prod.ext found_B.1 found_B.2.1
531 refine ⟨wf, no_loops, fun c u rim_L => ?_, ?_, ?_, ?_, ?_, ?_⟩
532 · -- a parent rim vertex: the check's rim vertex at some position `p`
533 obtain ⟨c_lt_n, u_lt, unglued⟩ := rim_L
534 -- `c` is a child
535 have c_lt : c < nk T := by rwa [ofLens_n] at c_lt_n
536 -- the edge before `u` is a parent rim edge, at some position `p`
537 obtain ⟨p, p_lt, at_p⟩ := own_surj (d := d) (ω := ω) len_pos c_lt
538 (by rw [← ofLens_E (d := d) (ω := ω) c_lt]; exact prv_lt u_lt) unglued
539 -- `gR p` is the port `L` at `u`
540 have gR_eq : gR T L d ω p = (c, u, false) := by
541 simp only [gR, at_p]; rw [nxt_prv u_lt]
542 -- turning about `u` reaches the start of the child edge at position `p - 1`
543 have turn := gR_rot (d := d) (ω := ω) len_pos p_lt
544 rw [gR_eq] at turn
545 refine ⟨_, _, turn, ?_⟩
546 -- the check's index of the vertex at position `p`
547 have vtx_t := vtx_eq (d := d) (ω := ω) (show rimN T L - 1 - p < rimN T L by omega)
548 rw [show rimN T L - 1 - (rimN T L - 1 - p) = p by omega] at vtx_t
549 by_cases is_A : rimN T L - 1 - p = (Comp.ofLens T L d ω).tA
550 · -- at the corner `A`
551 have p_eq : p = pA := by omega
552 subst p_eq
553 exact Or.inl ⟨by rw [own_A], Or.inl (by rw [own_A])⟩
554 · by_cases is_B : rimN T L - 1 - p = (Comp.ofLens T L d ω).tB
555 · -- at the corner `B`
556 have p_eq : p = pB := by omega
557 subst p_eq
558 exact Or.inl ⟨by rw [own_B], Or.inr (by rw [own_B])⟩
559 · -- a hook, by the check
560 have hook := hooks _ (by omega) is_A is_B
561 rw [vtx_t, gR_eq] at hook
562 exact Or.inr hook
563 · -- the Γ child is a child
565 -- every kind has a child
566 have := last_lt T
567 omega
568 · -- the Γ child's edge at `A` is on the parent's rim
569 have unglued := (own_mate (d := d) (ω := ω) len_pos (prv_lt pA_lt)).2.2
570 rwa [own_A] at unglued
571 · -- and so is its edge at `B`
572 have unglued := (own_mate (d := d) (ω := ω) len_pos (prv_lt pB_lt)).2.2
573 rwa [own_B] at unglued
574 · -- `R(A) ↔ R(B)`
575 rwa [found_A, found_B] at cross_R
576 · -- `L(A) ↔ L(B)`, from the vertices of `gR pA` and `gR pB`
577 -- turning about the vertex of `gR pA` reaches `A`
578 have rot_A := gR_rot (d := d) (ω := ω) len_pos pA_lt
579 rw [own_A] at rot_A
580 -- and about that of `gR pB`, `B`
581 have rot_B := gR_rot (d := d) (ω := ω) len_pos pB_lt
582 rw [own_B] at rot_B
583 exact ⟨_, _, _, _, gR_rimL len_pos pA_lt, rot_A, gR_rimL len_pos pB_lt, rot_B, cross_L⟩
585end FromCheck
587end SpectreKnot.Statement
589namespace SpectreKnot.Compose
591open Gluing Statement
593/-- Every level-1 letter length is positive (each is at least 5). -/
594theorem letterLen_one_pos : ∀ x, 1 ≤ letterLen 1 x := by intro x; cases x <;> decide
596/-- The Γ child's side 0 has at least two edges at level 1 (it has 7). -/
597theorem gamma_side0_one : ∀ T : Kind, 2 ≤ letterLen 1 (letterOf (kidAt T (nk T - 1)) 0) := by
598 intro T; cases T <;> decide
In the paper Computation 7.3 The compositions at the level-1 lengths
600/-- **The base case of the induction**: Computation 7.3, the kernel's check (`compositions_level1`), in the form
601`Sig` that the proof of Lemma 7.1 carries through cuts. -/
602theorem sig_base (T : Kind) (ω : Bool) : Sig (Comp.ofPattern T (letterLen 1) (dOff 1) ω).toGluing (nk T - 1) :=
603 sig_of_check (L := fun c j => letterLen 1 (letterOf (kidAt T c) j)) (fun _ _ => letterLen_one_pos _)
In the paper Computation 7.3 The compositions at the level-1 lengths
606/-- **Computation 7.3, as the paper words it**: for each of the nine kinds `T` and both signs `ω`, the composition
607`C_T(ℓ₁, d₁, ω)` has the signature (`CompSig`). -/
608theorem comp_7_3 (T : Kind) (ω : Bool) :
609 CompSig T (fun c j => letterLen 1 (letterOf (kidAt T c) j)) (dOff 1) ω :=
612end SpectreKnot.Compose

← SpectreKnot/Signature.leanSpectreKnot/Parity.lean →