The vertex-packed tables of the gap checker

The tables tpx … taz hold one 640-bit slot per outer vertex. vtxSplit visits exactly the vertices whose slot sign bit is set.

def Cayley.Pack.vt (t : ℕ) : ℤ × ℤ × ℤ

Vertex t of the kernel table.

Equations

• Cayley.Pack.vt t = Cayley.K.vtxI.getD t (0, 0, 0)

def Cayley.Pack.BT : ℕ

The slot offset of the tables.

Equations

• Cayley.Pack.BT = 2 ^ 170

theorem Cayley.Pack.tpx_eq : K.tpx = packN 640 (fun (t : ℕ) => ((vt t).1 + ↑BT).toNat) 90

theorem Cayley.Pack.tpy_eq : K.tpy = packN 640 (fun (t : ℕ) => ((vt t).2.1 + ↑BT).toNat) 90

theorem Cayley.Pack.tpz_eq : K.tpz = packN 640 (fun (t : ℕ) => ((vt t).2.2 + ↑BT).toNat) 90

theorem Cayley.Pack.tnx_eq : K.tnx = packN 640 (fun (t : ℕ) => (↑BT - (vt t).1).toNat) 90

theorem Cayley.Pack.tny_eq : K.tny = packN 640 (fun (t : ℕ) => (↑BT - (vt t).2.1).toNat) 90

theorem Cayley.Pack.tnz_eq : K.tnz = packN 640 (fun (t : ℕ) => (↑BT - (vt t).2.2).toNat) 90

theorem Cayley.Pack.tax_eq : K.tax = packN 640 (fun (t : ℕ) => BT - (vt t).1.natAbs) 90

theorem Cayley.Pack.tay_eq : K.tay = packN 640 (fun (t : ℕ) => BT - (vt t).2.1.natAbs) 90

theorem Cayley.Pack.taz_eq : K.taz = packN 640 (fun (t : ℕ) => BT - (vt t).2.2.natAbs) 90

theorem Cayley.Pack.onesT_eq : K.onesT = packN 640 (fun (x : ℕ) => 1) 90

theorem Cayley.Pack.vt_bound (t : ℕ) : t < 90 → (vt t).1.natAbs < 2 ^ 161 ∧ (vt t).2.1.natAbs < 2 ^ 161 ∧ (vt t).2.2.natAbs < 2 ^ 161

The vertex coordinates are below 2^161 in absolute value.

theorem Cayley.Pack.shiftRight_land_packN {W : ℕ} {d : ℕ → ℕ} {n : ℕ} (hd : ∀ j < n, d j < 2 ^ W) {t : ℕ} (ht : t < n) : ((packN W d n).shiftRight (W * t)).land (2 ^ W - 1) = d t

Slot extraction from a packed number.

theorem Cayley.Pack.slot_eq {d : ℕ → ℕ} (hd : ∀ j < 90, d j < 2 ^ 640) {t : ℕ} (ht : t < 90) : K.slot (packN 640 d 90) t = ↑(d t)

theorem Cayley.Pack.testBit_signT {t : ℕ} (ht : t < 90) : K.signT.testBit (640 * t + 639) = true

theorem Cayley.Pack.testBit_fails (V : ℕ) {t : ℕ} (ht : t < 90) : (K.signT.xor (V.land K.signT)).testBit (640 * t + 639) = !V.testBit (640 * t + 639)

A vertex either passes the packed test or its fail bit is set.

theorem Cayley.Pack.vtxSplit_sound (f : ℕ → ℤ → ℤ → ℤ → ℤ → ℤ → ℤ → Bool) (depth lo n m : ℕ) : K.vtxSplit f depth lo n m = true → ∀ i < n, m.testBit (640 * i + 639) = true → f (lo + i) (K.slot K.tpx (lo + i) - ↑(2 ^ 170)) (K.slot K.tpy (lo + i) - ↑(2 ^ 170)) (K.slot K.tpz (lo + i) - ↑(2 ^ 170)) (↑(2 ^ 170) - K.slot K.tax (lo + i)) (↑(2 ^ 170) - K.slot K.tay (lo + i)) (↑(2 ^ 170) - K.slot K.taz (lo + i)) = true

vtxSplit visits every vertex whose bit is set.