theorem Hex.GraphIso.Nauty.Sparse.Index.Run.key_iff {lab hits : Array Nat} {first last a b q : Nat} (h : Run lab hits first last a b) (hs : «Sort».Sorted lab hits first (last + 1 - first)) (hq : first ≤ q) (he : q ≤ last) : hits[lab[q]!]! = hits[lab[a]!]! ↔ a ≤ q ∧ q ≤ b

In a sorted cell, one maximal run contains every occurrence of its key.

theorem Hex.GraphIso.Nauty.Sparse.Index.Run.filter_perm {lab hits : Array Nat} {first last a b n : Nat} (h : Run lab hits first last a b) (hs : «Sort».Sorted lab hits first (last + 1 - first)) (hp : lab.toList.Perm (List.range n)) (hb : last < n) : (segN lab a (b + 1 - a)).Perm (List.filter (fun (v : Nat) => hits[v]! == hits[lab[a]!]!) (segN lab first (last + 1 - first)))

The vertices of a completed count run are exactly the original cell filtered by that count. Their internal order is immaterial.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_class {n a len : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (ha : first ≤ a) (hlen : 0 < len) (he : a + len ≤ s.cellend[first]! + 1) (ho : IsCell (splitCounts level first distance s).ptn level a len) : (segN (splitCounts level first distance s).lab a len).Perm (List.filter (fun (v : Nat) => s.hits[v]! == s.hits[(splitCounts level first distance s).lab[a]!]!) (segN s.lab first (s.cellend[first]! + 1 - first)))

The executed count splitter's ordered fragments have exactly their specified count-class vertex multisets.