theorem Hex.GraphIso.Nauty.Sparse.CountScan.read {n stamp v : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) (hv : v < n) (ht : starts[v]! ∈ touched.toList) : hits[v]! = List.count v seen

Counts in a touched nontrivial cell interpret the native neighbour scan.

theorem Hex.GraphIso.Nauty.Sparse.CountScan.zero {n stamp v : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) (hk : starts[v]! < n) (ht : ¬starts[v]! ∈ touched.toList) : List.count v seen = 0

Untouched nontrivial cells have zero semantic count, regardless of their retained scratch values. They therefore need no count split.

theorem Hex.GraphIso.Nauty.Sparse.CountScan.cell_key {n stamp : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) {lab ptn ends : Array Nat} {level first len : Nat} (hp : lab.toList.Perm (List.range n)) (hi : Index.Valid n lab ptn level starts ends) (hc : IsCell ptn level first len) (hl : 1 < len) (hb : first + len ≤ n) (ht : first ∈ touched.toList) (v : Nat) : v ∈ segN lab first len → hits[v]! = List.count v seen

The valid cache supplies the semantic key on every vertex of a touched cell, which is precisely the hypothesis used by splitCounts_constant.

theorem Hex.GraphIso.Nauty.Sparse.CountScan.cell_zero {n stamp : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) {lab ptn ends : Array Nat} {level first len : Nat} (hi : Index.Valid n lab ptn level starts ends) (hc : IsCell ptn level first len) (hl : 1 < len) (hb : first + len ≤ n) (ht : ¬first ∈ touched.toList) (v : Nat) : v ∈ segN lab first len → List.count v seen = 0

Every vertex of an untouched nontrivial cell has zero native count.