lean/SpectreKnot/Zigzag.lean
126 lines · 6 declarations, each with its own page · on GitHub ·
The zigzag lemma (paper Lemma 5.1), for every length n.
← SpectreKnot/Gluing.leanSpectreKnot/Lengths.lean →
All 39 files, and the declarations of this one
1/-
2The zigzag lemma (paper Lemma 5.1), for every length `n`.
4Setting: a path `u_0 u_1 … u_n` of `n ≥ 1` edges lies on the rims of two children `X_c` and `X_{c'}`; `X_c` traverses
5it from `u_0` to `u_n`, and `X_{c'}` (oriented in the same rotational sense) from `u_n` to `u_0`. None of
6`u_1, …, u_{n-1}` is a crossover corner of either child, so both children have hooks there.
8The ports involved are named by `Strip`: `c h k` is the port `h(u_k)` of `X_c` and `d h k` the port `h(u_k)` of
9`X_{c'}`, each in its own orientation. They live in some type `P` of ports (`ι : Strip → P`), on which `σ` is the
10straight-through rule (Def 3.2), undefined where nothing is glued, and `τ` is the pairing inside the children (their
11boxes). The lemma follows the alternation `σ, τ, σ, τ, …, σ` along the path (`Chain`). The lengthening (Lemma 7.1)
12uses it with `n = 3`, along an edge cut into three (`Gluing.Cut.OK.cross_cut`).
13-/
14import SpectreKnot.Basic
15import SpectreKnot.Box
17namespace SpectreKnot
19/-- Ports along the shared path: `c h k` = `h_c(u_k)`, `d h k` = `h_{c'}(u_k)`. -/
23 deriving DecidableEq, Repr
25namespace Zigzag
27/-- **A connection**: `Chain σ τ p q` says that from `p`, crossing an edge (`σ`, defined there) and then, until `q` is
28reached, going through a piece (`τ`) and crossing again, leads to `q`. -/
33/-- A chain goes on through one more piece and crossing at its end. -/
34theorem Chain.snoc {P : Type} {σ : P → Option P} {τ : P → P} {p q q' : P} (chain : Chain σ τ p q)
36 induction chain with
37 | one crosses => exact .more crosses (.one next)
38 | more crosses _ ih => exact .more crosses (ih next)
40section Chains
44/-- The connection through `R_c(u_0)`, crossing by crossing: after its `k + 1`-th crossing (`k < n`) it has arrived at
45`R_{c'}(u_{k+1})` (`k` even) or `L_c(u_{k+1})` (`k` odd). The four rules: across edge `k` from `R_c(u_k)` (`across_R`)
46and from `L_{c'}(u_k)` (`across_L`), and the hooks of `X_{c'}` (`hook_d`) and of `X_c` (`hook_c`) at the inner
47vertices. -/
48theorem walk_chain
49 (across_R : ∀ k, k < n → σ (ι (.c .R k)) = some (ι (.d .R (k + 1))))
50 (hook_d : ∀ k, 0 < k → k < n → τ (ι (.d .R k)) = ι (.d .L k))
51 (across_L : ∀ k, k < n → σ (ι (.d .L k)) = some (ι (.c .L (k + 1))))
52 (hook_c : ∀ k, 0 < k → k < n → τ (ι (.c .L k)) = ι (.c .R k)) :
53 ∀ k, k < n → Chain σ τ (ι (.c .R 0)) (if k % 2 = 0 then ι (.d .R (k + 1)) else ι (.c .L (k + 1))) := by
54 intro k k_lt
55 induction k with
56 | zero => exact .one (across_R 0 k_lt)
57 | succ k ih =>
58 -- the first `k + 1` crossings
59 have before := ih (by omega)
60 by_cases k_even : k % 2 = 0
61 · -- arrived at `R_{c'}(u_{k+1})`: the hook of `X_{c'}` there, then across edge `k + 1` from `L_{c'}(u_{k+1})`
62 rw [ite_eq_left k_even] at before
63 rw [ite_eq_right (show ¬ ((k + 1) % 2 = 0) by omega)]
64 exact before.snoc (by rw [hook_d (k + 1) (by omega) k_lt]; exact across_L (k + 1) k_lt)
65 · -- arrived at `L_c(u_{k+1})`: the hook of `X_c` there, then across edge `k + 1` from `R_c(u_{k+1})`
66 rw [ite_eq_right k_even] at before
67 rw [ite_eq_left (show (k + 1) % 2 = 0 by omega)]
68 exact before.snoc (by rw [hook_c (k + 1) (by omega) k_lt]; exact across_R (k + 1) k_lt)
70/-- The relabelling that exchanges the two children and `L` with `R`. It turns the connection through `L_{c'}(u_0)`
71into a connection through `R_c(u_0)`, so `walk_chain` also describes the second connection. -/
73 | .c .R k => .d .L k
74 | .c .L k => .d .R k
75 | .d .R k => .c .L k
76 | .d .L k => .c .R k
78/-- **Lemma 5.1 (the Zigzag Lemma).** Let `σ` be the straight-through rule across the edges `u_k u_{k+1}` of the path,
79and `τ` the hooks of both children at `u_1, …, u_{n-1}`. Alternately applying them joins the ports at the ends of the
80path as follows:
82* `n` even: `R_c(u_0) ↔ L_c(u_n)` and `L_{c'}(u_0) ↔ R_{c'}(u_n)`;
83* `n` odd: `R_c(u_0) ↔ R_{c'}(u_n)` and `L_{c'}(u_0) ↔ L_c(u_n)`.
85These two connections use every port on the edges of the path: after `k + 1` crossings they have arrived at the two
86ports `R_{c'}(u_{k+1})` and `L_c(u_{k+1})` of edge `k`, one each, so each crosses every edge once, and between them they
87leave from its other two ports, `R_c(u_k)` and `L_{c'}(u_k)`. -/
89 (across_R : ∀ k, k < n → σ (ι (.c .R k)) = some (ι (.d .R (k + 1))))
90 (across_L : ∀ k, k < n → σ (ι (.d .L k)) = some (ι (.c .L (k + 1))))
91 (hook_c : ∀ k, 0 < k → k < n → τ (ι (.c .L k)) = ι (.c .R k))
92 (hook_d : ∀ k, 0 < k → k < n → τ (ι (.d .R k)) = ι (.d .L k)) :
93 -- the connection through R_c(u_0)
95 -- the connection through L_{c'}(u_0)
97 -- every port on the edges of the path is used
98 (∀ k, k < n →
101 -- the connection through `R_c(u_0)`, crossing by crossing
102 have from_R := walk_chain σ τ ι n across_R hook_d across_L hook_c
103 -- the connection through `L_{c'}(u_0)`: the same rules for the relabelled strip
104 have from_L := walk_chain σ τ (fun s => ι (swap s)) n
110 refine ⟨?_, ?_, fun k k_lt => ⟨from_R k k_lt, from_L k k_lt⟩⟩
111 · have last := from_R (n - 1) (by omega) -- the last crossing of the connection through `R_c(u_0)`
112 rw [show n - 1 + 1 = n by omega] at last
113 by_cases n_even : n % 2 = 0
114 · rw [ite_eq_right (show ¬ ((n - 1) % 2 = 0) by omega)] at last; rw [ite_eq_left n_even]; exact last
115 · rw [ite_eq_left (show (n - 1) % 2 = 0 by omega)] at last; rw [ite_eq_right n_even]; exact last
116 · have last := from_L (n - 1) (by omega) -- the last crossing of the connection through `L_{c'}(u_0)`
117 rw [show n - 1 + 1 = n by omega] at last
118 by_cases n_even : n % 2 = 0
119 · rw [ite_eq_right (show ¬ ((n - 1) % 2 = 0) by omega)] at last; rw [ite_eq_left n_even]; exact last
120 · rw [ite_eq_left (show (n - 1) % 2 = 0 by omega)] at last; rw [ite_eq_right n_even]; exact last
122end Chains
124end Zigzag
126end SpectreKnot