theorem Hex.PermGroup.Chain.base_lt {n : Nat} {level : Level n} {tail : Chain n} {base : Nat} (h : (cons level tail).checkFrom base = true) : base < n

theorem Hex.PermGroup.Chain.orbit_valid {n : Nat} {level : Level n} {tail : Chain n} {base : Nat} (h : (cons level tail).checkFrom base = true) : Orbit.Valid level.generators ⟨base, ⋯⟩ level.orbit

theorem Hex.PermGroup.Chain.suffix_checked {n : Nat} {level : Level n} {tail : Chain n} {base : Nat} (h : (cons level tail).checkFrom base = true) : tail.checkFrom (base + 1) = true

theorem Hex.PermGroup.Chain.suffix_words {n : Nat} {level : Level n} {tail : Chain n} {base : Nat} (h : (cons level tail).checkFrom base = true) : checkWords level.generators tail.generators tail.words = true

def Hex.PermGroup.Chain.program {n : Nat} (c : Chain n) (base : Nat) : c.checkFrom base = true → (digits : c.Choice) → { w : Program // checkWord c.generators (c.value digits) w = true }

Compile the representative product for a successful sift. Each transition substitutes the next level's generators by their checked provenance programs, sharing those replacements rather than expanding repeated references.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.PermGroup.Chain.leaf S words).program x x_1 x_6 = ⟨{ nodes := #[Hex.PermGroup.Node.id], root := 0 }, ⋯⟩

def Hex.PermGroup.Group.program {n : Nat} (G : Group n) (digits : G.chain.Choice) : Program

Translate a chain representative product into the original input generators.

Equations

• G.program digits = Hex.PermGroup.Program.substitute G.generators G.chain.generators G.chain.words ⋯ (G.chain.program 0 ⋯ digits).val ⋯

theorem Hex.PermGroup.Group.check_program {n : Nat} (G : Group n) (digits : G.chain.Choice) : checkWord G.generators (G.chain.value digits) (G.program digits) = true

def Hex.PermGroup.Group.word? {n : Nat} (G : Group n) (p : Perm n) : Option Program

A checked program in the original generators exactly when the complete sift accepts. Negative queries do not allocate membership programs.

Equations

• G.word? p = Option.map G.program (G.chain.choose 0 p)

theorem Hex.PermGroup.Group.word?_isSome {n : Nat} (G : Group n) (p : Perm n) : (G.word? p).isSome = G.contains p

theorem Hex.PermGroup.Group.word?_sound {n : Nat} (G : Group n) (p : Perm n) (w : Program) (h : G.word? p = some w) : checkWord G.generators p w = true

theorem Hex.PermGroup.Group.word?_complete {n : Nat} (G : Group n) (p : Perm n) : (∃ (w : Program), G.word? p = some w ∧ checkWord G.generators p w = true) ↔ Generated G.generators p

def Hex.PermGroup.Group.subgroupWords {n : Nat} (H G : Group n) (h : H.IsSubgroup G) : Vector Program H.generators.size

Positive containment certificates, one checked membership program for each original generator of the smaller group.

Equations

• H.subgroupWords G h = Hex.Vector.ofFn' fun (i : Fin H.generators.size) => (G.word? H.generators[↑i]).get ⋯

theorem Hex.PermGroup.Group.check_subgroupWords {n : Nat} (H G : Group n) (h : H.IsSubgroup G) : checkWords G.generators H.generators (H.subgroupWords G h) = true

def Hex.PermGroup.Group.subgroupWords? {n : Nat} (H G : Group n) : Option (Vector Program H.generators.size)

Decide containment and, on success, retain the original generators' words.

Equations

• H.subgroupWords? G = if h : H.isSubgroup G = true then some (H.subgroupWords G ⋯) else none

theorem Hex.PermGroup.Group.subgroupWords?_isSome {n : Nat} (H G : Group n) : (H.subgroupWords? G).isSome = H.isSubgroup G

theorem Hex.PermGroup.Group.subgroupWords?_sound {n : Nat} (H G : Group n) (words : Vector Program H.generators.size) (h : H.subgroupWords? G = some words) : checkWords G.generators H.generators words = true