structure Hex.PermGroup.Action.Orbit {n : Nat} (G : Group n) (α : Type u) : Type u

An action orbit certificate retains transporters and their programs in the original permutation generators. The objects need not have a faithful action.

• objects : Array α
• reps : Vector (Element G) self.objects.size
• words : Vector Program self.objects.size

def Hex.PermGroup.Action.Orbit.Valid {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (x : α) (c : Orbit G α) : Prop

Reachability, identity at the base, and closure under signed generators. Only a complete certificate can justify a negative transporter answer.

Equations

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

@[instance_reducible]

instance Hex.PermGroup.Action.Orbit.instDecidableValid {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (x : α) (c : Orbit G α) : Decidable (Valid a x c)

Equations

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

theorem Hex.PermGroup.Action.Orbit.mem_iff {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (y : α) : y ∈ c.objects ↔ ∃ (p : Element G), a.act p x = y

@[simp]

theorem Hex.PermGroup.Action.Orbit.rep_apply {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (i : Fin c.objects.size) : a.act c.reps[↑i] x = c.objects[↑i]

def Hex.PermGroup.Action.Orbit.transporter? {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (_valid : Valid a x c) (y : α) : Option (Element G)

Read the stored representative only after establishing domain membership.

Equations

• Hex.PermGroup.Action.Orbit.transporter? _valid y = if hy : y ∈ c.objects then some c.reps[↑(Hex.PermGroup.Action.Domain.index y hy)] else none

theorem Hex.PermGroup.Action.Orbit.transporter_isSome {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (y : α) : (transporter? h y).isSome = true ↔ ∃ (p : Element G), a.act p x = y

theorem Hex.PermGroup.Action.Orbit.transporter_sound {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (y : α) (p : Element G) (hp : transporter? h y = some p) : a.act p x = y

def Hex.PermGroup.Action.checkOrbit {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (x : α) (c : Orbit G α) : Bool

Replay reachability programs and signed generator closure on action objects.

Equations

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

theorem Hex.PermGroup.Action.checkOrbit_sound {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : a.checkOrbit x c = true) (y : α) : y ∈ c.objects ↔ ∃ (p : Element G), a.act p x = y