lean/SpectreKnot/Statement.lean
476 lines · 60 declarations, each with its own page · on GitHub ·
The statements of Theorems A and B
← The Lean formalisationAxioms.lean →
All 39 files, and the declarations of this one
1/-
2# The statements of Theorems A and B
4This is the file to read to know what the Lean development proves. It holds every definition the main theorems depend
5on, and the theorems themselves, as claims (`def … : Prop`) in §5–§7. The proofs are in other files; Lean's kernel
6checks each of them against the claim written here. So "has the right thing been proved?" comes down to: do the
7definitions below say what the paper means? A guided reading, with a short introduction to Lean, is the proof site's
8page `statement.html`.
10Besides `Kind`, `iter`, `nxt`, `prv` and `fib` (from `Basic.lean`), the file uses two generated data files:
11`Data/Pattern.lean`, the paper's Tables 1–3 (with Table 4 and the level-1 lengths ℓ₁ and d₁, which only the proofs
12use, and check against the clusters), and `Data/Clusters.lean`, the nine level-1 supertiles, computed in exact
13arithmetic.
15There is no geometry here: a patch of tiles is described only by which edge of which tile is glued to which edge of
16which other tile. The link with real tilings is an assumption, (M), in three parts, each argued in the paper and
17none proved in Lean:
19 (M1) In every homochiral tiling by Tile(1,1), every level-m supertile of kind K, m ≥ 1, is glued exactly like
20 `super m K`, with its tiles numbered as `super` numbers them (child by child in the order of Table 1, down to
21 the order of the level-1 data) and its rim listed from vertex 0 in its own orientation. Argued in the paper:
22 Thm 2.1 (the hierarchy, from the spectre paper), Prop 2.4 (the composition pattern at every level, checked in
23 Remark 2.5), Lemma 2.6 (rigidity: the same numbering at every level), step (ii) of §7.1 (children meet only in
24 the sides they share). Level 0 is not part of it: `super 0 K` is one tile, the paper's level-0 Γ a Mystic.
25 (M2) So a tiling whose hierarchy covers the plane is the union of a chain of supertiles as in §7, and the chain
26 covers (`Chain.Covers`). Argued in the first half of the proof of Theorem A (§7.4), about points of the plane:
27 every tile lies in a supertile of the chain, and each edge, shared with exactly one other tile (Lemma 3.4),
28 lies inside a supertile that holds both.
29 (M3) The nest tiling of the paper is the union of the blocks `N b`, as `nestTiling` (§6), and covers the plane.
30 Argued in Props 8.2 and 8.4. Lemma 8.3(a), which Prop 8.4 uses, is proved here at the vertices of tiles
31 (`Grandparent`); the step from those to the points of the plane is part of (M3).
32-/
33import SpectreKnot.Basic
34import SpectreKnot.Data.Pattern
35import SpectreKnot.Data.Clusters
37namespace SpectreKnot.Statement
39/-! ## 1. Ports and pieces (the paper's §3.1) -/
41/-- A **port** `(t, i, s)`: a ribbon end on an edge of tile `t`, beside its vertex `v_i` (`i` = 0 … 13, numbered
42counter-clockwise; edge `e_i` runs from `v_i` to `v_{i+1}`). `s = true` is `R(v_i)`, on edge `e_i`; `s = false` is
43`L(v_i)`, on edge `e_{i-1}`. Each tile has 28 ports. -/
46/-- **Def 3.1, the decoration.** `pieceEnd p` is the other end of the ribbon piece that ends at port `p`. -/
48 -- The crossover: R(v_0) ↔ R(v_1) and L(v_0) ↔ L(v_1), two pieces that cross inside the tile.
49 | (t, 0, s) => (t, 1, s)
50 | (t, 1, s) => (t, 0, s)
51 -- Every other vertex: a hook round the corner, L(v_i) ↔ R(v_i).
52 | (t, i, s) => (t, i, !s)
54/-! ## 2. Patches and strands (the paper's §3.2–3.3) -/
56/-- A **patch**: `tiles` tiles, numbered `0 … tiles - 1`, and what lies across each edge. `glue t i = some (t', j)`
57means that edge `e_i` of tile `t` is edge `e_j` of tile `t'`; the two tiles run along it in opposite directions, so
58`v_i` of `t` is `v_{j+1}` of `t'`. `none` means the edge is on the rim. For supertiles, `rim` lists the rim edges in
59order from vertex 0, and `vtx` the positions in `rim` of the six vertices, then the rim's length. -/
61 tiles : Nat
62 glue : Nat → Nat → Option (Nat × Nat)
63 rim : List (Nat × Nat)
64 vtx : List Nat
66/-- **Def 3.2, the straight-through rule**, for a gluing `glue` like a patch's (or a tiling's, §6): the port where the
67ribbon at `p` continues across its edge, or `none` if nothing is glued there. -/
68def straightThrough (glue : Nat → Nat → Option (Nat × Nat)) : Port → Option Port
69 -- R(v_i) is on e_i. If e_i is e_j of t', the ribbon continues as R(v_j) of t'.
70 | (t, i, true) => (glue t i).map fun (t', j) => (t', j, true)
71 -- L(v_i) is on e_{i-1} (`(i + 13) % 14` is i - 1, round 14). If that is e_j of t', it continues as L(v_{j+1}).
72 | (t, i, false) => (glue t ((i + 13) % 14)).map fun (t', j) => (t', (j + 1) % 14, false)
74namespace Patch
78/-- `p` is a port of a tile of the patch. -/
81/-- The straight-through rule in the patch: `none` if the edge is on the rim. -/
82def across (p : Port) : Option Port := straightThrough P.glue p
84/-- **Following a ribbon.** `P.Follow p r`: from `p`, going along a piece, across an edge, along a piece, and so on,
85you leave the patch at the rim port `r`. It holds exactly when it follows from the two rules in finitely many steps. -/
87 -- The far end of p's piece is on the rim: leave there.
89 -- Otherwise cross to q, and carry on from q.
92/-- **No closed strand**: from every port of the patch, following the ribbon leads out of it. (A closed strand
93never reaches the rim.) -/
94def NoClosedStrand : Prop := ∀ p, P.IsPort p → ∃ r, P.Follow p r
96/-- **Same strand.** `P.Linked p q`: `q` is reached from `p` by moves along pieces and across glued edges, inside
97the patch. -/
103/-- **Turning about a point.** Corner `(t, i)` is vertex `v_i` of tile `t`. If edge `e_{i-1}` (which ends at `v_i`)
104is glued to edge `e_j` of tile `t'`, the same point is `v_j` of `t'`, the next corner about it (the two tiles run along
105the edge in opposite directions); `none` if the edge is on the rim. -/
108/-- Turning `n` times about a point, across glued edges only. -/
110 | 0, c => some c
113/-- Vertex `v_i` of tile `t` is **surrounded**: turning about it, across glued edges only, comes back to where it
114started. (A vertex on the rim is not: turning about it reaches the rim.) -/
115def Surrounded (t i : Nat) : Prop := ∃ n, 0 < n ∧ P.turns n (t, i) = some (t, i)
117/-- **Side `j` of a supertile**: its rim edges from vertex `j` to vertex `j+1`. -/
119 (P.rim.drop (P.vtx.getD j 0)).take (P.vtx.getD (j + 1) 0 - P.vtx.getD j 0)
121/-- The number of rim edges, which is also the number of rim vertices. -/
124/-- Rim edge number `k`. -/
127/-- **The rim ports** (the paper's §4.1). The rim is listed in the orientation `o`: `true` is counter-clockwise, the
128way each tile's own edges run, `false` clockwise. Rim vertex `k` is where rim edge `k` begins. `(k, true)` is its port
129`R(u_k)`, on rim edge `k` near the vertex; `(k, false)` is `L(u_k)`, on rim edge `k - 1` near the vertex. -/
131 | (k, true) =>
132 if o then ((P.edgeAt k).1, (P.edgeAt k).2, true) else ((P.edgeAt k).1, ((P.edgeAt k).2 + 1) % 14, false)
133 | (k, false) =>
137/-- The corner `(t, i)` of a port `(t, i, s)`: vertex `v_i` of tile `t`, which the port is beside. -/
140/-- The corner where turning about rim vertex `k` starts: beside its rim port `(k, o)`. -/
143/-- The corner where turning about rim vertex `k` ends: beside its other rim port. -/
146/-- **The patch is a disc at its rim**: turning about each rim vertex, from the corner beside one of its rim ports,
147reaches the corner beside the other. So consecutive rim edges meet at the rim vertex between them. -/
150end Patch
152/-- **Def 4.3, the signature's pairing** of the rim ports, with corners `A` and `B`: a hook at every other rim vertex
153(`L(u_k) ↔ R(u_k)`), and the crossover `R(A) ↔ R(B)`, `L(A) ↔ L(B)`. -/
155 | (k, s) => if k = A then (B, s) else if k = B then (A, s) else (k, !s)
157/-- **Def 4.3, a patch with the signature** at rim vertices `A`, `B`, its rim listed in the orientation `o`: the rim
158list holds exactly the unglued edges, each once; no strand is closed; and following the ribbon from each rim port
159leads to the port that `btau` pairs it with. -/
160structure Patch.HasSig (P : Patch) (o : Bool) (A B : Nat) : Prop where
161 tiles_pos : 0 < P.tiles
162 /-- the rim edges are edges of actual tiles, and are not glued -/
163 rim_ok : ∀ k, k < P.E → (P.edgeAt k).1 < P.tiles ∧ (P.edgeAt k).2 < 14 ∧ P.glue (P.edgeAt k).1 (P.edgeAt k).2 = none
164 /-- no edge is listed twice -/
165 rim_inj : ∀ k k', k < P.E → k' < P.E → P.edgeAt k = P.edgeAt k' → k = k'
166 /-- every unglued edge is listed -/
167 rim_all : ∀ t i, t < P.tiles → i < 14 → P.glue t i = none → ∃ k, k < P.E ∧ P.edgeAt k = (t, i)
168 /-- glued edges are edges of actual tiles -/
169 glue_ok : ∀ t i t' j, t < P.tiles → i < 14 → P.glue t i = some (t', j) → t' < P.tiles ∧ j < 14
170 noClosed : P.NoClosedStrand
171 /-- following the ribbon from a rim port leads to the port the signature pairs it with -/
174/-! ## 3. Supertiles (the paper's §2.2–2.4) -/
176/-- **Prop 2.4, as a construction**: the supertile of kind `T` with children `child 0`, `child 1`, … (Table 1). Its
177tiles are the children's, numbered child by child. Where Table 2 says that side `j` of child `c` is side `j'` of child
178`c'`, those sides are glued edge by edge, in opposite directions. The rim is the children's sides listed in Table 3,
179each traversed backwards (a parent's orientation is opposite to its children's). -/
181 -- n: the number of children (8, or 7 for Γ).
182 let n := (Pattern.kids T).length
183 -- off c: the number of the first tile of child c.
184 let off : Nat → Nat := fun c => ((List.range c).map fun c' => (child c').tiles).sum
185 -- owner t: the child that tile t belongs to.
186 let owner : Nat → Nat := fun t => ((List.range n).filter fun c => off c ≤ t).length - 1
187 -- shift c e: edge e of child c, renumbered as an edge of the parent.
188 let shift : Nat → Nat × Nat → Nat × Nat := fun c e => (e.1 + off c, e.2)
189 { -- The parent has the tiles of all its children.
190 tiles := off n
191 glue := fun t i =>
192 -- Tile t is tile t₀ of child c.
193 let c := owner t
194 let t₀ := t - off c
195 match (child c).glue t₀ i with
196 -- Glued inside the child: glued in the parent.
197 | some e => some (shift c e)
198 -- On the child's rim: the edge is at position pos of the rim, the o-th edge of side j.
199 | none =>
200 let pos := ((child c).rim.findIdx? (· == (t₀, i))).getD 0
201 let j := ((List.range 6).filter fun j => (child c).vtx.getD j 0 ≤ pos).length - 1
202 let o := pos - (child c).vtx.getD j 0
203 -- Table 2 for side j of child c.
204 match ((Pattern.adj T).getD c []).getD j none with
205 -- On the parent's rim: not glued.
206 | none => none
207 -- Side j' of child c': glued to its o-th edge counted from the end.
208 | some (c', j') =>
209 let s := (child c').side j'
210 (s[s.length - 1 - o]?).map (shift c')
211 -- Table 3: the children's sides, each backwards, in order.
212 rim := ((Pattern.pside T).flatMap id).flatMap fun (c, j) => ((child c).side j).reverse.map (shift c)
213 -- Vertex J: the total length of the pieces of sides 0 … J-1.
214 vtx := (List.range 7).map fun J =>
215 ((((Pattern.pside T).take J).flatMap id).map fun (c, j) => ((child c).side j).length).sum }
217/-- A single tile: nothing glued, its 14 edges round the rim. -/
220/-- The level-1 supertile of kind `K`, from the data file (the spectre paper's Fig. 4.1 clusters). -/
222 ⟨Clusters.tiles K, fun t i => ((Clusters.glue K).getD t []).getD i none, Clusters.rim K, Clusters.vtx K⟩
224/-- **`super m K`: the supertile of level `m` and kind `K`.** Level 0 is a single tile, for every kind (the paper's
225level-0 Γ, the Mystic, is not used), and level 1 the data; level `m + 2` is composed from children of level `m + 1`, of
226the kinds Table 1 lists. -/
230 | m + 2, T => compose T fun c => super (m + 1) ((Pattern.kids T).getD c .Gamma)
232/-! ## 4. The nest (the paper's §8) -/
234/-- The block `N_b` of the nest: the Δ-supertile of level `b`. -/
237/-- `N_b` is child 1 of `N_{b+1}`, after child 0, a Ξ: tile `t` of `N_b` is tile `t + nestShift b` of `N_{b+1}`. -/
240/-- `up b k t`: tile `t` of `N_b`, renumbered as a tile of `N_{b+k}`. -/
242 | 0, t => t
245/-- `upPort b k p`: port `p` of `N_b`, as a port of `N_{b+k}`. -/
248/-! ## 5. The theorems (claims; their proofs are in other files) -/
250/-- The crossover corner `A` of `super m K` (`m ≥ 1`), as a rim vertex: vertex 0, or for Σ the point `2 F_{3m+1}`
251along side 5 from vertex 5 (the paper's Lemma 6.4). -/
252def cornerA (m : Nat) (K : Kind) : Nat := if K = .Sigma then (super m K).vtx.getD 5 0 + 2 * fib (3 * m + 1) else 0
254/-- The other crossover corner, `B = A + ω_m` in the supertile's own order: the next rim vertex at even levels, the
255previous one at odd levels. -/
259/-- **The Signature Theorem** (the paper's Thm 7.6, for every level `m ≥ 1`). With its rim listed in its own
260orientation (counter-clockwise at even levels, clockwise at odd ones), every supertile `super m K` is a disc at its
261rim, and has the signature at its crossover corners: `A` (`cornerA`, a rim vertex) and `B = A + ω_m` (`cornerB`).
262(Proved in `ProofGrand.lean`.) -/
263def SignatureTheorem : Prop :=
267/-- **No supertile contains a closed strand**: the last sentence of the paper's Thm 7.6, at every level, level 0
268included (Theorem A for supertiles, in combinatorial form). The paper's Theorem A itself, for tilings, is
269`TheoremA_strand` (§7). (Proved in `ProofA.lean`.) -/
272/-- **Theorem B** (combinatorial form), three claims about the nest:
273(1) every edge of a block `N_b` (`b ≥ 1`) is glued to a tile in `N_{b+2}`: the nest has no boundary;
274(2) no block contains a closed strand;
275(3) any two ports of a block lie on the same strand of a larger block. (Proved in `ProofB.lean`.) -/
279 (∀ b p q, (N b).IsPort p → (N b).IsPort q → ∃ k, (N (b + k)).Linked (upPort b k p) (upPort b k q))
281/-- **Theorem B with the paper's bound**: for `b ≥ 1`, any two ports of `N_b` lie on one strand of `N_{b+4}`, and of
282`N_{b+3}` if `b` is even. (Proved in `ProofB.lean`.) -/
283def TheoremB_sharp : Prop :=
288/-- `k` levels up, the ports of `N_b` lie on exactly two strands of `N_{b+k}`: there are two ports `p`, `q` of `N_b`
289that are not on one strand there, and every port of `N_b` is on the strand of one of them. -/
290def TwoStrands (b k : Nat) : Prop :=
293 (N (b + k)).Linked (upPort b k x) (upPort b k p) ∨ (N (b + k)).Linked (upPort b k x) (upPort b k q)
295/-- **The bound is exact** (the last two rows of the paper's Table 5): for `b ≥ 1`, the ports of `N_b` lie on two
296strands of `N_{b+2}`, and, if `b` is odd, on two strands of `N_{b+3}`. With `TheoremB_sharp`: on 2, 1, 1 strands of
297`N_{b+2}`, `N_{b+3}`, `N_{b+4}` if `b` is even, and on 2, 2, 1 if `b` is odd. (Proved in `ProofExact.lean`.) -/
298def TheoremB_exact : Prop := ∀ b, 1 ≤ b → TwoStrands b 2 ∧ (b % 2 = 1 → TwoStrands b 3)
300/-- **The Grandparent Lemma** (the paper's Lemma 8.3(a), at the vertices of tiles): for `b ≥ 1`, every vertex of every
301tile of `N_b` is surrounded by tiles of `N_{b+2}`. So `N_b` does not meet the rim of `N_{b+2}`. (Proved in
302`ProofGrand.lean`.) -/
303def Grandparent : Prop :=
306/-! ## 6. Tilings, and the nest tiling's single strand -/
308/-- **A tiling**: infinitely many tiles, numbered 0, 1, 2, …, and what lies across each edge, `glue`, as in a patch.
309It is not a patch: it has no number of tiles and no rim, and the notions of §2 (`IsPort`, `NoClosedStrand`, …) are
310not defined for it. Its strands are followed one step at a time. -/
312 glue : Nat → Nat → Option (Nat × Nat)
314namespace Tiling
318/-- The straight-through rule in the tiling. -/
319def across (p : Port) : Option Port := straightThrough T.glue p
321/-- One step forwards along a strand: along the piece at `p`, then across the edge. -/
324/-- One step backwards: across the edge at `p`, then along the piece. -/
327end Tiling
329/-- **`gid b t`: the number, in the whole nest tiling, of tile `t` of `N_b`.** The numbers are chosen so that the
330tiles of every block `N_b` get 0 … |N_b| - 1. In `N_{b+1}`: a tile of child 1 (`N_b`) keeps its number in `N_b`; a
331tile of child 0 comes next, after those of `N_b`; a tile of a later child keeps its own number. -/
333 | 0, t => t
334 | b + 1, t =>
337 else t
339/-- **`loc b g`**: the tile of `N_b` whose number in the nest tiling is `g`; it undoes `gid b`. -/
341 | 0, g => g
342 | b + 1, g =>
345 else g
347/-- **The gluing of the nest tiling**: what lies across edge `e_i` of the tile numbered `g`. It is read off `N_{g+3}`,
348which contains the tile with two levels to spare. (By `NestModel` (d), every block gives the same answer.) -/
352/-- **The nest tiling**: the tiles of all the blocks, numbered by `gid`, glued by `nestGlue`. -/
353def nestTiling : Tiling := ⟨nestGlue⟩
355/-- **The nest tiling is a tiling, and the union of the blocks:**
356(a) every number `g` is a tile of `N_{g+1}`;
357(b) `gid b` numbers the tiles of `N_b` one to one with 0 … |N_b| - 1, and `loc b` is its inverse;
358(c) a tile keeps its number one level up;
359(d) whatever `N_b` glues, the nest tiling glues the same way;
360(e) every edge of every tile is glued, to an edge of a different tile, which is glued back. -/
368 (∀ g i, i < 14 → ∃ g' j, nestGlue g i = some (g', j) ∧ g' ≠ g ∧ j < 14 ∧ nestGlue g' j = some (g, i))
370/-- **Theorem B, final form: one two-way infinite strand.** Start at `R(v_0)` of the original tile, `(0, 0, true)`,
371and step forwards and backwards along its strand:
372(1) forwards, no port is met twice;
373(2) backwards, no port is met twice;
374(3) no port is met both backwards and forwards, except the start;
375(4) no piece is run through twice;
376(5) every port of every tile is met, or is the other end of the piece of one that is.
377(Proved in `ProofStrand.lean`.) -/
378def TheoremB_strand : Prop :=
379 (∀ i j, iter nestTiling.forward i (0, 0, true) = iter nestTiling.forward j (0, 0, true) → i = j) ∧
380 (∀ a a', iter nestTiling.backward a (0, 0, true) = iter nestTiling.backward a' (0, 0, true) → a = a') ∧
381 (∀ a b, iter nestTiling.backward a (0, 0, true) = iter nestTiling.forward b (0, 0, true) → a = 0 ∧ b = 0) ∧
382 (∀ i j, iter nestTiling.forward j (0, 0, true) ≠ pieceEnd (iter nestTiling.forward i (0, 0, true))) ∧
384 q = iter nestTiling.forward k (0, 0, true) ∨ q = iter nestTiling.backward k (0, 0, true) ∨
385 q = pieceEnd (iter nestTiling.forward k (0, 0, true)) ∨ q = pieceEnd (iter nestTiling.backward k (0, 0, true)))
387/-! ## 7. Any chain of supertiles (the paper's Theorem A, for tilings) -/
389/-- **A chain of supertiles** X_1 ⊂ X_2 ⊂ ⋯: for every level `m ≥ 1`, the kind `K m` of X_m and its position `c m`
390among the children of X_{m+1}, consistent with Table 1. In a tiling, the supertiles containing a given tile form a
391chain; the nest is the chain with `K m = Δ`, `c m = 1`. -/
394 c : Nat → Nat
395 child_lt : ∀ m, 1 ≤ m → c m < (Pattern.kids (K (m + 1))).length
396 child_kind : ∀ m, 1 ≤ m → (Pattern.kids (K (m + 1))).getD (c m) .Gamma = K m
398namespace Chain
400/-- The block X_m: the supertile of level `m` and kind `K m`. -/
403/-- Where X_m starts inside X_{m+1}: the number of tiles of the children before it. -/
405 ((List.range (X.c m)).map fun c' => (super m ((Pattern.kids (X.K (m + 1))).getD c' .Gamma)).tiles).sum
407/-- `X.up m k t`: tile `t` of X_m, renumbered as a tile of X_{m+k}. -/
409 | 0, t => t
412/-- **`X.gid m t`: the number, in the union of the chain, of tile `t` of X_m**, as `gid` of §6, from level 1. -/
414 | 0, t => t
415 | 1, t => t
416 | m + 2, t =>
417 if X.shift (m + 1) ≤ t ∧ t < X.shift (m + 1) + (X.block (m + 1)).tiles then gid X (m + 1) (t - X.shift (m + 1))
418 else if t < X.shift (m + 1) then (X.block (m + 1)).tiles + t
419 else t
421/-- **`X.loc m g`**: the tile of X_m whose number in the union is `g`; it undoes `X.gid m`. -/
423 | 0, g => g
424 | 1, g => g
425 | m + 2, g =>
427 else if g < (X.block (m + 1)).tiles + X.shift (m + 1) then g - (X.block (m + 1)).tiles
428 else g
430/-- **The chain covers**: every edge of every block is glued in some larger block, so the union of the chain has no
431rim. This is the combinatorial form of a hierarchy that covers the plane (see (M2)). -/
433 ∀ m t i, 1 ≤ m → t < (X.block m).tiles → i < 14 → ∃ k, ((X.block (m + k)).glue (X.up m k t) i).isSome
435/-- **`T` contains every block**: whatever X_m glues, the tiling `T` glues the same way. -/
437 ∀ m t i t' j, 1 ≤ m → t < (X.block m).tiles → i < 14 → (X.block m).glue t i = some (t', j) →
438 T.glue (X.gid m t) i = some (X.gid m t', j)
440end Chain
442/-- **The union of a chain is a tiling.** For every chain X:
443(a) every number `g` is a tile of X_{g+1};
444(b) `X.gid m` numbers the tiles of X_m one to one, and `X.loc m` is its inverse;
445(c) a tile keeps its number one level up;
446(d) there is a tiling `T` of the union that contains every block;
447(e) if the chain covers, every such `T` glues every edge of every tile, to a different tile, and back. -/
448def ChainModel : Prop :=
450 (∀ g, g < (X.block (g + 1)).tiles) ∧
451 (∀ m t, 1 ≤ m → t < (X.block m).tiles → X.gid m t < (X.block m).tiles ∧ X.loc m (X.gid m t) = t) ∧
452 (∀ m g, 1 ≤ m → g < (X.block m).tiles → X.loc m g < (X.block m).tiles ∧ X.gid m (X.loc m g) = g) ∧
453 (∀ m t, 1 ≤ m → t < (X.block m).tiles → X.gid (m + 1) (X.up m 1 t) = X.gid m t) ∧
456 ∀ g i, i < 14 → ∃ g' j, T.glue g i = some (g', j) ∧ g' ≠ g ∧ j < 14 ∧ T.glue g' j = some (g, i))
458/-- **Theorem A in strand form: in a tiling whose hierarchy covers the plane, every strand is two-way infinite.** For
459any chain that covers, any tiling `T` of its union that contains every block, and any port `p`:
460(1) forwards, no port is met twice;
461(2) backwards, no port is met twice;
462(3) no port is met both backwards and forwards, except the start;
463(4) no piece is run through twice.
464(Proved in `ProofChain.lean`.) -/
465def TheoremA_strand : Prop :=
472/-- **Chains that cover exist**: the nest, as a chain (every block a Δ, child 1 of the next), covers. So
473`TheoremA_strand` is not vacuous. (Proved in `ProofChain.lean`.) -/
474def NestCovers : Prop := ∃ X : Chain, (∀ m, X.K m = .Delta ∧ X.c m = 1) ∧ X.Covers
476end SpectreKnot.Statement