theorem Hex.Perm.Cycle.counts_size {n : Nat} (cs : List (Array (Fin n))) (a : Array Nat) : (List.foldl (fun (counts : Array Nat) (c : Array (Fin n)) => counts.modify c.size fun (x : Nat) => x + 1) a cs).size = a.size

theorem Hex.Perm.Cycle.counts_get {n : Nat} (cs : List (Array (Fin n))) (a : Array Nat) (k : Nat) (hk : k < a.size) : (List.foldl (fun (counts : Array Nat) (c : Array (Fin n)) => counts.modify c.size fun (x : Nat) => x + 1) a cs)[k]! = a[k]! + List.count k (List.map Array.size cs)

theorem Hex.Perm.Cycle.expand_count (ks : List Nat) (f : Nat → Nat) (k : Nat) (hd : ks.Nodup) : List.count k (List.flatMap (fun (j : Nat) => List.replicate (f j) j) ks) = if k ∈ ks then f k else 0

theorem Hex.Perm.Cycle.expand_sorted (ks : List Nat) (f : Nat → Nat) (hs : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) ks) : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) (List.flatMap (fun (j : Nat) => List.replicate (f j) j) ks)

theorem Hex.Perm.cycleType_count {n : Nat} (p : Perm n) (k : Nat) : List.count k p.cycleType.toList = List.count k (List.map Array.size p.allCycles.toList)

The length histogram retains exactly the multiplicity of every emitted cycle length, including singleton fixed points.

theorem Hex.Perm.cycleType_perm {n : Nat} (p : Perm n) : p.cycleType.toList.Perm (List.map Array.size p.allCycles.toList)

theorem Hex.Perm.cycleType_sorted {n : Nat} (p : Perm n) : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) p.cycleType.toList

theorem Hex.Perm.cycleType_sum {n : Nat} (p : Perm n) : p.cycleType.toList.sum = n

theorem Hex.Perm.cycleType_size {n : Nat} (p : Perm n) : p.cycleType.size = p.allCycles.size