theorem Hex.PermGroup.Kernel.sift_mem_iff {n : ℕ} {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 ↔ p.toEquiv ∈ closure S

An accepted certificate decides membership in Mathlib's closure.

theorem Hex.PermGroup.Kernel.card_closure {n : ℕ} {S : Array (Perm n)} {c : Certificate} (h : check n (List.map pack S.toList) c = true) : Nat.card ↥(closure S) = order c

An accepted certificate gives the cardinality of Mathlib's closure.

theorem Hex.PermGroup.Kernel.pack_ofEquiv_permOfImages {n : ℕ} {l : List ℕ} (h : imagesOk n l = true) : pack (Perm.ofEquiv (permOfImages n l)) = packList n l

def Hex.PermGroup.Kernel.images (n : ℕ) (g : Equiv.Perm (Fin n)) : List ℕ

The image-list API retained for certificate sources produced by earlier releases.

Equations

• Hex.PermGroup.Kernel.images n g = List.map (fun (i : Fin n) => ↑(g i)) (List.finRange n)

theorem Hex.PermGroup.Kernel.eq_top_of_hasOrder {n : ℕ} {gs : List (Equiv.Perm (Fin n))} (h : HasOrder (List.map Perm.ofEquiv gs).toArray n.factorial) : Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs} = ⊤

theorem Hex.PermGroup.Kernel.map_pack_nil {n : ℕ} : List.map pack (List.map Perm.ofEquiv []) = []

theorem Hex.PermGroup.Kernel.map_pack_cons {n : ℕ} {g : Equiv.Perm (Fin n)} {gs : List (Equiv.Perm (Fin n))} {x : ℕ} {xs : List ℕ} (h : pack (Perm.ofEquiv g) = x) (t : List.map pack (List.map Perm.ofEquiv gs) = xs) : List.map pack (List.map Perm.ofEquiv (g :: gs)) = x :: xs

theorem Hex.PermGroup.Kernel.check_gs {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {inputs : List ℕ} {c : Certificate} (hS : List.map pack (List.map Perm.ofEquiv gs) = inputs) (h : check n inputs c = true) : check n (List.map pack (List.map Perm.ofEquiv gs).toArray.toList) c = true

theorem Hex.PermGroup.Kernel.card_of_check {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {inputs : List ℕ} {c : Certificate} {N : ℕ} (hS : List.map pack (List.map Perm.ofEquiv gs) = inputs) (h : check n inputs c = true) (hN : order c = N) : Nat.card ↥(Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs}) = N

theorem Hex.PermGroup.Kernel.mem_of_check {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {inputs : List ℕ} {c : Certificate} {g : Equiv.Perm (Fin n)} {x : ℕ} (hS : List.map pack (List.map Perm.ofEquiv gs) = inputs) (h : check n inputs c = true) (hx : pack (Perm.ofEquiv g) = x) (hs : sift n (width n) (ident n (width n)) c x = true) : g ∈ Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs}

theorem Hex.PermGroup.Kernel.not_mem_of_check {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {inputs : List ℕ} {c : Certificate} {g : Equiv.Perm (Fin n)} {x : ℕ} (hS : List.map pack (List.map Perm.ofEquiv gs) = inputs) (h : check n inputs c = true) (hx : pack (Perm.ofEquiv g) = x) (hs : sift n (width n) (ident n (width n)) c x = false) : g ∉ Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs}

theorem Hex.PermGroup.Kernel.eq_top_of_check {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {inputs : List ℕ} {c : Certificate} (hS : List.map pack (List.map Perm.ofEquiv gs) = inputs) (h : check n inputs c = true) (hN : order c = n.factorial) : Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs} = ⊤