def Hex.PermGroup.Search.Node.assigned {n : Nat} {G : Group n} (t : Node G) : List (Fin n)

Assigned source points are stored in reverse order for successive transporter extension from point zero upward.

Equations

• t.assigned = (List.filter (fun (x : Fin n) => decide (↑x < t.base)) (List.finRange n)).reverse

theorem Hex.PermGroup.Search.Node.mem_assigned {n : Nat} {G : Group n} (t : Node G) (x : Fin n) : x ∈ t.assigned ↔ ↑x < t.base

def Hex.PermGroup.Search.Intersection.reject {n : Nat} {G : Group n} (H : Group n) (t : Node G) : Bool

A failed simultaneous transporter in H excludes every completion of the prefix. Individual point-orbit membership would not establish this.

Equations

• Hex.PermGroup.Search.Intersection.reject H t = (Hex.PermGroup.Search.transport H t.rep.val t.assigned).failed

theorem Hex.PermGroup.Search.Intersection.reject_sound {n : Nat} {G : Group n} (H : Group n) (t : Node G) (h : reject H t = true) (p : Perm n) (hp : t.Contains p) : (Predicate.subgroup H).test p = false

def Hex.PermGroup.Search.Intersection.constraint {n : Nat} (G H : Group n) : Constraint G (Predicate.subgroup H)

The replay repeats the successive stabilizer and orbit tests in H.

Equations

• Hex.PermGroup.Search.Intersection.constraint G H = Hex.PermGroup.Search.Constraint.ofTest (Hex.PermGroup.Search.Intersection.reject H) ⋯

def Hex.PermGroup.Group.intersectionSearch {n : Nat} (G H : Group n) : Search.Solution (Search.Intersection.constraint G H)

Equations

• G.intersectionSearch H = Hex.PermGroup.Search.solve (Hex.PermGroup.Search.Intersection.constraint G H)

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

Exact intersection with complete replay of simultaneous-prefix pruning.

Equations

• G.intersection H = (G.intersectionSearch H).group

theorem Hex.PermGroup.Group.mem_intersection {n : Nat} (G H : Group n) (p : Perm n) : Generated (G.intersection H).generators p ↔ Generated G.generators p ∧ Generated H.generators p