The 481 exact vertices in Parts' base graph

The order and coordinates are transcribed from JP/Pink/g481.vtx in the Polymath 16 data archive accompanying Jaan Parts, arXiv:2010.12661.

def HadwigerNelsonBounds.partsPointChunk0 (index : ℕ) : PartsPoint

Coordinate lookup chunk 0.

Equations

• HadwigerNelsonBounds.partsPointChunk0 0 = { a := 0, b := 0, c := 0, d := 0 }
• HadwigerNelsonBounds.partsPointChunk0 1 = { a := -5, b := 1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 2 = { a := 7, b := -1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 3 = { a := 2, b := 0, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 4 = { a := 2, b := 0, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 5 = { a := 7, b := -1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 6 = { a := -5, b := 1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 7 = { a := 5, b := -1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 8 = { a := -7, b := 1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 9 = { a := -2, b := 0, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 10 = { a := -2, b := 0, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 11 = { a := -7, b := 1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 12 = { a := 5, b := -1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 13 = { a := 12, b := -2, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk0 14 = { a := -10, b := 2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 15 = { a := 2, b := 0, c := -6, d := 4 }
• HadwigerNelsonBounds.partsPointChunk0 16 = { a := -3, b := 1, c := 7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk0 17 = { a := 9, b := -1, c := -5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk0 18 = { a := -8, b := 2, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 19 = { a := -8, b := 2, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 20 = { a := 9, b := -1, c := 5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk0 21 = { a := -3, b := 1, c := -7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk0 22 = { a := 2, b := 0, c := 6, d := -4 }
• HadwigerNelsonBounds.partsPointChunk0 23 = { a := -10, b := 2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 24 = { a := 12, b := -2, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk0 25 = { a := -12, b := 2, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk0 26 = { a := 10, b := -2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 27 = { a := -2, b := 0, c := 6, d := -4 }
• HadwigerNelsonBounds.partsPointChunk0 28 = { a := 3, b := -1, c := -7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk0 29 = { a := -9, b := 1, c := 5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk0 30 = { a := 8, b := -2, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 31 = { a := 8, b := -2, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 32 = { a := -9, b := 1, c := -5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk0 33 = { a := 3, b := -1, c := 7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk0 34 = { a := -2, b := 0, c := -6, d := 4 }
• HadwigerNelsonBounds.partsPointChunk0 35 = { a := 10, b := -2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 36 = { a := -12, b := 2, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk0 37 = { a := -5, b := 1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 38 = { a := 4, b := 0, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 39 = { a := -1, b := 1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 40 = { a := -1, b := 1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 41 = { a := 4, b := 0, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 42 = { a := -5, b := 1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 43 = { a := 5, b := -1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 44 = { a := -4, b := 0, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 45 = { a := 1, b := -1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 46 = { a := 1, b := -1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 47 = { a := -4, b := 0, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 48 = { a := 5, b := -1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 49 = { a := 7, b := -1, c := 5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 50 = { a := -3, b := 1, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk0 51 = { a := 4, b := 0, c := 6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk0 52 = { a := 11, b := -1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 53 = { a := -6, b := 2, c := 0, d := 0 }
• HadwigerNelsonBounds.partsPointChunk0 54 = { a := 11, b := -1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 55 = { a := 4, b := 0, c := -6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 56 = { a := -3, b := 1, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk0 57 = { a := 7, b := -1, c := -5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 58 = { a := -7, b := 1, c := -5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 59 = { a := 3, b := -1, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk0 60 = { a := -4, b := 0, c := -6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk0 61 = { a := -11, b := 1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk0 62 = { a := 6, b := -2, c := 0, d := 0 }
• HadwigerNelsonBounds.partsPointChunk0 63 = { a := -11, b := 1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk0 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPointChunk1 (index : ℕ) : PartsPoint

Coordinate lookup chunk 1.

Equations

• HadwigerNelsonBounds.partsPointChunk1 0 = { a := -4, b := 0, c := 6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 1 = { a := 3, b := -1, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk1 2 = { a := -7, b := 1, c := 5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 3 = { a := 0, b := 0, c := 4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 4 = { a := 2, b := 0, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 5 = { a := -1, b := 1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 6 = { a := 6, b := 0, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 7 = { a := 1, b := 1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 8 = { a := 1, b := 1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 9 = { a := 6, b := 0, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 10 = { a := -1, b := 1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 11 = { a := 2, b := 0, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 12 = { a := 0, b := 0, c := -4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 13 = { a := -2, b := 0, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 14 = { a := 1, b := -1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 15 = { a := -6, b := 0, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 16 = { a := -1, b := -1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 17 = { a := -1, b := -1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 18 = { a := -6, b := 0, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 19 = { a := 1, b := -1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 20 = { a := -2, b := 0, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 21 = { a := -8, b := 2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 22 = { a := 4, b := 0, c := -4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk1 23 = { a := -4, b := 2, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 24 = { a := -4, b := 2, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 25 = { a := 4, b := 0, c := 4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk1 26 = { a := -8, b := 2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 27 = { a := 8, b := -2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 28 = { a := -4, b := 0, c := 4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk1 29 = { a := 4, b := -2, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 30 = { a := 4, b := -2, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 31 = { a := -4, b := 0, c := -4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk1 32 = { a := 8, b := -2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 33 = { a := 7, b := -1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 34 = { a := 1, b := 1, c := 5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 35 = { a := 8, b := 0, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 36 = { a := 8, b := 0, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 37 = { a := 1, b := 1, c := -5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 38 = { a := 7, b := -1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 39 = { a := -7, b := 1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 40 = { a := -1, b := -1, c := -5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 41 = { a := -8, b := 0, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 42 = { a := -8, b := 0, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 43 = { a := -1, b := -1, c := 5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 44 = { a := -7, b := 1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 45 = { a := -5, b := 1, c := 7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 46 = { a := 9, b := -1, c := -1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk1 47 = { a := -6, b := 2, c := 4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 48 = { a := 13, b := -1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 49 = { a := 8, b := 0, c := 6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk1 50 = { a := 3, b := 1, c := -5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk1 51 = { a := 3, b := 1, c := 5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk1 52 = { a := 8, b := 0, c := -6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 53 = { a := 13, b := -1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 54 = { a := -6, b := 2, c := -4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 55 = { a := 9, b := -1, c := 1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk1 56 = { a := -5, b := 1, c := -7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 57 = { a := 5, b := -1, c := -7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk1 58 = { a := -9, b := 1, c := 1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk1 59 = { a := 6, b := -2, c := -4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk1 60 = { a := -13, b := 1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk1 61 = { a := -8, b := 0, c := -6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk1 62 = { a := -3, b := -1, c := 5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk1 63 = { a := -3, b := -1, c := -5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk1 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPointChunk2 (index : ℕ) : PartsPoint

Coordinate lookup chunk 2.

Equations

• HadwigerNelsonBounds.partsPointChunk2 0 = { a := -8, b := 0, c := 6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 1 = { a := -13, b := 1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 2 = { a := 6, b := -2, c := 4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk2 3 = { a := -9, b := 1, c := -1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk2 4 = { a := 5, b := -1, c := 7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 5 = { a := 2, b := 0, c := -2, d := 4 }
• HadwigerNelsonBounds.partsPointChunk2 6 = { a := -1, b := 1, c := 7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 7 = { a := 11, b := -1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 8 = { a := -4, b := 2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 9 = { a := -2, b := 2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 10 = { a := 10, b := 0, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 11 = { a := 10, b := 0, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 12 = { a := -2, b := 2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 13 = { a := -4, b := 2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 14 = { a := 11, b := -1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 15 = { a := -1, b := 1, c := -7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 16 = { a := 2, b := 0, c := 2, d := -4 }
• HadwigerNelsonBounds.partsPointChunk2 17 = { a := -2, b := 0, c := 2, d := -4 }
• HadwigerNelsonBounds.partsPointChunk2 18 = { a := 1, b := -1, c := -7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 19 = { a := -11, b := 1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 20 = { a := 4, b := -2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 21 = { a := 2, b := -2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 22 = { a := -10, b := 0, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 23 = { a := -10, b := 0, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 24 = { a := 2, b := -2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 25 = { a := 4, b := -2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 26 = { a := -11, b := 1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 27 = { a := 1, b := -1, c := 7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 28 = { a := -2, b := 0, c := -2, d := 4 }
• HadwigerNelsonBounds.partsPointChunk2 29 = { a := -10, b := 2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 30 = { a := 8, b := 0, c := -4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk2 31 = { a := -2, b := 2, c := 6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 32 = { a := -2, b := 2, c := -6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 33 = { a := 8, b := 0, c := 4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk2 34 = { a := -10, b := 2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 35 = { a := 10, b := -2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 36 = { a := -8, b := 0, c := 4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk2 37 = { a := 2, b := -2, c := -6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 38 = { a := 2, b := -2, c := 6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 39 = { a := -8, b := 0, c := -4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk2 40 = { a := 10, b := -2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 41 = { a := 12, b := -2, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk2 42 = { a := 3, b := 1, c := 9, d := -3 }
• HadwigerNelsonBounds.partsPointChunk2 43 = { a := 15, b := -1, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk2 44 = { a := 15, b := -1, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk2 45 = { a := 3, b := 1, c := -9, d := 3 }
• HadwigerNelsonBounds.partsPointChunk2 46 = { a := 12, b := -2, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk2 47 = { a := -12, b := 2, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk2 48 = { a := -3, b := -1, c := -9, d := 3 }
• HadwigerNelsonBounds.partsPointChunk2 49 = { a := -15, b := 1, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk2 50 = { a := -15, b := 1, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk2 51 = { a := -3, b := -1, c := 9, d := -3 }
• HadwigerNelsonBounds.partsPointChunk2 52 = { a := -12, b := 2, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk2 53 = { a := 4, b := 0, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk2 54 = { a := 1, b := 1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 55 = { a := 5, b := 1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 56 = { a := 5, b := 1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 57 = { a := 1, b := 1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 58 = { a := 4, b := 0, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 59 = { a := -4, b := 0, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk2 60 = { a := -1, b := -1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 61 = { a := -5, b := -1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk2 62 = { a := -5, b := -1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 63 = { a := -1, b := -1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk2 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPointChunk3 (index : ℕ) : PartsPoint

Coordinate lookup chunk 3.

Equations

• HadwigerNelsonBounds.partsPointChunk3 0 = { a := -4, b := 0, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 1 = { a := -5, b := 1, c := 5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 2 = { a := -3, b := 1, c := 1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk3 3 = { a := 6, b := 0, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 4 = { a := 3, b := 1, c := -1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk3 5 = { a := 10, b := 0, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 6 = { a := 5, b := 1, c := 5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 7 = { a := 0, b := 2, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 8 = { a := 12, b := 0, c := 0, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 9 = { a := 0, b := 2, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 10 = { a := 5, b := 1, c := -5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 11 = { a := 10, b := 0, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 12 = { a := 3, b := 1, c := 1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk3 13 = { a := 6, b := 0, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 14 = { a := -3, b := 1, c := -1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk3 15 = { a := -5, b := 1, c := -5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 16 = { a := 5, b := -1, c := -5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 17 = { a := 3, b := -1, c := -1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk3 18 = { a := -6, b := 0, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 19 = { a := -3, b := -1, c := 1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk3 20 = { a := -10, b := 0, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 21 = { a := -5, b := -1, c := -5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 22 = { a := 0, b := -2, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 23 = { a := -12, b := 0, c := 0, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 24 = { a := 0, b := -2, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 25 = { a := -5, b := -1, c := 5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 26 = { a := -10, b := 0, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 27 = { a := -3, b := -1, c := -1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk3 28 = { a := -6, b := 0, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 29 = { a := 3, b := -1, c := 1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk3 30 = { a := 5, b := -1, c := 5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 31 = { a := -1, b := 1, c := 5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 32 = { a := 8, b := 0, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 33 = { a := 7, b := 1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 34 = { a := 7, b := 1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 35 = { a := 8, b := 0, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 36 = { a := -1, b := 1, c := -5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 37 = { a := 1, b := -1, c := -5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 38 = { a := -8, b := 0, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 39 = { a := -7, b := -1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 40 = { a := -7, b := -1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 41 = { a := -8, b := 0, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 42 = { a := 1, b := -1, c := 5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 43 = { a := 2, b := 0, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 44 = { a := 5, b := 1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 45 = { a := 7, b := 1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 46 = { a := 7, b := 1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 47 = { a := 5, b := 1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 48 = { a := 2, b := 0, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 49 = { a := -2, b := 0, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 50 = { a := -5, b := -1, c := -3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 51 = { a := -7, b := -1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk3 52 = { a := -7, b := -1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 53 = { a := -5, b := -1, c := 3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk3 54 = { a := -2, b := 0, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 55 = { a := 0, b := 0, c := 8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 56 = { a := 4, b := 0, c := 0, d := 4 }
• HadwigerNelsonBounds.partsPointChunk3 57 = { a := -2, b := 2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 58 = { a := 12, b := 0, c := 4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 59 = { a := 2, b := 2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk3 60 = { a := 2, b := 2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 61 = { a := 12, b := 0, c := -4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk3 62 = { a := -2, b := 2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk3 63 = { a := 4, b := 0, c := 0, d := -4 }
• HadwigerNelsonBounds.partsPointChunk3 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPointChunk4 (index : ℕ) : PartsPoint

Coordinate lookup chunk 4.

Equations

• HadwigerNelsonBounds.partsPointChunk4 0 = { a := 0, b := 0, c := -8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 1 = { a := -4, b := 0, c := 0, d := -4 }
• HadwigerNelsonBounds.partsPointChunk4 2 = { a := 2, b := -2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 3 = { a := -12, b := 0, c := -4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 4 = { a := -2, b := -2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 5 = { a := -2, b := -2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 6 = { a := -12, b := 0, c := 4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 7 = { a := 2, b := -2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 8 = { a := -4, b := 0, c := 0, d := 4 }
• HadwigerNelsonBounds.partsPointChunk4 9 = { a := -6, b := 2, c := 8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 10 = { a := 15, b := -1, c := 1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 11 = { a := 9, b := 1, c := 7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 12 = { a := 9, b := 1, c := -7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 13 = { a := 15, b := -1, c := -1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 14 = { a := -6, b := 2, c := -8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 15 = { a := 6, b := -2, c := -8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 16 = { a := -15, b := 1, c := -1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 17 = { a := -9, b := -1, c := -7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 18 = { a := -9, b := -1, c := 7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 19 = { a := -15, b := 1, c := 1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 20 = { a := 6, b := -2, c := 8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 21 = { a := 7, b := -1, c := 7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk4 22 = { a := 9, b := -1, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 23 = { a := -4, b := 2, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 24 = { a := 8, b := 0, c := 0, d := 4 }
• HadwigerNelsonBounds.partsPointChunk4 25 = { a := 0, b := 2, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 26 = { a := 7, b := 1, c := 7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk4 27 = { a := 14, b := 0, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 28 = { a := 9, b := 1, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 29 = { a := 4, b := 2, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 30 = { a := 4, b := 2, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 31 = { a := 9, b := 1, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 32 = { a := 14, b := 0, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 33 = { a := 7, b := 1, c := -7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk4 34 = { a := 0, b := 2, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 35 = { a := 8, b := 0, c := 0, d := -4 }
• HadwigerNelsonBounds.partsPointChunk4 36 = { a := -4, b := 2, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 37 = { a := 9, b := -1, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 38 = { a := 7, b := -1, c := -7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk4 39 = { a := -7, b := 1, c := -7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk4 40 = { a := -9, b := 1, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 41 = { a := 4, b := -2, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 42 = { a := -8, b := 0, c := 0, d := -4 }
• HadwigerNelsonBounds.partsPointChunk4 43 = { a := 0, b := -2, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 44 = { a := -7, b := -1, c := -7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk4 45 = { a := -14, b := 0, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 46 = { a := -9, b := -1, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk4 47 = { a := -4, b := -2, c := -4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 48 = { a := -4, b := -2, c := 4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk4 49 = { a := -9, b := -1, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 50 = { a := -14, b := 0, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 51 = { a := -7, b := -1, c := 7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk4 52 = { a := 0, b := -2, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk4 53 = { a := -8, b := 0, c := 0, d := 4 }
• HadwigerNelsonBounds.partsPointChunk4 54 = { a := 4, b := -2, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 55 = { a := -9, b := 1, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk4 56 = { a := -7, b := 1, c := 7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk4 57 = { a := 2, b := 0, c := 2, d := 4 }
• HadwigerNelsonBounds.partsPointChunk4 58 = { a := 1, b := 1, c := 7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk4 59 = { a := 10, b := 0, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 60 = { a := 2, b := 2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 61 = { a := 4, b := 2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk4 62 = { a := 11, b := 1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk4 63 = { a := 11, b := 1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk4 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPointChunk5 (index : ℕ) : PartsPoint

Coordinate lookup chunk 5.

Equations

• HadwigerNelsonBounds.partsPointChunk5 0 = { a := 4, b := 2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 1 = { a := 2, b := 2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 2 = { a := 10, b := 0, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 3 = { a := 1, b := 1, c := -7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 4 = { a := 2, b := 0, c := -2, d := -4 }
• HadwigerNelsonBounds.partsPointChunk5 5 = { a := -2, b := 0, c := -2, d := -4 }
• HadwigerNelsonBounds.partsPointChunk5 6 = { a := -1, b := -1, c := -7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 7 = { a := -10, b := 0, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 8 = { a := -2, b := -2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 9 = { a := -4, b := -2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 10 = { a := -11, b := -1, c := -3, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 11 = { a := -11, b := -1, c := 3, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 12 = { a := -4, b := -2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 13 = { a := -2, b := -2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 14 = { a := -10, b := 0, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 15 = { a := -1, b := -1, c := 7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 16 = { a := -2, b := 0, c := 2, d := 4 }
• HadwigerNelsonBounds.partsPointChunk5 17 = { a := 4, b := 0, c := 6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 18 = { a := 3, b := 1, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk5 19 = { a := 7, b := 1, c := 5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 20 = { a := 11, b := 1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 21 = { a := 6, b := 2, c := 0, d := 0 }
• HadwigerNelsonBounds.partsPointChunk5 22 = { a := 11, b := 1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 23 = { a := 7, b := 1, c := -5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 24 = { a := 3, b := 1, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk5 25 = { a := 4, b := 0, c := -6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 26 = { a := -4, b := 0, c := -6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 27 = { a := -3, b := -1, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk5 28 = { a := -7, b := -1, c := -5, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 29 = { a := -11, b := -1, c := -1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 30 = { a := -6, b := -2, c := 0, d := 0 }
• HadwigerNelsonBounds.partsPointChunk5 31 = { a := -11, b := -1, c := 1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 32 = { a := -7, b := -1, c := 5, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 33 = { a := -3, b := -1, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk5 34 = { a := -4, b := 0, c := 6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 35 = { a := -3, b := 1, c := 5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk5 36 = { a := 8, b := 0, c := 6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 37 = { a := 5, b := 1, c := 7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 38 = { a := 9, b := 1, c := 1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk5 39 = { a := 6, b := 2, c := 4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk5 40 = { a := 13, b := 1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 41 = { a := 13, b := 1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 42 = { a := 6, b := 2, c := -4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk5 43 = { a := 9, b := 1, c := -1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk5 44 = { a := 5, b := 1, c := -7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 45 = { a := 8, b := 0, c := -6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 46 = { a := -3, b := 1, c := -5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk5 47 = { a := 3, b := -1, c := -5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk5 48 = { a := -8, b := 0, c := -6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 49 = { a := -5, b := -1, c := -7, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 50 = { a := -9, b := -1, c := -1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk5 51 = { a := -6, b := -2, c := -4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk5 52 = { a := -13, b := -1, c := 1, d := -1 }
• HadwigerNelsonBounds.partsPointChunk5 53 = { a := -13, b := -1, c := -1, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 54 = { a := -6, b := -2, c := 4, d := 0 }
• HadwigerNelsonBounds.partsPointChunk5 55 = { a := -9, b := -1, c := 1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk5 56 = { a := -5, b := -1, c := 7, d := 1 }
• HadwigerNelsonBounds.partsPointChunk5 57 = { a := -8, b := 0, c := 6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 58 = { a := 3, b := -1, c := 5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk5 59 = { a := 4, b := 0, c := 4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk5 60 = { a := 4, b := 2, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 61 = { a := 8, b := 2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk5 62 = { a := 8, b := 2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 63 = { a := 4, b := 2, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk5 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPointChunk6 (index : ℕ) : PartsPoint

Coordinate lookup chunk 6.

Equations

• HadwigerNelsonBounds.partsPointChunk6 0 = { a := 4, b := 0, c := -4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk6 1 = { a := -4, b := 0, c := -4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk6 2 = { a := -4, b := -2, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk6 3 = { a := -8, b := -2, c := 0, d := -2 }
• HadwigerNelsonBounds.partsPointChunk6 4 = { a := -8, b := -2, c := 0, d := 2 }
• HadwigerNelsonBounds.partsPointChunk6 5 = { a := -4, b := -2, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk6 6 = { a := -4, b := 0, c := 4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk6 7 = { a := 0, b := 0, c := 12, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 8 = { a := 6, b := 0, c := 0, d := 6 }
• HadwigerNelsonBounds.partsPointChunk6 9 = { a := 15, b := -1, c := 5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 10 = { a := 0, b := 2, c := 10, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 11 = { a := -3, b := 3, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 12 = { a := 18, b := 0, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 13 = { a := 3, b := 3, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 14 = { a := 15, b := 1, c := -5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 15 = { a := 15, b := 1, c := 5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 16 = { a := 3, b := 3, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 17 = { a := 18, b := 0, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 18 = { a := -3, b := 3, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 19 = { a := 0, b := 2, c := -10, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 20 = { a := 15, b := -1, c := -5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 21 = { a := 6, b := 0, c := 0, d := -6 }
• HadwigerNelsonBounds.partsPointChunk6 22 = { a := 0, b := 0, c := -12, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 23 = { a := -6, b := 0, c := 0, d := -6 }
• HadwigerNelsonBounds.partsPointChunk6 24 = { a := -15, b := 1, c := -5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 25 = { a := 0, b := -2, c := -10, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 26 = { a := 3, b := -3, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 27 = { a := -18, b := 0, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 28 = { a := -3, b := -3, c := 3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 29 = { a := -15, b := -1, c := 5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 30 = { a := -15, b := -1, c := -5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 31 = { a := -3, b := -3, c := -3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 32 = { a := -18, b := 0, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 33 = { a := 3, b := -3, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 34 = { a := 0, b := -2, c := 10, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 35 = { a := -15, b := 1, c := 5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 36 = { a := -6, b := 0, c := 0, d := 6 }
• HadwigerNelsonBounds.partsPointChunk6 37 = { a := 8, b := 0, c := 4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk6 38 = { a := 2, b := 2, c := 6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk6 39 = { a := 10, b := 2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk6 40 = { a := 10, b := 2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk6 41 = { a := 2, b := 2, c := -6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk6 42 = { a := 8, b := 0, c := -4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk6 43 = { a := -8, b := 0, c := -4, d := -4 }
• HadwigerNelsonBounds.partsPointChunk6 44 = { a := -2, b := -2, c := -6, d := -2 }
• HadwigerNelsonBounds.partsPointChunk6 45 = { a := -10, b := -2, c := 2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk6 46 = { a := -10, b := -2, c := -2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk6 47 = { a := -2, b := -2, c := 6, d := 2 }
• HadwigerNelsonBounds.partsPointChunk6 48 = { a := -8, b := 0, c := 4, d := 4 }
• HadwigerNelsonBounds.partsPointChunk6 49 = { a := 9, b := -1, c := 7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 50 = { a := 6, b := 2, c := 8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 51 = { a := 15, b := 1, c := -1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 52 = { a := 15, b := 1, c := 1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 53 = { a := 6, b := 2, c := -8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 54 = { a := 9, b := -1, c := -7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 55 = { a := -9, b := 1, c := -7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 56 = { a := -6, b := -2, c := -8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 57 = { a := -15, b := -1, c := 1, d := -3 }
• HadwigerNelsonBounds.partsPointChunk6 58 = { a := -15, b := -1, c := -1, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 59 = { a := -6, b := -2, c := 8, d := 0 }
• HadwigerNelsonBounds.partsPointChunk6 60 = { a := -9, b := 1, c := 7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 61 = { a := 2, b := 0, c := 6, d := 4 }
• HadwigerNelsonBounds.partsPointChunk6 62 = { a := 3, b := 1, c := 7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 63 = { a := 9, b := 1, c := 5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk6 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPointChunk7 (index : ℕ) : PartsPoint

Coordinate lookup chunk 7.

Equations

• HadwigerNelsonBounds.partsPointChunk7 0 = { a := 8, b := 2, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk7 1 = { a := 10, b := 2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk7 2 = { a := 12, b := 2, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 3 = { a := 12, b := 2, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 4 = { a := 10, b := 2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk7 5 = { a := 8, b := 2, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk7 6 = { a := 9, b := 1, c := -5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 7 = { a := 3, b := 1, c := -7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 8 = { a := 2, b := 0, c := -6, d := -4 }
• HadwigerNelsonBounds.partsPointChunk7 9 = { a := -2, b := 0, c := -6, d := -4 }
• HadwigerNelsonBounds.partsPointChunk7 10 = { a := -3, b := -1, c := -7, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 11 = { a := -9, b := -1, c := -5, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 12 = { a := -8, b := -2, c := -4, d := -2 }
• HadwigerNelsonBounds.partsPointChunk7 13 = { a := -10, b := -2, c := -2, d := -2 }
• HadwigerNelsonBounds.partsPointChunk7 14 = { a := -12, b := -2, c := -2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 15 = { a := -12, b := -2, c := 2, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 16 = { a := -10, b := -2, c := 2, d := 2 }
• HadwigerNelsonBounds.partsPointChunk7 17 = { a := -8, b := -2, c := 4, d := 2 }
• HadwigerNelsonBounds.partsPointChunk7 18 = { a := -9, b := -1, c := 5, d := 3 }
• HadwigerNelsonBounds.partsPointChunk7 19 = { a := -3, b := -1, c := 7, d := 3 }
• HadwigerNelsonBounds.partsPointChunk7 20 = { a := -2, b := 0, c := 6, d := 4 }
• HadwigerNelsonBounds.partsPointChunk7 21 = { a := -3, b := 1, c := 9, d := 3 }
• HadwigerNelsonBounds.partsPointChunk7 22 = { a := 15, b := 1, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk7 23 = { a := 12, b := 2, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 24 = { a := 12, b := 2, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 25 = { a := 15, b := 1, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 26 = { a := -3, b := 1, c := -9, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 27 = { a := 3, b := -1, c := -9, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 28 = { a := -15, b := -1, c := -3, d := -3 }
• HadwigerNelsonBounds.partsPointChunk7 29 = { a := -12, b := -2, c := -6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 30 = { a := -12, b := -2, c := 6, d := 0 }
• HadwigerNelsonBounds.partsPointChunk7 31 = { a := -15, b := -1, c := 3, d := 3 }
• HadwigerNelsonBounds.partsPointChunk7 32 = { a := 3, b := -1, c := 9, d := 3 }
• HadwigerNelsonBounds.partsPointChunk7 index = { a := 0, b := 0, c := 0, d := 0 }

def HadwigerNelsonBounds.partsPoint (v : Fin 481) : PartsPoint

The exact coordinate attached to a vertex number in the base graph.

Equations

• One or more equations did not get rendered due to their size.

def HadwigerNelsonBounds.partsAdjacent (v w : Fin 481) : Bool

Decidable unit adjacency used by the lower-bound certificate checker.

Equations

• HadwigerNelsonBounds.partsAdjacent v w = ((HadwigerNelsonBounds.partsPoint v).sub (HadwigerNelsonBounds.partsPoint w)).IsUnit

theorem HadwigerNelsonBounds.dist_partsPoint_eq_one {v w : Fin 481} (h : partsAdjacent v w = true) : dist (partsPoint v).toR2 (partsPoint w).toR2 = 1

theorem HadwigerNelsonBounds.unitDistanceGraph_adj_of_partsAdjacent {v w : Fin 481} (h : partsAdjacent v w = true) : unitDistanceGraph.Adj (partsPoint v).toR2 (partsPoint w).toR2