theorem Hex.Perm.Cycle.Valid.formPerm_get {n : ℕ} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (x : Fin n) (hx : x ∈ c) : c.toList.formPerm x = p.get x

theorem Hex.Perm.Cycle.prod_apply {n : ℕ} (p : Perm n) (cs : List (Array (Fin n))) (hv : ∀ c ∈ cs, Valid p c) (hd : (List.flatMap Array.toList cs).Nodup) (x : Fin n) : (List.map (fun (c : Array (Fin n)) => c.toList.formPerm) cs).prod x = if x ∈ List.flatMap Array.toList cs then p.get x else x

A product of disjoint recorded cycles acts as the permutation on their union and fixes every point outside that union.

theorem Hex.Perm.allCycles_prod {n : ℕ} (p : Perm n) : (List.map (fun (c : Array (Fin n)) => c.toList.formPerm) p.allCycles.toList).prod = p.toEquiv

Multiplying the recorded cycles reconstructs the Mathlib permutation.

theorem Hex.Perm.cycles_prod {n : ℕ} (p : Perm n) : (List.map (fun (c : Array (Fin n)) => c.toList.formPerm) p.cycles.toList).prod = p.toEquiv

theorem Hex.Perm.cycles_disjoint {n : ℕ} (p : Perm n) : List.Pairwise Equiv.Perm.Disjoint (List.map (fun (c : Array (Fin n)) => c.toList.formPerm) p.cycles.toList)

theorem Hex.Perm.cycle_support {n : ℕ} (p : Perm n) (c : Array (Fin n)) (hc : c ∈ p.cycles) : c.toList.formPerm.support.card = c.size

theorem Hex.Perm.cycleType_factors {n : ℕ} (p : Perm n) : Equiv.Perm.cycleType p.toEquiv = ↑(List.map Array.size p.cycles.toList)

Mathlib omits fixed points from its cycle type. Its entries are precisely the lengths of the nontrivial cycles returned by the executable traversal.