def Hex.PermGroup.Chain.encode {n : Nat} (c : Chain n) : c.Choice → Fin c.orbitProduct

Mixed-radix encoding, with the top-level orbit digit most significant.

Equations

• (Hex.PermGroup.Chain.leaf generators words).encode x_2 = ⟨0, Nat.zero_lt_one⟩
• (Hex.PermGroup.Chain.cons level tail).encode digits = ⟨↑digits.fst * tail.orbitProduct + ↑(tail.encode digits.snd), ⋯⟩

def Hex.PermGroup.Chain.decode {n : Nat} (c : Chain n) : Fin c.orbitProduct → c.Choice

Exact division and remainder recover the mixed-radix digits. An in-range index itself proves that every radix encountered on its path is positive.

Equations

• (Hex.PermGroup.Chain.leaf generators words).decode x_2 = PUnit.unit
• (Hex.PermGroup.Chain.cons level tail).decode k = (⟨↑k / tail.orbitProduct, ⋯⟩, tail.decode ⟨↑k % tail.orbitProduct, ⋯⟩)

theorem Hex.PermGroup.Chain.encode_decode {n : Nat} (c : Chain n) (k : Fin c.orbitProduct) : c.encode (c.decode k) = k

theorem Hex.PermGroup.Chain.decode_encode {n : Nat} (c : Chain n) (digits : c.Choice) : c.decode (c.encode digits) = digits

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

Sifting with bounded orbit digits. Failures carry no choice and cannot be used as a rank; membership still comes from the complete-chain checker.

Equations

• One or more equations did not get rendered due to their size.
• (Hex.PermGroup.Chain.leaf generators words).choose x✝¹ x✝ = if x✝ = Hex.Perm.id n then some PUnit.unit else none

theorem Hex.PermGroup.Chain.choose_isSome {n : Nat} (c : Chain n) (base : Nat) (p : Perm n) : (c.choose base p).isSome = c.accepts base p

theorem Hex.PermGroup.Chain.choose_sound {n : Nat} {c : Chain n} {base : Nat} {p : Perm n} {digits : c.Choice} (h : c.choose base p = some digits) : c.value digits = p

def Hex.PermGroup.Chain.choice {n : Nat} (c : Chain n) (base : Nat) (p : Perm n) (h : c.accepts base p = true) : c.Choice

Obtain a choice from a known successful sift, without repeating membership checks or searching through possible choices.

Equations

• c.choice base p h = (c.choose base p).get ⋯

theorem Hex.PermGroup.Chain.value_choice {n : Nat} (c : Chain n) (base : Nat) (p : Perm n) (h : c.accepts base p = true) : c.value (c.choice base p h) = p

theorem Hex.PermGroup.Group.checked {n : Nat} (G : Group n) : G.chain.checkFrom 0 = true

def Hex.PermGroup.Group.rank {n : Nat} (G : Group n) (p : Element G) : Fin G.order

The position of an element in the stored chain's mixed-radix ordering.

Equations

• G.rank p = G.chain.encode (G.chain.choice 0 p.val ⋯)

def Hex.PermGroup.Group.unrank {n : Nat} (G : Group n) (k : Fin G.order) : Element G

Recover an element by exact digit extraction and representative multiplication.

Equations

• G.unrank k = ⟨G.chain.value (G.chain.decode k), ⋯⟩

theorem Hex.PermGroup.Group.unrank_rank {n : Nat} (G : Group n) (p : Element G) : G.unrank (G.rank p) = p

theorem Hex.PermGroup.Group.rank_unrank {n : Nat} (G : Group n) (k : Fin G.order) : G.rank (G.unrank k) = k

def Hex.PermGroup.Group.rank? {n : Nat} (G : Group n) (p : Perm n) : Option (Fin G.order)

Raw permutations are ranked only after a complete membership check.

Equations

• G.rank? p = Option.map G.chain.encode (G.chain.choose 0 p)

def Hex.PermGroup.Group.unrank? {n : Nat} (G : Group n) (k : Nat) : Option (Element G)

Reject out-of-range indices before digit extraction.

Equations

• G.unrank? k = if h : k < G.order then some (G.unrank ⟨k, h⟩) else none

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

theorem Hex.PermGroup.Group.rank?_rank {n : Nat} (G : Group n) (p : Element G) : G.rank? p.val = some (G.rank p)

theorem Hex.PermGroup.Group.unrank?_unrank {n : Nat} (G : Group n) (k : Fin G.order) : G.unrank? ↑k = some (G.unrank k)

theorem Hex.PermGroup.Group.unrank?_isSome {n : Nat} (G : Group n) (k : Nat) : (G.unrank? k).isSome = decide (k < G.order)

def Hex.PermGroup.Group.sampleFrom {n : Nat} {m : Type → Type} [Functor m] (draw : (bound : Nat) → 0 < bound → m (Fin bound)) (G : Group n) : m (Element G)

Apply unranking to one index from the supplied source. The source receives the positive exact order; its effects and failures are preserved by map.

Equations

• Hex.PermGroup.Group.sampleFrom draw G = G.unrank <$> draw G.order ⋯

theorem Hex.PermGroup.Group.sampleFrom_error {n : Nat} {ε : Type} (error : ε) (G : Group n) : sampleFrom (fun (x : Nat) (x_1 : 0 < x) => Except.error error) G = Except.error error