structure Hex.PermGroup.Orbit (n : Nat) : Type

Raw orbit certificate. Shape indices are checked when decoding the arrays; mathematical validity is established independently by checkOrbit.

• points : Array (Fin n)
• lookup : Vector (Option (Fin self.points.size)) n
• reps : Vector (Perm n) self.points.size
• words : Vector Program self.points.size
• invs : Vector (Perm n) self.points.size

  The inverse of each representative, computed once so that compiled sifting never inverts.

• invs_eq (j : Fin self.points.size) : self.invs[↑j] = self.reps[↑j].inv
• idReps : Vector Bool self.points.size

  Which representatives are the identity, so that compiled sifting can skip multiplying by them.

• idReps_eq (j : Fin self.points.size) : self.idReps[↑j] = true → self.reps[↑j] = Perm.id n

def Hex.PermGroup.Orbit.Valid {n : Nat} (S : Array (Perm n)) (a : Fin n) (c : Orbit n) : Prop

Finite checks for both reachability and closure. Closure includes inverse input generators, so the check accepts arbitrary original generator arrays.

Equations

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

@[instance_reducible]

instance Hex.PermGroup.Orbit.instDecidableValid {n : Nat} (S : Array (Perm n)) (a : Fin n) (c : Orbit n) : Decidable (Valid S a c)

Equations

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

theorem Hex.PermGroup.Orbit.Valid.invariant {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {p : Perm n} (hp : Generated S p) (x : Fin n) : x ∈ c.points ↔ p.get x ∈ c.points

Generator closure implies invariance under every generated permutation.

theorem Hex.PermGroup.Orbit.Valid.mem_iff {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (x : Fin n) : x ∈ c.points ↔ ∃ (p : Perm n), Generated S p ∧ p.get a = x

Reachability and closure together identify the full orbit.

def Hex.PermGroup.checkOrbit {n : Nat} (S : Array (Perm n)) (a : Fin n) (c : Orbit n) : Bool

Independently check a complete point orbit and its transporters.

Equations

• Hex.PermGroup.checkOrbit S a c = decide (Hex.PermGroup.Orbit.Valid S a c)

theorem Hex.PermGroup.checkOrbit_sound {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : checkOrbit S a c = true) (x : Fin n) : x ∈ c.points ↔ ∃ (p : Perm n), Generated S p ∧ p.get a = x