lean/SpectreKnot/Gluing.lean
162 lines · 21 declarations, each with its own page · on GitHub ·
A patch glued from children (the paper's §4 and §7.1): the setting of Lemma 4.2, for compositions.
← SpectreKnot/Box.leanSpectreKnot/Zigzag.lean →
All 39 files, and the declarations of this one
1/-
2A patch glued from children (the paper's §4 and §7.1): the setting of Lemma 4.2, for compositions.
4Child `c` has `E c` rim vertices `0 … E c - 1`, numbered in its orientation (all children in the same rotational
5sense); edge `k` runs from vertex `k` to vertex `k+1`. Each child carries the signature's pairing at its crossover
6corners `A c`, `B c` (Def 4.3, `tau`). `mate c k = some (c', k')` says that edge `k` of child `c` is edge `k'` of child
7`c'`, traversed the other way; `none` says that it lies on the parent's rim. Nothing here refers to the tables. Results
8about gluings assume at most that they are well formed (`WF`), which asks only that each child's corners be distinct,
9not that they be adjacent, and nothing about the children's interiors.
10-/
11import SpectreKnot.Basic
12import SpectreKnot.Box
14namespace SpectreKnot
16-- `nxt` and `prv`, the cyclic successor and predecessor on `0 … E-1`, are in `Basic.lean`.
18/-- The successor of a vertex is a vertex. -/
21/-- The predecessor of a vertex is a vertex. -/
24/-- The predecessor undoes the successor. -/
28/-- The successor undoes the predecessor. -/
32/-- Rim ports are `(c, u, s)`: `R_c(u)` if `s = true`, `L_c(u)` if `false`. -/
35/-- `R` as `true`, `L` as `false`, as in `GPort`. -/
37 | .R => true
38 | .L => false
40/-- The data of a patch glued from children. -/
42 n : Nat
43 E : Nat → Nat
44 A : Nat → Nat
45 B : Nat → Nat
46 mate : Nat → Nat → Option (Nat × Nat)
48namespace Gluing
52/-- A port of an actual child, at an actual rim vertex. -/
55/-- Well-formed: every child has a rim with its corners on it, and gluing pairs edges of children with each other. -/
57 E_pos : ∀ c, c < G.n → 0 < G.E c
58 A_lt : ∀ c, c < G.n → G.A c < G.E c
59 B_lt : ∀ c, c < G.n → G.B c < G.E c
60 A_ne_B : ∀ c, c < G.n → G.A c ≠ G.B c
61 mate_valid : ∀ c k c' k', c < G.n → k < G.E c → G.mate c k = some (c', k') →
62 c' < G.n ∧ k' < G.E c' ∧ G.mate c' k' = some (c, k)
64/-- `WF` as a computation, for concrete gluings. -/
66 (List.range G.n).all fun c =>
67 decide (0 < G.E c) && decide (G.A c < G.E c) && decide (G.B c < G.E c) && G.A c != G.B c &&
68 (List.range (G.E c)).all fun k =>
69 match G.mate c k with
70 | none => true
71 | some (c', k') => decide (c' < G.n) && decide (k' < G.E c') && G.mate c' k' == some (c, k)
73/-- If `wfCheck` returns `true`, the gluing is well formed. -/
74theorem wfCheck_sound (checked : G.wfCheck = true) : G.WF := by
75 simp only [wfCheck, List.all_eq_true, List.mem_range, Bool.and_eq_true, decide_eq_true_eq, bne_iff_ne,
76 ne_eq] at checked
77 refine ⟨fun c c_lt => (checked c c_lt).1.1.1.1, fun c c_lt => (checked c c_lt).1.1.1.2,
78 fun c c_lt => (checked c c_lt).1.1.2, fun c c_lt => (checked c c_lt).1.2, fun c k c' k' c_lt k_lt glued => ?_⟩
79 -- what the check says about edge `k` of child `c`, which is glued to edge `k'` of `c'`
80 have edge_ok := (checked c c_lt).2 k k_lt
81 rw [glued] at edge_ok
82 simp only [Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq] at edge_ok
83 exact ⟨edge_ok.1.1, edge_ok.1.2, edge_ok.2⟩
85/-! ### The full walk (Lemma 4.2) -/
87/-- `u` is a crossover corner of child `c`. -/
90/-- `τ`: inside a child, by its signature (Def 4.3): a hook at every rim vertex but the corners, where
91`R(A) ↔ R(B)` and `L(A) ↔ L(B)`. -/
93 | (c, u, s) => if u = G.A c then (c, G.B c, s) else if u = G.B c then (c, G.A c, s) else (c, u, !s)
95section
97variable {G}
99/-- A vertex that is not a crossover corner is neither `A` nor `B`. -/
100theorem corner_false {c u : Nat} (not_corner : G.corner c u = false) : u ≠ G.A c ∧ u ≠ G.B c := by
103/-- Away from the crossover corners, `τ` is the hook: it swaps `L` and `R` at the same vertex. -/
104theorem tau_of_not_corner {c u : Nat} {s : Bool} (not_corner : G.corner c u = false) :
105 G.tau (c, u, s) = (c, u, !s) := by
106 obtain ⟨ne_A, ne_B⟩ := corner_false not_corner
109/-- In a well-formed gluing, `τ` sends a port of an actual child to a port of the same child. -/
111 obtain ⟨c, u, s⟩ := x
112 obtain ⟨c_lt, u_lt⟩ := x_valid
114 split
115 · exact ⟨c_lt, wf.B_lt c c_lt⟩
116 · split
117 · exact ⟨c_lt, wf.A_lt c c_lt⟩
118 · exact ⟨c_lt, u_lt⟩
120end
122/-- `σ`: the straight-through rule (Def 3.2). `R_c(u)` lies on edge `u` near `u`; if that edge is edge `k'` of `c'`,
123it is joined to the port of `c'` on it near the other end, `R_{c'}(k')`. `L_c(u)` lies on edge `u-1` near `u`, and is
124joined to `L_{c'}(k'+1)`. `none` on the parent's rim. -/
126 | (c, u, true) => (G.mate c u).map fun (c', k') => (c', k', true)
129/-- Lemma 4.2, as a relation: from port `x`, `FReach k x r` says that alternately applying `τ` and `σ`, with `k`
130crossings, ends at the rim port `r` of the parent. -/
133 | step {k : Nat} {x y r : GPort} : G.sigma (G.tau x) = some y → FReach G k y r → FReach G (k + 1) x r
135/-- The full walk from `x` ends at `r`. For a rim port `x` of the parent, `r` is `π_P(x)` (Lemma 4.2). -/
138/-! ### Computable walks -/
140/-- The full walk as a computation with fuel: `none` if the fuel runs out. -/
142 | 0, _ => none
143 | f + 1, x =>
144 match G.sigma (G.tau x) with
145 | none => some (G.tau x)
148/-- If the computed full walk from `x` ends at `r`, then `FullReach x r`. -/
149theorem fullWalk_sound {f : Nat} {x r : GPort} (walk_eq : G.fullWalk f x = some r) : G.FullReach x r := by
150 induction f generalizing x with
152 | succ f ih =>
154 split at walk_eq
155 · -- on the parent's rim: the walk stops here
156 rename_i on_rim; cases walk_eq; exact ⟨0, .stop on_rim⟩
157 · -- across to `y`, and on from there
158 rename_i y crosses; obtain ⟨k, rest⟩ := ih walk_eq; exact ⟨k + 1, .step crosses rest⟩
160end Gluing
162end SpectreKnot