def Hex.PermGroup.Kernel.width (n : Nat) : Nat

The field width for degree n: the least W ≥ 1 with n < 2^W. It is computed by n doubling steps rather than Nat.log2, which the kernel reduces through well-founded recursion.

Equations

• Hex.PermGroup.Kernel.width n = Nat.rec 1 (fun (x w : Nat) => bif (Nat.shiftLeft 1 w).ble n then w.succ else w) n

def Hex.PermGroup.Kernel.mask (W : Nat) : Nat

2^W - 1, the mask of one field.

Equations

• Hex.PermGroup.Kernel.mask W = (Nat.shiftLeft 1 W).sub 1

def Hex.PermGroup.Kernel.field (W x i : Nat) : Nat

Field i of x.

Equations

• Hex.PermGroup.Kernel.field W x i = (x.shiftRight (i.mul W)).land (Hex.PermGroup.Kernel.mask W)

def Hex.PermGroup.Kernel.packFn (W : Nat) (f : Nat → Nat) (k : Nat) : Nat

The number whose field i is f i for i < k, with no higher bits, assuming every f i is below 2^W.

Equations

• Hex.PermGroup.Kernel.packFn W f k = Nat.rec 0 (fun (i acc : Nat) => acc.add ((f i).shiftLeft (i.mul W))) k

def Hex.PermGroup.Kernel.comp (n W x y : Nat) : Nat

Composition (x * y)(i) = x(y(i)) of packed permutations of degree n.

Equations

• Hex.PermGroup.Kernel.comp n W x y = Hex.PermGroup.Kernel.packFn W (fun (i : Nat) => Hex.PermGroup.Kernel.field W x (Hex.PermGroup.Kernel.field W y i)) n

def Hex.PermGroup.Kernel.ident (n W : Nat) : Nat

The packed identity of degree n.

Equations

• Hex.PermGroup.Kernel.ident n W = Hex.PermGroup.Kernel.packFn W (fun (i : Nat) => i) n

def Hex.PermGroup.Kernel.pack {n : Nat} (p : Perm n) : Nat

The packing of a permutation of Fin n, with the width width n.

Equations

• Hex.PermGroup.Kernel.pack p = Hex.PermGroup.Kernel.packFn (Hex.PermGroup.Kernel.width n) (fun (i : Nat) => if h : i < n then ↑(p.get ⟨i, h⟩) else 0) n

theorem Hex.PermGroup.Kernel.one_le_width_go (n k : Nat) : 1 ≤ Nat.rec 1 (fun (x w : Nat) => bif (Nat.shiftLeft 1 w).ble n then w.succ else w) k

theorem Hex.PermGroup.Kernel.one_le_width (n : Nat) : 1 ≤ width n

theorem Hex.PermGroup.Kernel.width_go_spec (n k : Nat) : have w := Nat.rec 1 (fun (x w : Nat) => bif (Nat.shiftLeft 1 w).ble n then w.succ else w) k; n < 2 ^ w ∨ w = k + 1

After k steps the width is either k + 1 or already large enough.

theorem Hex.PermGroup.Kernel.lt_two_pow_width (n : Nat) : n < 2 ^ width n

theorem Hex.PermGroup.Kernel.mask_eq (W : Nat) : mask W = 2 ^ W - 1

theorem Hex.PermGroup.Kernel.field_eq (W x i : Nat) : field W x i = x / 2 ^ (i * W) % 2 ^ W

theorem Hex.PermGroup.Kernel.field_lt (W x i : Nat) : field W x i < 2 ^ W

theorem Hex.PermGroup.Kernel.packFn_succ (W : Nat) (f : Nat → Nat) (k : Nat) : packFn W f (k + 1) = packFn W f k + f k * 2 ^ (k * W)

theorem Hex.PermGroup.Kernel.packFn_lt (W : Nat) (f : Nat → Nat) (k : Nat) : (∀ (i : Nat), i < k → f i < 2 ^ W) → packFn W f k < 2 ^ (k * W)

theorem Hex.PermGroup.Kernel.field_packFn (W : Nat) (f : Nat → Nat) (k : Nat) : (∀ (i : Nat), i < k → f i < 2 ^ W) → ∀ (i : Nat), i < k → field W (packFn W f k) i = f i

Reading back a field of a packed value.

theorem Hex.PermGroup.Kernel.field_ident {n W i : Nat} (hn : n < 2 ^ W) (hi : i < n) : field W (ident n W) i = i

theorem Hex.PermGroup.Kernel.field_comp (n W x y : Nat) {i : Nat} (hi : i < n) : field W (comp n W x y) i = field W x (field W y i)

theorem Hex.PermGroup.Kernel.field_pack {n : Nat} (p : Perm n) (i : Fin n) : field (width n) (pack p) ↑i = ↑(p.get i)