The Spectre Knot the proofPictures and ideas →
Draft proof, not peer reviewed. What has been checked

lean/SpectreKnot/PatchSig.lean

197 lines · 24 declarations, each with its own page · on GitHub ·

The signature of a patch of tiles (Def 4.3 at tile level), for the proof of Theorem A.

← SpectreKnot/Parity.leanSpectreKnot/ComposeTiles.lean →

All 39 files, and the declarations of this one
1/-
2The signature of a patch of tiles (Def 4.3 at tile level), for the proof of Theorem A.
3
4A supertile is a *box*: its rim is a cycle of tile edges, and at each rim vertex there are two ports, `R` (on the rim
5edge that starts there) and `L` (on the rim edge that ends there). `Patch.HasSig P o A B`, defined in `Statement.lean`,
6says: the rim list is the set of unglued edges, without repeats; no strand of `P` is closed; and following the ribbon
7from any rim port leads to the port the signature pairs it with: the other port at the same vertex (a hook), except at
8the corners `A` and `B`, where `R(A) ↔ R(B)` and `L(A) ↔ L(B)`. The rim runs in the patch's own orientation `o`
9(`true`: counter-clockwise, as the tiles' own; `false`: clockwise), which decides which end of a tile edge is "near the
10start".
12The base cases: a single tile, and the nine level-1 supertiles (checked by the kernel).
13-/
19namespace SpectreKnot.Statement
21open Pattern
23-- The rim ports (`Patch.E`, `edgeAt`, `bport`), the signature's pairing `btau` and `Patch.HasSig` itself are in
24-- `Statement.lean`, where the claim `SignatureTheorem` uses them.
26/-! ### Following a ribbon, as a computation -/
28namespace Patch
30variable (P : Patch)
32/-- Following the ribbon from `p`, with at most `f` steps. -/
33def follow : Nat → Port → Option Port
34 | 0, _ => none
35 | f + 1, p =>
36 match P.across (pieceEnd p) with
37 | none => some (pieceEnd p)
38 | some q => follow f q
40/-- The computation is sound: if `follow` finds a port within its fuel, following the ribbon really leaves the patch
41there. -/
42theorem follow_sound : ∀ f p r, P.follow f p = some r → P.Follow p r := by
43 intro f
44 induction f with
45 | zero => intro p r found; simp [follow] at found
46 | succ f ih =>
47 intro p r found
48 simp only [follow] at found
49 cases across_eq : P.across (pieceEnd p) with
50 | none =>
51 -- the other end of the piece is on the rim: the walk leaves there
52 rw [across_eq] at found; simp only [Option.some.injEq] at found; subst found; exact .leave across_eq
53 | some q =>
54 -- the ribbon crosses to `q`, and the rest of the walk starts there
55 rw [across_eq] at found; exact .next across_eq (ih q r found)
57/-- The checks of `HasSig`, as a computation (`f`: the fuel for each walk). -/
58def sigCheck (o : Bool) (A B f : Nat) : Bool :=
59 decide (0 < P.tiles) &&
60 ((List.range P.E).all fun k =>
61 decide ((P.edgeAt k).1 < P.tiles) && decide ((P.edgeAt k).2 < 14) &&
62 (P.glue (P.edgeAt k).1 (P.edgeAt k).2).isNone) &&
63 ((List.range P.E).all fun k => (List.range P.E).all fun k' => !(P.edgeAt k == P.edgeAt k') || k == k') &&
64 ((List.range P.tiles).all fun t => (List.range 14).all fun i =>
65 (P.glue t i).isSome || (List.range P.E).any fun k => P.edgeAt k == (t, i)) &&
66 ((List.range P.tiles).all fun t => (List.range 14).all fun i =>
67 match P.glue t i with
68 | none => true
69 | some (t', j) => decide (t' < P.tiles) && decide (j < 14)) &&
70 ((List.range P.tiles).all fun t => (List.range 14).all fun i => [true, false].all fun s =>
71 (P.follow f (t, i, s)).isSome) &&
72 ((List.range P.E).all fun k => [true, false].all fun s =>
73 P.follow f (P.bport o (k, s)) == some (P.bport o (btau A B (k, s))))
75/-- The checker is sound: if `sigCheck` returns `true` (for any fuel), the patch has the signature at `A`, `B`. -/
76theorem sigCheck_sound {o : Bool} {A B f : Nat} (check : P.sigCheck o A B f = true) : P.HasSig o A B := by
77 simp only [sigCheck, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, List.mem_range, Bool.or_eq_true,
78 Option.isNone_iff_eq_none, Bool.not_eq_true', beq_iff_eq, List.any_eq_true, Option.isSome_iff_exists] at check
79 obtain ⟨⟨⟨⟨⟨⟨tiles_pos, rim_ok⟩, rim_inj⟩, rim_all⟩, glue_ok⟩, all_leave⟩, sig_ok⟩ := check
80 refine ⟨tiles_pos, fun k on_rim => ⟨(rim_ok k on_rim).1.1, (rim_ok k on_rim).1.2, (rim_ok k on_rim).2⟩,
81 fun k k' on_rim on_rim' same_edge => ?_, fun t i is_tile is_vertex unglued => ?_,
82 fun t i t' j is_tile is_vertex glued => ?_, fun p is_port => ?_, fun k s on_rim => ?_⟩
83 · -- two positions with the same edge: the check says they are equal
84 rcases rim_inj k on_rim k' on_rim' with differ | equal
85 · rw [same_edge] at differ; simp at differ
86 · exact equal
87 · -- an unglued edge: the check finds it on the rim list
88 rcases rim_all t is_tile i is_vertex with ⟨x, glued⟩ | ⟨k, on_rim, at_k⟩
89 · rw [unglued] at glued; contradiction
90 · exact ⟨k, on_rim, at_k⟩
91 · have bound := glue_ok t is_tile i is_vertex -- the check's bound on the edge across this glued edge
92 rw [glued] at bound
93 simpa using bound
94 · obtain ⟨t, i, s⟩ := p
95 obtain ⟨is_tile, is_vertex⟩ := is_port
96 -- the check found where the walk from this port leaves the patch
97 have leaves := all_leave t is_tile i is_vertex s (by cases s <;> simp)
98 obtain ⟨r, found⟩ := leaves
99 exact ⟨r, P.follow_sound f _ r found⟩
100 · have found := sig_ok k on_rim s (by cases s <;> simp) -- the walk from this rim port ends at its partner
101 exact P.follow_sound f _ _ found
In the paper Lemma 4.1 The box of a patch
103/-- **The box of a patch with the signature** (Lemma 4.1, for the patches the proof uses): the ribbon from each rim
104port leaves the patch at the rim port that `btau` pairs it with, and `btau` is an involution on the rim ports without
105fixed points. -/
106theorem HasSig.box {o : Bool} {A B : Nat} (has_sig : P.HasSig o A B) (A_lt : A < P.E) (B_lt : B < P.E)
107 (A_ne_B : A ≠ B) (k : Nat) (s : Bool) (k_lt : k < P.E) :
108 P.Follow (P.bport o (k, s)) (P.bport o (btau A B (k, s))) ∧ (btau A B (k, s)).1 < P.E ∧
109 btau A B (btau A B (k, s)) = (k, s) ∧ btau A B (k, s) ≠ (k, s) := by
110 refine ⟨has_sig.sig k s k_lt, ?_⟩
111 simp only [btau]
112 by_cases at_A : k = A
113 · subst at_A; simp [Ne.symm A_ne_B, B_lt]
114 · by_cases at_B : k = B
115 · subst at_B; simp [at_A, A_lt, Ne.symm at_A]
116 · simp [at_A, at_B, k_lt]
118end Patch
120/-! ### The level-`m` data: lengths, orientation, corners -/
122/-- ℓ_m(K, j), as a function of the side `j`. -/
123def lenAt (m : Nat) (K : Kind) (j : Nat) : Nat := letterLen m (letterOf K j)
125/-- The own orientation at level `m`: counter-clockwise (as the tiles) at even levels, clockwise at odd ones
126(Def 2.2). It is also the sign `ω_m`: `B = A + 1` at even levels and `B = A - 1` at odd ones. -/
127def ori (m : Nat) : Bool := m % 2 == 0
129/-- Where vertex `j` of a level-`m` `K`-supertile sits on its rim. -/
130def vpos (m : Nat) (K : Kind) (j : Nat) : Nat := Compose.pos (lenAt m K) j
132/-- The crossover corner `A` of a level-`m` `K`-supertile: vertex 0, or for Σ the point `d_m` along side 5
133(Lemma 6.4). -/
134def aPos (m : Nat) (K : Kind) : Nat := if K = .Sigma then vpos m K 5 + dOff m else 0
136/-- The other crossover corner `B = A + ω_m`. -/
137def bPos (m : Nat) (K : Kind) : Nat :=
138 if ori m then nxt (vpos m K 6) (aPos m K) else prv (vpos m K 6) (aPos m K)
140/-- **The induction hypothesis of Thm 7.6, at tile level**: the level-`m` `K`-supertile has the signature with its
141corners where `aPos`, `bPos` say, its six vertices where the side lengths ℓ_m put them. -/
142structure Good (m : Nat) (K : Kind) : Prop where
143 sig : (super m K).HasSig (ori m) (aPos m K) (bPos m K)
144 vtx : (super m K).vtx = (List.range 7).map (vpos m K)
145 len : (super m K).E = vpos m K 6
147/-! ### The base cases -/
In the paper Lemma 4.4 Signature of the tile
149/-- **Lemma 4.4: a tile has the signature**, at its corners `A = v_0` and `B = v_1`, its rim listed counter-clockwise
150(checked by the kernel). In particular it has no closed strand. -/
151theorem tile_hasSig : tile.HasSig true 0 1 := tile.sigCheck_sound (f := 2) (by decide +kernel)
153/-- The kernel's check of the nine level-1 supertiles. -/
154def level1Check (K : Kind) : Bool :=
155 (level1 K).sigCheck (ori 1) (aPos 1 K) (bPos 1 K) 300 &&
156 (level1 K).vtx == (List.range 7).map (vpos 1 K) && (level1 K).E == vpos 1 K 6
158/-- The kernel's check passes for the level-1 Γ-supertile. -/
159theorem level1Check_Gamma : level1Check .Gamma = true := by decide +kernel
160/-- The kernel's check passes for the level-1 Δ-supertile. -/
161theorem level1Check_Delta : level1Check .Delta = true := by decide +kernel
162/-- The kernel's check passes for the level-1 Θ-supertile. -/
163theorem level1Check_Theta : level1Check .Theta = true := by decide +kernel
164/-- The kernel's check passes for the level-1 Λ-supertile. -/
165theorem level1Check_Lambda : level1Check .Lambda = true := by decide +kernel
166/-- The kernel's check passes for the level-1 Ξ-supertile. -/
167theorem level1Check_Xi : level1Check .Xi = true := by decide +kernel
168/-- The kernel's check passes for the level-1 Π-supertile. -/
169theorem level1Check_Pi : level1Check .Pi = true := by decide +kernel
170/-- The kernel's check passes for the level-1 Σ-supertile. -/
171theorem level1Check_Sigma : level1Check .Sigma = true := by decide +kernel
172/-- The kernel's check passes for the level-1 Φ-supertile. -/
173theorem level1Check_Phi : level1Check .Phi = true := by decide +kernel
174/-- The kernel's check passes for the level-1 Ψ-supertile. -/
175theorem level1Check_Psi : level1Check .Psi = true := by decide +kernel
177/-- The kernel's check passes for all nine level-1 supertiles. -/
178theorem level1Check_all : ∀ K, level1Check K = true
182 | .Lambda => level1Check_Lambda
In the paper Computation 7.5 Base case
189/-- **The base of the induction**: the level-1 supertiles have the signature (Computation 7.5). -/
190theorem good_one (K : Kind) : Good 1 K := by
191 -- the kernel's check for this kind, split into its three parts
192 have check := level1Check_all K
193 simp only [level1Check, Bool.and_eq_true, beq_iff_eq] at check
194 obtain ⟨⟨sig_ok, vtx_eq⟩, len_eq⟩ := check
195 exact ⟨(level1 K).sigCheck_sound sig_ok, vtx_eq, len_eq⟩
197end SpectreKnot.Statement

← SpectreKnot/Parity.leanSpectreKnot/ComposeTiles.lean →