structure Hex.PermGroup.Search.Transporter {n : Nat} (H : Group n) (target : Perm n) (points : List (Fin n)) : Type

A simultaneous point transporter and the full stabilizer of all points already assigned. The extending permutations form its represented coset.

• rep : Element H
• agrees (x : Fin n) : x ∈ points → self.rep.val.get x = target.get x
• group : Group n
• stabilizer (q : Perm n) : Generated self.group.generators q ↔ Generated H.generators q ∧ ∀ (x : Fin n), x ∈ points → q.get x = x

theorem Hex.PermGroup.Search.Transporter.contains_iff {n : Nat} {H : Group n} {target : Perm n} {points : List (Fin n)} (t : Transporter H target points) (q : Perm n) : Generated t.group.generators (t.rep.val.inv.comp q) ↔ Generated H.generators q ∧ ∀ (x : Fin n), x ∈ points → q.get x = target.get x

The maintained coset contains exactly the permutations extending the assigned images, including all simultaneous constraints.

def Hex.PermGroup.Search.Transporter.empty {n : Nat} (H : Group n) (target : Perm n) : Transporter H target []

Equations

• Hex.PermGroup.Search.Transporter.empty H target = { rep := Hex.PermGroup.Element.id H, agrees := ⋯, group := H, stabilizer := ⋯ }

def Hex.PermGroup.Search.Transporter.extend {n : Nat} {H : Group n} {target : Perm n} {points : List (Fin n)} (t : Transporter H target points) (x : Fin n) (k : Element t.group) (hk : k.val.get x = t.rep.val.inv.get (target.get x)) : Transporter H target (x :: points)

Extend one point using a transporter in the current full point stabilizer, then replace that stabilizer by its stabilizer of the new source point.

Equations

• t.extend x k hk = { rep := t.rep.comp ⟨k.val, ⋯⟩, agrees := ⋯, group := t.group.stabilizer x, stabilizer := ⋯ }

theorem Hex.PermGroup.Search.Transporter.cannot_extend {n : Nat} {H : Group n} {target : Perm n} {points : List (Fin n)} (t : Transporter H target points) (x : Fin n) (h : t.group.transporter? x (t.rep.val.inv.get (target.get x)) = none) : ¬∃ (q : Element H), ∀ (y : Fin n), y ∈ x :: points → q.val.get y = target.get y

inductive Hex.PermGroup.Search.TransportResult {n : Nat} (H : Group n) (target : Perm n) (points : List (Fin n)) : Type

Failure of simultaneous extension is justified by a failed orbit test, not by a bound on the amount of search performed.

• found {n : Nat} {H : Group n} {target : Perm n} {points : List (Fin n)} (transporter : Transporter H target points) : TransportResult H target points
• impossible {n : Nat} {H : Group n} {target : Perm n} {points : List (Fin n)} (proof : ¬∃ (q : Element H), ∀ (x : Fin n), x ∈ points → q.val.get x = target.get x) : TransportResult H target points

def Hex.PermGroup.Search.TransportResult.failed {n : Nat} {H : Group n} {target : Perm n} {points : List (Fin n)} : TransportResult H target points → Bool

Equations

• (Hex.PermGroup.Search.TransportResult.found transporter).failed = false
• (Hex.PermGroup.Search.TransportResult.impossible proof).failed = true

theorem Hex.PermGroup.Search.TransportResult.failed_iff {n : Nat} {H : Group n} {target : Perm n} {points : List (Fin n)} (r : TransportResult H target points) : r.failed = true ↔ ¬∃ (q : Element H), ∀ (x : Fin n), x ∈ points → q.val.get x = target.get x

def Hex.PermGroup.Search.transport {n : Nat} (H : Group n) (target : Perm n) (points : List (Fin n)) : TransportResult H target points

Build a transporter coset by successive point stabilizers. Points are processed from the list's end, so callers storing prefixes in reverse order extend them in natural source-point order.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Search.transport H target [] = Hex.PermGroup.Search.TransportResult.found (Hex.PermGroup.Search.Transporter.empty H target)