theorem Hex.GraphIso.Nauty.Sparse.segment_keys_map {n first len : Nat} (σ : Renaming n) (lab out hits keys : Array Nat) (hp : lab.toList.Perm (List.range n)) (hb : first + len ≤ n) (hc : (segN out first len).Perm (segN (Array.map σ.toFun lab) first len)) (hk : ∀ (v : Nat), v ∈ segN lab first len → keys[σ.toFun v]! = hits[v]!) : (List.map (fun (v : Nat) => keys[v]!) (segN out first len)).Perm (List.map (fun (v : Nat) => hits[v]!) (segN lab first len))

Transporting vertices and their keys preserves the segment's count multiset, including a further permutation within the segment.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_map {n : Nat} (σ : Renaming n) (level first last : Nat) (distance : Bool) (s t : RefineSt n) (hsl : s.lab.toList.Perm (List.range n)) (htl : t.lab.toList.Perm (List.range n)) (hsp : s.ptn.size = n) (htp : t.ptn = s.ptn) (hse : s.cellend[first]! = last) (hte : t.cellend[first]! = last) (hf : first ≤ last) (hb : last < n) (hsk : ∀ (q : Nat), first ≤ q → q ≤ last → s.hits[s.lab[q]!]! < n + 2) (htk : ∀ (q : Nat), first ≤ q → q ≤ last → t.hits[t.lab[q]!]! < n + 2) (hk : ∀ (v : Nat), v ∈ segN s.lab first (last + 1 - first) → t.hits[σ.toFun v]! = s.hits[v]!) (hc : IsCell s.ptn level first (last + 1 - first)) (hp : cellsPerm s.ptn level t.lab (Array.map σ.toFun s.lab)) : (splitCounts level first distance s).ptn = (splitCounts level first distance t).ptn ∧ cellsPerm (splitCounts level first distance s).ptn level (splitCounts level first distance t).lab (Array.map σ.toFun (splitCounts level first distance s).lab)

Count classes commute with vertex transport. This law permits different admissible index storage and different orders within a cell.