theorem Hex.PermGroup.Search.checkSearch_mathlib {n : ℕ} {G : Group n} {P : Predicate n} (C : Constraint G P) (K : Group n) (certificate : Certificate C.Reason) (h : checkSearch C K certificate = true) (e : Equiv.Perm (Fin n)) : e ∈ closure K.generators ↔ e ∈ closure G.generators ∧ P.test (Perm.ofEquiv e) = true

Accepted completeness certificates identify the mathematical subgroup by the same executable predicate used by the search.

theorem Hex.PermGroup.Search.Predicate.centralizer_spec {n : ℕ} (H : Group n) (p : Perm n) : (centralizer H).test p = true ↔ p.toEquiv ∈ Subgroup.centralizer ↑(closure H.generators)

theorem Hex.PermGroup.Group.centralizer_spec {n : ℕ} (G H : Group n) : closure (G.centralizer H).generators = closure G.generators ⊓ Subgroup.centralizer ↑(closure H.generators)

theorem Hex.PermGroup.Group.center_spec {n : ℕ} (G : Group n) : closure G.center.generators = closure G.generators ⊓ Subgroup.centralizer ↑(closure G.generators)

theorem Hex.PermGroup.Group.centralizerPerm_spec {n : ℕ} (G : Group n) (q : Perm n) : closure (G.centralizerPerm q).generators = closure G.generators ⊓ Subgroup.centralizer {q.toEquiv}

theorem Hex.PermGroup.Group.intersection_spec {n : ℕ} (G H : Group n) : closure (G.intersection H).generators = closure G.generators ⊓ closure H.generators

theorem Hex.PermGroup.Search.Predicate.normalizer_spec {n : ℕ} (H : Group n) (p : Perm n) : (normalizer H).test p = true ↔ p.toEquiv ∈ Subgroup.normalizer ↑(closure H.generators)

theorem Hex.PermGroup.Group.normalizer_spec {n : ℕ} (G H : Group n) : closure (G.normalizer H).generators = closure G.generators ⊓ Subgroup.normalizer ↑(closure H.generators)

theorem Hex.PermGroup.Search.Predicate.setStabilizer_spec {n : ℕ} (A : Vector Bool n) (p : Perm n) : (setStabilizer A).test p = true ↔ p.toEquiv ∈ MulAction.stabilizer (Equiv.Perm (Fin n)) {x : Fin n | A.get x = true}

theorem Hex.PermGroup.Group.setStabilizer_spec {n : ℕ} (G : Group n) (A : Vector Bool n) : closure (G.setStabilizer A).generators = closure G.generators ⊓ MulAction.stabilizer (Equiv.Perm (Fin n)) {x : Fin n | A.get x = true}

theorem Hex.PermGroup.Search.Sets.test_image {n : ℕ} (A B : Vector Bool n) (p : Perm n) : test A B p = true ↔ ⇑p.toEquiv '' {x : Fin n | A.get x = true} = {x : Fin n | B.get x = true}

theorem Hex.PermGroup.Group.setTransporter_spec {n : ℕ} (G : Group n) (A B : Vector Bool n) (p : Element G) (h : G.setTransporter? A B = some p) : ⇑(↑p).toEquiv '' {x : Fin n | A.get x = true} = {x : Fin n | B.get x = true}

theorem Hex.PermGroup.Group.setTransporter_none_spec {n : ℕ} (G : Group n) (A B : Vector Bool n) : G.setTransporter? A B = none ↔ ¬∃ e ∈ closure G.generators, ⇑e '' {x : Fin n | A.get x = true} = {x : Fin n | B.get x = true}

theorem Hex.PermGroup.Group.transporter_coset_spec {n : ℕ} (G : Group n) (A B : Vector Bool n) (t : Element G) (ht : (Action.subsets G).act t A = B) (e : Equiv.Perm (Fin n)) : (↑t).toEquiv⁻¹ * e ∈ closure (G.setStabilizer A).generators ↔ e ∈ closure G.generators ∧ ⇑e '' {x : Fin n | A.get x = true} = {x : Fin n | B.get x = true}