lean/SpectreKnot/Turn.lean
513 lines · 28 declarations, each with its own page · on GitHub ·
Turning about a point, for the Grandparent Lemma (ProofGrand.lean). A corner (t, i) is vertex v_i of tile t; turning about it (Statement.turn) crosses the edge that ends there into the next tile round the point.
← SpectreKnot/NestStep.leanTests.lean →
All 39 files, and the declarations of this one
1/-
2**Turning about a point**, for the Grandparent Lemma (`ProofGrand.lean`). A corner `(t, i)` is vertex `v_i` of tile
3`t`; turning about it (`Statement.turn`) crosses the edge that ends there into the next tile round the point.
5In a patch with the signature, the corners about a rim vertex `k` inside the patch form a chain, from the corner `sC k`
6beside one of its rim ports to the corner `fC k` beside the other (`RimChains`: the patch is a disc at its rim). Every
7other corner is surrounded, or on such a chain (`surrounded_or_chain`, by counting: turning backwards either comes round
8or stops at the start of a chain). In a composition, a chain of the parent is made of chains of children, joined across
9the children's glued sides as the abstract gluing turns about a vertex (`bstep`, as `Rot` or `RotB`); so the parent has
10`RimChains` if its children do (`Kids.rimChains`), and a corner on a child's chain is surrounded in the parent if the
11gluing's turning about that child vertex comes round (`Kids.surrounded_of_cycle`).
12-/
13import SpectreKnot.Linked
15namespace SpectreKnot.Statement
17open Pattern Compose Gluing
19/-! ### Counting -/
21/-- **Pigeonhole**: among `M + 1` numbers below `M`, two are equal. -/
22theorem pigeonhole : ∀ (M : Nat) (f : Nat → Nat), (∀ j, j ≤ M → f j < M) → ∃ a b, a < b ∧ b ≤ M ∧ f a = f b := by
23 intro M
24 induction M with
25 | zero => intro f below; exact absurd (below 0 (Nat.le_refl 0)) (Nat.not_lt_zero _)
26 | succ M ih =>
27 intro f below
28 by_cases hit : ∃ a, a ≤ M ∧ f a = f (M + 1)
29 · obtain ⟨a, a_le, same⟩ := hit
30 exact ⟨a, M + 1, by omega, Nat.le_refl _, same⟩
31 · -- no earlier number equals the last, so squeezing out its value leaves `M + 1` numbers below `M`
32 have missed : ∀ a, a ≤ M → f a ≠ f (M + 1) := fun a a_le same => hit ⟨a, a_le, same⟩
33 obtain ⟨a, b, a_lt, b_le, same⟩ := ih (fun j => if f j < f (M + 1) then f j else f j - 1) (fun j j_le => by
34 have below_j := below j (by omega) -- the number `j`
35 have below_last := below (M + 1) (Nat.le_refl _) -- the last number
36 have missed_j := missed j j_le -- they differ
37 split <;> omega)
38 refine ⟨a, b, a_lt, by omega, ?_⟩
39 have missed_a := missed a (by omega) -- `f a` is not the last value
40 have missed_b := missed b b_le -- nor is `f b`
41 split at same <;> split at same <;> omega
43namespace Patch
47/-! ### Turning, several times -/
49/-- Turning `n` times, then `m` more. -/
50theorem turns_add (n m : Nat) (c : Nat × Nat) : P.turns (n + m) c = (P.turns n c).bind (P.turns m) := by
51 induction n generalizing c with
53 | succ n ih =>
54 rw [Nat.add_right_comm]
56 congr 1
57 funext y
58 exact ih y
60/-- Turning `n + 1` times is turning `n` times, then once more. -/
61theorem turns_succ' (n : Nat) (c : Nat × Nat) : P.turns (n + 1) c = (P.turns n c).bind P.turn := by
63 congr 1
64 funext y
65 show (P.turn y).bind (P.turns 0) = P.turn y
66 cases P.turn y <;> rfl
68/-- Turning keeps to the corners of actual tiles. -/
69theorem turn_valid {o : Bool} {A B : Nat} (sig : P.HasSig o A B) {c d : Nat × Nat} (c_tile : c.1 < P.tiles)
70 (turned : P.turn c = some d) : d.1 < P.tiles ∧ d.2 < 14 :=
71 sig.glue_ok c.1 _ d.1 d.2 c_tile (Nat.mod_lt _ (by omega)) turned
73/-! ### Turning backwards, and where every corner lies -/
75/-- Turning backwards about a point: across edge `e_i` (which leaves `v_i`) of corner `(t, i)`. -/
76def turnB (P : Patch) (c : Nat × Nat) : Option (Nat × Nat) := (P.glue c.1 c.2).map fun e => (e.1, (e.2 + 1) % 14)
78/-- Turning backwards `n` times. -/
80 | 0, c => some c
81 | n + 1, c => (P.turnB c).bind (P.turnsB n)
83/-- Turning backwards, then forwards, comes back (with symmetric gluing). -/
84theorem turn_turnB {o : Bool} {A B : Nat} (sig : P.HasSig o A B) (symm : P.GlueSymm) {c d : Nat × Nat}
85 (c_tile : c.1 < P.tiles) (c_vertex : c.2 < 14) (back : P.turnB c = some d) :
86 P.turn d = some c ∧ d.1 < P.tiles ∧ d.2 < 14 := by
88 cases glue_eq : P.glue c.1 c.2 with
89 | none => rw [glue_eq] at back; contradiction
90 | some e =>
91 rw [glue_eq] at back
92 simp only [Option.map_some, Option.some.injEq] at back
93 subst back
94 -- the edge across is an actual edge
95 obtain ⟨e_tile, e_edge⟩ := sig.glue_ok c.1 c.2 e.1 e.2 c_tile c_vertex glue_eq
96 refine ⟨?_, e_tile, Nat.mod_lt _ (by omega)⟩
98 exact symm c.1 c.2 e.1 e.2 c_tile c_vertex glue_eq
100/-- Turning backwards `n` times to `d`, then forwards `n` times, comes back. -/
101theorem turnsB_sound {o : Bool} {A B : Nat} (sig : P.HasSig o A B) (symm : P.GlueSymm) :
102 ∀ n {c d : Nat × Nat}, c.1 < P.tiles → c.2 < 14 → P.turnsB n c = some d →
103 P.turns n d = some c ∧ d.1 < P.tiles ∧ d.2 < 14 := by
104 intro n
105 induction n with
106 | zero => intro c d c_tile c_vertex back; cases back; exact ⟨rfl, c_tile, c_vertex⟩
107 | succ n ih =>
108 intro c d c_tile c_vertex back
110 cases back_eq : P.turnB c with
111 | none => rw [back_eq] at back; contradiction
112 | some c₁ =>
113 rw [back_eq] at back
114 -- one step back, and forwards again
115 have one := turn_turnB sig symm c_tile c_vertex back_eq
116 -- the other `n` steps
117 have rest := ih one.2.1 one.2.2 back
118 refine ⟨?_, rest.2⟩
119 rw [turns_succ', rest.1]
120 exact one.1
122/-- If turning backwards stops within `n` steps, it stops at some corner with nothing behind it. -/
123theorem turnsB_stop : ∀ n {c : Nat × Nat}, P.turnsB n c = none → ∃ m d, P.turnsB m c = some d ∧ P.turnB d = none := by
124 intro n
125 induction n with
126 | zero => intro c stopped; simp [turnsB] at stopped
127 | succ n ih =>
128 intro c stopped
129 simp only [turnsB] at stopped
130 cases back_eq : P.turnB c with
131 | none => exact ⟨0, c, rfl, back_eq⟩
132 | some c₁ =>
133 rw [back_eq] at stopped
134 obtain ⟨m, d, reached, stops⟩ := ih stopped
135 exact ⟨m + 1, d, by simp only [turnsB, back_eq]; exact reached, stops⟩
137-- The corners `corner`, `sC`, `fC` and the claim that a patch is a disc at its rim, `RimChains`, are in
138-- `Statement.lean`, where the claim `SignatureTheorem` uses them.
140/-- The start of a chain is a corner of an actual tile. -/
142 (P.sC o k).1 < P.tiles ∧ (P.sC o k).2 < 14 := by
143 cases o
145 · exact (sig.rim_ok k k_lt).imp id fun rest => rest.1
147/-- **Every corner is surrounded, or on the chain of a rim vertex** (in a patch with the signature and symmetric
148gluing): turning backwards from it either comes round to it again, or stops at the start of the chain of a rim
149vertex. -/
150theorem surrounded_or_chain {o : Bool} {A B : Nat} (sig : P.HasSig o A B) (symm : P.GlueSymm) {t i : Nat}
151 (t_lt : t < P.tiles) (i_lt : i < 14) :
152 P.Surrounded t i ∨ ∃ k, k < P.E ∧ ∃ n, P.turns n (P.sC o k) = some (t, i) := by
153 by_cases stops : ∃ n, P.turnsB n (t, i) = none
154 · -- turning backwards stops at a corner whose edge `e_i` is on the rim: the start of a chain
155 right
156 obtain ⟨n, stopped⟩ := stops
157 obtain ⟨m, d, reached, nothing_behind⟩ := turnsB_stop n stopped
158 -- turning forwards from there comes back
159 obtain ⟨forwards, d_tile, d_vertex⟩ := turnsB_sound sig symm m t_lt i_lt reached
160 -- the edge behind `d` is unglued
161 have unglued : P.glue d.1 d.2 = none := by
163 -- so it is a rim edge
164 obtain ⟨k, k_lt, at_k⟩ := sig.rim_all d.1 d.2 d_tile d_vertex unglued
165 cases o
166 · -- clockwise: rim edge `k` arrives at rim vertex `k + 1`, beside its rim port `L`
170 exact forwards
171 · -- counter-clockwise: rim edge `k` leaves rim vertex `k`, beside its rim port `R`
172 refine ⟨k, k_lt, m, ?_⟩
173 show P.turns m (P.edgeAt k) = some (t, i)
174 rw [at_k]
175 exact forwards
176 · -- turning backwards never stops: two of the first corners agree, so the turning comes round
177 left
178 -- the corner reached after `n` steps back
179 have reached : ∀ n, ∃ d, P.turnsB n (t, i) = some d := fun n => by
180 cases back_n : P.turnsB n (t, i) with
181 | none => exact absurd ⟨n, back_n⟩ stops
182 | some d => exact ⟨d, rfl⟩
183 -- name them
184 let y : Nat → Nat × Nat := fun n => (P.turnsB n (t, i)).getD (0, 0)
185 -- each is reached
186 have y_eq : ∀ n, P.turnsB n (t, i) = some (y n) := fun n => by
187 obtain ⟨d, found⟩ := reached n
188 simp only [y, found, Option.getD_some]
189 -- and turning forwards from it comes back
190 have y_back : ∀ n, P.turns n (y n) = some (t, i) ∧ (y n).1 < P.tiles ∧ (y n).2 < 14 :=
191 fun n => turnsB_sound sig symm n t_lt i_lt (y_eq n)
192 obtain ⟨a, b, a_lt, _, same⟩ := pigeonhole (14 * P.tiles) (fun n => (y n).1 * 14 + (y n).2) (fun j _ => by
193 have bounds := (y_back j).2 -- `y j` is a corner of an actual tile
194 omega)
195 -- the two corners are the same
196 have same_corner : y a = y b := by
197 have bounds_a := (y_back a).2 -- `y a` is a corner of an actual tile
198 have bounds_b := (y_back b).2 -- and so is `y b`
199 exact Prod.ext (by omega) (by omega)
200 refine ⟨b - a, by omega, ?_⟩
201 -- from `y b`, `b` turns reach `(t, i)`; the first `a` of them reach `(t, i)` too, since `y b = y a`
203 rw [show a + (b - a) = b by omega, same_corner, (y_back b).1, ← same_corner, (y_back a).1] at split
204 exact split.symm
206end Patch
208/-! ### Turning about a vertex of a child, in the abstract gluing -/
210/-- **One step of turning about a point, at the level of the children's rim vertices**, in the sense in which turning
211about a tile vertex goes. For children oriented clockwise (`o = false`), across the edge that leaves the vertex, as
212`Rot`; for children oriented counter-clockwise, across the edge that arrives, as `RotB`. -/
214 if o then G.mate x.1 (prv (G.E x.1) x.2) else (G.mate x.1 x.2).map fun e => (e.1, nxt (G.E e.1) e.2)
216/-- `n` such steps. -/
218 | 0, x => some x
221/-- Turning about a vertex (`Rot`) is a number of steps, for children oriented clockwise. -/
222theorem rot_bsteps {G : Gluing} {x r : Nat × Nat} (turn : G.Rot x r) : ∃ n, bsteps G false n x = some r := by
223 induction turn with
224 | stop _ => exact ⟨0, rfl⟩
225 | @step c u c' k' r glued _ ih =>
226 obtain ⟨n, rest⟩ := ih
227 refine ⟨n + 1, ?_⟩
228 simp only [bsteps, bstep, Bool.false_eq_true, ite_false, glued, Option.map_some, Option.bind_some]
229 exact rest
231/-- Turning backwards about a vertex (`RotB`) is a number of steps, for children oriented counter-clockwise. -/
232theorem rotB_bsteps {G : Gluing} {x r : Nat × Nat} (turn : G.RotB x r) : ∃ n, bsteps G true n x = some r := by
233 induction turn with
234 | stop _ => exact ⟨0, rfl⟩
235 | @step c u c' k' r glued _ ih =>
236 obtain ⟨n, rest⟩ := ih
237 refine ⟨n + 1, ?_⟩
239 exact rest
241/-! ### Chains in a composition -/
243/-- Corner `x` of child `c`, renumbered as a corner of the parent. -/
244def shiftC (child : Nat → Patch) (c : Nat) (x : Nat × Nat) : Nat × Nat := (x.1 + offC child c, x.2)
246/-- The child vertex where the parent's chain about its rim position `p` starts: that of the parent's port `R(p)` for
247clockwise children, of `L(p)` for counter-clockwise ones. -/
251namespace Kids
253set_option linter.unusedSectionVars false
258include kids
260/-- Turning inside a child is turning in the parent. -/
262 (turned : (child c).turn x = some y) : (compose T child).turn (shiftC child c x) = some (shiftC child c y) := by
263 simp only [Patch.turn, shiftC] at turned ⊢
264 rw [kids.glue_shift c_lt x_tile]
267/-- Turning several times inside a child is turning in the parent. -/
268theorem turns_lift {c : Nat} (c_lt : c < nk T) :
269 ∀ n {x y : Nat × Nat}, x.1 < (child c).tiles → (child c).turns n x = some y →
271 intro n
272 induction n with
273 | zero => intro x y _ turned; cases turned; rfl
274 | succ n ih =>
275 intro x y x_tile turned
276 simp only [Patch.turns] at turned ⊢
277 cases turn_eq : (child c).turn x with
278 | none => rw [turn_eq] at turned; contradiction
279 | some x₁ =>
280 rw [turn_eq] at turned
281 rw [kids.turn_lift c_lt x_tile turn_eq]
282 exact ih (Patch.turn_valid (kids.sig c c_lt) x_tile turn_eq).1 turned
284/-- A step of the gluing keeps to the rim vertices of actual children. -/
285theorem bstep_valid {c u : Nat} (c_lt : c < nk T) (u_lt : u < (child c).E) {y : Nat × Nat}
286 (stepped : bstep (Comp.ofLens T L d ω).toGluing o (c, u) = some y) : y.1 < nk T ∧ y.2 < (child y.1).E := by
287 -- the composition is well formed
288 have wf := kids.csig.wf
289 -- `c` is a child of the composition
290 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact c_lt
291 -- and `u` a rim vertex of it
292 have u_lt_E : u < (Comp.ofLens T L d ω).toGluing.E c := by rw [kids.E_eq c_lt]; exact u_lt
293 cases o
295 cases mate_eq : (Comp.ofLens T L d ω).toGluing.mate c u with
296 | none => rw [mate_eq] at stepped; contradiction
297 | some e =>
298 rw [mate_eq] at stepped
299 simp only [Option.map_some, Option.some.injEq] at stepped
300 subst stepped
301 obtain ⟨c'_lt, k'_lt, _⟩ := wf.mate_valid c u e.1 e.2 c_lt_n u_lt_E mate_eq
302 -- `e.1` is a child
307 -- `y.1` is a child
309 exact ⟨c'_lt', by rw [← kids.E_eq c'_lt']; exact k'_lt⟩
311/-- Steps of the gluing keep to the rim vertices of actual children. -/
312theorem bsteps_valid : ∀ a {c u : Nat} {y : Nat × Nat}, c < nk T → u < (child c).E →
313 bsteps (Comp.ofLens T L d ω).toGluing o a (c, u) = some y → y.1 < nk T ∧ y.2 < (child y.1).E := by
314 intro a
315 induction a with
316 | zero => intro c u y c_lt u_lt stepped; cases stepped; exact ⟨c_lt, u_lt⟩
317 | succ a ih =>
318 intro c u y c_lt u_lt stepped
320 cases step_eq : bstep (Comp.ofLens T L d ω).toGluing o (c, u) with
321 | none => rw [step_eq] at stepped; contradiction
322 | some z =>
323 rw [step_eq] at stepped
324 -- the next vertex is a rim vertex of an actual child
325 have z_valid := kids.bstep_valid c_lt u_lt step_eq
326 exact ih z_valid.1 z_valid.2 stepped
328/-- **Across the end of a child's chain**: from the corner where the chain about child vertex `u` ends, turning crosses
329a rim edge of the child into the sibling the gluing's step names, at the start of its chain; or it reaches the
330parent's rim. -/
333 (bstep (Comp.ofLens T L d ω).toGluing o (c, u)).map fun y => shiftC child y.1 ((child y.1).sC o y.2) := by
334 -- the composition is well formed
335 have wf := kids.csig.wf
336 -- `c` is a child of the composition
337 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact c_lt
338 cases o
339 · -- clockwise children: the chain ends beside the rim edge `u`
340 -- which is an actual edge
341 have i_lt := ((kids.sig c c_lt).rim_ok u u_lt).2.1
343 (((((child c).edgeAt u).2 + 1) % 14 + 13) % 14) = _
346 cases mate_eq : (Comp.ofLens T L d ω).toGluing.mate c u with
347 | none => rfl
348 | some e =>
349 obtain ⟨c'_lt, k'_lt, _⟩ :=
350 wf.mate_valid c u e.1 e.2 c_lt_n (by rw [kids.E_eq c_lt]; exact u_lt) mate_eq
351 -- `e.1` is a child
353 simp only [Option.map_some, shiftC, Patch.sC, Patch.corner, Patch.bport, Bool.false_eq_true, ite_false,
355 · -- counter-clockwise children: the chain ends beside the rim edge `u - 1`
356 -- which is an actual edge
362 cases (Comp.ofLens T L d ω).toGluing.mate c (prv (child c).E u) with
363 | none => rfl
364 | some e => rfl
366/-- **One step of the gluing, at tile level**: from the start of the chain about child vertex `u`, turning runs along
367the chain and then, once more, on to what the gluing's step names. -/
368theorem chain_step (chains : ∀ c, c < nk T → (child c).RimChains o) {c u : Nat} (c_lt : c < nk T)
369 (u_lt : u < (child c).E) :
371 (bstep (Comp.ofLens T L d ω).toGluing o (c, u)).map fun y => shiftC child y.1 ((child y.1).sC o y.2) := by
372 obtain ⟨n, along⟩ := chains c c_lt u u_lt
373 refine ⟨n, ?_⟩
374 rw [Patch.turns_succ', kids.turns_lift c_lt n (Patch.sC_valid (kids.sig c c_lt) u_lt).1 along]
375 exact kids.turn_fC c_lt u_lt
377/-- **Steps of the gluing, at tile level**: if `a` steps of the gluing lead from vertex `u` of child `c` to vertex `u'`
378of child `c'`, then turning in the parent leads, in at least `a` turns, from the start of the chain about the first to
379the start of the chain about the second. -/
380theorem chain_path (chains : ∀ c, c < nk T → (child c).RimChains o) :
382 bsteps (Comp.ofLens T L d ω).toGluing o a (c, u) = some (c', u') →
385 intro a
386 induction a with
387 | zero => intro c u c' u' _ _ stepped; cases stepped; exact ⟨0, Nat.le_refl _, rfl⟩
388 | succ a ih =>
389 intro c u c' u' c_lt u_lt stepped
391 cases step_eq : bstep (Comp.ofLens T L d ω).toGluing o (c, u) with
392 | none => rw [step_eq] at stepped; contradiction
393 | some y =>
394 rw [step_eq] at stepped
395 -- the next vertex is a rim vertex of an actual child
396 have y_valid := kids.bstep_valid c_lt u_lt step_eq
397 obtain ⟨n₁, first⟩ := kids.chain_step chains c_lt u_lt
398 rw [step_eq] at first
399 obtain ⟨n₂, a_le, rest⟩ := ih y_valid.1 y_valid.2 stepped
400 refine ⟨n₁ + 1 + n₂, by omega, ?_⟩
401 rw [Patch.turns_add, first]
402 exact rest
404/-- **A corner on a child's chain is surrounded in the parent** if the gluing's turning about that child vertex comes
405round to it. -/
406theorem surrounded_of_cycle (chains : ∀ c, c < nk T → (child c).RimChains o) {c u a : Nat} (c_lt : c < nk T)
407 (u_lt : u < (child c).E) (a_pos : 0 < a)
408 (cycle : bsteps (Comp.ofLens T L d ω).toGluing o a (c, u) = some (c, u)) {m : Nat} {x : Nat × Nat}
409 (on_chain : (child c).turns m ((child c).sC o u) = some x) :
411 obtain ⟨n, a_le, round⟩ := kids.chain_path chains a c_lt u_lt cycle
412 -- the corner, in the parent, on the lifted chain
413 have to_x := kids.turns_lift c_lt m (Patch.sC_valid (kids.sig c c_lt) u_lt).1 on_chain
414 refine ⟨n, by omega, ?_⟩
415 -- `m` turns then `n` from the start of the chain: `n` turns from the corner
416 have m_then_n := Patch.turns_add (P := compose T child) m n (shiftC child c ((child c).sC o u))
417 -- `n` turns then `m`: round to the start, and on to the corner
418 have n_then_m := Patch.turns_add (P := compose T child) n m (shiftC child c ((child c).sC o u))
419 rw [to_x, Option.bind_some] at m_then_n
420 rw [round, Option.bind_some, to_x, Nat.add_comm n m] at n_then_m
421 exact m_then_n.symm.trans n_then_m
423/-- Where the parent's chain about rim position `p` starts: at the start of the chain about the child vertex of
424`R(p)` (for clockwise children) or of `L(p)` (for counter-clockwise ones). -/
428 cases o
429 · show Patch.corner ((compose T child).bport (!false) (p, true)) = _
430 rw [kids.bport_R p_lt]; rfl
431 · show Patch.corner ((compose T child).bport (!true) (p, false)) = _
432 rw [kids.bport_L p_lt]; rfl
434/-- **On the parent's chain**: a corner on the chain about a child vertex that steps of the gluing reach from the
435start of the parent's chain about rim position `p` is on that chain. -/
436theorem on_parent_chain (chains : ∀ c, c < nk T → (child c).RimChains o) {p : Nat} (p_lt : p < rimN T L)
437 {a c u : Nat} (path : bsteps (Comp.ofLens T L d ω).toGluing o a (vS T L d ω o p) = some (c, u)) {n : Nat}
438 {x : Nat × Nat} (on_chain : (child c).turns n ((child c).sC o u) = some x) :
440 -- the vertex of `R(p)` and that of `L(p)`, as rim vertices of actual children
441 obtain ⟨cR_lt, uR_lt⟩ := kids.gR_valid p_lt
442 -- (that of `L(p)`)
443 obtain ⟨cL_lt, uL_lt⟩ := kids.gL_valid p_lt
445 rw [kids.E_eq cR_lt] at uR_lt
446 rw [kids.E_eq cL_lt] at uL_lt
447 -- the start of the parent's chain is a rim vertex of an actual child
448 have start_valid : (vS T L d ω o p).1 < nk T ∧ (vS T L d ω o p).2 < (child (vS T L d ω o p).1).E := by
449 cases o
450 · exact ⟨cR_lt, uR_lt⟩
451 · exact ⟨cL_lt, uL_lt⟩
452 obtain ⟨n₁, _, to_vertex⟩ := kids.chain_path chains a start_valid.1 start_valid.2 path
453 -- the end of that path is a rim vertex of an actual child
454 have end_valid := kids.bsteps_valid a start_valid.1 start_valid.2 path
455 refine ⟨n₁ + n, ?_⟩
456 rw [kids.sC_parent p_lt, Patch.turns_add, to_vertex]
457 exact kids.turns_lift end_valid.1 n (Patch.sC_valid (kids.sig c end_valid.1) end_valid.2).1 on_chain
459/-- **The parent is a disc at its rim** if its children are: the chain about a parent rim vertex is made of the
460children's chains, joined as the gluing turns about the vertex. -/
461theorem rimChains (chains : ∀ c, c < nk T → (child c).RimChains o) : (compose T child).RimChains (!o) := by
462 -- the composition is well formed
463 have wf := kids.csig.wf
464 intro p p_lt
466 -- the vertex of `R(p)` and that of `L(p)`, as rim vertices of actual children
467 obtain ⟨cR_lt, uR_lt⟩ := kids.gR_valid p_lt
468 -- (that of `L(p)`)
469 obtain ⟨cL_lt, uL_lt⟩ := kids.gL_valid p_lt
471 rw [kids.E_eq cR_lt] at uR_lt
472 rw [kids.E_eq cL_lt] at uL_lt
473 -- turning about the vertex of `R(p)` reaches that of `L(p)`
474 have turn := kids.gR_rot p_lt
475 cases o
476 · -- clockwise children: the parent's chain runs from beside `R(p)` to beside `L(p)`
477 obtain ⟨a, path⟩ := rot_bsteps turn
478 obtain ⟨n₁, _, to_L⟩ := kids.chain_path chains a cR_lt uR_lt path
479 obtain ⟨n₂, along⟩ := chains _ cL_lt _ uL_lt
480 refine ⟨n₁ + n₂, ?_⟩
481 -- the parent's chain starts beside `R(p)`, at the start of the chain about its vertex
482 have start_eq : Patch.corner (ιP child false (gR T L d ω p)) =
484 -- and ends beside `L(p)`, at the end of the chain about its vertex
485 have end_eq : Patch.corner (ιP child false (gL T L p)) =
487 show (compose T child).turns (n₁ + n₂) (Patch.corner ((compose T child).bport (!false) (p, true))) =
488 some (Patch.corner ((compose T child).bport (!false) (p, false)))
489 rw [kids.bport_R p_lt, kids.bport_L p_lt, start_eq, end_eq, Patch.turns_add, to_L]
490 exact kids.turns_lift cL_lt n₂ (Patch.sC_valid (kids.sig _ cL_lt) uL_lt).1 along
491 · -- counter-clockwise children: from beside `L(p)` to beside `R(p)`, turning backwards about the vertex
492 -- the edge before the vertex of `R(p)` is on the parent's rim
493 have rim_R := kids.gR_rimL p_lt
494 -- so turning backwards from the vertex of `L(p)` reaches it
495 have back := turn.rotB wf rim_R.1 rim_R.2.1 _ (.stop rim_R.2.2)
496 obtain ⟨a, path⟩ := rotB_bsteps back
497 obtain ⟨n₁, _, to_R⟩ := kids.chain_path chains a cL_lt uL_lt path
498 obtain ⟨n₂, along⟩ := chains _ cR_lt _ uR_lt
499 refine ⟨n₁ + n₂, ?_⟩
500 -- the parent's chain starts beside `L(p)`, at the start of the chain about its vertex
501 have start_eq : Patch.corner (ιP child true (gL T L p)) =
503 -- and ends beside `R(p)`, at the end of the chain about its vertex
504 have end_eq : Patch.corner (ιP child true (gR T L d ω p)) =
506 show (compose T child).turns (n₁ + n₂) (Patch.corner ((compose T child).bport (!true) (p, false))) =
507 some (Patch.corner ((compose T child).bport (!true) (p, true)))
508 rw [kids.bport_R p_lt, kids.bport_L p_lt, start_eq, end_eq, Patch.turns_add, to_R]
509 exact kids.turns_lift cR_lt n₂ (Patch.sC_valid (kids.sig _ cR_lt) uR_lt).1 along
511end Kids
513end SpectreKnot.Statement