def Hex.PermGroup.checkWords {n : Nat} (S T : Array (Perm n)) (words : Vector Program T.size) : Bool

Check every generator's provenance in the preceding generator array.

Equations

• Hex.PermGroup.checkWords S T words = decide (∀ (i : Fin T.size), Hex.PermGroup.checkWord S T[↑i] words[↑i] = true)

theorem Hex.PermGroup.checkWords_sound {n : Nat} {S T : Array (Perm n)} {words : Vector Program T.size} (h : checkWords S T words = true) {p : Perm n} (hp : Generated T p) : Generated S p

def Hex.PermGroup.Chain.reword {n : Nat} (c : Chain n) (words : Vector Program c.generators.size) : Chain n

Replace provenance at the top level. Internal chain checking does not inspect these words; the caller checks them against the new preceding generator array.

Equations

• (Hex.PermGroup.Chain.leaf S words_2).reword words_3 = Hex.PermGroup.Chain.leaf S words_3
• (Hex.PermGroup.Chain.cons level tail).reword words_2 = Hex.PermGroup.Chain.cons { generators := level.generators, words := words_2, orbit := level.orbit } tail

@[simp]

theorem Hex.PermGroup.Chain.generators_reword {n : Nat} (c : Chain n) (words : Vector Program c.generators.size) : (c.reword words).generators = c.generators

@[simp]

theorem Hex.PermGroup.Chain.words_reword {n : Nat} (c : Chain n) (words : Vector Program c.generators.size) : (c.reword words).words.toArray = words.toArray

@[simp]

theorem Hex.PermGroup.Chain.checkWords_reword {n : Nat} (S : Array (Perm n)) (c : Chain n) (words : Vector Program c.generators.size) : checkWords S (c.reword words).generators (c.reword words).words = checkWords S c.generators words

def Hex.PermGroup.Chain.before {n : Nat} (p q : Perm n) : Prop

Strict lexicographic order of permutation image arrays.

Equations

• Hex.PermGroup.Chain.before p q = (compare (List.map Fin.val p.vec.toList) (List.map Fin.val q.vec.toList) = Ordering.lt)

@[instance_reducible]

instance Hex.PermGroup.Chain.instDecidableBefore {n : Nat} (p q : Perm n) : Decidable (before p q)

Equations

• Hex.PermGroup.Chain.instDecidableBefore p q = Hex.PermGroup.Chain.instDecidableBefore._aux_1 p q

def Hex.PermGroup.Chain.Working {n : Nat} (S : Array (Perm n)) : Prop

The normalized working-array invariants, checked independently of sorting.

Equations

• Hex.PermGroup.Chain.Working S = (List.Pairwise Hex.PermGroup.Chain.before S.toList ∧ S.toList.Nodup ∧ ∀ (i : Fin S.size), S[↑i] ≠ Hex.Perm.id n ∧ S[↑i].inv ∈ S)

@[instance_reducible]

instance Hex.PermGroup.Chain.instDecidableWorking {n : Nat} (S : Array (Perm n)) : Decidable (Working S)

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Chain.Fixed {n : Nat} (base : Nat) (S : Array (Perm n)) : Prop

Every level generator fixes all preceding points of the fixed base.

Equations

• Hex.PermGroup.Chain.Fixed base S = ∀ (i : Fin S.size) (x : Fin n), ↑x < base → S[↑i].get x = x

@[instance_reducible]

instance Hex.PermGroup.Chain.instDecidableFixed {n : Nat} (base : Nat) (S : Array (Perm n)) : Decidable (Fixed base S)

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Chain.Normalized {n : Nat} (S T : Array (Perm n)) : Prop

The initial working array is exactly the sorted, deduplicated nonidentity input generators and their inverses. Original indices are retained by the separate provenance programs.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.PermGroup.Chain.instDecidableNormalized {n : Nat} (S T : Array (Perm n)) : Decidable (Normalized S T)

Equations

• One or more equations did not get rendered due to their size.

def Hex.PermGroup.Chain.checkFrom {n : Nat} : Chain n → Nat → Bool

Complete suffix checking. Each level recomputes every Schreier generator; no producer-supplied list is used as evidence that all pairs were considered.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.PermGroup.Chain.leaf S words).checkFrom x✝ = decide (x✝ = n ∧ Hex.PermGroup.Chain.Fixed x✝ S ∧ ∀ (i : Fin S.size), S[↑i] = Hex.Perm.id n)

@[simp]

theorem Hex.PermGroup.Chain.checkFrom_reword {n : Nat} (c : Chain n) (words : Vector Program c.generators.size) (base : Nat) : (c.reword words).checkFrom base = c.checkFrom base

Changing top-level provenance preserves the independently checked suffix.

theorem Hex.PermGroup.Chain.checkFrom_fixed {n : Nat} {c : Chain n} {base : Nat} (h : c.checkFrom base = true) : Fixed base c.generators

Accepted suffixes retain the fixed-point conditions, including at the terminal stage.

theorem Hex.PermGroup.Chain.checkFrom_length {n : Nat} {c : Chain n} {base : Nat} (h : c.checkFrom base = true) : base + c.length = n

Completeness checking enforces the full base length.

theorem Hex.PermGroup.Chain.checkFrom_sound {n : Nat} {c : Chain n} {base : Nat} (h : c.checkFrom base = true) (p : Perm n) : c.accepts base p = true ↔ Generated c.generators p

Successful and failed sifts are exact membership decisions after complete suffix verification. The induction uses only the already checked suffix when interpreting its Schreier-pair sifts as membership evidence.

def Hex.PermGroup.checkChain {n : Nat} (S : Array (Perm n)) (c : Chain n) : Bool

A complete chain for precisely the original input generators.

Equations

• Hex.PermGroup.checkChain S c = decide (Hex.PermGroup.Chain.Normalized S c.generators ∧ Hex.PermGroup.checkWords S c.generators c.words = true ∧ c.checkFrom 0 = true)

theorem Hex.PermGroup.checkChain_length {n : Nat} {S : Array (Perm n)} {c : Chain n} (h : checkChain S c = true) : c.length = n

A checked chain has exactly one level for every point of the fixed base.

theorem Hex.PermGroup.sift_iff {n : Nat} {S : Array (Perm n)} {c : Chain n} (h : checkChain S c = true) (p : Perm n) : c.accepts 0 p = true ↔ Generated S p

Complete checking makes sifting equivalent to membership in the original generated subgroup, for every query permutation.

theorem Hex.PermGroup.checkChain_sound {n : Nat} {S : Array (Perm n)} {c : Chain n} (h : checkChain S c = true) {p : Perm n} (hp : c.accepts 0 p = true) : Generated S p

Membership soundness of a complete-chain check.