theorem Hex.PermGroup.Search.Node.symmetric {n : Nat} {G : Group n} (t : Node G) (p : Perm n) (hp : p ∈ t.suffix.generators) : p.inv ∈ t.suffix.generators

def Hex.PermGroup.Search.Node.orbit {n : Nat} {G : Group n} (t : Node G) (x : Fin n) : Array (Fin n)

A remaining point orbit is computed directly from the suffix generators; there is no need to rebuild a group or enumerate its elements.

Equations

• t.orbit x = (Hex.PermGroup.Orbit.ofSymmetric t.suffix.generators x ⋯).val.points

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

def Hex.PermGroup.Search.Node.imagePossible {n : Nat} {G : Group n} (t : Node G) (x y : Fin n) : Bool

A forced image is feasible exactly when it belongs to the prefix image of the relevant suffix orbit.

Equations

• t.imagePossible x y = decide (t.rep.val.inv.get y ∈ t.orbit x)

theorem Hex.PermGroup.Search.Node.imagePossible_iff {n : Nat} {G : Group n} (t : Node G) (x y : Fin n) : t.imagePossible x y = true ↔ ∃ (p : Perm n), t.Contains p ∧ p.get x = y

theorem Hex.PermGroup.Search.Node.imagePossible_of_contains {n : Nat} {G : Group n} (t : Node G) {p : Perm n} (hp : t.Contains p) (x : Fin n) : t.imagePossible x (p.get x) = true

theorem Hex.PermGroup.Search.Node.orbit_invariant {n : Nat} {G : Group n} (t : Node G) {q : Perm n} (hq : Generated t.suffix.generators q) (x y : Fin n) : y ∈ t.orbit x ↔ q.get y ∈ t.orbit x

theorem Hex.PermGroup.Search.Node.orbit_perm {n : Nat} {G : Group n} (t : Node G) {q : Perm n} (hq : Generated t.suffix.generators q) (x : Fin n) : (List.map q.get (t.orbit x).toList).Perm (t.orbit x).toList

Suffix elements permute each remaining point orbit, so any membership count on such an orbit is preserved by reindexing along a completion.