def Hex.PermGroup.Chain.Choice {n : Nat} : Chain n → Type

One representative choice at each chain level.

Equations

• (Hex.PermGroup.Chain.leaf generators words).Choice = PUnit
• (Hex.PermGroup.Chain.cons level tail).Choice = (Fin level.orbit.points.size × tail.Choice)

def Hex.PermGroup.Chain.value {n : Nat} (c : Chain n) : c.Choice → Perm n

Multiply the selected representatives in sifting order, with level zero on the left. No group elements are enumerated.

Equations

• (Hex.PermGroup.Chain.leaf generators words).value x_2 = Hex.Perm.id n
• (Hex.PermGroup.Chain.cons level tail).value digits = level.orbit.reps[↑digits.fst].comp (tail.value digits.snd)

theorem Hex.PermGroup.Chain.fixed_generated {n : Nat} {S : Array (Perm n)} {base : Nat} (h : Fixed base S) {p : Perm n} (hp : Generated S p) (x : Fin n) (hx : ↑x < base) : p.get x = x

Fixed-point conditions on generators extend to the whole generated subgroup.

theorem Hex.PermGroup.Chain.value_generated {n : Nat} {c : Chain n} {base : Nat} (h : c.checkFrom base = true) (digits : c.Choice) : Generated c.generators (c.value digits)

Every Cartesian choice is an element of the checked suffix group.

theorem Hex.PermGroup.Chain.value_injective {n : Nat} {c : Chain n} {base : Nat} (h : c.checkFrom base = true) {u v : c.Choice} (he : c.value u = c.value v) : u = v

Distinct orbit choices give distinct permutations. The first differing choice is detected at that level's base point.

theorem Hex.PermGroup.Chain.value_surjective {n : Nat} {c : Chain n} {base : Nat} (h : c.checkFrom base = true) {p : Perm n} (hp : Generated c.generators p) : ∃ (digits : c.Choice), c.value digits = p

Every member is a product of orbit representatives, obtained by sifting.

theorem Hex.PermGroup.Chain.orbitProduct_pos {n : Nat} {c : Chain n} {base : Nat} (h : c.checkFrom base = true) : 0 < c.orbitProduct

Each radix is positive in a checked chain, including the empty product one.