`lean/SpectreKnot/Data/Clusters.lean`

59 lines · generated data · on GitHub · hide comments

GENERATED by tools/gen_clusters.py from paper/code/exact/exact.py (exact arithmetic). Do not edit by hand.

← SpectreKnot/Data/Pattern.leanSpectreKnot/Data/Level2.lean →

All 39 files, and the declarations of this one

1/-

2GENERATED by tools/gen_clusters.py from paper/code/exact/exact.py (exact arithmetic). Do not edit by hand.

3-/

4import SpectreKnot.Basic

6namespace SpectreKnot.Clusters

8open Kind

10/-- The number of tiles of the level-1 supertile of each kind. -/

11def tiles : Kind → Nat

12 | .Gamma => 8

13 | .Delta => 9

14 | .Theta => 9

15 | .Lambda => 9

16 | .Xi => 9

17 | .Pi => 9

18 | .Sigma => 9

19 | .Phi => 9

20 | .Psi => 9

22/-- `glue K` lists, for each tile and each of its edges `e_0 … e_13`, the tile and edge it is glued to inside

23the level-1 supertile of kind `K`, or `none` for a rim edge. -/

24def glue : Kind → List (List (Option (Nat × Nat)))

25 | .Gamma => [[some (6, 5), some (6, 4), some (6, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (7, 3), some (7, 2), some (0, 13), some (0, 12), some (0, 11), none, none, none, none, none, some (2, 1), some (2, 0), some (7, 5), some (7, 4)], [some (1, 11), some (1, 10), none, none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (7, 7), some (7, 6), some (2, 13), some (2, 12), some (2, 11), none, none, some (4, 2), some (4, 1), some (4, 0), some (5, 1), some (5, 0), some (7, 9), some (7, 8)], [some (3, 9), some (3, 8), some (3, 7), none, none, none, none, none, none, none, none, some (5, 4), some (5, 3), some (5, 2)], [some (3, 11), some (3, 10), some (4, 13), some (4, 12), some (4, 11), none, none, none, none, none, none, some (6, 10), some (7, 11), some (7, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (7, 1), some (7, 0), some (7, 13), some (7, 12), some (5, 11), none, none, none], [some (6, 7), some (6, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (3, 1), some (3, 0), some (3, 13), some (3, 12), some (5, 13), some (5, 12), some (6, 9), some (6, 8)]]

26 | .Delta => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

27 | .Theta => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

28 | .Lambda => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

29 | .Xi => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

30 | .Pi => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

31 | .Sigma => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

32 | .Phi => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

33 | .Psi => [[some (7, 5), some (7, 4), some (7, 3), none, none, none, none, none, none, none, none, some (1, 4), some (1, 3), some (1, 2)], [some (8, 3), some (8, 2), some (0, 13), some (0, 12), some (0, 11), none, none, some (2, 2), some (2, 1), some (2, 0), some (3, 1), some (3, 0), some (8, 5), some (8, 4)], [some (1, 9), some (1, 8), some (1, 7), none, none, none, none, none, none, none, none, some (3, 4), some (3, 3), some (3, 2)], [some (1, 11), some (1, 10), some (2, 13), some (2, 12), some (2, 11), none, none, none, none, none, none, some (4, 4), some (4, 3), some (4, 2)], [some (8, 7), some (8, 6), some (3, 13), some (3, 12), some (3, 11), none, none, some (5, 2), some (5, 1), some (5, 0), some (6, 1), some (6, 0), some (8, 9), some (8, 8)], [some (4, 9), some (4, 8), some (4, 7), none, none, none, none, none, none, none, none, some (6, 4), some (6, 3), some (6, 2)], [some (4, 11), some (4, 10), some (5, 13), some (5, 12), some (5, 11), none, none, none, none, none, none, some (7, 10), some (8, 11), some (8, 10)], [none, none, none, some (0, 2), some (0, 1), some (0, 0), some (8, 1), some (8, 0), some (8, 13), some (8, 12), some (6, 11), none, none, none], [some (7, 7), some (7, 6), some (1, 1), some (1, 0), some (1, 13), some (1, 12), some (4, 1), some (4, 0), some (4, 13), some (4, 12), some (6, 13), some (6, 12), some (7, 9), some (7, 8)]]

35/-- The rim of the level-1 supertile as tile edges `(tile, i)`, in its own orientation, from its vertex 0. -/

36def rim : Kind → List (Nat × Nat)

37 | .Gamma => [(6, 13), (6, 12), (6, 11), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (4, 10), (4, 9), (4, 8), (4, 7), (4, 6), (4, 5), (4, 4), (4, 3), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (2, 2), (1, 9), (1, 8), (1, 7), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (6, 2), (6, 1), (6, 0)]

38 | .Delta => [(7, 13), (7, 12), (7, 11), (6, 10), (6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0)]

39 | .Theta => [(7, 13), (7, 12), (7, 11), (6, 10), (6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0)]

40 | .Lambda => [(7, 13), (7, 12), (7, 11), (6, 10), (6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0)]

41 | .Xi => [(7, 13), (7, 12), (7, 11), (6, 10), (6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0)]

42 | .Pi => [(7, 13), (7, 12), (7, 11), (6, 10), (6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0)]

43 | .Sigma => [(6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0), (7, 13), (7, 12), (7, 11), (6, 10)]

44 | .Phi => [(7, 13), (7, 12), (7, 11), (6, 10), (6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0)]

45 | .Psi => [(7, 13), (7, 12), (7, 11), (6, 10), (6, 9), (6, 8), (6, 7), (6, 6), (6, 5), (5, 10), (5, 9), (5, 8), (5, 7), (5, 6), (5, 5), (5, 4), (5, 3), (4, 6), (4, 5), (3, 10), (3, 9), (3, 8), (3, 7), (3, 6), (3, 5), (2, 10), (2, 9), (2, 8), (2, 7), (2, 6), (2, 5), (2, 4), (2, 3), (1, 6), (1, 5), (0, 10), (0, 9), (0, 8), (0, 7), (0, 6), (0, 5), (0, 4), (0, 3), (7, 2), (7, 1), (7, 0)]

47/-- The rim positions of the vertices 0 … 5 of the level-1 supertile, and its rim length. -/

48def vtx : Kind → List Nat

49 | .Gamma => [0, 7, 14, 24, 34, 39, 44]

50 | .Delta => [0, 10, 15, 23, 30, 40, 46]

51 | .Theta => [0, 10, 15, 26, 31, 41, 46]

52 | .Lambda => [0, 10, 15, 23, 30, 41, 46]

53 | .Xi => [0, 7, 15, 26, 31, 41, 46]

54 | .Pi => [0, 7, 15, 23, 30, 41, 46]

55 | .Sigma => [0, 6, 11, 19, 26, 36, 46]

56 | .Phi => [0, 10, 15, 23, 31, 41, 46]

57 | .Psi => [0, 7, 15, 23, 31, 41, 46]

59end SpectreKnot.Clusters

← SpectreKnot/Data/Pattern.leanSpectreKnot/Data/Level2.lean →