structure Hex.PermGroup.SizeLimit : Type

A requested complete output exceeds the caller's allocation bound.

• required : Nat
• capacity : Nat

@[instance_reducible]

instance Hex.PermGroup.instDecidableEqSizeLimit : DecidableEq SizeLimit

Equations

• Hex.PermGroup.instDecidableEqSizeLimit = Hex.PermGroup.instDecidableEqSizeLimit.decEq

def Hex.PermGroup.instDecidableEqSizeLimit.decEq (x✝ x✝¹ : SizeLimit) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.PermGroup.instReprSizeLimit : Repr SizeLimit

Equations

• Hex.PermGroup.instReprSizeLimit = { reprPrec := Hex.PermGroup.instReprSizeLimit.repr }

def Hex.PermGroup.instReprSizeLimit.repr : SizeLimit → Nat → Std.Format

Equations

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

def Hex.PermGroup.Element.le {n : Nat} (G : Group n) (p q : Element G) : Bool

Image-array comparison for deterministic public enumeration.

Equations

• Hex.PermGroup.Element.le G p q = (compare (Hex.PermGroup.Generator.images p.val) (Hex.PermGroup.Generator.images q.val)).isLE

theorem Hex.PermGroup.Element.le_trans {n : Nat} (G : Group n) (p q r : Element G) (hpq : le G p q = true) (hqr : le G q r = true) : le G p r = true

theorem Hex.PermGroup.Element.le_total {n : Nat} (G : Group n) (p q : Element G) : (le G p q || le G q p) = true

theorem Hex.PermGroup.Element.before_of_le {n : Nat} (G : Group n) (p q : Element G) (hle : le G p q = true) (hne : p ≠ q) : Chain.before p.val q.val

def Hex.PermGroup.Group.enumerate {n : Nat} (G : Group n) : Array (Element G)

Enumerate by the orbit-choice bijection, then sort by image arrays. This uncapped helper is used only after the public allocation check.

Equations

• G.enumerate = ((List.map G.unrank (List.finRange G.order)).mergeSort (Hex.PermGroup.Element.le G)).toArray

theorem Hex.PermGroup.Group.enumerate_size {n : Nat} (G : Group n) : G.enumerate.size = G.order

theorem Hex.PermGroup.Group.mem_enumerate {n : Nat} (G : Group n) (p : Element G) : p ∈ G.enumerate

theorem Hex.PermGroup.Group.enumerate_nodup {n : Nat} (G : Group n) : G.enumerate.toList.Nodup

theorem Hex.PermGroup.Group.enumerate_sorted {n : Nat} (G : Group n) : List.Pairwise (fun (p q : Element G) => Chain.before p.val q.val) G.enumerate.toList

def Hex.PermGroup.Group.elementsCapped {n : Nat} (cap : Nat) (G : Group n) : Except SizeLimit (Array (Element G))

Test the exact group order before allocating any enumeration. A size-limit result reports the required output size and is distinct from an empty result.

Equations

• Hex.PermGroup.Group.elementsCapped cap G = if G.order ≤ cap then Except.ok G.enumerate else Except.error { required := G.order, capacity := cap }

theorem Hex.PermGroup.Group.elementsCapped_ok {n : Nat} (cap : Nat) (G : Group n) : elementsCapped cap G = Except.ok G.enumerate ↔ G.order ≤ cap

theorem Hex.PermGroup.Group.elementsCapped_error {n : Nat} (cap : Nat) (G : Group n) : elementsCapped cap G = Except.error { required := G.order, capacity := cap } ↔ cap < G.order

theorem Hex.PermGroup.Group.elementsCapped_spec {n : Nat} (cap : Nat) (G : Group n) (values : Array (Element G)) (h : elementsCapped cap G = Except.ok values) : values.size = G.order ∧ values.size ≤ cap ∧ (∀ (p : Element G), p ∈ values) ∧ values.toList.Nodup ∧ List.Pairwise (fun (p q : Element G) => Chain.before p.val q.val) values.toList