lean/SpectreKnot/Data/Pattern.lean
76 lines · generated data · on GitHub ·
GENERATED by tools/gen_pattern.py from paper/code/hierarchy/combin_8.json and letters.json. Do not edit by hand.
← TestsSlow.leanSpectreKnot/Data/Clusters.lean →
All 39 files, and the declarations of this one
1/-
2GENERATED by tools/gen_pattern.py from paper/code/hierarchy/combin_8.json and letters.json. Do not edit by hand.
3-/
4import SpectreKnot.Basic
6namespace SpectreKnot.Pattern
8open Kind Letter
10/-- Paper Table 1: the kinds of the children of a supertile of each kind, child 0 first. -/
12 | .Gamma => [.Pi, .Delta, .Theta, .Sigma, .Xi, .Phi, .Gamma]
13 | .Delta => [.Xi, .Delta, .Xi, .Phi, .Sigma, .Pi, .Phi, .Gamma]
14 | .Theta => [.Psi, .Delta, .Pi, .Phi, .Sigma, .Pi, .Phi, .Gamma]
15 | .Lambda => [.Psi, .Delta, .Xi, .Phi, .Sigma, .Pi, .Phi, .Gamma]
16 | .Xi => [.Psi, .Delta, .Pi, .Phi, .Sigma, .Psi, .Phi, .Gamma]
17 | .Pi => [.Psi, .Delta, .Xi, .Phi, .Sigma, .Psi, .Phi, .Gamma]
18 | .Sigma => [.Xi, .Delta, .Xi, .Phi, .Sigma, .Pi, .Lambda, .Gamma]
19 | .Phi => [.Psi, .Delta, .Psi, .Phi, .Sigma, .Pi, .Phi, .Gamma]
20 | .Psi => [.Psi, .Delta, .Psi, .Phi, .Sigma, .Psi, .Phi, .Gamma]
22/-- Paper Table 2: for child `c` and side `j`, `some (c', j')` if side `j` of child `c` is side `j'` of child
23`c'`, and `none` if it lies on the parent's rim. -/
25 | .Gamma => [[some (6, 1), none, none, none, none, some (1, 1)], [some (6, 2), some (0, 5), none, none, some (2, 0), some (3, 0)], [some (1, 4), none, none, none, none, some (3, 1)], [some (1, 5), some (2, 5), none, some (4, 0), some (5, 0), some (6, 3)], [some (3, 3), none, none, none, none, some (5, 1)], [some (3, 4), some (4, 5), none, none, none, some (6, 4)], [none, some (0, 0), some (1, 0), some (3, 5), some (5, 5), none]]
26 | .Delta => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
27 | .Theta => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
28 | .Lambda => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
29 | .Xi => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
30 | .Pi => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
31 | .Sigma => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
32 | .Phi => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
33 | .Psi => [[some (7, 1), none, none, none, none, some (1, 1)], [some (7, 2), some (0, 5), none, some (2, 0), some (3, 0), some (4, 0)], [some (1, 3), none, none, none, none, some (3, 1)], [some (1, 4), some (2, 5), none, none, none, some (4, 1)], [some (1, 5), some (3, 5), none, some (5, 0), some (6, 0), some (7, 3)], [some (4, 3), none, none, none, none, some (6, 1)], [some (4, 4), some (5, 5), none, none, none, some (7, 4)], [none, some (0, 0), some (1, 0), some (4, 5), some (6, 5), none]]
35/-- Paper Table 3: side `J` of the parent is the concatenation of the children's sides `(c, j)` listed, in the
36parent's own order. -/
38 | .Gamma => [[(6, 5), (5, 4), (5, 3)], [(5, 2), (4, 4), (4, 3)], [(4, 2), (4, 1), (3, 2), (2, 4), (2, 3)], [(2, 2), (2, 1), (1, 3), (1, 2), (0, 4)], [(0, 3), (0, 2)], [(0, 1), (6, 0)]]
39 | .Delta => [[(7, 5), (6, 4), (6, 3), (6, 2), (5, 4)], [(5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3)], [(3, 2), (2, 4), (2, 3)], [(2, 2), (2, 1), (1, 2), (0, 4), (0, 3)], [(0, 2), (0, 1), (7, 0)]]
40 | .Theta => [[(7, 5), (6, 4), (6, 3), (6, 2), (5, 4)], [(5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3), (3, 2), (2, 4)], [(2, 3), (2, 2)], [(2, 1), (1, 2), (0, 4), (0, 3), (0, 2)], [(0, 1), (7, 0)]]
41 | .Lambda => [[(7, 5), (6, 4), (6, 3), (6, 2), (5, 4)], [(5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3)], [(3, 2), (2, 4), (2, 3)], [(2, 2), (2, 1), (1, 2), (0, 4), (0, 3), (0, 2)], [(0, 1), (7, 0)]]
42 | .Xi => [[(7, 5), (6, 4), (6, 3)], [(6, 2), (5, 4), (5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3), (3, 2), (2, 4)], [(2, 3), (2, 2)], [(2, 1), (1, 2), (0, 4), (0, 3), (0, 2)], [(0, 1), (7, 0)]]
43 | .Pi => [[(7, 5), (6, 4), (6, 3)], [(6, 2), (5, 4), (5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3)], [(3, 2), (2, 4), (2, 3)], [(2, 2), (2, 1), (1, 2), (0, 4), (0, 3), (0, 2)], [(0, 1), (7, 0)]]
44 | .Sigma => [[(6, 3), (6, 2), (5, 4)], [(5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3)], [(3, 2), (2, 4), (2, 3)], [(2, 2), (2, 1), (1, 2), (0, 4), (0, 3)], [(0, 2), (0, 1), (7, 0), (7, 5), (6, 4)]]
45 | .Phi => [[(7, 5), (6, 4), (6, 3), (6, 2), (5, 4)], [(5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3)], [(3, 2), (2, 4), (2, 3), (2, 2)], [(2, 1), (1, 2), (0, 4), (0, 3), (0, 2)], [(0, 1), (7, 0)]]
46 | .Psi => [[(7, 5), (6, 4), (6, 3)], [(6, 2), (5, 4), (5, 3), (5, 2)], [(5, 1), (4, 2), (3, 4), (3, 3)], [(3, 2), (2, 4), (2, 3), (2, 2)], [(2, 1), (1, 2), (0, 4), (0, 3), (0, 2)], [(0, 1), (7, 0)]]
48/-- Paper Table 4: the letter of side `j` of a supertile of each kind. -/
50 | .Gamma => [.alpha, .alpha, .gamma, .delta, .beta, .beta]
51 | .Delta => [.gamma, .beta, .epsilon, .alpha, .gamma, .zeta]
52 | .Theta => [.gamma, .beta, .theta, .beta, .eta, .beta]
53 | .Lambda => [.gamma, .beta, .epsilon, .alpha, .theta, .beta]
54 | .Xi => [.alpha, .epsilon, .theta, .beta, .eta, .beta]
55 | .Pi => [.alpha, .epsilon, .epsilon, .alpha, .theta, .beta]
56 | .Sigma => [.zeta, .beta, .epsilon, .alpha, .gamma, .delta]
57 | .Phi => [.gamma, .beta, .epsilon, .epsilon, .eta, .beta]
58 | .Psi => [.alpha, .epsilon, .epsilon, .epsilon, .eta, .beta]
60/-- The side lengths of the level-1 supertiles, counted on the actual tiles by `hierarchy/combin.js` (paper §6);
61the kernel checks them against the clusters of `Data/Clusters.lean` (`level1Check`). -/
63 | .Gamma => [7, 7, 10, 10, 5, 5]
64 | .Delta => [10, 5, 8, 7, 10, 6]
65 | .Theta => [10, 5, 11, 5, 10, 5]
66 | .Lambda => [10, 5, 8, 7, 11, 5]
67 | .Xi => [7, 8, 11, 5, 10, 5]
68 | .Pi => [7, 8, 8, 7, 11, 5]
69 | .Sigma => [6, 5, 8, 7, 10, 10]
70 | .Phi => [10, 5, 8, 8, 10, 5]
71 | .Psi => [7, 8, 8, 8, 10, 5]
73/-- The level-1 Σ-supertile's crossover corner lies on its side 5, at this distance from vertex 5 (Lemma 6.4). -/
74def d1 : Nat := 6
76end SpectreKnot.Pattern