def Hex.PermGroup.Kernel.fixedPoint (fixed i : Nat) : Bool

Membership in the bitmask of fixed base points, with raw kernel operations.

Equations

• Hex.PermGroup.Kernel.fixedPoint fixed i = !((fixed.shiftRight i).land 1).beq 0

def Hex.PermGroup.Kernel.scan (fixed bound k : Nat) : Nat × Bool

Scan once for an unfixed point; a second unfixed point makes the verdict false.

Equations

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

def Hex.PermGroup.Kernel.fullLevel (n fixed : Nat) (L : Level) : Bool

Coverage and fixed-point checks for one certified orbit and transversal.

Equations

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

def Hex.PermGroup.Kernel.full (n fixed : Nat) : Certificate → Bool

Check that the certificate covers every permutation fixing the bitmask fixed. Each orbit covers its unfixed points, its transversal fixes fixed, and a single terminal scan leaves at most one point unfixed.

Equations

• Hex.PermGroup.Kernel.full n fixed [] = (Hex.PermGroup.Kernel.scan fixed n n).snd
• Hex.PermGroup.Kernel.full n fixed (L :: rest) = (Hex.PermGroup.Kernel.fullLevel n fixed L && Hex.PermGroup.Kernel.full n (fixed.lor (Nat.shiftLeft 1 L.base)) rest)

theorem Hex.PermGroup.Kernel.full_cons_of {n fixed : Nat} {L : Level} {rest : Certificate} (hL : fullLevel n fixed L = true) (hrest : full n (fixed.lor (Nat.shiftLeft 1 L.base)) rest = true) : full n fixed (L :: rest) = true

Assemble independently checked coverage levels.

theorem Hex.PermGroup.Kernel.all_of_check {n : Nat} {gs : List (Perm n)} {inputs : List Nat} {c : Certificate} (hS : List.map pack gs = inputs) (h : check n inputs c = true) (hf : full n 0 c = true) : GeneratesAll gs.toArray

A full accepted certificate proves that every permutation is generated.