def Hex.PermGroup.Kernel.Rep (n x : Nat) (σ : Perm n) : Prop

x represents σ: its field i is σ i for every i < n.

Equations

• Hex.PermGroup.Kernel.Rep n x σ = ∀ (i : Fin n), Hex.PermGroup.Kernel.field (Hex.PermGroup.Kernel.width n) x ↑i = ↑(σ.get i)

def Hex.PermGroup.Kernel.Canon (n x : Nat) : Prop

x is determined by its fields 0..n-1, as the output of packFn is.

Equations

• Hex.PermGroup.Kernel.Canon n x = (x = Hex.PermGroup.Kernel.packFn (Hex.PermGroup.Kernel.width n) (fun (i : Nat) => Hex.PermGroup.Kernel.field (Hex.PermGroup.Kernel.width n) x i) n)

theorem Hex.PermGroup.Kernel.packFn_congr (W : Nat) {f g : Nat → Nat} (k : Nat) : (∀ (i : Nat), i < k → f i = g i) → packFn W f k = packFn W g k

theorem Hex.PermGroup.Kernel.canon_packFn {n : Nat} (f : Nat → Nat) (hf : ∀ (i : Nat), i < n → f i < 2 ^ width n) : Canon n (packFn (width n) f n)

theorem Hex.PermGroup.Kernel.canon_comp {n : Nat} (x y : Nat) : Canon n (comp n (width n) x y)

theorem Hex.PermGroup.Kernel.canon_ident {n : Nat} : Canon n (ident n (width n))

theorem Hex.PermGroup.Kernel.canon_pack {n : Nat} (p : Perm n) : Canon n (pack p)

theorem Hex.PermGroup.Kernel.rep_pack {n : Nat} (p : Perm n) : Rep n (pack p) p

theorem Hex.PermGroup.Kernel.rep_ident {n : Nat} : Rep n (ident n (width n)) 1

theorem Hex.PermGroup.Kernel.rep_comp {n x y : Nat} {σ τ : Perm n} (hx : Rep n x σ) (hy : Rep n y τ) : Rep n (comp n (width n) x y) (σ * τ)

theorem Hex.PermGroup.Kernel.Rep.unique {n x : Nat} {σ τ : Perm n} (hσ : Rep n x σ) (hτ : Rep n x τ) : σ = τ

theorem Hex.PermGroup.Kernel.rep_inv {n x y : Nat} {τ : Perm n} (hy : Rep n y τ) (h : comp n (width n) x y = ident n (width n)) : Rep n x τ⁻¹

A value that composes on the right with a representative of τ to the identity represents τ⁻¹.

theorem Hex.PermGroup.Kernel.Canon.eq_of_rep {n x y : Nat} {σ : Perm n} (hx : Canon n x) (hy : Canon n y) (hxσ : Rep n x σ) (hyσ : Rep n y σ) : x = y

Two canonical values with the same representative are equal.

theorem Hex.PermGroup.Kernel.allRange_iff (k : Nat) (p : Nat → Bool) : Kernel.allRange k p = true ↔ ∀ (i : Nat), i < k → p i = true

theorem Hex.PermGroup.Kernel.shapeOk_iff {n : Nat} {L : Level} : shapeOk n (width n) L = true ↔ L.base < n ∧ 0 < L.size ∧ L.orbit.get 0 = L.base ∧ (∀ (j : Nat), j < L.size → L.orbit.get j < n ∧ field (width n) L.lookup (L.orbit.get j) = j + 1) ∧ ∀ (x : Nat), x < n → field (width n) L.lookup x = 0 ∨ field (width n) L.lookup x ≤ L.size ∧ L.orbit.get (field (width n) L.lookup x - 1) = x

theorem Hex.PermGroup.Kernel.transversalOk_iff {n : Nat} {L : Level} : transversalOk n (width n) (ident n (width n)) L = true ↔ L.reps.get 0 = ident n (width n) ∧ (∀ (j : Nat), j < L.size → j ≠ 0 → (L.parents.get j).fst < L.gens.length ∧ (L.parents.get j).snd < j ∧ field (width n) (gen L (L.parents.get j).fst) (L.orbit.get (L.parents.get j).snd) = L.orbit.get j ∧ L.reps.get j = comp n (width n) (gen L (L.parents.get j).fst) (L.reps.get (L.parents.get j).snd)) ∧ ∀ (j : Nat), j < L.size → comp n (width n) (L.invs.get j) (L.reps.get j) = ident n (width n)

theorem Hex.PermGroup.Kernel.pairsOk_iff {n : Nat} {L : Level} {rest : List Level} (lo hi : Nat) : pairsOk n (width n) (ident n (width n)) L rest lo hi = true ↔ ∀ (p : Nat), lo ≤ p → p < hi → field (width n) L.lookup (field (width n) (gen L (p / L.size)) (L.orbit.get (p % L.size))) ≠ 0 ∧ sift n (width n) (ident n (width n)) rest (schreier n (width n) L (p / L.size) (p % L.size)) = true

theorem Hex.PermGroup.Kernel.nextOk_iff {n : Nat} {L : Level} (nextGens : List Nat) : nextOk n (width n) (ident n (width n)) L nextGens = true ↔ L.next.length = nextGens.length ∧ ∀ (q : List (Nat × Nat) × Nat), q ∈ L.next.zip nextGens → (∀ (p : Nat × Nat), p ∈ q.fst → p.fst < L.gens.length ∧ p.snd < L.size) ∧ schreierProduct n (width n) (ident n (width n)) L q.fst = q.snd

def Hex.PermGroup.Kernel.genSet (n : Nat) (L : Level) : Perm n → Prop

The permutations represented by the generators of a level.

Equations

• Hex.PermGroup.Kernel.genSet n L σ = ∃ (s : Nat), s ∈ L.gens ∧ Hex.PermGroup.Kernel.Rep n s σ

def Hex.PermGroup.Kernel.levelGroup (n : Nat) (L : Level) : Perm n → Prop

The subgroup generated by a level's generators.

Equations

• Hex.PermGroup.Kernel.levelGroup n L = Hex.PermGroup.Kernel.Span (Hex.PermGroup.Kernel.genSet n L)

def Hex.PermGroup.Kernel.groupOf (n : Nat) : List Level → Perm n → Prop

The subgroup of the first of a list of levels, trivial for no levels.

Equations

• Hex.PermGroup.Kernel.groupOf n [] = Hex.PermGroup.Kernel.Span fun (x : Hex.Perm n) => False
• Hex.PermGroup.Kernel.groupOf n (L :: tail) = Hex.PermGroup.Kernel.levelGroup n L

theorem Hex.PermGroup.Kernel.inv_eq_pow {n : Nat} (σ : Perm n) : σ.inv = σ.pow (σ.order - 1)

The inverse of a permutation is one of its powers.

theorem Hex.PermGroup.Kernel.gen_eq_getElem {L : Level} {i : Nat} (hi : i < L.gens.length) : gen L i = L.gens[i]

theorem Hex.PermGroup.Kernel.gen_mem {L : Level} {i : Nat} (hi : i < L.gens.length) : gen L i ∈ L.gens

theorem Hex.PermGroup.Kernel.exists_gen_eq {L : Level} {s : Nat} (hs : s ∈ L.gens) : ∃ (i : Nat), i < L.gens.length ∧ gen L i = s

structure Hex.PermGroup.Kernel.LevelBase (n : Nat) (L : Level) (rest : List Level) : Prop

The checks of one level of an accepted certificate, and representatives for its generators.

• shape : shapeOk n (width n) L = true
• trans : transversalOk n (width n) (ident n (width n)) L = true
• next : nextOk n (width n) (ident n (width n)) L (headGens rest) = true
• pairs : pairsOk n (width n) (ident n (width n)) L rest 0 (L.gens.length * L.size) = true
• gens (s : Nat) : s ∈ L.gens → ∃ (σ : Perm n), Rep n s σ

theorem Hex.PermGroup.Kernel.LevelBase.base_lt {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) : L.base < n

theorem Hex.PermGroup.Kernel.LevelBase.size_pos {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) : 0 < L.size

theorem Hex.PermGroup.Kernel.LevelBase.orbit_zero {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) : L.orbit.get 0 = L.base

theorem Hex.PermGroup.Kernel.LevelBase.orbit_lt {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : L.orbit.get j < n

theorem Hex.PermGroup.Kernel.LevelBase.lookup_orbit {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : field (width n) L.lookup (L.orbit.get j) = j + 1

theorem Hex.PermGroup.Kernel.LevelBase.lookup_spec {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {x : Nat} (hx : x < n) (h0 : field (width n) L.lookup x ≠ 0) : field (width n) L.lookup x ≤ L.size ∧ L.orbit.get (field (width n) L.lookup x - 1) = x

def Hex.PermGroup.Kernel.LevelBase.Ω {n : Nat} {L : Level} {rest : List Level} : LevelBase n L rest → Fin n → Prop

The orbit as a set of points.

Equations

• x✝.Ω x = (Hex.PermGroup.Kernel.field (Hex.PermGroup.Kernel.width n) L.lookup ↑x ≠ 0)

def Hex.PermGroup.Kernel.LevelBase.pt {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) (j : Nat) (hj : j < L.size) : Fin n

The orbit point j.

Equations

• h.pt j hj = ⟨L.orbit.get j, ⋯⟩

def Hex.PermGroup.Kernel.LevelBase.idx {n : Nat} {L : Level} {rest : List Level} : LevelBase n L rest → (x : Fin n) → Nat

The orbit index of a point of the orbit.

Equations

• x✝.idx x = Hex.PermGroup.Kernel.field (Hex.PermGroup.Kernel.width n) L.lookup ↑x - 1

theorem Hex.PermGroup.Kernel.LevelBase.idx_lt {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {x : Fin n} (hx : h.Ω x) : h.idx x < L.size

theorem Hex.PermGroup.Kernel.LevelBase.pt_idx {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {x : Fin n} (hx : h.Ω x) : h.pt (h.idx x) ⋯ = x

theorem Hex.PermGroup.Kernel.LevelBase.pt_mem {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : h.Ω (h.pt j hj)

theorem Hex.PermGroup.Kernel.LevelBase.idx_pt {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : h.idx (h.pt j hj) = j

theorem Hex.PermGroup.Kernel.LevelBase.pt_zero {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) : h.pt 0 ⋯ = ⟨L.base, ⋯⟩

theorem Hex.PermGroup.Kernel.LevelBase.pair_facts {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {i j : Nat} (hi : i < L.gens.length) (hj : j < L.size) : field (width n) L.lookup (field (width n) (gen L i) (L.orbit.get j)) ≠ 0 ∧ sift n (width n) (ident n (width n)) rest (schreier n (width n) L i j) = true

The facts checked for one Schreier pair.

theorem Hex.PermGroup.Kernel.LevelBase.gen_maps {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {σ : Perm n} (hσ : genSet n L σ) {x : Fin n} (hx : h.Ω x) : h.Ω (σ.get x)

theorem Hex.PermGroup.Kernel.LevelBase.pow_maps {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {σ : Perm n} (hσ : genSet n L σ) (k : Nat) (x : Fin n) : h.Ω x → h.Ω ((σ.pow k).get x)

theorem Hex.PermGroup.Kernel.LevelBase.group_maps {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {σ : Perm n} (hσ : levelGroup n L σ) (x : Fin n) : h.Ω x → h.Ω (σ.get x)

theorem Hex.PermGroup.Kernel.LevelBase.trans_exists {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) (j : Nat) (hj : j < L.size) : ∃ (τ : Perm n), levelGroup n L τ ∧ Rep n (L.reps.get j) τ ∧ τ.get ⟨L.base, ⋯⟩ = h.pt j hj

noncomputable def Hex.PermGroup.Kernel.LevelBase.tr {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) (j : Nat) : Perm n

The transversal element for orbit point j.

Equations

• h.tr j = if hj : j < L.size then Classical.choose ⋯ else 1

theorem Hex.PermGroup.Kernel.LevelBase.tr_spec {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : levelGroup n L (h.tr j) ∧ Rep n (L.reps.get j) (h.tr j) ∧ (h.tr j).get ⟨L.base, ⋯⟩ = h.pt j hj

theorem Hex.PermGroup.Kernel.LevelBase.tr_mem {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : levelGroup n L (h.tr j)

theorem Hex.PermGroup.Kernel.LevelBase.tr_apply {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : (h.tr j).get ⟨L.base, ⋯⟩ = h.pt j hj

theorem Hex.PermGroup.Kernel.LevelBase.rep_reps {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : Rep n (L.reps.get j) (h.tr j)

theorem Hex.PermGroup.Kernel.LevelBase.rep_invs {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {j : Nat} (hj : j < L.size) : Rep n (L.invs.get j) (h.tr j)⁻¹

theorem Hex.PermGroup.Kernel.LevelBase.tr_zero {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) : h.tr 0 = 1

theorem Hex.PermGroup.Kernel.LevelBase.rep_gen {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {i : Nat} (hi : i < L.gens.length) : ∃ (σ : Perm n), Rep n (gen L i) σ

The permutation represented by generator i.

noncomputable def Hex.PermGroup.Kernel.LevelBase.schreierElt {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) (σ : Perm n) (j : Nat) (hj : j < L.size) : Perm n

The Schreier element of σ at orbit point j.

Equations

• h.schreierElt σ j hj = (h.tr (h.idx (σ.get (h.pt j hj))))⁻¹ * σ * h.tr j

theorem Hex.PermGroup.Kernel.LevelBase.rep_schreier {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {i j : Nat} (hi : i < L.gens.length) (hj : j < L.size) {σ : Perm n} (hσ : Rep n (gen L i) σ) : Rep n (schreier n (width n) L i j) (h.schreierElt σ j hj)

theorem Hex.PermGroup.Kernel.LevelBase.schreierElt_fixes {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {σ : Perm n} (hσ : ∀ (x : Fin n), h.Ω x → h.Ω (σ.get x)) {j : Nat} (hj : j < L.size) : (h.schreierElt σ j hj).get ⟨L.base, ⋯⟩ = ⟨L.base, ⋯⟩

theorem Hex.PermGroup.Kernel.LevelBase.schreierElt_mem {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {σ : Perm n} (hσ : levelGroup n L σ) {j : Nat} (hj : j < L.size) : levelGroup n L (h.schreierElt σ j hj)

theorem Hex.PermGroup.Kernel.LevelBase.schreierProduct_spec {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) (qs : List (Nat × Nat)) : (∀ (p : Nat × Nat), p ∈ qs → p.fst < L.gens.length ∧ p.snd < L.size) → ∃ (τ : Perm n), Rep n (schreierProduct n (width n) (ident n (width n)) L qs) τ ∧ levelGroup n L τ ∧ τ.get ⟨L.base, ⋯⟩ = ⟨L.base, ⋯⟩

A product of Schreier generators of this level fixes the base point and lies in the level's group.

theorem Hex.PermGroup.Kernel.LevelBase.next_gens {n : Nat} {L : Level} {rest : List Level} (h : LevelBase n L rest) {L' : Level} {rest' : List Level} (hrest : rest = L' :: rest') {t : Nat} (ht : t ∈ L'.gens) : ∃ (τ : Perm n), Rep n t τ ∧ levelGroup n L τ ∧ τ.get ⟨L.base, ⋯⟩ = ⟨L.base, ⋯⟩

The next level's generators are products of Schreier elements of this level.

structure Hex.PermGroup.Kernel.LevelHyp (n : Nat) (L : Level) (rest : List Level) extends Hex.PermGroup.Kernel.LevelBase n L rest : Prop

The checks of one level together with the soundness of sifting through the levels after it.

• shape : shapeOk n (width n) L = true
• trans : transversalOk n (width n) (ident n (width n)) L = true
• next : nextOk n (width n) (ident n (width n)) L (headGens rest) = true
• pairs : pairsOk n (width n) (ident n (width n)) L rest 0 (L.gens.length * L.size) = true
• gens (s : Nat) : s ∈ L.gens → ∃ (σ : Perm n), Rep n s σ
• sift (x : Nat) (σ : Perm n) : Rep n x σ → Canon n x → (Kernel.sift n (width n) (ident n (width n)) rest x = true ↔ groupOf n rest σ)

theorem Hex.PermGroup.Kernel.LevelHyp.gen_schreier_mem {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {σ : Perm n} (hσ : genSet n L σ) {j : Nat} (hj : j < L.size) : groupOf n rest (⋯.schreierElt σ j hj)

theorem Hex.PermGroup.Kernel.LevelHyp.schreier_step {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {a b : Perm n} (ha : genSet n L a) (hb : levelGroup n L b) (ih : ∀ (j : Nat) (hj : j < L.size), groupOf n rest (⋯.schreierElt b j hj)) (j : Nat) (hj : j < L.size) : groupOf n rest (⋯.schreierElt (a.comp b) j hj)

One generator step of Schreier's lemma.

theorem Hex.PermGroup.Kernel.LevelHyp.schreier_pow {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {a b : Perm n} (ha : genSet n L a) (hb : levelGroup n L b) (ih : ∀ (j : Nat) (hj : j < L.size), groupOf n rest (⋯.schreierElt b j hj)) (k : Nat) : levelGroup n L ((a.pow k).comp b) ∧ ∀ (j : Nat) (hj : j < L.size), groupOf n rest (⋯.schreierElt ((a.pow k).comp b) j hj)

theorem Hex.PermGroup.Kernel.LevelHyp.schreier_mem {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {σ : Perm n} (hσ : levelGroup n L σ) (j : Nat) (hj : j < L.size) : groupOf n rest (⋯.schreierElt σ j hj)

Schreier's lemma for the certified transversal.

theorem Hex.PermGroup.Kernel.LevelHyp.mem_rest_of_fixes {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {σ : Perm n} (hσ : levelGroup n L σ) (hb : σ.get ⟨L.base, ⋯⟩ = ⟨L.base, ⋯⟩) : groupOf n rest σ

theorem Hex.PermGroup.Kernel.LevelHyp.rest_le {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {σ : Perm n} (hσ : groupOf n rest σ) : levelGroup n L σ ∧ σ.get ⟨L.base, ⋯⟩ = ⟨L.base, ⋯⟩

theorem Hex.PermGroup.Kernel.LevelHyp.mem_rest_iff {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {σ : Perm n} : groupOf n rest σ ↔ levelGroup n L σ ∧ σ.get ⟨L.base, ⋯⟩ = ⟨L.base, ⋯⟩

theorem Hex.PermGroup.Kernel.LevelHyp.base_mem {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) : ⋯.Ω ⟨L.base, ⋯⟩

theorem Hex.PermGroup.Kernel.LevelHyp.sift_iff {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) {x : Nat} {σ : Perm n} (hx : Rep n x σ) : Kernel.sift n (width n) (ident n (width n)) (L :: rest) x = true ↔ levelGroup n L σ

Sifting from this level accepts exactly the packings of its subgroup.

noncomputable def Hex.PermGroup.Kernel.LevelHyp.decompose {n : Nat} {L : Level} {rest : List Level} (h : LevelHyp n L rest) : Bijection { p : Perm n // levelGroup n L p } (Fin L.size × { p : Perm n // groupOf n rest p })

The certified transversal decomposes each generated permutation uniquely into its orbit index and a permutation in the point stabilizer.

Equations

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

theorem Hex.PermGroup.Kernel.levelsOk_cons {n : Nat} {L : Level} {rest : List Level} : levelsOk n (width n) (ident n (width n)) (L :: rest) = true ↔ (shapeOk n (width n) L = true ∧ transversalOk n (width n) (ident n (width n)) L = true ∧ nextOk n (width n) (ident n (width n)) L (headGens rest) = true) ∧ pairsOk n (width n) (ident n (width n)) L rest 0 (L.gens.length * L.size) = true ∧ levelsOk n (width n) (ident n (width n)) rest = true

theorem Hex.PermGroup.Kernel.order_cons (L : Level) (rest : List Level) : order (L :: rest) = L.size * order rest

theorem Hex.PermGroup.Kernel.levels_sound {n : Nat} (ls : List Level) : levelsOk n (width n) (ident n (width n)) ls = true → (∀ (s : Nat), s ∈ headGens ls → ∃ (σ : Perm n), Rep n s σ) → (∀ (x : Nat) (σ : Perm n), Rep n x σ → Canon n x → (sift n (width n) (ident n (width n)) ls x = true ↔ groupOf n ls σ)) ∧ Nonempty (Bijection { p : Perm n // groupOf n ls p } (Fin (order ls)))

Soundness of sifting and the mixed-radix enumeration, from the last level upward.

theorem Hex.PermGroup.Kernel.check_iff {n : Nat} (inputs : List Nat) (c : Certificate) : check n inputs c = true ↔ inputsOk n (width n) (ident n (width n)) inputs c = true ∧ levelsOk n (width n) (ident n (width n)) c = true

theorem Hex.PermGroup.Kernel.inputProduct_rep {n : Nat} {S : Array (Perm n)} (w : List Nat) : (∀ (i : Nat), i ∈ w → i < S.size) → ∃ (σ : Perm n), Rep n (inputProduct n (width n) (ident n (width n)) (List.map pack S.toList) w) σ ∧ Generated S σ

theorem Hex.PermGroup.Kernel.input_reps {n : Nat} {S : Array (Perm n)} {c : Certificate} (hin : inputsOk n (width n) (ident n (width n)) (List.map pack S.toList) c = true) (s : Nat) : s ∈ headGens c → ∃ (σ : Perm n), Rep n s σ ∧ Generated S σ

Every first-level generator of an accepted certificate is a product of inputs.

theorem Hex.PermGroup.Kernel.groupOf_iff_generated {n : Nat} {S : Array (Perm n)} {c : Certificate} (h : check n (List.map pack S.toList) c = true) (p : Perm n) : groupOf n c p ↔ Generated S p

The first level of an accepted certificate generates exactly the inputs.

theorem Hex.PermGroup.Kernel.sift_pack_iff {n : Nat} {S : Array (Perm n)} {c : Certificate} (h : check n (List.map pack S.toList) c = true) (p : Perm n) : sift n (width n) (ident n (width n)) c (pack p) = true ↔ Generated S p

An accepted certificate decides generation for every Hex permutation.

theorem Hex.PermGroup.Kernel.order_of_check {n : Nat} {S : Array (Perm n)} {c : Certificate} (h : check n (List.map pack S.toList) c = true) : HasOrder S (order c)

An accepted certificate enumerates exactly the generated permutations.