structure Hex.PermGroup.Search.Node {n : Nat} (G : Group n) : Type

A search node describes the coset prefix * <suffix.generators>. The checked suffix fixes every point preceding the current base position.

• base : Nat
• suffix : Chain n
• checked : self.suffix.checkFrom self.base = true
• inside (p : Perm n) : Generated self.suffix.generators p → Generated G.generators p
• rep : Element G

def Hex.PermGroup.Search.Node.root {n : Nat} (G : Group n) : Node G

Equations

• Hex.PermGroup.Search.Node.root G = { base := 0, suffix := G.chain, checked := ⋯, inside := ⋯, rep := Hex.PermGroup.Element.id G }

def Hex.PermGroup.Search.Node.Contains {n : Nat} {G : Group n} (t : Node G) (p : Perm n) : Prop

Membership in the node's entire remaining search region.

Equations

• t.Contains p = Hex.PermGroup.Generated t.suffix.generators (t.rep.val.inv.comp p)

def Hex.PermGroup.Search.Node.contains {n : Nat} {G : Group n} (t : Node G) (p : Perm n) : Bool

Equations

• t.contains p = t.suffix.accepts t.base (t.rep.val.inv.comp p)

theorem Hex.PermGroup.Search.Node.contains_iff {n : Nat} {G : Group n} (t : Node G) (p : Perm n) : t.contains p = true ↔ t.Contains p

theorem Hex.PermGroup.Search.Node.root_contains {n : Nat} (G : Group n) (p : Perm n) : (root G).Contains p ↔ Generated G.generators p

theorem Hex.PermGroup.Search.Node.contains_rep {n : Nat} {G : Group n} (t : Node G) : t.Contains t.rep.val

theorem Hex.PermGroup.Search.Node.generated {n : Nat} {G : Group n} (t : Node G) {p : Perm n} (hp : t.Contains p) : Generated G.generators p

theorem Hex.PermGroup.Search.Node.agrees {n : Nat} {G : Group n} (t : Node G) {p : Perm n} (hp : t.Contains p) (x : Fin n) (hx : ↑x < t.base) : p.get x = t.rep.val.get x

Every completion agrees with the stored prefix on assigned source points.

theorem Hex.PermGroup.Search.Node.level_checked {n : Nat} {G : Group n} (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) : (Chain.cons level tail).checkFrom t.base = true

theorem Hex.PermGroup.Search.Node.tail_inside {n : Nat} {G : Group n} (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) {p : Perm n} (hp : Generated tail.generators p) : Generated G.generators p

theorem Hex.PermGroup.Search.Node.rep_inside {n : Nat} {G : Group n} (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) (i : Fin level.orbit.points.size) : Generated G.generators level.orbit.reps[↑i]

def Hex.PermGroup.Search.Node.child {n : Nat} {G : Group n} (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) (i : Fin level.orbit.points.size) : Node G

Extend by one stored orbit representative in its discovery order.

Equations

• t.child hs i = { base := t.base + 1, suffix := tail, checked := ⋯, inside := ⋯, rep := t.rep.comp ⟨level.orbit.reps[↑i], ⋯⟩ }

theorem Hex.PermGroup.Search.Node.child_contains {n : Nat} {G : Group n} (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) (i : Fin level.orbit.points.size) (p : Perm n) : (t.child hs i).Contains p ↔ Generated tail.generators (level.orbit.reps[↑i].inv.comp (t.rep.val.inv.comp p))

theorem Hex.PermGroup.Search.Node.contains_children {n : Nat} {G : Group n} (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) (p : Perm n) : t.Contains p ↔ ∃ (i : Fin level.orbit.points.size), (t.child hs i).Contains p

Every parent completion belongs to a child, and every child stays in its parent. The children are reconstructed from the checked chain.

theorem Hex.PermGroup.Search.Node.child_disjoint {n : Nat} {G : Group n} (t : Node G) {level : Level n} {tail : Chain n} (hs : t.suffix = Chain.cons level tail) {i j : Fin level.orbit.points.size} {p : Perm n} (hi : (t.child hs i).Contains p) (hj : (t.child hs j).Contains p) : i = j

Distinct children are disjoint, detected at the next assigned base point.

theorem Hex.PermGroup.Search.Node.leaf_contains {n : Nat} {G : Group n} (t : Node G) {S : Array (Perm n)} {words : Vector Program S.size} (hs : t.suffix = Chain.leaf S words) (p : Perm n) : t.Contains p ↔ p = t.rep.val

At a checked terminal suffix the only completion is the prefix itself.