lean/Tests.lean
261 lines · no declarations · on GitHub ·
Tests of statements on concrete cases (evaluated by the interpreter, not the kernel). They are not part of any proof: they check that the definitions say what they are meant to say, on the 18 compositions of Computation 7.3.
← SpectreKnot/Turn.leanTestsSlow.lean →
All 39 files, and the declarations of this one
1/-
2Tests of statements on concrete cases (evaluated by the interpreter, not the kernel). They are not part of any proof:
3they check that the definitions say what they are meant to say, on the 18 compositions of Computation 7.3.
4-/
5import SpectreKnot
6import SpectreKnot.Data.Level2
8open SpectreKnot Compose
11 allKinds.flatMap fun T => [true, false].map fun ω => Comp.ofPattern T (letterLen m) (dOff m) ω
13-- the compositions are well formed
14#guard (cases18 1).all fun C => C.toGluing.wfCheck
15#guard (cases18 2).all fun C => C.toGluing.wfCheck
17-- rim lengths: E₂(Γ) = 160, E₂(Δ) = 182 (for Δ, the paper's Table 5), from the composition of level-1 children
18#guard ((Comp.ofPattern .Gamma (letterLen 1) (dOff 1) true).rimEdges.length,
19 (Comp.ofPattern .Delta (letterLen 1) (dOff 1) true).rimEdges.length) == (160, 182)
21-- the check is not vacuous: wrong orientation sign, or non-adjacent corners in any child, are rejected
22#guard (allKinds.all fun T => [true, false].all fun ω => !(Comp.ofPattern T (letterLen 1) (dOff 1) ω).check (!ω))
23#guard (List.range 8).all fun c => !((Comp.ofPattern .Delta (letterLen 1) (dOff 1) true).spreadCorners c).check true
25-- the paper's negative control for Computation 7.3, as `compositions.py` runs it: with every child's corner `B` placed
26-- two vertices from `A` (`B = A ± 2`), all 18 compositions fail the check
28 { C with kids := C.kids.map fun k => { k with B := if ω then (k.A + 2) % k.E else (k.A + k.E - 2) % k.E } }
30 !(spreadAll (Comp.ofPattern T (letterLen 1) (dOff 1) ω) ω).check ω
32/-- The kernel's check of Computation 9.2 (`Statement.stepCheck`), with the junction map `tg` in place of Table 6. -/
33def stepCheckWith (tg : Bool → (Nat → Nat) → Nat → Bool → Option Nat) (ω : Bool) : Bool :=
34 let C := Comp.ofLens .Delta (L₁ .Delta) (dOff 1) ω
37 | none => true
38 | some q =>
39 C.toGluing.fullWalk C.fuel (1, u, s) == some (Statement.jR (L₁ .Delta) q) ||
40 C.toGluing.fullWalk C.fuel (1, u, s) == some (Statement.jL (L₁ .Delta) q)
42/-- Table 6 with junctions 12 and 16 exchanged. -/
43def tgtSwapped (ω : Bool) (f : Nat → Nat) (u : Nat) (s : Bool) : Option Nat :=
44 (Statement.tgt ω f u s).map fun q => if q = 12 then 16 else if q = 16 then 12 else q
46-- the check passes with Table 6 (as `step_base` proves in the kernel), and the paper's negative control for
47-- Computation 9.2: with junctions 12 and 16 exchanged it fails, for both signs
48#guard [true, false].all fun ω => stepCheckWith Statement.tgt ω
49#guard [true, false].all fun ω => !stepCheckWith tgtSwapped ω
51/-! ## Tests of the statement file (`Statement.lean`)
53They check that its definitions mean what they are meant to: the supertiles it builds are the real ones, and the
54strand counts of the paper come out of its notions of "following a ribbon" and "the nest". The counts are computed
55with a memoised copy of `Statement.super` (`mlevels`), which is checked against `Statement.super` itself at levels
561 and 2. Slower checks at level 5 are in `TestsSlow.lean` (`./build.sh --slow`). -/
58namespace StatementTests
60open Statement
62/-! A memoised copy of `Statement.super`, for tests at higher levels. -/
64 | .Gamma => 0 | .Delta => 1 | .Theta => 2 | .Lambda => 3 | .Xi => 4 | .Pi => 5 | .Sigma => 6 | .Phi => 7 | .Psi => 8
66structure MPatch where
67 tiles : Nat
68 glue : Array (Option (Nat × Nat)) -- entry t * 14 + i
69 rim : Array (Nat × Nat)
70 vtx : Array Nat
71 rimPos : Array Nat -- entry t * 14 + i: position of (t, i) in rim
72 deriving Inhabited
74def MPatch.side (M : MPatch) (j : Nat) : Array (Nat × Nat) := M.rim.extract (M.vtx.getD j 0) (M.vtx.getD (j + 1) 0)
77 ⟨M.tiles, fun t i => M.glue.getD (t * 14 + i) none, M.rim.toList, M.vtx.toList⟩
79def mkRimPos (tiles : Nat) (rim : Array (Nat × Nat)) : Array Nat := Id.run do
80 let mut a := Array.replicate (tiles * 14) 0
81 for k in [0:rim.size] do
82 let (t, i) := rim[k]!
83 a := a.set! (t * 14 + i) k
84 return a
88 let rim := P.rim.toArray
89 { tiles := P.tiles, glue := ((List.range P.tiles).flatMap fun t => (List.range 14).map fun i => P.glue t i).toArray,
90 rim, vtx := P.vtx.toArray, rimPos := mkRimPos P.tiles rim }
93 let n := ch.size
94 let mut off := #[0]
95 for c in [0:n] do off := off.push (off[c]! + ch[c]!.tiles)
96 let tiles := off[n]!
97 let mut glue := Array.replicate (tiles * 14) none
98 for c in [0:n] do
99 let C := ch[c]!
100 for t₀ in [0:C.tiles] do
101 for i in [0:14] do
102 let g := match C.glue[t₀ * 14 + i]! with
103 | some (t', j) => some (t' + off[c]!, j)
104 | none =>
108 match ((Pattern.adj T).getD c []).getD j none with
109 | none => none
110 | some (c', j') =>
111 let s := ch[c']!.side j'
112 (s[s.size - 1 - o]?).map fun (t', i') => (t' + off[c']!, i')
113 glue := glue.set! ((t₀ + off[c]!) * 14 + i) g
114 let mut rim := #[]
115 for (c, j) in (Pattern.pside T).flatMap id do
116 rim := rim ++ ((ch[c]!.side j).reverse.map fun (t, i) => (t + off[c]!, i))
117 let vtx := ((List.range 7).map fun J =>
118 ((((Pattern.pside T).take J).flatMap id).map fun (c, j) => (ch[c]!.side j).size).sum).toArray
119 return { tiles, glue, rim, vtx, rimPos := mkRimPos tiles rim }
123/-- `mlevels m`: the nine supertiles of level `m`, by kind index. -/
124def mlevels : Nat → Array MPatch
125 | 0 => #[]
126 | 1 => (allK.map mlevel1).toArray
127 | m + 2 => let prev := mlevels (m + 1)
128 (allK.map fun T => mcompose T ((Pattern.kids T).map fun K => prev[kindIdx K]!).toArray).toArray
131 P.tiles == Q.tiles && P.rim == Q.rim && P.vtx == Q.vtx &&
132 (List.range P.tiles).all fun t => (List.range 14).all fun i => P.glue t i == Q.glue t i
136 | (t, i, true) => (M.glue.getD (t * 14 + i) none).map fun (t', j) => (t', j, true)
137 | (t, i, false) => (M.glue.getD (t * 14 + (i + 13) % 14) none).map fun (t', j) => (t', (j + 1) % 14, false)
140 | 0, _ => none
143 | some q => mfollow M f q
147/-- The strand of `M` through port `p`, named by its two ends on the rim. -/
149 let f := 28 * M.tiles + 1
150 let a := code ((mfollow M f p).getD (0, 0, false))
152 (min a b, max a b)
154/-- The number of strands of `M` through the tiles `off … off + n - 1` (one port per piece suffices). -/
155def strandsThrough (M : MPatch) (off n : Nat) : Nat :=
156 let ps := (List.range n).flatMap fun t => (List.range 14).map fun i => (t + off, i, true)
157 (ps.map (arcId M)).eraseDups.length
159/-- Where `N_b` sits in `N_{b+k}`: the offset of its first tile. -/
160def nestOff (b : Nat) : Nat → Nat
161 | 0 => 0
162 | k + 1 => nestOff (b + 1) k + (if b = 0 then 1 else ((mlevels b)[kindIdx .Xi]!).tiles)
164def nestTiles (b : Nat) : Nat := if b = 0 then 1 else ((mlevels b)[kindIdx .Delta]!).tiles
166def nestCount (b k : Nat) : Nat :=
167 strandsThrough ((mlevels (b + k))[kindIdx .Delta]!) (nestOff b k) (nestTiles b)
170/-- The chain of the paper's §10: X_m is a Θ for odd m and a Γ for even m; X_m is child 2 of X_{m+1} for odd m
171and child 7 for even m. `chainKind m`, and the offset of X_m's first tile in X_{m+1}. -/
173def chainStep (m : Nat) : Nat :=
174 let T := chainKind (m + 1); let c := if m % 2 = 1 then 2 else 7
175 (((Pattern.kids T).take c).map fun K => ((mlevels m)[kindIdx K]!).tiles).sum
176def chainOff (m : Nat) : Nat → Nat
177 | 0 => 0
178 | k + 1 => chainOff (m + 1) k + chainStep m
179def chainCount (m k : Nat) : Nat :=
180 strandsThrough ((mlevels (m + k))[kindIdx (chainKind (m + k))]!) (chainOff m k)
181 ((mlevels m)[kindIdx (chainKind m)]!).tiles
184-- `super` at level 2 is the real level-2 supertile: built here from the tables, it equals, edge for edge, the one
185-- built directly from the tile placements in exact arithmetic (`Data/Level2.lean`), with the same six vertices.
186#guard allK.all fun K =>
188 (List.range P.tiles).map (fun t => (List.range 14).map fun i => P.glue t i) == Level2.glue K && P.vtx == Level2.vtx K
190-- level 1: the sides have the lengths of the paper's Prop 6.1
191#guard allK.all fun K => (List.range 6).map (fun j => ((super 1 K).side j).length) == Pattern.len1 K
193-- the memoised copy agrees with `super` at levels 1 and 2
197-- sizes (for Δ, the paper's Table 5): tiles 9, 71, 559, 4401 and rims 46, 182, 758, 3198 for Δ; 8, 62, 488, 3842 and
198-- 44, 160, 652, 2736 for Γ
199#guard (List.range 4).map (fun m => ((mlevels (m + 1))[kindIdx .Delta]!).tiles) == [9, 71, 559, 4401]
200#guard (List.range 4).map (fun m => ((mlevels (m + 1))[kindIdx .Delta]!).rim.size) == [46, 182, 758, 3198]
201#guard (List.range 4).map (fun m => ((mlevels (m + 1))[kindIdx .Gamma]!).rim.size) == [44, 160, 652, 2736]
203-- the paper's Table 5: the strands of N_{b+k} through the tiles of N_b
204#guard [nestCount 0 1, nestCount 0 2, nestCount 0 3] == [5, 2, 1]
205#guard [nestCount 1 1, nestCount 1 2, nestCount 1 3] == [10, 2, 2]
206#guard [nestCount 2 1, nestCount 2 2] == [37, 2]
208-- Negative control: along that chain the same definitions give three strands, not one (§10). So "one strand"
209-- is not built into the definitions.
210#guard [chainCount 1 1, chainCount 1 2, chainCount 1 3] == [32, 3, 3]
212-- the Grandparent Lemma on instances: every vertex of every tile of N_1 is surrounded in N_3, and of N_2 in N_4; but not
213-- one level up (side 2 of N_b lies on the rim of N_{b+1}). So "surrounded" is not built into the definitions.
215 (List.range 30).any fun n => 0 < n && P.turns n (t, i) == some (t, i)
216def nestSurrounded (b k : Nat) : Bool :=
217 let P := ((mlevels (b + k))[kindIdx .Delta]!).toPatch
218 (List.range (nestTiles b)).all fun t => (List.range 14).all fun i => surroundedIn P (t + nestOff b k) i
219#guard nestSurrounded 1 2 && nestSurrounded 2 2
220#guard !nestSurrounded 1 1 && !nestSurrounded 2 1
222/-- Another decoration, given as a pairing of the 28 ports of a tile: port `2i` is R(v_i), and port `2i - 1` (round
22328) is L(v_i). -/
225 | (t, i, s) =>
226 let k := pairing[if s then 2 * i else (2 * i + 27) % 28]!
227 if k % 2 = 0 then (t, k / 2, true) else (t, (k + 1) / 2 % 14, false)
229/-- Following a ribbon of `M` with the decoration `e`, as `mfollow` does with `pieceEnd`. -/
231 | 0, _ => none
232 | f + 1, p => match M.across (e p) with
233 | none => some (e p)
234 | some q => dfollow M e f q
236/-- The ports of the tiles `off … off + n - 1` of `M` whose ribbon, with the decoration `e`, never reaches the rim: those
237on closed strands (an open strand reaches the rim within `28 * M.tiles` steps). -/
239 ((List.range n).flatMap fun t => (List.range 14).flatMap fun i => [(t + off, i, true), (t + off, i, false)]).countP
240 fun p => (dfollow M e (28 * M.tiles + 1) p).isNone
242/-- Three decorations, given that way: the Spectre Knot's; the Spectre Knot's with its crossing moved from corner 0 to
243corner 5; and no crossing, a hook at every corner. -/
244def knotDesign : Array Nat :=
245 #[2, 27, 0, 4, 3, 6, 5, 8, 7, 10, 9, 12, 11, 14, 13, 16, 15, 18, 17, 20, 19, 22, 21, 24, 23, 26, 25, 1]
246def crossAt5 : Array Nat :=
247 #[27, 2, 1, 4, 3, 6, 5, 8, 7, 11, 12, 9, 10, 14, 13, 16, 15, 18, 17, 20, 19, 22, 21, 24, 23, 26, 25, 0]
248def noCrossing : Array Nat :=
249 #[27, 2, 1, 4, 3, 6, 5, 8, 7, 10, 9, 12, 11, 14, 13, 16, 15, 18, 17, 20, 19, 22, 21, 24, 23, 26, 25, 0]
251-- Negative control for Theorem A on real supertiles: the Spectre Knot's pairing, read this way, is `pieceEnd`; with it
252-- no port of N_1 inside N_3 lies on a closed strand. With the crossing moved to corner 5, the same gluing and the same
253-- rule for following a ribbon find 226 of N_1's 252 ports on closed strands of N_3; with no crossing, 28 ports of the
254-- level-1 Δ already lie on closed strands. So "no closed strand" comes from the design, not from the definitions or
255-- the gluing.
256#guard (List.range 14).all fun i => [true, false].all fun s => designEnd knotDesign (5, i, s) == pieceEnd (5, i, s)
257#guard closedPorts ((mlevels 3)[kindIdx .Delta]!) (designEnd knotDesign) (nestOff 1 2) 9 == 0
258#guard closedPorts ((mlevels 3)[kindIdx .Delta]!) (designEnd crossAt5) (nestOff 1 2) 9 == 226
259#guard closedPorts ((mlevels 1)[kindIdx .Delta]!) (designEnd noCrossing) 0 9 == 28
261end StatementTests