structure Hex.GraphIso.Nauty.Sparse.Counts (n : Nat) (starts hits : Array Nat) (cells seen : List Nat) : Prop

Counts are exact on every touched nontrivial cell. Untouched scratch entries remain unrestricted; every observed nonsentinel vertex is covered.

• size : hits.size = n
• covered (v : Nat) : v ∈ seen → starts[v]! < n → starts[v]! ∈ cells
• get (v : Nat) : v < n → starts[v]! < n → starts[v]! ∈ cells → hits[v]! = List.count v seen

theorem Hex.GraphIso.Nauty.Sparse.Counts.initial {n : Nat} {starts hits : Array Nat} (hs : hits.size = n) : Counts n starts hits [] []

theorem Hex.GraphIso.Nauty.Sparse.Counts.repeated {n k : Nat} {starts hits : Array Nat} {cells seen : List Nat} (h : Counts n starts hits cells seen) (hk : k ∈ cells) : Counts n starts hits (cells ++ [k]) seen

Recording an already touched key leaves every count invariant intact.

theorem Hex.GraphIso.Nauty.Sparse.Counts.reset {n k : Nat} {starts hits cleared : Array Nat} {cells seen : List Nat} (h : Counts n starts hits cells seen) (hk : ¬k ∈ cells) (hs : cleared.size = n) (hc : ∀ (v : Nat), v < n → cleared[v]! = if starts[v]! = k then 0 else hits[v]!) : Counts n starts cleared (cells ++ [k]) seen

First-touch clearing initializes the new cell to its exact zero count; previously touched cells retain all accumulated counts.

theorem Hex.GraphIso.Nauty.Sparse.Counts.increment {n j : Nat} {starts hits : Array Nat} {cells seen : List Nat} (h : Counts n starts hits cells seen) (hj : j < n) (hk : starts[j]! < n) (hm : starts[j]! ∈ cells) : Counts n starts (hits.setIfInBounds j (hits[j]! + 1)) cells (seen ++ [j])

The actual count increment accounts for precisely one observed vertex.

theorem Hex.GraphIso.Nauty.Sparse.Counts.sentinel {n j : Nat} {starts hits : Array Nat} {cells seen : List Nat} (h : Counts n starts hits cells seen) (hj : starts[j]! = n) : Counts n starts hits (cells ++ [n]) (seen ++ [j])

Singleton neighbours add no count work and cannot affect a nontrivial cell's multiplicities.