structure Hex.Perm.Cycle.Decomposition {n : Nat} (p : Perm n) (seen : Vector Bool n) (cs : Array (Array (Fin n))) : Prop

The accumulated cycles are valid and disjoint, and account for exactly the marked points.

• valid (c : Array (Fin n)) : c ∈ cs → Valid p c
• distinct : (List.flatMap Array.toList cs.toList).Nodup
• marked (x : Fin n) : seen[↑x] = true ↔ ∃ (c : Array (Fin n)), c ∈ cs ∧ x ∈ c

theorem Hex.Perm.Cycle.Decomposition.empty {n : Nat} (p : Perm n) : Decomposition p (Vector.replicate n false) #[]

theorem Hex.Perm.Cycle.Decomposition.invariant {n : Nat} {p : Perm n} {seen : Vector Bool n} {cs : Array (Array (Fin n))} (h : Decomposition p seen cs) : Invariant p seen

theorem Hex.Perm.Cycle.Decomposition.push {n : Nat} {p : Perm n} {seen next : Vector Bool n} {cs : Array (Array (Fin n))} {c : Array (Fin n)} (h : Decomposition p seen cs) (hc : Valid p c) (hm : ∀ (x : Fin n), next[↑x] = true ↔ seen[↑x] = true ∨ x ∈ c) (hd : ∀ (x : Fin n), x ∈ c → seen[↑x] = false) : Decomposition p next (cs.push c)

theorem Hex.Perm.Cycle.scan_complete {n : Nat} (p : Perm n) (xs : List (Fin n)) (seen : Vector Bool n) (cs : Array (Array (Fin n))) (h : Decomposition p seen cs) (outside : ∀ (x : Fin n), ¬x ∈ xs → seen[↑x] = true) : have result := p.scanCycles xs seen cs; Decomposition p result.fst result.snd ∧ ∀ (x : Fin n), result.fst[↑x] = true

The scan preserves the partial decomposition. Every point outside the remaining list is marked, so exhausting that list gives a full partition.

theorem Hex.Perm.allCycles_valid {n : Nat} (p : Perm n) (c : Array (Fin n)) (hc : c ∈ p.allCycles) : Cycle.Valid p c

Every emitted cycle follows the permutation, including wrap-around.

theorem Hex.Perm.allCycles_distinct {n : Nat} (p : Perm n) : (List.flatMap Array.toList p.allCycles.toList).Nodup

No point occurs twice in the cycle decomposition.

theorem Hex.Perm.mem_allCycles {n : Nat} (p : Perm n) (x : Fin n) : ∃ (c : Array (Fin n)), c ∈ p.allCycles ∧ x ∈ c

Every point occurs in an emitted cycle, including fixed points.

theorem Hex.Perm.allCycles_get {n : Nat} (p : Perm n) (c : Array (Fin n)) (hc : c ∈ p.allCycles) (i : Nat) (hi : i < c.size) : p.get c[i] = c[(i + 1) % c.size]

Reading the successor in the emitted cycle reconstructs the original action.

theorem Hex.Perm.allCycles_length {n : Nat} (p : Perm n) : (List.map Array.size p.allCycles.toList).sum = n