lean/SpectreKnot/Box.lean
67 lines · 9 declarations, each with its own page · on GitHub ·
The two hands of a rim port (Hand), used throughout. The rest is the pilot's model of a tile, not used by the main results: boxes and the signature (paper §4: Lemma 4.1, Def 4.3), the decoration as a pairing of the tile's 28 ports (Def 3.1), and the tile's signature (Lemma 4.4; the main results use Statement.tile_hasSig, for the statement file's decoration pieceEnd).
← SpectreKnot/Strands.leanSpectreKnot/Gluing.lean →
All 39 files, and the declarations of this one
1/-
2The two hands of a rim port (`Hand`), used throughout. The rest is the pilot's model of a tile, not used by the main
3results: boxes and the signature (paper §4: Lemma 4.1, Def 4.3), the decoration as a pairing of the tile's 28 ports
4(Def 3.1), and the tile's signature (Lemma 4.4; the main results use `Statement.tile_hasSig`, for the statement file's
5decoration `pieceEnd`).
6-/
7import SpectreKnot.Basic
9namespace SpectreKnot
11/-- The two ports at a rim vertex `u`: `R` on the rim edge after `u`, near `u`; `L` on the rim edge before `u`,
12near `u` (in a chosen orientation of the rim; reversing it exchanges `L` and `R`). -/
14 | L | R
15 deriving DecidableEq, Repr
17/-- A rim port of a patch with `E` rim vertices `u_0, …, u_{E-1}`. -/
20/-- A claim about every rim port can be decided vertex by vertex, both hands at each. -/
22 decidable_of_iff (∀ i : Fin E, q (i, .L) ∧ q (i, .R))
23 ⟨fun both_hands p => by rcases p with ⟨i, _ | _⟩ <;> simp [both_hands i],
24 fun every_port i => ⟨every_port _, every_port _⟩⟩
26/-- The box of a patch (Lemma 4.1): the pairing of its rim ports by its arcs, and its number `κ` of closed strands
27(the count of the paper's long version, 19 October 2026). -/
30 closed : Nat
32/-- A box is *proper* if its pairing is an involution without fixed points (Lemma 4.1). -/
33def Box.Proper {E : Nat} (b : Box E) : Prop :=
34 ∀ p, b.pair (b.pair p) = p ∧ b.pair p ≠ p
36instance {E : Nat} (b : Box E) : Decidable b.Proper := by unfold Box.Proper; infer_instance
38/-- **Def 4.3.** The box has the *signature at* `(A, B)`: a hook at every rim vertex other than `A` and `B`, the
39crossover `R(A) ↔ R(B)`, `L(A) ↔ L(B)`, and no closed strand. -/
40def Box.Signature {E : Nat} (b : Box E) (A B : Fin E) : Prop :=
41 (∀ u : Fin E, u ≠ A → u ≠ B → b.pair (u, .L) = (u, .R)) ∧
42 b.pair (A, .R) = (B, .R) ∧ b.pair (A, .L) = (B, .L) ∧ b.closed = 0
45 unfold Box.Signature; infer_instance
47/-! ### The tile -/
49/-- **Def 3.1.** The decoration of the tile, as a pairing of its 28 ports `R(v_i)`, `L(v_i)` (vertices counted
50counter-clockwise from `v_0`): twelve hooks `L(v_i) ↔ R(v_i)` for `2 ≤ i ≤ 13`, and the crossover
51`R(v_0) ↔ R(v_1)`, `L(v_0) ↔ L(v_1)`. -/
53 | (⟨0, _⟩, hand) => (1, hand)
54 | (⟨1, _⟩, hand) => (0, hand)
55 | (i, .L) => (i, .R)
56 | (i, .R) => (i, .L)
58/-- The tile seen as a patch: its pieces are its arcs, and it has no closed strand. -/
61/-- The tile's pairing is a proper box: every port is paired with another port, which is paired back. -/
62theorem tileBox_proper : tileBox.Proper := by decide
64/-- **Lemma 4.4** (tile). A tile has the signature at `(v_0, v_1)`. -/
65theorem tile_signature : tileBox.Signature 0 1 := by decide
67end SpectreKnot