theorem Hex.GraphIso.Nauty.Sparse.Target.count_cell {n a len first : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level : Nat) (s : Scratch) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Index.Valid n lab ptn level s.cellstart s.cellend) (hc : IsCell ptn level a len) (hb : a + len ≤ n) (hn : 1 < len) (hf : first < n) : List.count a (row (Graph.ofGraph G) lab s first) = (worksetOf n lab a (a + len - 1)).cardInter (Graph.context G).g[lab[first]!]!

The target selector's native row count is the number of neighbours in the specified cell. This connects its index representation to equitability.

theorem Hex.GraphIso.Nauty.Sparse.Target.count_workset {n a first : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level : Nat) (s : Scratch) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Index.Valid n lab ptn level s.cellstart s.cellend) (ha : a ∈ nontrivial (cells ptn level n)) (hf : first < n) : List.count a (row (Graph.ofGraph G) lab s first) = (worksetOf n lab a s.cellend[a]!).cardInter (Graph.context G).g[lab[first]!]!

On each enumerated nontrivial cell the cached endpoint and the shared set-valued count describe the same partial join.