Integer data for the kernel checker

Boxes with integer coordinates, the vertices as integers, the packed-table vertex walk, and the integer chart bases and group elements used by Cayley.Checker.KPack.

Scales: box coordinates are integers over U = 2^K; vertices are integers over 2^160.

structure Cayley.K.KBox : Type

A box with integer coordinates over 2^K.

• chart : Nat
• face : Nat
• K : Nat
• c : List Int
• h : List Int

@[instance_reducible]

instance Cayley.K.instInhabitedKBox : Inhabited KBox

Equations

• Cayley.K.instInhabitedKBox = { default := Cayley.K.instInhabitedKBox.default }

def Cayley.K.vtxI : List (Int × Int × Int)

The vertices, exactly vertexTab, as integers over 2^160.

Equations

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

def Cayley.K.vtxIdx : List (Nat × (Int × Int × Int) × Int × Int × Int)

The vertices with their indices and coordinate absolute values.

Equations

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

def Cayley.K.signT : Nat

The sign bits of the packed slots, Σ_T 2^(640 T + 639).

def Cayley.K.slot (tab t : Nat) : Int

Coordinate t of a packed table, (tab >>> 640 t) mod 2^640.

Equations

• Cayley.K.slot tab t = ↑((tab.shiftRight (640 * t)).land (2 ^ 640 - 1))

def Cayley.K.vtxSplit (f : Nat → Int → Int → Int → Int → Int → Int → Bool) : Nat → Nat → Nat → Nat → Bool

Run f on every vertex lo + i (i < n) whose slot bit 640 i + 639 is set in m, by binary splitting (depth bounds the recursion).

Equations

• One or more equations did not get rendered due to their size.
• Cayley.K.vtxSplit f 0 x✝² x✝¹ x✝ = (x✝ == 0)

def Cayley.K.p2 (k : Nat) : Int

2^k as an integer.

Equations

• Cayley.K.p2 k = ↑(2 ^ k)

def Cayley.K.chartMI : Nat → Int × Int × Int × Int × Int × Int × Int × Int × Int

The chart base M_j (integer entries; B_j = M_j / κ_j).

Equations

• One or more equations did not get rendered due to their size.
• Cayley.K.chartMI 0 = (1, 0, 0, 0, 1, 0, 0, 0, 1)
• Cayley.K.chartMI 1 = (1, 0, 0, 0, -1, 0, 0, 0, -1)
• Cayley.K.chartMI 2 = (-1, 0, 0, 0, 1, 0, 0, 0, -1)
• Cayley.K.chartMI 3 = (-1, 0, 0, 0, -1, 0, 0, 0, 1)

def Cayley.K.chartKI : Nat → Int

Equations

• Cayley.K.chartKI 4 = Cayley.kappaTau
• Cayley.K.chartKI x✝ = 1

def Cayley.K.kPair (chart j : Nat) : Option Nat

The paired vertex for the blown-up charts.

Equations

• Cayley.K.kPair chart j = Cayley.pairOf chart j

def Cayley.K.mtm (A B : Int × Int × Int × Int × Int × Int × Int × Int × Int) : Int × Int × Int × Int × Int × Int × Int × Int × Int

Aᵀ B for integer matrices.

Equations

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

def Cayley.K.mmI (A B : Int × Int × Int × Int × Int × Int × Int × Int × Int) : Int × Int × Int × Int × Int × Int × Int × Int × Int

Integer matrix product.

Equations

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