theorem Hex.GraphIso.Nauty.Sparse.count_map {n : Nat} (σ : Renaming n) (seen : List Nat) (v : Nat) : List.count (σ.toFun v) (List.map σ.toFun seen) = List.count v seen

Injective vertex renaming preserves every observed multiplicity.

theorem Hex.GraphIso.Nauty.Sparse.CountScan.equiv {n stamp : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} {next : Nat} {old final visits other keys : Array Nat} {observed : List Nat} (σ : Renaming n) (hs : CountScan n stamp before marks touched starts hits seen) (ht : CountScan n next old final visits other keys observed) (ho : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) touched.toList) (ho' : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) visits.toList) (hb : ∀ (v : Nat), v ∈ seen → v < n) (hkeys : ∀ (v : Nat), v < n → other[σ.toFun v]! = starts[v]!) (hp : observed.Perm (List.map σ.toFun seen)) : touched = visits ∧ ∀ (v : Nat), v < n → starts[v]! ∈ touched.toList → keys[σ.toFun v]! = hits[v]!

Exact native counts and sorted first-touch lists transport from the observed neighbour multiset. Retained counts outside touched cells are unrestricted and need not agree.