def Hex.PermGroup.sieveStep {n : Nat} (s : (T : Array (Perm n)) × Construction T 0) (p : Perm n) : (T : Array (Perm n)) × Construction T 0

Keep p unless the complete chain for the generators kept so far already accepts it; a kept generator extends the chain.

Equations

• Hex.PermGroup.sieveStep s p = if s.snd.chain.accepts 0 p = true then s else ⟨s.fst.push p, Hex.PermGroup.Build.extend 0 ⋯ s.fst s.snd p ⋯⟩

def Hex.PermGroup.sieve {n : Nat} (S : Array (Perm n)) : Array (Perm n)

The generators of S, in order, omitting each one generated by those kept before it. The result generates the same group. Each kept generator at least doubles the group generated so far, so at most log₂ of its order are kept.

Equations

• Hex.PermGroup.sieve S = (Array.foldl Hex.PermGroup.sieveStep ⟨#[], Hex.PermGroup.Build.empty 0 ⋯⟩ S).fst

theorem Hex.PermGroup.generated_sieve {n : Nat} (S : Array (Perm n)) (p : Perm n) : Generated (sieve S) p ↔ Generated S p