theorem Hex.PermGroup.Program.evalNodes_generators {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) {i : Nat} (hi : Node.generator i ∈ nodes) : i < S.size

theorem Hex.PermGroup.Program.generator_bound {n : Nat} {S : Array (Perm n)} {w : Program} {p : Perm n} (h : eval S w = some p) {i : Nat} (hi : Node.generator i ∈ w.nodes) : i < S.size

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

A shared prefix containing replacement programs for the first k generators. The first node is identity, used to redirect generator nodes through products. Semantic caches occur only in erased proofs, not in the runtime prefix.

• nodes : Array Node
• roots : Vector Nat k
• size : k ≤ T.size
• valid : ∃ (values : Array { p : Perm n // Generated S p }), evalNodes S self.nodes.toList #[] = some values ∧ (∃ (h : 0 < values.size), values[0].val = Perm.id n) ∧ ∀ (j : Fin k), ∃ (h : self.roots[↑j] < values.size), values[self.roots[↑j]].val = T[↑j]

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

Equations

• Hex.PermGroup.Program.Substitution.empty S T = { nodes := #[Hex.PermGroup.Node.id], roots := #v[], size := ⋯, valid := ⋯ }

def Hex.PermGroup.Program.Substitution.push {n : Nat} {S T : Array (Perm n)} {k : Nat} (c : Substitution S T k) (hk : k < T.size) (w : Program) (hw : checkWord S T[k] w = true) : Substitution S T (k + 1)

Append one replacement program once, preserving all earlier roots.

Equations

• c.push hk w hw = { nodes := c.nodes ++ Array.map (Hex.PermGroup.Program.shift c.nodes.size) w.nodes, roots := c.roots.push (c.nodes.size + w.root), size := hk, valid := ⋯ }

@[irreducible]

def Hex.PermGroup.Program.Substitution.finish {n : Nat} {S T : Array (Perm n)} {k : Nat} (c : Substitution S T k) (words : Vector Program T.size) (hw : checkWords S T words = true) : Substitution S T T.size

Equations

• c.finish words hw = if hk : k < T.size then (c.push hk words[k] ⋯).finish words hw else cast ⋯ c

theorem Hex.PermGroup.Program.Substitution.finish_size {n : Nat} {S T : Array (Perm n)} {k : Nat} (c : Substitution S T k) (words : Vector Program T.size) (hw : checkWords S T words = true) : (c.finish words hw).nodes.size = c.nodes.size + (List.map (fun (w : Program) => w.nodes.size) (List.drop k words.toList)).sum

theorem Hex.PermGroup.Program.Substitution.generated {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) {p : Perm n} (hp : Generated T p) : Generated S p

def Hex.PermGroup.Program.Substitution.lift {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (p : { p : Perm n // Generated T p }) : { p : Perm n // Generated S p }

Convert cached source values in proofs of substitution correctness.

Equations

• c.lift p = ⟨p.val, ⋯⟩

def Hex.PermGroup.Program.Substitution.node {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (source : Node) (h : ∀ (i : Nat), source = Node.generator i → i < T.size) : Node

Translate one node with a fixed offset. A generator becomes a reference to its shared replacement root multiplied by the prefix's identity node.

Equations

• c.node Hex.PermGroup.Node.id h_2 = Hex.PermGroup.Node.id
• c.node (Hex.PermGroup.Node.generator i) h_2 = Hex.PermGroup.Node.comp c.roots[i] 0
• c.node (Hex.PermGroup.Node.inv i) h_2 = Hex.PermGroup.Node.inv (c.nodes.size + i)
• c.node (Hex.PermGroup.Node.comp i j) h_2 = Hex.PermGroup.Node.comp (c.nodes.size + i) (c.nodes.size + j)

def Hex.PermGroup.Program.Substitution.translate {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (nodes : List Node) : (∀ (i : Nat), Node.generator i ∈ nodes → i < T.size) → List Node

Equations

• c.translate [] x_2 = []
• c.translate (source :: nodes) h = c.node source ⋯ :: c.translate nodes ⋯

theorem Hex.PermGroup.Program.Substitution.translate_length {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (nodes : List Node) (h : ∀ (i : Nat), Node.generator i ∈ nodes → i < T.size) : (c.translate nodes h).length = nodes.length

theorem Hex.PermGroup.Program.Substitution.evalNode_node {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (pre : Array { p : Perm n // Generated S p }) (hs : pre.size = c.nodes.size) (hz : 0 < pre.size) (hid : pre[0].val = Perm.id n) (hr : ∀ (j : Fin T.size), ∃ (h : c.roots[↑j] < pre.size), pre[c.roots[↑j]].val = T[↑j]) (values : Array { p : Perm n // Generated T p }) (source : Node) (hbound : ∀ (i : Nat), source = Node.generator i → i < T.size) (p : { p : Perm n // Generated T p }) (h : evalNode T values source = some p) : evalNode S (pre ++ Array.map c.lift values) (c.node source hbound) = some (c.lift p)

theorem Hex.PermGroup.Program.Substitution.evalNodes_translate {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (pre : Array { p : Perm n // Generated S p }) (hs : pre.size = c.nodes.size) (hz : 0 < pre.size) (hid : pre[0].val = Perm.id n) (hr : ∀ (j : Fin T.size), ∃ (h : c.roots[↑j] < pre.size), pre[c.roots[↑j]].val = T[↑j]) (nodes : List Node) (hbound : ∀ (i : Nat), Node.generator i ∈ nodes → i < T.size) (values result : Array { p : Perm n // Generated T p }) (h : evalNodes T nodes values = some result) : evalNodes S (c.translate nodes hbound) (pre ++ Array.map c.lift values) = some (pre ++ Array.map c.lift result)

def Hex.PermGroup.Program.Substitution.program {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (w : Program) {p : Perm n} (hw : checkWord T p w = true) : Program

Substitute a checked program, adding its nodes once after the shared prefix.

Equations

• c.program w hw = { nodes := c.nodes ++ (c.translate w.nodes.toList ⋯).toArray, root := c.nodes.size + w.root }

theorem Hex.PermGroup.Program.Substitution.program_size {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (w : Program) {p : Perm n} (hw : checkWord T p w = true) : (c.program w hw).nodes.size = c.nodes.size + w.nodes.size

theorem Hex.PermGroup.Program.Substitution.check_program {n : Nat} {S T : Array (Perm n)} (c : Substitution S T T.size) (w : Program) {p : Perm n} (hw : checkWord T p w = true) : checkWord S p (c.program w hw) = true

def Hex.PermGroup.Program.substitute {n : Nat} (S T : Array (Perm n)) (words : Vector Program T.size) (hwords : checkWords S T words = true) (w : Program) {p : Perm n} (hw : checkWord T p w = true) : Program

Substitute replacement programs once per input generator, then redirect all references to their shared roots. This does not expand a program into a word.

Equations

• Hex.PermGroup.Program.substitute S T words hwords w hw = ((Hex.PermGroup.Program.Substitution.empty S T).finish words hwords).program w hw

theorem Hex.PermGroup.Program.check_substitute {n : Nat} (S T : Array (Perm n)) (words : Vector Program T.size) (hwords : checkWords S T words = true) (w : Program) {p : Perm n} (hw : checkWord T p w = true) : checkWord S p (substitute S T words hwords w hw) = true

theorem Hex.PermGroup.Program.substitute_size {n : Nat} (S T : Array (Perm n)) (words : Vector Program T.size) (hwords : checkWords S T words = true) (w : Program) {p : Perm n} (hw : checkWord T p w = true) : (substitute S T words hwords w hw).nodes.size = 1 + (List.map (fun (w : Program) => w.nodes.size) words.toList).sum + w.nodes.size

Each replacement and each source node is stored exactly once, with one additional identity node. Repeated references do not increase this bound.