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

lean/SpectreKnot/Bridge.lean

438 lines · 23 declarations, each with its own page · on GitHub ·

Lemma 4.2 at tile level. If the children of compose T child have the signature, with the corners and side lengths of the abstract composition Comp.ofLens T L d ω, then following a ribbon of the parent is a walk of that composition: from a child's rim port, the ribbon runs through the child to the port its signature pairs it with (τ), then straight across into the next child (σ) or out of the parent. So the parent has no closed strand when the composition has none (Kids.noClosed), and its rim ports are joined as the composition's walks say (Kids.follow_of_reach).

← SpectreKnot/Reverse.leanSpectreKnot/ParentSig.lean →

All 39 files, and the declarations of this one
1/-
2**Lemma 4.2 at tile level.** If the children of `compose T child` have the signature, with the corners and side
3lengths of the abstract composition `Comp.ofLens T L d ω`, then following a ribbon of the parent is a walk of that
4composition: from a child's rim port, the ribbon runs through the child to the port its signature pairs it with
5(`τ`), then straight across into the next child (`σ`) or out of the parent. So the parent has no closed strand when
6the composition has none (`Kids.noClosed`), and its rim ports are joined as the composition's walks say
7(`Kids.follow_of_reach`).
8-/
13namespace SpectreKnot.Statement
15open Pattern Compose Gluing
17/-- Port `q` of child `c`, renumbered as a port of the parent. -/
18def shiftP (child : Nat → Patch) (c : Nat) (q : Port) : Port := (q.1 + offC child c, q.2.1, q.2.2)
20/-- Renumbering a child's port into the parent commutes with going to the other end of its piece. -/
21theorem pieceEnd_shift (child : Nat → Patch) (c : Nat) (q : Port) :
22 pieceEnd (shiftP child c q) = shiftP child c (pieceEnd q) := by
23 obtain ⟨t, i, s⟩ := q
24 rcases i with _ | _ | i <;> rfl
26/-- The other end of a piece is on the same tile, at an actual vertex. -/
27theorem pieceEnd_valid {q : Port} (i_lt : q.2.1 < 14) : (pieceEnd q).1 = q.1 ∧ (pieceEnd q).2.1 < 14 := by
28 obtain ⟨t, i, s⟩ := q
29 rcases i with _ | _ | i
30 · exact ⟨rfl, (by decide : (1 : Nat) < 14)⟩
31 · exact ⟨rfl, (by decide : (0 : Nat) < 14)⟩
32 · exact ⟨rfl, i_lt⟩
34/-- The edge before vertex `i + 1` (counted round the 14 vertices) is edge `i`. -/
35theorem mod14 {i : Nat} (i_lt : i < 14) : ((i + 1) % 14 + 13) % 14 = i := by omega
37namespace Patch
39variable {P : Patch}
41/-- In a patch with the signature, the port across a glued edge is a port of an actual tile. -/
42theorem across_valid {o : Bool} {A B : Nat} (has_sig : P.HasSig o A B) {p q : Port}
43 (t_lt : p.1 < P.tiles) (i_lt : p.2.1 < 14) (across_eq : P.across p = some q) : q.1 < P.tiles ∧ q.2.1 < 14 := by
44 obtain ⟨t, i, s⟩ := p
45 simp only at t_lt i_lt
46 cases s with
47 | true =>
48 -- port `R(v_i)`, on edge `e_i`
49 simp only [across, straightThrough] at across_eq
50 cases glue_eq : P.glue t i with
51 | none => rw [glue_eq] at across_eq; contradiction
52 | some edge =>
53 obtain ⟨t', j⟩ := edge
54 rw [glue_eq] at across_eq
55 simp only [Option.map_some, Option.some.injEq] at across_eq
56 subst across_eq
57 exact has_sig.glue_ok t i t' j t_lt i_lt glue_eq
58 | false =>
59 -- port `L(v_i)`, on edge `e_{i-1}`
60 simp only [across, straightThrough] at across_eq
61 cases glue_eq : P.glue t ((i + 13) % 14) with
62 | none => rw [glue_eq] at across_eq; contradiction
63 | some edge =>
64 obtain ⟨t', j⟩ := edge
65 rw [glue_eq] at across_eq
66 simp only [Option.map_some, Option.some.injEq] at across_eq
67 subst across_eq
68 exact ⟨(has_sig.glue_ok t _ t' j t_lt (by omega) glue_eq).1, Nat.mod_lt _ (by omega)⟩
70/-- Following a ribbon ends at a rim port, and stays among the patch's ports. -/
71theorem Follow.end_ {o : Bool} {A B : Nat} (has_sig : P.HasSig o A B) {q r : Port} (follow : P.Follow q r) :
72 q.1 < P.tiles → q.2.1 < 14 → P.across r = none ∧ r.1 < P.tiles ∧ r.2.1 < 14 := by
73 induction follow with
74 | @leave q leaves =>
75 intro t_lt i_lt
76 -- the other end of the piece is a port of the same tile
77 have end_valid := pieceEnd_valid i_lt
78 exact ⟨leaves, end_valid.1 ▸ t_lt, end_valid.2⟩
79 | @next q q' r crosses _ ih =>
80 intro t_lt i_lt
81 -- the other end of the piece is a port of the same tile
82 have end_valid := pieceEnd_valid i_lt
83 -- and the port across from it is a port of an actual tile
84 have next_valid := across_valid has_sig (end_valid.1 ▸ t_lt) end_valid.2 crosses
85 exact ih next_valid.1 next_valid.2
87/-- A port with nothing across it is a rim port: one of the two at a rim vertex. -/
88theorem rim_port {o : Bool} {A B : Nat} (has_sig : P.HasSig o A B) {r : Port} (t_lt : r.1 < P.tiles)
89 (i_lt : r.2.1 < 14) (unglued : P.across r = none) : ∃ u s, u < P.E ∧ r = P.bport o (u, s) := by
90 obtain ⟨t, i, s⟩ := r
91 simp only at t_lt i_lt
92 -- the rim is not empty, since this port's edge is on it
93 have rim_pos : 0 < P.E := by
94 cases s with
95 | true =>
96 simp only [across, straightThrough, Option.map_eq_none_iff] at unglued
97 obtain ⟨k, k_lt, _⟩ := has_sig.rim_all t i t_lt i_lt unglued
98 omega
99 | false =>
100 simp only [across, straightThrough, Option.map_eq_none_iff] at unglued
101 obtain ⟨k, k_lt, _⟩ := has_sig.rim_all t _ t_lt (Nat.mod_lt _ (by omega)) unglued
102 omega
103 cases s with
104 | true =>
105 -- `R(v_i)` lies on rim edge `k`, near its start in the tile's own sense
106 simp only [across, straightThrough, Option.map_eq_none_iff] at unglued
107 obtain ⟨k, k_lt, at_k⟩ := has_sig.rim_all t i t_lt i_lt unglued
108 cases o with
109 | true => exact ⟨k, true, k_lt, by simp [bport, at_k]⟩
110 | false => exact ⟨nxt P.E k, false, nxt_lt k_lt, by simp [bport, prv_nxt k_lt, at_k]⟩
111 | false =>
112 -- `L(v_i)` lies on rim edge `k`, near its end in the tile's own sense
113 simp only [across, straightThrough, Option.map_eq_none_iff] at unglued
114 obtain ⟨k, k_lt, at_k⟩ := has_sig.rim_all t _ t_lt (Nat.mod_lt _ (by omega)) unglued
115 -- the vertex after edge `e_{i-1}` is `v_i`
116 have mod_eq : ((i + 13) % 14 + 1) % 14 = i := by omega
117 cases o with
118 | true => exact ⟨nxt P.E k, false, nxt_lt k_lt, by simp [bport, prv_nxt k_lt, at_k, mod_eq]⟩
119 | false => exact ⟨k, true, k_lt, by simp [bport, at_k, mod_eq]⟩
121end Patch
123/-- What the children must satisfy: positive side lengths, glued sides of equal length, vertices where the lengths
124put them, the signature with the composition's corners, and the composition itself with the signature. -/
125structure Kids (T : Kind) (child : Nat → Patch) (L : Nat → Nat → Nat) (d : Nat) (ω o : Bool) : Prop where
126 len_pos : ∀ c j, 1 ≤ L c j
127 pair : ∀ c, c < nk T → ∀ j, j < 6 → ∀ c' j', adjAt T c j = some (c', j') → L c' j' = L c j
128 shape : ∀ c, c < nk T → (child c).vtx = (List.range 7).map (pos (L c)) ∧ (child c).E = pos (L c) 6
129 sig : ∀ c, c < nk T →
130 (child c).HasSig o ((Comp.ofLens T L d ω).toGluing.A c) ((Comp.ofLens T L d ω).toGluing.B c)
131 csig : CompSig T L d ω
133/-- The parent's port for the gluing's port `(c, u, s)`: the port of child `c` at its rim vertex `u`. -/
134def ιP (child : Nat → Patch) (o : Bool) : GPort → Port
135 | (c, u, s) => shiftP child c ((child c).bport o (u, s))
137namespace Kids
139set_option linter.unusedSectionVars false
141variable {T : Kind} {child : Nat → Patch} {L : Nat → Nat → Nat} {d : Nat} {ω o : Bool}
142 (kids : Kids T child L d ω o)
144include kids
146/-- Every child has a tile. -/
147theorem tiles_pos : ∀ c, c < nk T → 0 < (child c).tiles := fun c c_lt => (kids.sig c c_lt).tiles_pos
149/-- The composition's rim length for child `c` is that of child `c`'s rim. -/
150theorem E_eq {c : Nat} (c_lt : c < nk T) : (Comp.ofLens T L d ω).toGluing.E c = (child c).E := by
151 rw [ofLens_E c_lt, (kids.shape c c_lt).2]
153/-- What the parent glues across an edge of tile `t` of child `c` is what `glueAt` says. -/
154theorem glue_shift {c t : Nat} (c_lt : c < nk T) (t_lt : t < (child c).tiles) (i : Nat) :
155 (compose T child).glue (t + offC child c) i = glueAt T child c t i := by
156 rw [Nat.add_comm]; exact compose_glue kids.tiles_pos c_lt t_lt i
158/-- Across an edge inside a child, the parent glues as the child does. -/
159theorem across_in {c t i : Nat} {s : Bool} {q' : Port} (c_lt : c < nk T) (t_lt : t < (child c).tiles)
160 (across_eq : (child c).across (t, i, s) = some q') :
161 (compose T child).across (shiftP child c (t, i, s)) = some (shiftP child c q') := by
162 cases s with
163 | true =>
164 -- port `R(v_i)`, on edge `e_i`
165 simp only [Patch.across, straightThrough] at across_eq
166 cases glue_eq : (child c).glue t i with
167 | none => rw [glue_eq] at across_eq; contradiction
168 | some edge =>
169 obtain ⟨t', j⟩ := edge
170 rw [glue_eq] at across_eq
171 simp only [Option.map_some, Option.some.injEq] at across_eq
172 subst across_eq
174 rw [kids.glue_shift c_lt t_lt]
175 simp only [glueAt, glue_eq, Option.map_some]
176 | false =>
177 -- port `L(v_i)`, on edge `e_{i-1}`
178 simp only [Patch.across, straightThrough] at across_eq
179 cases glue_eq : (child c).glue t ((i + 13) % 14) with
180 | none => rw [glue_eq] at across_eq; contradiction
181 | some edge =>
182 obtain ⟨t', j⟩ := edge
183 rw [glue_eq] at across_eq
184 simp only [Option.map_some, Option.some.injEq] at across_eq
185 subst across_eq
187 rw [kids.glue_shift c_lt t_lt]
188 simp only [glueAt, glue_eq, Option.map_some]
190/-- Across child `c`'s rim edge `k`, the parent glues what the composition's `mate` says. -/
191theorem glue_rimEdge {c k : Nat} (c_lt : c < nk T) (k_lt : k < (child c).E) :
192 (compose T child).glue (((child c).edgeAt k).1 + offC child c) ((child c).edgeAt k).2 =
193 ((Comp.ofLens T L d ω).toGluing.mate c k).map fun (c', k') =>
194 (((child c').edgeAt k').1 + offC child c', ((child c').edgeAt k').2) := by
195 -- child `c` has the signature
196 have has_sig := kids.sig c c_lt
197 obtain ⟨t_lt, _, unglued⟩ := has_sig.rim_ok k k_lt
198 rw [kids.glue_shift c_lt t_lt]
199 exact glue_rim (fun c _ j _ => kids.len_pos c j) kids.pair kids.shape c_lt
200 (by rw [← (kids.shape c c_lt).2]; exact k_lt) unglued
201 (fun k' k'_lt same_edge => has_sig.rim_inj k' k k'_lt k_lt same_edge)
203/-- **Across a child's rim port, the parent continues as `σ` says.** -/
204theorem across_rim {c u : Nat} {s : Bool} (c_lt : c < nk T) (u_lt : u < (child c).E) :
205 (compose T child).across (ιP child o (c, u, s)) =
206 ((Comp.ofLens T L d ω).toGluing.sigma (c, u, s)).map (ιP child o) := by
207 -- child `c` has the signature
208 have has_sig := kids.sig c c_lt
209 -- the composition is well formed
210 have wf := kids.csig.wf
211 -- `c` is a child of the composition
212 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact c_lt
213 cases s with
214 | true =>
215 -- port `R(u)`, on rim edge `u`
216 -- the edge is an actual edge of its tile
217 have i_lt := (has_sig.rim_ok u u_lt).2.1
218 simp only [Gluing.sigma]
219 cases mate_eq : (Comp.ofLens T L d ω).toGluing.mate c u with
220 | none =>
221 -- the parent's gluing across rim edge `u`
222 have glue_eq := kids.glue_rimEdge c_lt u_lt
223 rw [mate_eq] at glue_eq
224 cases o <;> simp only [ιP, shiftP, Patch.bport, Patch.across, straightThrough, ite_true, ite_false,
225 Bool.false_eq_true, mod14 i_lt, glue_eq] <;> rfl
226 | some p =>
227 obtain ⟨c', k'⟩ := p
228 -- the parent's gluing across rim edge `u`
229 have glue_eq := kids.glue_rimEdge c_lt u_lt
230 rw [mate_eq] at glue_eq
231 obtain ⟨c'_lt, k'_lt, _⟩ := wf.mate_valid c u c' k' c_lt_n (by rw [kids.E_eq c_lt]; exact u_lt) mate_eq
232 -- the edge across is an actual edge of its tile in child `c'`
233 have i_lt' := ((kids.sig c' (by rwa [ofLens_n] at c'_lt)).rim_ok k'
234 (by rw [← kids.E_eq (by rwa [ofLens_n] at c'_lt)]; exact k'_lt)).2.1
235 cases o <;> simp only [ιP, shiftP, Patch.bport, Patch.across, straightThrough, ite_true, ite_false,
236 Bool.false_eq_true, mod14 i_lt, glue_eq, Option.map_some]
237 | false =>
238 -- port `L(u)`, on rim edge `u - 1`
239 -- the edge before `u` is a rim edge
240 have prv_lt_E := prv_lt u_lt
241 -- and an actual edge of its tile
242 have i_lt := (has_sig.rim_ok _ prv_lt_E).2.1
243 simp only [Gluing.sigma]
244 rw [kids.E_eq c_lt]
245 cases mate_eq : (Comp.ofLens T L d ω).toGluing.mate c (prv (child c).E u) with
246 | none =>
247 -- the parent's gluing across rim edge `u - 1`
248 have glue_eq := kids.glue_rimEdge c_lt prv_lt_E
249 rw [mate_eq] at glue_eq
250 cases o <;> simp only [ιP, shiftP, Patch.bport, Patch.across, straightThrough, ite_true, ite_false,
251 Bool.false_eq_true, mod14 i_lt, glue_eq] <;> rfl
252 | some p =>
253 obtain ⟨c', k'⟩ := p
254 -- the parent's gluing across rim edge `u - 1`
255 have glue_eq := kids.glue_rimEdge c_lt prv_lt_E
256 rw [mate_eq] at glue_eq
257 obtain ⟨c'_lt_n, k'_lt, _⟩ := wf.mate_valid c _ c' k' c_lt_n (by rw [kids.E_eq c_lt]; exact prv_lt_E) mate_eq
258 -- `c'` is a child
259 have c'_lt : c' < nk T := by rwa [ofLens_n] at c'_lt_n
260 simp only [Option.map_some]
261 rw [kids.E_eq c'_lt] at k'_lt ⊢
262 -- the edge across is an actual edge of its tile in child `c'`
263 have i_lt' := ((kids.sig c' c'_lt).rim_ok k' k'_lt).2.1
264 cases o <;> simp only [ιP, shiftP, Patch.bport, Patch.across, straightThrough, ite_true, ite_false,
265 Bool.false_eq_true, mod14 i_lt, glue_eq, Option.map_some, prv_nxt k'_lt]
267/-- `across_in`, for a port not yet split into its tile, vertex and hand. -/
268theorem across_in' {c : Nat} {p q' : Port} (c_lt : c < nk T) (t_lt : p.1 < (child c).tiles)
269 (across_eq : (child c).across p = some q') :
270 (compose T child).across (shiftP child c p) = some (shiftP child c q') := by
271 obtain ⟨t, i, s⟩ := p
272 exact kids.across_in c_lt t_lt across_eq
274/-- A strand of child `c` is a stretch of a strand of the parent. -/
275theorem lift {c : Nat} (c_lt : c < nk T) : ∀ q r, (child c).Follow q r → q.1 < (child c).tiles → q.2.1 < 14 →
276 ∀ r', ((compose T child).across (shiftP child c r) = none ∧ r' = shiftP child c r) ∨
277 (∃ q₁, (compose T child).across (shiftP child c r) = some q₁ ∧ (compose T child).Follow q₁ r') →
278 (compose T child).Follow (shiftP child c q) r' := by
279 intro q r follow
280 induction follow with
281 | @leave q leaves =>
282 intro _ _ r' after
283 rcases after with ⟨on_rim, rfl⟩ | ⟨q₁, crosses, follow_on⟩
284 · -- the child's strand ends on the parent's rim too
285 -- so the parent's strand leaves there
286 have leave :=
287 Patch.Follow.leave (P := compose T child) (p := shiftP child c q) (by rw [pieceEnd_shift]; exact on_rim)
288 rwa [pieceEnd_shift] at leave
289 · -- the child's strand ends on the child's rim, and the parent's strand crosses into a sibling
290 exact .next (by rw [pieceEnd_shift]; exact crosses) follow_on
291 | @next q q' r crosses _ ih =>
292 intro t_lt i_lt r' after
293 -- the other end of the piece is a port of the same tile
294 have end_valid := pieceEnd_valid i_lt
295 -- and the port across from it is a port of an actual tile of the child
296 have next_valid := Patch.across_valid (kids.sig c c_lt) (end_valid.1 ▸ t_lt) end_valid.2 crosses
297 refine .next ?_ (ih next_valid.1 next_valid.2 r' after)
299 exact kids.across_in' c_lt (end_valid.1 ▸ t_lt) crosses
301/-- A rim port of child `c` is a port of an actual tile. -/
302theorem bport_valid {c u : Nat} {s : Bool} (c_lt : c < nk T) (u_lt : u < (child c).E) :
303 ((child c).bport o (u, s)).1 < (child c).tiles ∧ ((child c).bport o (u, s)).2.1 < 14 := by
304 -- child `c` has the signature
305 have has_sig := kids.sig c c_lt
306 cases s with
307 | true =>
308 obtain ⟨t_lt, i_lt, _⟩ := has_sig.rim_ok u u_lt
309 cases o <;> exact ⟨t_lt, by simp only [Patch.bport]; first | exact i_lt | exact Nat.mod_lt _ (by omega)⟩
310 | false =>
311 obtain ⟨t_lt, i_lt, _⟩ := has_sig.rim_ok _ (prv_lt u_lt)
312 cases o <;> exact ⟨t_lt, by simp only [Patch.bport]; first | exact i_lt | exact Nat.mod_lt _ (by omega)⟩
314/-- The composition's `τ` on child `c` is the child's signature pairing `btau`, with the composition's corners. -/
315theorem tau_btau (c u : Nat) (s : Bool) :
316 (Comp.ofLens T L d ω).toGluing.tau (c, u, s) =
317 (c, (btau ((Comp.ofLens T L d ω).toGluing.A c) ((Comp.ofLens T L d ω).toGluing.B c) (u, s)).1,
318 (btau ((Comp.ofLens T L d ω).toGluing.A c) ((Comp.ofLens T L d ω).toGluing.B c) (u, s)).2) := by
319 simp only [Gluing.tau, btau]
320 by_cases at_A : u = (Comp.ofLens T L d ω).toGluing.A c
321 · simp [at_A]
322 · by_cases at_B : u = (Comp.ofLens T L d ω).toGluing.B c
323 · subst at_B
324 by_cases B_eq_A : (Comp.ofLens T L d ω).toGluing.B c = (Comp.ofLens T L d ω).toGluing.A c <;> simp [B_eq_A]
325 · simp [at_A, at_B]
327/-- The signature pairing keeps rim vertices on the rim. -/
328theorem btau_lt {c u : Nat} {s : Bool} (c_lt : c < nk T) (u_lt : u < (child c).E) :
329 (btau ((Comp.ofLens T L d ω).toGluing.A c) ((Comp.ofLens T L d ω).toGluing.B c) (u, s)).1 < (child c).E := by
330 -- the composition is well formed
331 have wf := kids.csig.wf
332 -- `c` is a child of the composition
333 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact c_lt
334 -- corner `A` is on the child's rim
335 have A_lt := wf.A_lt c c_lt_n
336 -- and so is corner `B`
337 have B_lt := wf.B_lt c c_lt_n
338 rw [kids.E_eq c_lt] at A_lt B_lt
339 simp only [btau]
340 split
341 · exact B_lt
342 · split
343 · exact A_lt
344 · exact u_lt
In the paper Lemma 4.2 Gluing
346/-- **A walk of the composition is a strand of the parent** (Lemma 4.2). -/
347theorem follow_of_reach : ∀ k x r, (Comp.ofLens T L d ω).toGluing.FReach k x r →
348 (Comp.ofLens T L d ω).toGluing.Valid x → (compose T child).Follow (ιP child o x) (ιP child o r) := by
349 -- the composition is well formed
350 have wf := kids.csig.wf
351 intro k x r reach
352 induction reach with
353 | @stop x on_rim =>
354 -- through child `c` by its signature, then out of the parent
355 intro valid
356 obtain ⟨c, u, s⟩ := x
357 obtain ⟨c_lt_n, u_lt_E⟩ := valid
358 -- `c` is a child
359 have c_lt : c < nk T := by rwa [ofLens_n] at c_lt_n
360 -- `u` is a vertex of child `c`'s rim
361 have u_lt : u < (child c).E := by rwa [kids.E_eq c_lt] at u_lt_E
362 rw [kids.tau_btau] at on_rim ⊢
363 -- the start is a port of an actual tile
364 have port_valid := kids.bport_valid (s := s) c_lt u_lt
365 refine kids.lift c_lt _ _ ((kids.sig c c_lt).sig u s u_lt) port_valid.1 port_valid.2 _ (Or.inl ⟨?_, rfl⟩)
366 -- across the far port, the parent continues as `σ` says: nowhere
367 have across_eq :=
368 kids.across_rim (s := (btau ((Comp.ofLens T L d ω).toGluing.A c) ((Comp.ofLens T L d ω).toGluing.B c)
369 (u, s)).2) c_lt (kids.btau_lt (s := s) c_lt u_lt)
370 simp only [ιP] at across_eq
371 rw [across_eq, on_rim]; rfl
372 | @step k x y r first_step _ ih =>
373 -- through child `c` by its signature, then across into the next child, and on by induction
374 intro valid
375 obtain ⟨c, u, s⟩ := x
376 obtain ⟨c_lt_n, u_lt_E⟩ := valid
377 -- `c` is a child
378 have c_lt : c < nk T := by rwa [ofLens_n] at c_lt_n
379 -- `u` is a vertex of child `c`'s rim
380 have u_lt : u < (child c).E := by rwa [kids.E_eq c_lt] at u_lt_E
381 -- the next port is a port of an actual child
382 have y_valid := sigma_valid wf (tau_valid wf ⟨c_lt_n, u_lt_E⟩) first_step
383 rw [kids.tau_btau] at first_step
384 -- the start is a port of an actual tile
385 have port_valid := kids.bport_valid (s := s) c_lt u_lt
386 refine kids.lift c_lt _ _ ((kids.sig c c_lt).sig u s u_lt) port_valid.1 port_valid.2 _
387 (Or.inr ⟨ιP child o y, ?_, ih y_valid⟩)
388 -- across the far port, the parent continues as `σ` says: to `y`
389 have across_eq :=
390 kids.across_rim (s := (btau ((Comp.ofLens T L d ω).toGluing.A c) ((Comp.ofLens T L d ω).toGluing.B c)
391 (u, s)).2) c_lt (kids.btau_lt (s := s) c_lt u_lt)
392 simp only [ιP] at across_eq
393 rw [across_eq, first_step]; rfl
395/-- `follow_of_reach`, for the full walk with any number of crossings. -/
396theorem follow_of_fullReach {x r : GPort} (reach : (Comp.ofLens T L d ω).toGluing.FullReach x r)
397 (valid : (Comp.ofLens T L d ω).toGluing.Valid x) : (compose T child).Follow (ιP child o x) (ιP child o r) := by
398 obtain ⟨k, reach_k⟩ := reach
399 exact kids.follow_of_reach k x r reach_k valid
In the paper Lemma 4.2 Gluing
401/-- **No closed strand in the parent.** -/
402theorem noClosed : (compose T child).NoClosedStrand := by
403 -- the composition is well formed
404 have wf := kids.csig.wf
405 intro p is_port
406 obtain ⟨t, i, s⟩ := p
407 obtain ⟨t_lt, i_lt⟩ := is_port
408 simp only at t_lt i_lt
409 -- the child `c` that tile `t` belongs to, and its number `t₀` there
410 obtain ⟨c, c_lt, start_le, lt_end⟩ := owner_exists child (nk T) t t_lt
411 obtain ⟨t₀, rfl⟩ : ∃ t₀, t = t₀ + offC child c := ⟨t - offC child c, by omega⟩
412 -- child `c` has the signature
413 have has_sig := kids.sig c c_lt
414 -- in the child, the ribbon leaves at a rim port `(u, s')`
415 obtain ⟨r, follow⟩ := has_sig.noClosed (t₀, i, s) ⟨by simp only; omega, i_lt⟩
416 obtain ⟨leaves, r_tile, r_vertex⟩ := Patch.Follow.end_ has_sig follow (by simp only; omega) i_lt
417 obtain ⟨u, s', u_lt, rfl⟩ := Patch.rim_port has_sig r_tile r_vertex leaves
418 -- `c` is a child of the composition
419 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact c_lt
420 -- across that rim port, the parent continues as `σ` says
421 have across_eq := kids.across_rim (s := s') c_lt u_lt
422 simp only [ιP] at across_eq
423 cases sigma_eq : (Comp.ofLens T L d ω).toGluing.sigma (c, u, s') with
424 | none =>
425 -- on the parent's rim: the ribbon leaves the parent there
426 exact ⟨_, kids.lift c_lt _ _ follow (by simp only; omega) i_lt _ (Or.inl ⟨by rw [across_eq, sigma_eq]; rfl, rfl⟩)⟩
427 | some y =>
428 -- into a sibling at `y`
429 -- `y` is a port of an actual child
430 have y_valid := sigma_valid wf ⟨c_lt_n, by rw [kids.E_eq c_lt]; exact u_lt⟩ sigma_eq
431 -- the composition's walk from `y` reaches its rim
432 obtain ⟨r', reach'⟩ := kids.csig.noLoops y y_valid
433 exact ⟨_, kids.lift c_lt _ _ follow (by simp only; omega) i_lt _
434 (Or.inr ⟨ιP child o y, by rw [across_eq, sigma_eq]; rfl, kids.follow_of_fullReach reach' y_valid⟩)⟩
436end Kids
438end SpectreKnot.Statement

← SpectreKnot/Reverse.leanSpectreKnot/ParentSig.lean →