def Hex.Perm.Cycle.Least {n : Nat} (c : Array (Fin n)) : Prop

The first entry is the least point in the cycle.

Equations

• Hex.Perm.Cycle.Least c = ∀ (hc : 0 < c.size) (x : Fin n), x ∈ c → c[0] ≤ x

def Hex.Perm.Cycle.Precedes {n : Nat} (c d : Array (Fin n)) : Prop

Cycles are ordered by their first entries.

Equations

• Hex.Perm.Cycle.Precedes c d = ∀ (hc : 0 < c.size) (hd : 0 < d.size), c[0] < d[0]

theorem Hex.Perm.Cycle.scan_canonical {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) (sorted : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) xs) (least : ∀ (c : Array (Fin n)), c ∈ cs → Least c) (ordered : List.Pairwise Precedes cs.toList) (before : ∀ (c : Array (Fin n)), c ∈ cs → ∀ (x : Fin n), x ∈ xs → ∀ (hc : 0 < c.size), c[0] < x) : have result := (p.scanCycles xs seen cs).snd; (∀ (c : Array (Fin n)), c ∈ result → Least c) ∧ List.Pairwise Precedes result.toList

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

theorem Hex.Perm.allCycles_ordered {n : Nat} (p : Perm n) : List.Pairwise Cycle.Precedes p.allCycles.toList

theorem Hex.Perm.cycles_least {n : Nat} (p : Perm n) (c : Array (Fin n)) (hc : c ∈ p.cycles) : Cycle.Least c

theorem Hex.Perm.cycles_ordered {n : Nat} (p : Perm n) : List.Pairwise Cycle.Precedes p.cycles.toList