structure Hex.PermGroup.Kernel.Level : Type

One level of a kernel certificate. orbit, reps, invs and parents are read at indices below size only.

• base : Nat

  The base point.

• size : Nat

  The number of orbit points.

• gens : List Nat

  The packed generators of this level.

• orbit : Lean.RArray Nat

  Orbit point j, with orbit.get 0 = base.

• reps : Lean.RArray Nat

  The packed transversal element mapping base to orbit point j.

• invs : Lean.RArray Nat

  The packed inverse of reps.get j.

• parents : Lean.RArray (Nat × Nat)

  For 0 < j, the Schreier-tree edge (i, k) with reps.get j = gens[i] * reps.get k.

• lookup : Nat

  Field x is j + 1 when x is orbit point j, and 0 off the orbit.

• next : List (List (Nat × Nat))

  For each generator of the next level, the Schreier-pair indices (i, j) of the Schreier generators whose product it is.

• inputWords : List (List Nat)

  At the first level only, for each generator, the indices of the inputs whose product it is. Ignored at later levels.

@[instance_reducible]

instance Hex.PermGroup.Kernel.instInhabitedLevel : Inhabited Level

Equations

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

@[reducible, inline]

abbrev Hex.PermGroup.Kernel.Certificate : Type

A kernel certificate: the nontrivial levels of a stabilizer chain.

Equations

• Hex.PermGroup.Kernel.Certificate = List Hex.PermGroup.Kernel.Level

def Hex.PermGroup.Kernel.gen (L : Level) (i : Nat) : Nat

Generator i of a level (0 out of range).

Equations

• Hex.PermGroup.Kernel.gen L i = L.gens.getD i 0

def Hex.PermGroup.Kernel.schreier (n W : Nat) (L : Level) (i j : Nat) : Nat

The Schreier generator t_k⁻¹ * s_i * t_j with t_k(base) = s_i(t_j(base)).

Equations

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

def Hex.PermGroup.Kernel.sift (n W e : Nat) : List Level → Nat → Bool

Sift a packed permutation through the levels, accepting as soon as the residual is e.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Kernel.sift n W e [] x✝ = x✝.beq e

def Hex.PermGroup.Kernel.pairsOk (n W e : Nat) (L : Level) (rest : List Level) (lo hi : Nat) : Bool

Items 3 and 5 of the SPEC's checker for the Schreier pairs p with lo ≤ p < hi, where pair p is generator p / size and orbit point p % size.

Equations

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

def Hex.PermGroup.Kernel.shapeOk (n W : Nat) (L : Level) : Bool

Item 1: the orbit and lookup table agree, and every point is below n.

Equations

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

def Hex.PermGroup.Kernel.transversalOk (n W e : Nat) (L : Level) : Bool

Item 4: the transversal follows its Schreier tree, and the stored inverses are inverses.

Equations

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

def Hex.PermGroup.Kernel.schreierProduct (n W e : Nat) (L : Level) : List (Nat × Nat) → Nat

The product of the Schreier generators at the given pairs, leftmost outermost; e for no pairs.

Equations

• Hex.PermGroup.Kernel.schreierProduct n W e L [] = e
• Hex.PermGroup.Kernel.schreierProduct n W e L (q :: qs) = Hex.PermGroup.Kernel.comp n W (Hex.PermGroup.Kernel.schreier n W L q.fst q.snd) (Hex.PermGroup.Kernel.schreierProduct n W e L qs)

def Hex.PermGroup.Kernel.nextOk (n W e : Nat) (L : Level) (nextGens : List Nat) : Bool

Item 6: each generator of the next level is the product of the Schreier generators at its recorded indices.

Equations

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

def Hex.PermGroup.Kernel.headGens : List Level → List Nat

The generators of the first of the given levels, or none.

Equations

• Hex.PermGroup.Kernel.headGens [] = []
• Hex.PermGroup.Kernel.headGens (L :: tail) = L.gens

def Hex.PermGroup.Kernel.levelOk (n W e : Nat) (L : Level) (rest : List Level) : Bool

Items 1, 4 and 6 for one level followed by rest. Generators need not be closed under inverses: in a finite group the inverse of a generator is one of its powers.

Equations

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

def Hex.PermGroup.Kernel.inputProduct (n W e : Nat) (inputs : List Nat) : List Nat → Nat

The product of the inputs at the given indices, leftmost outermost; e for no indices.

Equations

• Hex.PermGroup.Kernel.inputProduct n W e inputs [] = e
• Hex.PermGroup.Kernel.inputProduct n W e inputs (i :: is) = Hex.PermGroup.Kernel.comp n W (inputs.getD i e) (Hex.PermGroup.Kernel.inputProduct n W e inputs is)

def Hex.PermGroup.Kernel.inputsOk (n W e : Nat) (inputs : List Nat) (c : List Level) : Bool

Item 2 for the inputs: every input sifts through the certificate, and each first-level generator is the product of the inputs at its recorded indices.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Kernel.inputsOk n W e inputs [] = ((inputs.all fun (x : Nat) => Hex.PermGroup.Kernel.sift n W e [] x) && true)

def Hex.PermGroup.Kernel.levelsOk (n W e : Nat) : List Level → Bool

Every level checked, each against the levels after it.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Kernel.levelsOk n W e [] = true

def Hex.PermGroup.Kernel.check (n : Nat) (inputs : List Nat) (c : Certificate) : Bool

The complete kernel check of a certificate for packed inputs of degree n.

Equations

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

def Hex.PermGroup.Kernel.order (c : Certificate) : Nat

The order certified by c: the product of its orbit sizes.

Equations

• Hex.PermGroup.Kernel.order c = List.foldr (fun (L : Hex.PermGroup.Kernel.Level) (acc : Nat) => L.size.mul acc) 1 c

theorem Hex.PermGroup.Kernel.pairsOk_append (n W e : Nat) (L : Level) (rest : List Level) {lo mid hi : Nat} (h₁ : lo ≤ mid) (h₂ : mid ≤ hi) (ha : pairsOk n W e L rest lo mid = true) (hb : pairsOk n W e L rest mid hi = true) : pairsOk n W e L rest lo hi = true

theorem Hex.PermGroup.Kernel.pairsOk_nil (n W e : Nat) (L : Level) (rest : List Level) (k : Nat) : pairsOk n W e L rest k k = true