lean/SpectreKnot/Compose.lean
184 lines · 21 declarations, each with its own page · on GitHub ·
The abstract composition of paper §7.1, built in Lean from the tables, and its box computed by gluing (Lemma 4.2), port by port, with no reduction.
← SpectreKnot/Lengths.leanSpectreKnot/CompFull.lean →
All 39 files, and the declarations of this one
1/-
2The abstract composition of paper §7.1, built in Lean from the tables, and its box computed by gluing (Lemma 4.2),
3port by port, with no reduction.
5`Comp.ofPattern T λ d ω` is the composition `P = ⋃ X_c` of §7.1: child `c` is a hexagon of kind `K_c` (Table 1)
6whose side `j` has `λ(letter)` edges (Table 4); its crossover corners are `A_c` (vertex 0, or for Σ the point of side 5
7at distance `d` from vertex 5) and `B_c = A_c + ω`; sides are glued in pairs by Table 2, reversing direction; the
8parent's rim is listed by Table 3. Every child is given the signature box (Def 4.3). `Comp.toGluing` makes it a
9`Gluing`, whose full walk computes the parent's box exactly as Lemma 4.2 says.
11`Comp.check` tests the signature of the composition as §7.1 words it, and `check_sound` says what a `true` means: the
12parent has no closed strand and has the signature at the Γ child's corners. (The induction of Prop 7.4 carries another
13form of it, `Gluing.Sig`, which finds each parent rim vertex by turning about a child's vertex; `CompSig.lean` derives
14it from `check`.) Run at `(ℓ₁, d₁, ±1)` for the nine kinds, this is Computation 7.3, from the tables alone and without
15the reduced walk or the exported skeletons.
16-/
17import SpectreKnot.Lengths
18import SpectreKnot.Gluing
20namespace SpectreKnot.Compose
22open Pattern
24/-- `prefixSums [l₀, …, l₅] 0 = [0, l₀, l₀+l₁, …, E]`. -/
25def prefixSums : List Nat → Nat → List Nat
26 | [], a => [a]
27 | x :: xs, a => a :: prefixSums xs (a + x)
29/-- A child of the composition. Rim vertices and rim edges are numbered `0 … E-1` in the child's own order; edge `k`
30runs from vertex `k` to vertex `k+1`. -/
33 len : List Nat
34 U : List Nat
35 E : Nat
36 A : Nat
37 B : Nat
38 deriving Repr
40/-- A child of kind `K` whose sides `0 … 5` have the lengths `len`, with Σ offset `d` and sign `ω` (`true` for
41`+1`): its crossover corner `A` is vertex 0, or for Σ the point of side 5 at distance `d` from vertex 5, and
42`B = A + ω`. -/
44 let U := prefixSums len 0
45 let E := U.getD 6 0
46 let A := if K = .Sigma then U.getD 5 0 + d else 0
48 ⟨K, len, U, E, A, B⟩
50/-- A composition: the parent's kind and its children. -/
55/-- The composition of kind `T` in which side `j` of child `c` has `L c j` edges. (Used for the parity lemma, where
56sides are lengthened one pair at a time.) -/
57def Comp.ofLens (T : Kind) (L : Nat → Nat → Nat) (d : Nat) (ω : Bool) : Comp :=
58 ⟨T, (List.range (Pattern.kids T).length).map fun c => mkKidL (kidAt T c) ((List.range 6).map (L c)) d ω⟩
60/-- The composition of §7.1: every side with letter `x` has `lam x` edges. -/
61def Comp.ofPattern (T : Kind) (lam : Letter → Nat) (d : Nat) (ω : Bool) : Comp :=
62 Comp.ofLens T (fun c j => lam (letterOf (kidAt T c) j)) d ω
64namespace Comp
68/-- Child `c` (a dummy one-vertex child if there is none). -/
71/-- `sideIdx U k i`: the last `j ≤ i` with `U[j] ≤ k`, or 0. -/
73 | 0 => 0
76/-- The side of child `c` containing edge `k`, and the offset of `k` in it. -/
78 let U := (C.kid c).U
80 (j, k - U.getD j 0)
82/-- Table 2 with direction reversed: edge `k` of child `c` is edge `mate c k` of a sibling, or on the parent's rim. -/
84 let (j, o) := C.sideOf c k
86 | none => none
87 | some (c', j') =>
88 let k' := C.kid c'
89 some (c', k'.U.getD j' 0 + k'.len.getD j' 0 - 1 - o)
91/-- The composition as a gluing of children with the signature. -/
93 ⟨C.kids.length, fun c => (C.kid c).E, fun c => (C.kid c).A, fun c => (C.kid c).B, C.mate⟩
95/-- All ports of all children. -/
97 (List.range C.kids.length).flatMap fun c =>
98 (List.range (C.kid c).E).flatMap fun u => [(c, u, true), (c, u, false)]
100/-- Every port of an actual child is in the list `ports`. -/
102 obtain ⟨c, u, s⟩ := x
103 obtain ⟨c_lt, u_lt⟩ := x_valid
105 exact ⟨c, c_lt, u, u_lt, by cases s <;> simp⟩
107/-- Enough fuel for any walk: a walk never repeats a port. -/
110/-- The parent's rim edges `(c, k)` in the children's rotational sense, from Table 3 (which lists the parent's sides in
111the parent's own order, the opposite sense). -/
114 let k := C.kid c
115 (List.range (k.len.getD j 0)).map fun i => (c, k.U.getD j 0 + k.len.getD j 0 - 1 - i)
116 own.reverse
118/-- The parent's rim ports at the vertex between consecutive rim edges `e₁ = (c₁, k₁)` and `e₂ = (c₂, k₂)`:
119`L` on `e₁` and `R` on `e₂`. -/
120def rimVertexPorts : List (GPort × GPort) :=
121 let es := C.rimEdges
122 let n := es.length
123 (List.range n).map fun t =>
124 let (c₁, k₁) := es.getD t (0, 0)
125 let (c₂, k₂) := es.getD ((t + 1) % n) (0, 0)
128/-- Rim vertex number `t` of the parent, as its pair of ports. -/
131/-- The rim indices of the Γ child's crossover corners `A` and `B` (the Γ child is the last). -/
133 let g := C.kids.length - 1
134 (C.rimVertexPorts.findIdx? fun (_, pR) => pR == (g, (C.kid g).A, true)).getD C.rimVertexPorts.length
136/-- The rim index of the Γ child's crossover corner `B` (see `tA`). -/
138 let g := C.kids.length - 1
139 (C.rimVertexPorts.findIdx? fun (_, pR) => pR == (g, (C.kid g).B, true)).getD C.rimVertexPorts.length
141/-- The conclusion of the induction step for this composition (see `check_sound` for what `true` means):
142(1) the gluing is well formed;
143(2) no closed strand: the walk from every port ends on the parent's rim;
144(3) a hook at every parent rim vertex except the Γ child's corners `A` and `B`;
145(4) `A` and `B` are rim vertices of the parent and adjacent, `B` after `A` in the children's sense if `ω = +1` and
146before it if `ω = -1` (so `B = A + ω_{m+1}` in the parent's own order, the opposite sense);
147(5) the crossover `R(A) ↔ R(B)`, `L(A) ↔ L(B)`. -/
149 let G := C.toGluing
150 let n := C.rimVertexPorts.length
151 G.wfCheck &&
152 (C.ports.all fun x => (G.fullWalk C.fuel x).isSome) &&
153 ((List.range n).all fun t => t == C.tA || t == C.tB || G.fullWalk C.fuel (C.vtx t).1 == some (C.vtx t).2) &&
154 decide (C.tA < n) && decide (C.tB < n) &&
155 C.tB == (if ω then (C.tA + 1) % n else (C.tA + n - 1) % n) &&
156 G.fullWalk C.fuel (C.vtx C.tA).2 == some (C.vtx C.tB).2 &&
157 G.fullWalk C.fuel (C.vtx C.tA).1 == some (C.vtx C.tB).1
159/-- What `check` establishes, as theorems about the gluing (`FullReach x r`: the parent's arcs join `x` to `r`). -/
160theorem check_sound {ω : Bool} (checked : C.check ω = true) :
161 let G := C.toGluing
162 let n := C.rimVertexPorts.length
163 G.WF ∧
164 (∀ x, G.Valid x → ∃ r, G.FullReach x r) ∧
165 (∀ t, t < n → t ≠ C.tA → t ≠ C.tB → G.FullReach (C.vtx t).1 (C.vtx t).2) ∧
166 C.tA < n ∧ C.tB < n ∧ C.tB = (if ω then (C.tA + 1) % n else (C.tA + n - 1) % n) ∧
167 G.FullReach (C.vtx C.tA).2 (C.vtx C.tB).2 ∧ G.FullReach (C.vtx C.tA).1 (C.vtx C.tB).1 := by
168 simp only [check, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq, List.all_eq_true, List.mem_range,
169 Bool.or_eq_true] at checked
170 obtain ⟨⟨⟨⟨⟨⟨⟨wf_checked, all_end⟩, hooks⟩, A_lt⟩, B_lt⟩, adjacent⟩, cross_R⟩, cross_L⟩ := checked
171 refine ⟨Gluing.wfCheck_sound _ wf_checked, fun x x_valid => ?_, fun t t_lt ne_A ne_B => ?_, A_lt, B_lt, adjacent,
172 Gluing.fullWalk_sound _ cross_R, Gluing.fullWalk_sound _ cross_L⟩
173 · have ends := all_end x (C.mem_ports x_valid) -- the computed walk from `x` ends within the fuel
174 cases walk_eq : C.toGluing.fullWalk C.fuel x with
175 | none => rw [walk_eq] at ends; contradiction
176 | some r => exact ⟨r, Gluing.fullWalk_sound _ walk_eq⟩
177 · rcases hooks t t_lt with (is_A | is_B) | hook
178 · exact absurd is_A ne_A
179 · exact absurd is_B ne_B
180 · exact Gluing.fullWalk_sound _ hook
182end Comp
184end SpectreKnot.Compose