lean/SpectreKnot/Linked.lean
218 lines · 15 declarations, each with its own page · on GitHub ·
Strands as an equivalence relation. Linked (same strand, Statement.lean) is transitive, contains Follow, lifts from a child to its parent, and in every supertile is symmetric: gluing is symmetric (if edge e_i of tile t is glued to edge e_j of tile t', then e_j of t' is glued to e_i of t), so every move along a strand can be undone. Used for Theorem B (ProofB.lean).
← SpectreKnot/StepMap.leanSpectreKnot/NestStep.lean →
All 39 files, and the declarations of this one
1/-
2**Strands as an equivalence relation.** `Linked` (same strand, `Statement.lean`) is transitive, contains `Follow`,
3lifts from a child to its parent, and in every supertile is symmetric: gluing is symmetric (if edge `e_i` of tile `t`
4is glued to edge `e_j` of tile `t'`, then `e_j` of `t'` is glued to `e_i` of `t`), so every move along a strand can be
5undone. Used for Theorem B (`ProofB.lean`).
6-/
7import SpectreKnot.ProofA
9namespace SpectreKnot.Statement
11open Pattern Compose Gluing
13namespace Patch
17/-- **Same strand is transitive**: if `q` is on the strand of `p`, and `r` on the strand of `q`, then `r` is on the
18strand of `p`. -/
19theorem Linked.trans {p q r : Port} (first : P.Linked p q) (second : P.Linked q r) : P.Linked p r := by
20 induction second with
21 | refl => exact first
22 | piece _ ih => exact .piece ih
23 | edge _ across_eq ih => exact .edge ih across_eq
25/-- Following a ribbon stays on one strand. -/
26theorem Linked.of_follow {p r : Port} (follows : P.Follow p r) : P.Linked p r := by
27 induction follows with
28 | leave _ => exact .piece .refl
31/-- A strand stays among the ports of actual tiles. -/
32theorem Linked.valid {o : Bool} {A B : Nat} (sig : P.HasSig o A B) {p q : Port} (linked : P.Linked p q)
33 (p_port : P.IsPort p) : P.IsPort q := by
34 induction linked with
35 | refl => exact p_port
36 | piece _ ih =>
37 -- the other end of a piece is on the same tile, at an actual vertex
38 have end_valid := pieceEnd_valid ih.2
39 exact ⟨end_valid.1 ▸ ih.1, end_valid.2⟩
40 | edge _ across_eq ih => exact across_valid sig ih.1 ih.2 across_eq
42/-- **Gluing is symmetric.** -/
44 ∀ t i t' j, t < P.tiles → i < 14 → P.glue t i = some (t', j) → P.glue t' j = some (t, i)
46/-- The other end of the piece at the other end is the port itself. -/
47theorem pieceEnd_pieceEnd (p : Port) : pieceEnd (pieceEnd p) = p := by
48 obtain ⟨t, i, s⟩ := p
49 rcases i with _ | _ | i
50 · rfl
51 · rfl
54/-- **Crossing an edge can be undone**: in a patch with the signature and symmetric gluing, if port `q` lies across
55the edge from port `p`, then `p` lies across from `q`. -/
56theorem across_symm {o : Bool} {A B : Nat} (sig : P.HasSig o A B) (symm : P.GlueSymm) {p q : Port}
57 (p_port : P.IsPort p) (across_eq : P.across p = some q) : P.across q = some p := by
58 obtain ⟨t, i, s⟩ := p
59 obtain ⟨ht, hi⟩ := p_port
60 simp only at ht hi
61 cases s with
62 | true =>
63 simp only [across, straightThrough] at across_eq
64 cases glued : P.glue t i with
65 | none => rw [glued] at across_eq; contradiction
66 | some e =>
67 obtain ⟨t', j⟩ := e
68 rw [glued] at across_eq
69 simp only [Option.map_some, Option.some.injEq] at across_eq
70 subst across_eq
71 simp only [across, straightThrough, symm t i t' j ht hi glued, Option.map_some]
72 | false =>
73 simp only [across, straightThrough] at across_eq
74 cases glued : P.glue t ((i + 13) % 14) with
75 | none => rw [glued] at across_eq; contradiction
76 | some e =>
77 obtain ⟨t', j⟩ := e
78 rw [glued] at across_eq
79 simp only [Option.map_some, Option.some.injEq] at across_eq
80 subst across_eq
81 -- the far edge is an actual edge
82 have hj := (sig.glue_ok t _ t' j ht (by omega) glued).2
83 simp only [across, straightThrough, mod14 hj, symm t _ t' j ht (by omega) glued, Option.map_some,
84 Option.some.injEq, Prod.mk.injEq]
85 refine ⟨trivial, ?_, trivial⟩
86 -- vertex `i - 1`, counted round the 14 vertices, without `%`
87 have wrap : (i + 13) % 14 = (i + 13) - 14 ∨ (i + 13) % 14 = i + 13 := by omega
88 rcases wrap with wrap_eq | wrap_eq <;> rw [wrap_eq] <;> omega
90/-- **Same strand is symmetric** (in a patch with the signature and symmetric gluing). -/
91theorem Linked.symm {o : Bool} {A B : Nat} (sig : P.HasSig o A B) (symm : P.GlueSymm) {p q : Port}
92 (linked : P.Linked p q) (p_port : P.IsPort p) : P.Linked q p := by
93 induction linked with
94 | refl => exact .refl
95 | @piece q _ ih =>
96 -- back along the piece
98 -- one move along the piece from its other end
100 rwa [pieceEnd_pieceEnd] at along
101 exact back_along.trans ih
102 | @edge q q' to_q across_eq ih =>
103 -- back across the edge
104 exact (Linked.edge .refl (across_symm sig symm (to_q.valid sig p_port) across_eq)).trans ih
106end Patch
108/-! ### Lifting to the parent, and symmetry of the parent's gluing -/
110namespace Kids
112set_option linter.unusedSectionVars false
114-- `kids`: the children satisfy what the composition needs
118include kids
120/-- **A strand of a child is part of a strand of the parent.** -/
121theorem linked_lift {c : Nat} (hc : c < nk T) {p q : Port} (linked : (child c).Linked p q)
122 (p_port : (child c).IsPort p) : (compose T child).Linked (shiftP child c p) (shiftP child c q) := by
123 induction linked with
124 | refl => exact .refl
125 | piece _ ih => rw [← pieceEnd_shift]; exact .piece ih
126 | @edge q q' to_q across_eq ih =>
127 exact .edge ih (kids.across_in' hc (to_q.valid (kids.sig c hc) p_port).1 across_eq)
129/-- The parent's gluing is symmetric if the children's are. -/
130theorem glue_symm (children_symm : ∀ c, c < nk T → (child c).GlueSymm) : (compose T child).GlueSymm := by
131 -- the composition is well formed
132 have wf := kids.csig.wf
133 intro t i t' j ht hi glued
134 -- the child `c` that tile `t` belongs to
135 obtain ⟨c, hc, after_start, before_end⟩ := owner_exists child (nk T) t ht
137 -- its number `t₀` in child `c`
138 have ht₀ : t₀ < (child c).tiles := by omega
139 -- child `c` has the signature
140 have sig := kids.sig c hc
141 cases inside : (child c).glue t₀ i with
142 | some e =>
143 -- glued inside the child: the child's own gluing, shifted, which is symmetric
144 obtain ⟨t₂, j₂⟩ := e
145 rw [kids.glue_shift hc ht₀] at glued
147 obtain ⟨rfl, rfl⟩ := glued
148 -- the far tile is an actual tile of child `c`
149 have far_valid := sig.glue_ok t₀ i t₂ j₂ ht₀ hi inside
150 rw [kids.glue_shift hc far_valid.1]
152 | none =>
153 -- on the child's rim, at rim edge `k`: glued to a sibling's edge, as the gluing's `mate` says
154 obtain ⟨k, hk, at_k⟩ := sig.rim_all t₀ i ht₀ hi inside
155 -- `c` is a child of the gluing
156 have c_lt_n : c < (Comp.ofLens T L d ω).toGluing.n := by rw [ofLens_n]; exact hc
157 -- the parent glues rim edge `k` of child `c` as `mate` says
158 have formula := kids.glue_rimEdge hc hk
159 rw [at_k] at formula
160 rw [formula] at glued
161 cases mated : (Comp.ofLens T L d ω).toGluing.mate c k with
162 | none => rw [mated] at glued; contradiction
163 | some m =>
164 obtain ⟨c', k'⟩ := m
165 rw [mated] at glued
166 simp only [Option.map_some, Option.some.injEq, Prod.mk.injEq] at glued
167 obtain ⟨rfl, rfl⟩ := glued
168 -- the sibling's edge `k'` is an actual rim edge, glued back to edge `k` of `c`
169 obtain ⟨sib_lt_n, sib_edge_lt, mated_back⟩ :=
170 wf.mate_valid c k c' k' c_lt_n (by rw [kids.E_eq hc]; exact hk) mated
171 -- the sibling is an actual child
173 -- the parent glues the sibling's rim edge `k'` as `mate` says
174 have formula' := kids.glue_rimEdge sib_lt (by rw [← kids.E_eq sib_lt]; exact sib_edge_lt)
175 rw [formula', mated_back]
176 simp only [Option.map_some, at_k]
178end Kids
180/-! ### Every supertile has symmetric gluing -/
182/-- A single tile glues nothing, so its gluing is symmetric. -/
183theorem tile_glueSymm : tile.GlueSymm := fun _ _ _ _ _ _ glued => by simp [tile] at glued
185/-- The kernel's check of the level-1 data. -/
186def level1Symm (K : Kind) : Bool :=
189 | none => true
192/-- The check passes for all nine kinds. -/
193theorem level1Symm_all : ∀ K, level1Symm K = true := by intro K; cases K <;> decide +kernel
195/-- Every level-1 supertile has symmetric gluing. -/
196theorem level1_glueSymm (K : Kind) : (level1 K).GlueSymm := by
197 intro t i t' j ht hi glued
198 -- the kernel's check
199 have check := level1Symm_all K
200 simp only [level1Symm, List.all_eq_true, List.mem_range] at check
201 -- at tile `t` and edge `i`
202 have at_edge := check t ht i hi
203 rw [glued] at at_edge
204 simpa using at_edge
206/-- **Every supertile has symmetric gluing**, by induction on the level. -/
207theorem super_glueSymm : ∀ m K, (super m K).GlueSymm
208 | 0, _ => tile_glueSymm
209 | 1, K => level1_glueSymm K
210 | m + 2, T => (kids_at (m := m + 1) (by omega) T (fun K => good (m + 1) K (by omega))).glue_symm
211 (fun c _ => super_glueSymm (m + 1) _)
213/-- **Same strand is symmetric in every supertile of level `m ≥ 1`.** -/
214theorem linked_symm {m : Nat} (m_pos : 1 ≤ m) {K : Kind} {p q : Port} (linked : (super m K).Linked p q)
216 linked.symm (good m K m_pos).sig (super_glueSymm m K) p_port
218end SpectreKnot.Statement