theorem Hex.PermGroup.Search.Normalizer.orbit_image {n : Nat} (H : Group n) (p : Perm n) (hp : (Predicate.normalizer H).test p = true) (x y : Fin n) : y ∈ H.orbit x ↔ p.get y ∈ H.orbit (p.get x)

theorem Hex.PermGroup.Search.Normalizer.orbit_size {n : Nat} (H : Group n) (p : Perm n) (hp : (Predicate.normalizer H).test p = true) (x : Fin n) : (H.orbit x).size = (H.orbit (p.get x)).size

inductive Hex.PermGroup.Search.Normalizer.Reason (n : Nat) : Type

Orbit cardinalities and the equivalence relation are invariants, while individual orbits are allowed to be permuted.

• size {n : Nat} (x : Fin n) : Reason n
• relation {n : Nat} (x y : Fin n) : Reason n

def Hex.PermGroup.Search.Normalizer.reject {n : Nat} {G : Group n} (H : Group n) (t : Node G) : Reason n → Bool

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.Normalizer.reject H t (Hex.PermGroup.Search.Normalizer.Reason.size x_1) = (decide (↑x_1 < t.base) && decide ((H.orbit x_1).size ≠ (H.orbit (t.rep.val.get x_1)).size))

theorem Hex.PermGroup.Search.Normalizer.reject_sound {n : Nat} {G : Group n} (H : Group n) (t : Node G) (r : Reason n) (hr : reject H t r = true) (p : Perm n) (hp : t.Contains p) : (Predicate.normalizer H).test p = false

def Hex.PermGroup.Search.Normalizer.constraint {n : Nat} (G H : Group n) : Constraint G (Predicate.normalizer H)

Equations

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

def Hex.PermGroup.Group.normalizerSearch {n : Nat} (G H : Group n) : Search.Solution (Search.Normalizer.constraint G H)

Equations

• G.normalizerSearch H = Hex.PermGroup.Search.solve (Hex.PermGroup.Search.Normalizer.constraint G H)

def Hex.PermGroup.Group.normalizer {n : Nat} (G H : Group n) : Group n

Exact normalization requires the leaf conjugation test as well as the sound orbit refinements used to exclude partial prefixes.

Equations

• G.normalizer H = (G.normalizerSearch H).group

theorem Hex.PermGroup.Group.mem_normalizer {n : Nat} (G H : Group n) (p : Perm n) : Generated (G.normalizer H).generators p ↔ Generated G.generators p ∧ ∀ (q : Perm n), Generated H.generators q ↔ Generated H.generators (p.conj q)