structure Hex.PermGroup.Level (n : Nat) : Type

One raw chain level, including generator provenance in the preceding level (or the original input array at level zero).

• generators : Array (Perm n)
• words : Vector Program self.generators.size
• orbit : Orbit n

inductive Hex.PermGroup.Chain (n : Nat) : Type

Raw stabilizer-chain data. The terminal generator array is checked explicitly; only a successful complete check makes this a group certificate.

• leaf {n : Nat} (generators : Array (Perm n)) (words : Vector Program generators.size) : Chain n
• cons {n : Nat} (level : Level n) (tail : Chain n) : Chain n

inductive Hex.PermGroup.SiftResult (n : Nat) : Type

A raw sift records either all orbit digits or its first failure. Negative results have mathematical meaning only after the chain has passed its checker.

• member {n : Nat} (digits : List Nat) : SiftResult n
• missing {n : Nat} (level : Nat) (image : Fin n) : SiftResult n
• residual {n : Nat} (value : Perm n) : SiftResult n
• shape {n : Nat} (level : Nat) : SiftResult n

def Hex.PermGroup.SiftResult.accepted {n : Nat} : SiftResult n → Bool

Equations

• (Hex.PermGroup.SiftResult.member digits).accepted = true
• x✝.accepted = false

def Hex.PermGroup.SiftResult.prepend {n : Nat} (digit : Nat) : SiftResult n → SiftResult n

Prepend the current orbit digit, preserving the first failure unchanged.

Equations

• Hex.PermGroup.SiftResult.prepend digit (Hex.PermGroup.SiftResult.member digits) = Hex.PermGroup.SiftResult.member (digit :: digits)
• Hex.PermGroup.SiftResult.prepend digit (Hex.PermGroup.SiftResult.missing level image) = Hex.PermGroup.SiftResult.missing level image
• Hex.PermGroup.SiftResult.prepend digit (Hex.PermGroup.SiftResult.residual value) = Hex.PermGroup.SiftResult.residual value
• Hex.PermGroup.SiftResult.prepend digit (Hex.PermGroup.SiftResult.shape level) = Hex.PermGroup.SiftResult.shape level

@[simp]

theorem Hex.PermGroup.SiftResult.accepted_prepend {n : Nat} (digit : Nat) (result : SiftResult n) : (prepend digit result).accepted = result.accepted

def Hex.PermGroup.Chain.generators {n : Nat} : Chain n → Array (Perm n)

Equations

• (Hex.PermGroup.Chain.leaf S words).generators = S
• (Hex.PermGroup.Chain.cons level tail).generators = level.generators

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

Equations

• (Hex.PermGroup.Chain.leaf S words).words = words
• (Hex.PermGroup.Chain.cons level tail).words = level.words

def Hex.PermGroup.Chain.length {n : Nat} : Chain n → Nat

Number of stored nonterminal levels. The checker requires exactly the remaining number of points in the fixed base.

Equations

• (Hex.PermGroup.Chain.leaf S words).length = 0
• (Hex.PermGroup.Chain.cons level tail).length = tail.length + 1

def Hex.PermGroup.Chain.sift {n : Nat} : Chain n → Nat → Perm n → SiftResult n

Sift by multiplying the current residual on the left by the inverse of its selected representative. Digits are stored with level zero most significant.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.PermGroup.Chain.leaf generators words).sift x✝¹ x✝ = if x✝ = Hex.Perm.id n then Hex.PermGroup.SiftResult.member [] else Hex.PermGroup.SiftResult.residual x✝

def Hex.PermGroup.Chain.siftImpl {n : Nat} : Chain n → Nat → Perm n → SiftResult n

sift for compiled code: it multiplies by the stored inverse representatives and skips identity representatives, which the chains of Group.ofGenerators have at every level whose orbit is a single point.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.PermGroup.Chain.leaf generators words).siftImpl x✝¹ x✝ = if x✝ = Hex.Perm.id n then Hex.PermGroup.SiftResult.member [] else Hex.PermGroup.SiftResult.residual x✝

@[csimp]

theorem Hex.PermGroup.Chain.sift_eq_siftImpl : @sift = @siftImpl

def Hex.PermGroup.Chain.accepts {n : Nat} (c : Chain n) (base : Nat) (p : Perm n) : Bool

Boolean acceptance of a raw sift. This does not assert completeness.

Equations

• c.accepts base p = (c.sift base p).accepted

@[simp]

theorem Hex.PermGroup.Chain.accepts_leaf {n : Nat} (S : Array (Perm n)) (w : Vector Program S.size) (base : Nat) (p : Perm n) : (leaf S w).accepts base p = decide (p = Perm.id n)

theorem Hex.PermGroup.Chain.accepts_cons {n : Nat} (level : Level n) (tail : Chain n) (base : Nat) (p : Perm n) : (cons level tail).accepts base p = if hb : base < n then match level.orbit.lookup[↑(p.get ⟨base, hb⟩)] with | none => false | some x => tail.accepts (base + 1) (level.orbit.reps[↑x].inv.comp p) else false

def Hex.PermGroup.Chain.orbitProduct {n : Nat} : Chain n → Nat

The raw orbit-size product, before its interpretation as a group order has been justified by complete checking.

Equations

• (Hex.PermGroup.Chain.leaf S words).orbitProduct = 1
• (Hex.PermGroup.Chain.cons level tail).orbitProduct = level.orbit.points.size * tail.orbitProduct