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

lean/SpectreKnot/ParentSig.lean

399 lines · 24 declarations, each with its own page · on GitHub ·

The induction step of Thm 7.6, at tile level. If the children of compose T child have the signature (with the corners and side lengths of the abstract composition), and the composition has the signature as §7.1 words it (CompSig), then so does the parent (Kids.parent_sig): its rim is Table 3's (rim_edgeAt), its six vertices are where the parent's side lengths put them (parent_vtx), and its rim ports are joined as hooks except at the corners cA, cB, where they cross over.

← SpectreKnot/Bridge.leanSpectreKnot/NewWalk.lean →

All 39 files, and the declarations of this one
1/-
2**The induction step of Thm 7.6, at tile level.** If the children of `compose T child` have the signature (with the
3corners and side lengths of the abstract composition), and the composition has the signature as §7.1 words it
4(`CompSig`), then so does the parent (`Kids.parent_sig`): its rim is Table 3's (`rim_edgeAt`), its six vertices are
5where the parent's side lengths put them (`parent_vtx`), and its rim ports are joined as hooks except at the corners
6`cA`, `cB`, where they cross over.
7-/
9
10namespace SpectreKnot.Statement
12open Pattern Compose Gluing
14/-- Later children start later: the first tile number `offC child c` grows with `c`. -/
15theorem offC_mono (child : Nat → Patch) {a b : Nat} (a_le : a ≤ b) : offC child a ≤ offC child b := by
16 induction b with
17 | zero =>
18 -- `a ≤ 0`, so `a = 0`
19 have a_zero : a = 0 := by omega
20 subst a_zero; exact Nat.le_refl _
21 | succ b ih =>
22 by_cases a_eq : a = b + 1
23 · subst a_eq; exact Nat.le_refl _
24 · have := ih (by omega) -- up to `b` by induction
25 rw [offC_succ]; omega
27/-- Tile `t` of child `c`, renumbered in the parent, comes before the first tile of any later child `n`. -/
28theorem tile_lt (child : Nat → Patch) {c t n : Nat} (c_lt : c < n) (t_lt : t < (child c).tiles) :
29 t + offC child c < offC child n := by
30 -- child `n` starts no earlier than child `c + 1`
31 have later_start := offC_mono child (show c + 1 ≤ n by omega)
32 rw [offC_succ] at later_start; omega
34/-! ### The parent's rim and vertices -/
36section Rim
38variable {T : Kind} {child : Nat → Patch} {L : Nat → Nat → Nat}
40/-- The parent's rim edges, child by child (`compose`'s rim). -/
41abbrev rimPiece (child : Nat → Patch) : Nat × Nat → List (Nat × Nat)
42 | (c, j) => ((child c).side j).reverse.map fun e => (e.1 + offC child c, e.2)
44/-- `compose`'s rim is made of the children's sides listed in Table 3, each backwards and renumbered. -/
45theorem compose_rim : (compose T child).rim = (pcs T).flatMap (rimPiece child) := rfl
47/-- If the children's vertices sit where the side lengths `L` put them, the rim made of the pieces `l` has length
48`totL L l`. -/
49theorem rimPiece_length (shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧
50 (child c).E = pos (L c) 6) : ∀ (l : List (Nat × Nat)), (∀ x ∈ l, x.1 < nk T ∧ x.2 < 6) →
51 (l.flatMap (rimPiece child)).length = totL L l := by
52 intro l
53 induction l with
54 | nil => intro _; rfl
55 | cons x rest ih =>
56 obtain ⟨c, j⟩ := x
57 intro valid
58 obtain ⟨c_lt, j_lt⟩ := valid (c, j) List.mem_cons_self
59 obtain ⟨vtx_eq, len_eq⟩ := shape c c_lt
60 rw [List.flatMap_cons, List.length_append, ih (fun x mem => valid x (List.mem_cons_of_mem _ mem))]
61 simp only [rimPiece, List.length_map, List.length_reverse, side_length vtx_eq len_eq j_lt, totL]
63/-- If the children's vertices sit where the side lengths `L` put them, entry `p` of the rim made of the pieces `l`
64is the child's edge `ownGo L l p`, renumbered as an edge of the parent. -/
65theorem rimPiece_getD (shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧
66 (child c).E = pos (L c) 6) : ∀ (l : List (Nat × Nat)), (∀ x ∈ l, x.1 < nk T ∧ x.2 < 6) →
67 ∀ p, p < totL L l → (l.flatMap (rimPiece child)).getD p (0, 0) =
68 (((child (ownGo L l p).1).edgeAt (ownGo L l p).2).1 + offC child (ownGo L l p).1,
69 ((child (ownGo L l p).1).edgeAt (ownGo L l p).2).2) := by
70 intro l
71 induction l with
72 | nil => intro _ p p_lt; simp [totL] at p_lt
73 | cons x rest ih =>
74 obtain ⟨c, j⟩ := x
75 intro valid p p_lt
76 obtain ⟨c_lt, j_lt⟩ := valid (c, j) List.mem_cons_self
77 obtain ⟨vtx_eq, len_eq⟩ := shape c c_lt
78 -- the first piece has the length of its side
79 have piece_len : (rimPiece child (c, j)).length = L c j := by
80 simp only [rimPiece, List.length_map, List.length_reverse, side_length vtx_eq len_eq j_lt]
81 simp only [totL] at p_lt
82 rw [List.flatMap_cons, List.getD_eq_getElem?_getD]
83 by_cases in_head : p < L c j
84 · -- in the first piece: an edge of side `j`, counted from its end
85 rw [List.getElem?_append_left (by rw [piece_len]; exact in_head)]
86 simp only [ownGo, ite_eq_left in_head]
87 -- side `j` has `L c j` edges
88 have side_len := side_length vtx_eq len_eq j_lt
89 simp only [rimPiece, List.getElem?_map]
90 rw [List.getElem?_reverse (by rw [side_len]; exact in_head), side_len,
91 side_getElem? vtx_eq len_eq j_lt (show L c j - 1 - p < L c j by omega),
92 show pos (L c) j + (L c j - 1 - p) = pos (L c) j + L c j - 1 - p by omega]
93 rfl
94 · -- in a later piece: by induction
95 rw [List.getElem?_append_right (by rw [piece_len]; omega), piece_len, ← List.getD_eq_getElem?_getD,
96 ih (fun x mem => valid x (List.mem_cons_of_mem _ mem)) (p - L c j) (by omega)]
97 simp only [ownGo, ite_eq_right in_head]
99variable (T) in
100/-- Table 3's pieces are sides of actual children. -/
101theorem pcs_valid' : ∀ x ∈ pcs T, x.1 < nk T ∧ x.2 < 6 :=
102 fun x mem => ⟨(pcs_valid T x mem).1, (pcs_valid T x mem).2.1⟩
104/-- The parent's rim length. -/
105theorem compose_E (shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧
106 (child c).E = pos (L c) 6) : (compose T child).E = rimN T L := by
107 show (compose T child).rim.length = _
110/-- **The parent's rim is Table 3's**: rim edge `p` of the parent is edge `k` of child `c`, `(c, k) = ownGo p`. -/
111theorem rim_edgeAt (shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧
112 (child c).E = pos (L c) 6) {p : Nat} (p_lt : p < rimN T L) :
113 (compose T child).edgeAt p =
114 (((child (ownGo L (pcs T) p).1).edgeAt (ownGo L (pcs T) p).2).1 + offC child (ownGo L (pcs T) p).1,
115 ((child (ownGo L (pcs T) p).1).edgeAt (ownGo L (pcs T) p).2).2) := by
116 show (compose T child).rim.getD p (0, 0) = _
118 exact rimPiece_getD shape _ (pcs_valid' T) p p_lt
120/-- The parent's side lengths: the sum over Table 3's pieces. -/
121def parentLen (T : Kind) (L : Nat → Nat → Nat) (J : Nat) : Nat := totL L ((pside T).getD J [])
123/-- Table 3 has a row for each of the parent's six sides. -/
124theorem pside_length : ∀ T, (pside T).length = 6 := by intro T; cases T <;> rfl
126/-- The pieces of the parent's first `J` sides have total length `pos (parentLen T L) J`: where vertex `J` sits. -/
127theorem totL_take (L : Nat → Nat → Nat) (T : Kind) : ∀ J, J ≤ 6 →
128 totL L (((pside T).take J).flatMap id) = pos (parentLen T L) J := by
129 intro J
130 induction J with
131 | zero => intro _; rfl
132 | succ J ih =>
133 intro J_le
134 -- Table 3 has a row for side `J`
135 have J_lt : J < (pside T).length := by rw [pside_length]; omega
136 rw [List.take_add_one, List.flatMap_append, totL_append, ih (by omega), pos_succ, List.getElem?_eq_getElem J_lt]
137 simp only [Option.toList_some, List.flatMap_cons, List.flatMap_nil, List.append_nil, id, parentLen,
138 List.getD_eq_getElem?_getD, List.getElem?_eq_getElem J_lt, Option.getD_some]
140/-- If the children's vertices sit where the side lengths `L` put them, the sides listed in `l` have total length
141`totL L l`. -/
142theorem sideLens_sum (shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧
143 (child c).E = pos (L c) 6) : ∀ (l : List (Nat × Nat)), (∀ x ∈ l, x.1 < nk T ∧ x.2 < 6) →
144 (l.map fun (c, j) => ((child c).side j).length).sum = totL L l := by
145 intro l
146 induction l with
147 | nil => intro _; rfl
148 | cons x rest ih =>
149 obtain ⟨c, j⟩ := x
150 intro valid
151 obtain ⟨c_lt, j_lt⟩ := valid (c, j) List.mem_cons_self
152 obtain ⟨vtx_eq, len_eq⟩ := shape c c_lt
153 simp only [List.map_cons, List.sum_cons, totL, side_length vtx_eq len_eq j_lt,
154 ih (fun x mem => valid x (List.mem_cons_of_mem _ mem))]
156/-- **The parent's vertices** sit where the parent's side lengths put them. -/
157theorem parent_vtx (shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧
158 (child c).E = pos (L c) 6) : (compose T child).vtx = (List.range 7).map (pos (parentLen T L)) := by
159 show (List.range 7).map (fun J => ((((Pattern.pside T).take J).flatMap id).map fun (c, j) =>
160 ((child c).side j).length).sum) = _
161 apply List.map_congr_left
162 intro J J_mem
163 rw [List.mem_range] at J_mem
164 -- the pieces of the first `J` sides are sides of actual children
165 have first_valid : ∀ x ∈ ((pside T).take J).flatMap id, x.1 < nk T ∧ x.2 < 6 := by
166 intro x mem
167 apply pcs_valid' T
168 simp only [pcs, List.mem_flatMap, id] at mem ⊢
169 obtain ⟨l, l_mem, x_mem⟩ := mem
170 exact ⟨l, List.mem_of_mem_take l_mem, x_mem⟩
171 rw [sideLens_sum shape _ first_valid, totL_take L T J (by omega)]
173/-- The parent's rim length is the total of its six side lengths. -/
174theorem rimN_eq (L : Nat → Nat → Nat) (T : Kind) : rimN T L = pos (parentLen T L) 6 := by
175 rw [← totL_take L T 6 (Nat.le_refl _)]
176 simp only [rimN, pcs]
177 rw [List.take_of_length_le (by simp [pside_length])]
179end Rim
181/-! ### The parent's signature -/
183namespace Kids
185set_option linter.unusedSectionVars false
187variable {T : Kind} {child : Nat → Patch} {L : Nat → Nat → Nat} {d : Nat} {ω o : Bool}
188 (kids : Kids T child L d ω o)
190include kids
192/-- The parent's port `R(p)` (its orientation `!o` is opposite to the children's) is the gluing's port `gR p`. -/
193theorem bport_R {p : Nat} (p_lt : p < rimN T L) :
194 (compose T child).bport (!o) (p, true) = ιP child o (gR T L d ω p) := by
195 obtain ⟨c_lt, k_lt, _⟩ := own_mate (d := d) (ω := ω) kids.len_pos p_lt
196 -- the composition's rim length for the child is the child's
197 have E_eq := kids.E_eq c_lt
198 rw [ofLens_E c_lt] at E_eq
199 -- so the edge is on the child's rim
200 have k_lt' : (ownGo L (pcs T) p).2 < (child (ownGo L (pcs T) p).1).E := by rw [← E_eq]; exact k_lt
201 simp only [gR, ιP, Patch.bport, rim_edgeAt kids.shape p_lt, ofLens_E c_lt, E_eq, prv_nxt k_lt']
202 cases o <;> rfl
204/-- The parent's port `L(p)` is the gluing's port `gL p`. -/
205theorem bport_L {p : Nat} (p_lt : p < rimN T L) :
206 (compose T child).bport (!o) (p, false) = ιP child o (gL T L p) := by
207 -- the position before `p` is on the rim too
208 have prv_lt_N : prv (rimN T L) p < rimN T L := prv_lt p_lt
209 simp only [gL, ιP, Patch.bport, compose_E kids.shape, rim_edgeAt kids.shape prv_lt_N]
210 cases o <;> rfl
212/-- The vertex of `gR p` is a parent rim vertex reached along the rim: the edge before it is unglued. -/
213theorem gR_rimL {p : Nat} (p_lt : p < rimN T L) :
214 (Comp.ofLens T L d ω).toGluing.RimL (gR T L d ω p).1 (gR T L d ω p).2.1 :=
215 Statement.gR_rimL kids.len_pos p_lt
217/-- Turning about the vertex of `gR p` reaches the start of the child edge at position `p - 1`, the vertex of
218`gL p`. -/
219theorem gR_rot {p : Nat} (p_lt : p < rimN T L) :
220 (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)) :=
221 Statement.gR_rot kids.len_pos p_lt
223/-- `gR p` is a port of an actual child, at an actual rim vertex. -/
224theorem gR_valid {p : Nat} (p_lt : p < rimN T L) : (Comp.ofLens T L d ω).toGluing.Valid (gR T L d ω p) :=
225 Statement.gR_valid kids.len_pos p_lt
227/-- `gL p` is a port of an actual child, at an actual rim vertex. -/
228theorem gL_valid {p : Nat} (p_lt : p < rimN T L) : (Comp.ofLens T L d ω).toGluing.Valid (gL T L p) :=
229 Statement.gL_valid kids.len_pos p_lt
231/-- `gR p` is on the parent's rim: nothing lies across it. -/
232theorem gR_sigma {p : Nat} (p_lt : p < rimN T L) :
233 (Comp.ofLens T L d ω).toGluing.sigma (gR T L d ω p) = none :=
234 Statement.gR_sigma kids.len_pos p_lt
236/-- `gL p` is on the parent's rim: nothing lies across it. -/
237theorem gL_sigma {p : Nat} (p_lt : p < rimN T L) :
238 (Comp.ofLens T L d ω).toGluing.sigma (gL T L p) = none :=
239 Statement.gL_sigma kids.len_pos p_lt
In the paper Theorem 7.6 Signature Theorem
241/-- **The parent has the signature** (Thm 7.6's induction step, at tile level), at the rim positions `cA`, `cB` of the
242Γ child's corners: Prop 7.4 for the composition of the children (`Kids.csig`), read port by port. -/
243theorem parent_sig : (compose T child).HasSig (!o) (cA T L) (cB T L ω) := by
244 -- the composition is well formed
245 have wf := kids.csig.wf
246 -- the children's vertices sit where the side lengths put them
247 have shape := kids.shape
248 -- the parent's rim length
249 have E_eq := compose_E (child := child) shape
250 -- the corners' positions are on the rim
251 have pA_lt := kids.csig.cA_lt
252 -- (both of them)
253 have pB_lt := kids.csig.cB_lt
254 refine ⟨?_, ?_, ?_, ?_, ?_, kids.noClosed, ?_⟩
255 · -- tiles
256 show 0 < offC child (nk T)
257 -- there is a child
258 have has_child : 0 < nk T := by cases T <;> decide
259 -- whose tiles come before the end
260 have := tile_lt child has_child (kids.tiles_pos 0 has_child)
261 omega
262 · -- rim edges
263 intro p p_lt
264 rw [E_eq] at p_lt
265 obtain ⟨c_lt, k_lt, unglued⟩ := own_mate (d := d) (ω := ω) kids.len_pos p_lt
266 -- the child edge is on the child's rim
267 have k_lt' : (ownGo L (pcs T) p).2 < (child (ownGo L (pcs T) p).1).E := by rw [(shape _ c_lt).2]; exact k_lt
268 obtain ⟨t_lt, i_lt, _⟩ := (kids.sig _ c_lt).rim_ok _ k_lt'
269 rw [rim_edgeAt shape p_lt]
270 refine ⟨tile_lt child c_lt t_lt, i_lt, ?_⟩
271 rw [kids.glue_rimEdge c_lt k_lt', unglued]; rfl
272 · -- no edge twice
273 intro p p' p_lt p_lt' same_edge
274 rw [E_eq] at p_lt p_lt'
275 rw [rim_edgeAt shape p_lt, rim_edgeAt shape p_lt'] at same_edge
276 simp only [Prod.mk.injEq] at same_edge
277 obtain ⟨c_lt, k_lt, _⟩ := own_mate (d := d) (ω := ω) kids.len_pos p_lt
278 obtain ⟨c_lt', k_lt', _⟩ := own_mate (d := d) (ω := ω) kids.len_pos p_lt'
279 -- both child edges are on their children's rims
280 have on_rim : (ownGo L (pcs T) p).2 < (child (ownGo L (pcs T) p).1).E := by rw [(shape _ c_lt).2]; exact k_lt
281 -- (the second)
282 have on_rim' : (ownGo L (pcs T) p').2 < (child (ownGo L (pcs T) p').1).E := by
283 rw [(shape _ c_lt').2]; exact k_lt'
284 obtain ⟨t_lt, _, _⟩ := (kids.sig _ c_lt).rim_ok _ on_rim
285 obtain ⟨t_lt', _, _⟩ := (kids.sig _ c_lt').rim_ok _ on_rim'
286 -- the same parent tile: the same child, and the same tile in it
287 obtain ⟨same_child, same_tile⟩ := owner_unique child t_lt t_lt' (by omega)
288 -- the same child edge, so the same position on the child's rim
289 have same_k : (ownGo L (pcs T) p).2 = (ownGo L (pcs T) p').2 := by
290 apply (kids.sig _ c_lt).rim_inj _ _ on_rim (by rw [same_child]; exact on_rim')
291 rw [same_child]; rw [same_child] at same_tile same_edge; exact Prod.ext same_tile same_edge.2
292 exact own_inj kids.len_pos p_lt p_lt' (Prod.ext same_child same_k)
293 · -- every unglued edge is a rim edge
294 intro t i t_lt i_lt unglued
295 -- the child `c` that tile `t` belongs to, and its number `t₀` there
296 obtain ⟨c, c_lt, start_le, lt_end⟩ := owner_exists child (nk T) t t_lt
297 obtain ⟨t₀, rfl⟩ : ∃ t₀, t = t₀ + offC child c := ⟨t - offC child c, by omega⟩
298 -- `t₀` is a tile of child `c`
299 have t₀_lt : t₀ < (child c).tiles := by omega
300 rw [kids.glue_shift c_lt t₀_lt] at unglued
301 cases glue_eq : (child c).glue t₀ i with
302 | some edge => simp [glueAt, glue_eq] at unglued
303 | none =>
304 -- unglued in the child: rim edge `k` of the child
305 obtain ⟨k, k_lt, at_k⟩ := (kids.sig c c_lt).rim_all t₀ i t₀_lt i_lt glue_eq
306 -- what the parent glues there, by the composition
307 have rim_glue := kids.glue_rimEdge c_lt k_lt
308 rw [at_k, kids.glue_shift c_lt t₀_lt, unglued] at rim_glue
309 -- so the composition leaves it unglued
310 have mate_none : (Comp.ofLens T L d ω).toGluing.mate c k = none := by
311 cases mate_eq : (Comp.ofLens T L d ω).toGluing.mate c k with
312 | none => rfl
313 | some q => rw [mate_eq] at rim_glue; simp at rim_glue
314 obtain ⟨p, p_lt, at_p⟩ :=
315 own_surj (d := d) (ω := ω) kids.len_pos c_lt (by rw [← (shape c c_lt).2]; exact k_lt) mate_none
316 refine ⟨p, by rw [E_eq]; exact p_lt, ?_⟩
317 rw [rim_edgeAt shape p_lt, at_p, at_k]
318 · -- glued edges are edges of actual tiles
319 intro t i t' j t_lt i_lt glued
320 -- the child `c` that tile `t` belongs to, and its number `t₀` there
321 obtain ⟨c, c_lt, start_le, lt_end⟩ := owner_exists child (nk T) t t_lt
322 obtain ⟨t₀, rfl⟩ : ∃ t₀, t = t₀ + offC child c := ⟨t - offC child c, by omega⟩
323 -- `t₀` is a tile of child `c`
324 have t₀_lt : t₀ < (child c).tiles := by omega
325 rw [kids.glue_shift c_lt t₀_lt] at glued
326 cases glue_eq : (child c).glue t₀ i with
327 | some edge =>
328 -- glued inside the child
329 obtain ⟨t₁, i₁⟩ := edge
330 simp only [glueAt, glue_eq, Option.some.injEq, Prod.mk.injEq] at glued
331 obtain ⟨rfl, rfl⟩ := glued
332 obtain ⟨t₁_lt, i₁_lt⟩ := (kids.sig c c_lt).glue_ok t₀ i t₁ i₁ t₀_lt i_lt glue_eq
333 exact ⟨tile_lt child c_lt t₁_lt, i₁_lt⟩
334 | none =>
335 -- on the child's rim, at rim edge `k`: glued to a sibling's rim edge
336 obtain ⟨k, k_lt, at_k⟩ := (kids.sig c c_lt).rim_all t₀ i t₀_lt i_lt glue_eq
337 -- what the parent glues there, by the composition
338 have rim_glue := kids.glue_rimEdge c_lt k_lt
339 rw [at_k, kids.glue_shift c_lt t₀_lt, glued] at rim_glue
340 -- `c` is a child of the composition
341 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact c_lt
342 cases mate_eq : (Comp.ofLens T L d ω).toGluing.mate c k with
343 | none => rw [mate_eq] at rim_glue; simp at rim_glue
344 | some q =>
345 obtain ⟨c', k'⟩ := q
346 rw [mate_eq] at rim_glue
347 simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at rim_glue
348 obtain ⟨c'_lt_n, k'_lt, _⟩ := wf.mate_valid c k c' k' c_lt_n (by rw [kids.E_eq c_lt]; exact k_lt) mate_eq
349 -- `c'` is a child
350 have c'_lt : c' < nk T := by rwa [ofLens_n] at c'_lt_n
351 rw [kids.E_eq c'_lt] at k'_lt
352 obtain ⟨t'_lt, j_lt, _⟩ := (kids.sig c' c'_lt).rim_ok k' k'_lt
353 obtain ⟨tile_eq, edge_eq⟩ := rim_glue
354 subst tile_eq edge_eq
355 exact ⟨tile_lt child c'_lt t'_lt, j_lt⟩
356 · -- the signature
357 intro p s p_lt
358 rw [E_eq] at p_lt
359 by_cases p_eq_A : p = cA T L
360 · -- at the corner `cA`
361 subst p_eq_A
362 simp only [btau, ↓reduceIte]
363 cases s with
364 | true =>
365 -- `R(cA) ↔ R(cB)`: the composition's crossover `L(A) ↔ L(B)`
366 rw [kids.bport_R p_lt, kids.bport_R pB_lt]
367 exact kids.follow_of_fullReach kids.csig.crossL (kids.gR_valid p_lt)
368 | false =>
369 -- `L(cA) ↔ L(cB)`: the composition's crossover `R(A) ↔ R(B)`
370 rw [kids.bport_L p_lt, kids.bport_L pB_lt]
371 exact kids.follow_of_fullReach kids.csig.crossR (kids.gL_valid p_lt)
372 · by_cases p_eq_B : p = cB T L ω
373 · -- at the corner `cB`: the crossover walks, backwards
374 subst p_eq_B
375 simp only [btau, ite_eq_right p_eq_A, ↓reduceIte]
376 cases s with
377 | true =>
378 rw [kids.bport_R p_lt, kids.bport_R pA_lt]
379 exact kids.follow_of_fullReach (kids.csig.crossL.reverse wf (kids.gR_valid pA_lt) (kids.gR_sigma pA_lt))
380 (kids.gR_valid p_lt)
381 | false =>
382 rw [kids.bport_L p_lt, kids.bport_L pA_lt]
383 exact kids.follow_of_fullReach (kids.csig.crossR.reverse wf (kids.gL_valid pA_lt) (kids.gL_sigma pA_lt))
384 (kids.gL_valid p_lt)
385 · -- a hook of the composition
386 simp only [btau, ite_eq_right p_eq_A, ite_eq_right p_eq_B]
387 have reach := kids.csig.hooks p p_lt p_eq_A p_eq_B -- the composition's walk from `gR p` to `gL p`
388 cases s with
389 | true =>
390 rw [kids.bport_R p_lt, Bool.not_true, kids.bport_L p_lt]
391 exact kids.follow_of_fullReach reach (kids.gR_valid p_lt)
392 | false =>
393 rw [kids.bport_L p_lt, Bool.not_false, kids.bport_R p_lt]
394 exact kids.follow_of_fullReach (reach.reverse wf (kids.gR_valid p_lt) (kids.gR_sigma p_lt))
395 (kids.gL_valid p_lt)
397end Kids
399end SpectreKnot.Statement

← SpectreKnot/Bridge.leanSpectreKnot/NewWalk.lean →