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

Inclusion of the represented permutation subgroups.

Equations

• H.IsSubgroup G = ∀ (p : Hex.Perm n), Hex.PermGroup.Generated H.generators p → Hex.PermGroup.Generated G.generators p

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

Containment needs only the original generators of the smaller group.

Equations

• H.isSubgroup G = decide (∀ (i : Fin H.generators.size), G.contains H.generators[↑i] = true)

theorem Hex.PermGroup.Group.isSubgroup_iff {n : Nat} (H G : Group n) : H.isSubgroup G = true ↔ H.IsSubgroup G

def Hex.PermGroup.Group.subgroupFailure? {n : Nat} (H G : Group n) : Option (Fin H.generators.size)

The first original generator whose complete sift disproves containment.

Equations

• H.subgroupFailure? G = List.find? (fun (i : Fin H.generators.size) => !G.contains H.generators[↑i]) (List.finRange H.generators.size)

theorem Hex.PermGroup.Group.subgroupFailure_none {n : Nat} (H G : Group n) : H.subgroupFailure? G = none ↔ H.isSubgroup G = true

theorem Hex.PermGroup.Group.subgroupFailure_sound {n : Nat} (H G : Group n) (i : Fin H.generators.size) (h : H.subgroupFailure? G = some i) : ¬Generated G.generators H.generators[↑i]

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

Equality of subgroups, independent of their presentations.

Equations

• G.sameGroup H = (G.isSubgroup H && H.isSubgroup G)

theorem Hex.PermGroup.Group.sameGroup_iff {n : Nat} (G H : Group n) : G.sameGroup H = true ↔ SameGroup G H

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

Concatenate the original generators and rebuild a complete chain.

Equations

• G.join H = Hex.PermGroup.Group.ofGenerators (G.generators ++ H.generators)

theorem Hex.PermGroup.Group.left_subgroup_join {n : Nat} (G H : Group n) : G.IsSubgroup (G.join H)

theorem Hex.PermGroup.Group.right_subgroup_join {n : Nat} (G H : Group n) : H.IsSubgroup (G.join H)

theorem Hex.PermGroup.Group.join_le {n : Nat} (G H K : Group n) : (G.join H).IsSubgroup K ↔ G.IsSubgroup K ∧ H.IsSubgroup K

def Hex.PermGroup.Group.working {n : Nat} (G : Group n) : Normalized G.generators

Normalize once for orbit operations; signed input references retain the connection to the group's original generator array.

Equations

• G.working = Hex.PermGroup.normalize G.generators

theorem Hex.PermGroup.Group.chain_symmetric {n : Nat} (G : Group n) (p : Perm n) (hp : p ∈ G.chain.generators) : p.inv ∈ G.chain.generators

The top working array already has checked symmetry and original-generator provenance; point-orbit replay need not normalize the input again.

theorem Hex.PermGroup.Group.chain_generated {n : Nat} (G : Group n) (p : Perm n) : Generated G.chain.generators p ↔ Generated G.generators p

def Hex.PermGroup.Group.orbitData {n : Nat} (G : Group n) (a : Fin n) : { c : Orbit n // Orbit.Valid G.chain.generators a c }

Equations

• G.orbitData a = Hex.PermGroup.Orbit.ofSymmetric G.chain.generators a ⋯

def Hex.PermGroup.Group.orbit {n : Nat} (G : Group n) (a : Fin n) : Array (Fin n)

Sorted point orbit, retaining fixed points. The discovery order remains in the certificate and is independent of this public serialization.

Equations

• G.orbit a = (List.filter (fun (x : Fin n) => (G.orbitData a).val.lookup[↑x].isSome) (List.finRange n)).toArray

theorem Hex.PermGroup.Group.mem_orbit {n : Nat} (G : Group n) (a x : Fin n) : x ∈ G.orbit a ↔ ∃ (p : Perm n), Generated G.generators p ∧ p.get a = x

theorem Hex.PermGroup.Group.orbit_sorted {n : Nat} (G : Group n) (a : Fin n) : List.Pairwise (fun (x y : Fin n) => ↑x < ↑y) (G.orbit a).toList

theorem Hex.PermGroup.Group.orbit_nodup {n : Nat} (G : Group n) (a : Fin n) : (G.orbit a).toList.Nodup

theorem Hex.PermGroup.Group.self_mem_orbit {n : Nat} (G : Group n) (a : Fin n) : a ∈ G.orbit a

theorem Hex.PermGroup.Group.orbit_eq {n : Nat} (G : Group n) (a b : Fin n) (hb : b ∈ G.orbit a) : G.orbit a = G.orbit b

def Hex.PermGroup.Group.orbitAt? {n : Nat} (G : Group n) (a : Fin n) : Option (Array (Fin n))

Retain an orbit at its least point. This gives a deterministic partition with both point arrays and the list of orbits sorted.

Equations

• G.orbitAt? a = if (G.orbit a)[0]? = some a then some (G.orbit a) else none

def Hex.PermGroup.Group.orbits {n : Nat} (G : Group n) : Array (Array (Fin n))

Equations

• G.orbits = (List.filterMap G.orbitAt? (List.finRange n)).toArray

theorem Hex.PermGroup.Group.orbit_mem_orbits {n : Nat} (G : Group n) (a : Fin n) : G.orbit a ∈ G.orbits

theorem Hex.PermGroup.Group.mem_orbits {n : Nat} (G : Group n) (points : Array (Fin n)) : points ∈ G.orbits ↔ ∃ (a : Fin n), points = G.orbit a

theorem Hex.PermGroup.Group.orbits_disjoint {n : Nat} (G : Group n) {xs ys : Array (Fin n)} (hx : xs ∈ G.orbits) (hy : ys ∈ G.orbits) (hne : xs ≠ ys) (x : Fin n) : x ∈ xs → ¬x ∈ ys

theorem Hex.PermGroup.Group.orbits_sorted {n : Nat} (G : Group n) : List.Pairwise (fun (xs ys : Array (Fin n)) => ∃ (a : Fin n), ∃ (b : Fin n), xs[0]? = some a ∧ ys[0]? = some b ∧ ↑a < ↑b) G.orbits.toList

theorem Hex.PermGroup.Group.orbits_cover {n : Nat} (G : Group n) (a : Fin n) : ∃ (points : Array (Fin n)), points ∈ G.orbits ∧ a ∈ points

theorem Hex.PermGroup.Group.orbits_nodup {n : Nat} (G : Group n) : G.orbits.toList.Nodup

def Hex.PermGroup.Group.transporter? {n : Nat} (G : Group n) (a b : Fin n) : Option (Element G)

A transporter is returned exactly when the target is in the point orbit.

Equations

• G.transporter? a b = match (G.orbitData a).val.lookup[↑b] with | none => none | some j => some ⟨(G.orbitData a).val.reps[↑j], ⋯⟩

theorem Hex.PermGroup.Group.transporter_image {n : Nat} (G : Group n) (a b : Fin n) (p : Element G) (h : G.transporter? a b = some p) : p.val.get a = b

theorem Hex.PermGroup.Group.transporter_isSome {n : Nat} (G : Group n) (a b : Fin n) : (G.transporter? a b).isSome = true ↔ b ∈ G.orbit a

theorem Hex.PermGroup.Group.transporter_none {n : Nat} (G : Group n) (a b : Fin n) : G.transporter? a b = none ↔ ¬∃ (p : Element G), p.val.get a = b

def Hex.PermGroup.Group.stabilizer {n : Nat} (G : Group n) (a : Fin n) : Group n

The full point stabilizer, generated by the Schreier generators of the point orbit that are not generated by earlier ones.

Equations

• G.stabilizer a = Hex.PermGroup.Group.ofGenerators (Hex.PermGroup.sieve (Hex.PermGroup.Orbit.stabilizerGens ⋯))

theorem Hex.PermGroup.Group.mem_stabilizer {n : Nat} (G : Group n) (a : Fin n) (p : Perm n) : Generated (G.stabilizer a).generators p ↔ Generated G.generators p ∧ p.get a = a

def Hex.PermGroup.Group.pointwise {n : Nat} (G : Group n) : List (Fin n) → Group n

Iterate full point stabilizers in the supplied order.

Equations

• G.pointwise [] = G
• G.pointwise (a :: points) = (G.stabilizer a).pointwise points

theorem Hex.PermGroup.Group.mem_pointwise {n : Nat} (G : Group n) (points : List (Fin n)) (p : Perm n) : Generated (G.pointwise points).generators p ↔ Generated G.generators p ∧ ∀ (a : Fin n), a ∈ points → p.get a = a

theorem Hex.PermGroup.Group.pointwise_same {n : Nat} (G : Group n) (xs ys : List (Fin n)) (h : ∀ (a : Fin n), a ∈ xs ↔ a ∈ ys) : SameGroup (G.pointwise xs) (G.pointwise ys)

Pointwise stabilizers depend on the listed point set, so reordering or repeating points leaves the represented subgroup unchanged.