theorem Hex.PermGroup.Program.evalNodes_append {n : Nat} (S : Array (Perm n)) (xs ys : List Node) (values : Array { p : Perm n // Generated S p }) : evalNodes S (xs ++ ys) values = (evalNodes S xs values).bind (evalNodes S ys)

Evaluation of a concatenated program continues from the first prefix's values.

theorem Hex.PermGroup.Program.evalNodes_size {n : Nat} {S : Array (Perm n)} {nodes : List Node} {values result : Array { p : Perm n // Generated S p }} (h : evalNodes S nodes values = some result) : result.size = values.size + nodes.length

Every accepted node contributes exactly one value.

structure Hex.PermGroup.Program.Builder {n : Nat} (S : Array (Perm n)) : Type

An append-only program under construction, with cached values and checked provenance. References share earlier nodes instead of expanding earlier words. The invariant proof is erased during compilation.

• nodes : Array Node
• values : Array { p : Perm n // Generated S p }
• valid : evalNodes S self.nodes.toList #[] = some self.values

def Hex.PermGroup.Program.Builder.empty {n : Nat} (S : Array (Perm n)) : Builder S

The empty program, before a root is chosen.

Equations

• Hex.PermGroup.Program.Builder.empty S = { nodes := #[], values := #[], valid := ⋯ }

theorem Hex.PermGroup.Program.Builder.size_eq {n : Nat} {S : Array (Perm n)} (b : Builder S) : b.values.size = b.nodes.size

def Hex.PermGroup.Program.Builder.push {n : Nat} {S : Array (Perm n)} (b : Builder S) (node : Node) (p : { p : Perm n // Generated S p }) (h : evalNode S b.values node = some p) : Builder S

Append one node and its known value. The proof only relates this node to cached earlier values; it never re-evaluates the preceding program at runtime.

Equations

• b.push node p h = { nodes := b.nodes.push node, values := b.values.push p, valid := ⋯ }

def Hex.PermGroup.Program.Builder.root {n : Nat} {S : Array (Perm n)} (b : Builder S) (node : Node) (p : { p : Perm n // Generated S p }) (h : evalNode S b.values node = some p) : Fin (b.push node p h).values.size

The root added by a push; earlier roots remain valid after the append.

Equations

• b.root node p h = ⟨b.values.size, ⋯⟩

def Hex.PermGroup.Program.Builder.id {n : Nat} {S : Array (Perm n)} (b : Builder S) : Builder S

Equations

• b.id = b.push Hex.PermGroup.Node.id ⟨Hex.Perm.id n, ⋯⟩ ⋯

def Hex.PermGroup.Program.Builder.generator {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin S.size) : Builder S

Equations

• b.generator i = b.push (Hex.PermGroup.Node.generator ↑i) ⟨S[↑i], ⋯⟩ ⋯

def Hex.PermGroup.Program.Builder.inv {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin b.values.size) : Builder S

Equations

• b.inv i = b.push (Hex.PermGroup.Node.inv ↑i) ⟨b.values[↑i].val.inv, ⋯⟩ ⋯

def Hex.PermGroup.Program.Builder.comp {n : Nat} {S : Array (Perm n)} (b : Builder S) (i j : Fin b.values.size) : Builder S

Equations

• b.comp i j = b.push (Hex.PermGroup.Node.comp ↑i ↑j) ⟨b.values[↑i].val.comp b.values[↑j].val, ⋯⟩ ⋯

@[simp]

theorem Hex.PermGroup.Program.Builder.size_generator {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin S.size) : (b.generator i).values.size = b.values.size + 1

@[simp]

theorem Hex.PermGroup.Program.Builder.size_comp {n : Nat} {S : Array (Perm n)} (b : Builder S) (i j : Fin b.values.size) : (b.comp i j).values.size = b.values.size + 1

def Hex.PermGroup.Program.Builder.act {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin S.size) (j : Fin b.values.size) : Builder S

Append a generator and its left product with an existing value. This is the parent-edge operation used when compiling orbit discovery trees.

Equations

• b.act i j = (b.generator i).comp ⟨b.values.size, ⋯⟩ ⟨↑j, ⋯⟩

@[simp]

theorem Hex.PermGroup.Program.Builder.size_id {n : Nat} {S : Array (Perm n)} (b : Builder S) : b.id.values.size = b.values.size + 1

@[simp]

theorem Hex.PermGroup.Program.Builder.size_act {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin S.size) (j : Fin b.values.size) : (b.act i j).values.size = b.values.size + 2

theorem Hex.PermGroup.Program.Builder.get_id {n : Nat} {S : Array (Perm n)} (b : Builder S) (j : Fin b.values.size) : b.id.values[↑j] = b.values[↑j]

theorem Hex.PermGroup.Program.Builder.last_id {n : Nat} {S : Array (Perm n)} (b : Builder S) : b.id.values[b.values.size].val = Perm.id n

theorem Hex.PermGroup.Program.Builder.get_act {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin S.size) (j k : Fin b.values.size) : (b.act i j).values[↑k] = b.values[↑k]

theorem Hex.PermGroup.Program.Builder.last_act {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin S.size) (j : Fin b.values.size) : (b.act i j).values[b.values.size + 1].val = S[↑i].comp b.values[↑j].val

def Hex.PermGroup.Program.Builder.program {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin b.values.size) : Program

Select any already evaluated node as the root. The resulting raw certificate shares the builder's node array; cached values and proof fields are not serialized.

Equations

• b.program i = { nodes := b.nodes, root := ↑i }

theorem Hex.PermGroup.Program.Builder.eval_program {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin b.values.size) : eval S (b.program i) = some b.values[↑i].val

theorem Hex.PermGroup.Program.Builder.check_program {n : Nat} {S : Array (Perm n)} (b : Builder S) (i : Fin b.values.size) : checkWord S b.values[↑i].val (b.program i) = true