structure Hex.GraphIso.Nauty.Sparse.CountScan (n stamp : Nat) (before marks touched starts hits : Array Nat) (seen : List Nat) : Prop

A neighbour scan couples first-touch generations with exact accumulated counts. Its observation list includes skipped singleton neighbours.

• touch : Touched n stamp before marks touched (List.map (fun (v : Nat) => starts[v]!) seen)
• counts : Counts n starts hits (List.map (fun (v : Nat) => starts[v]!) seen) seen

theorem Hex.GraphIso.Nauty.Sparse.CountScan.initial {n stamp : Nat} {before starts hits : Array Nat} (hm : Scratch.Marks n stamp before) (hs : hits.size = n) : CountScan n stamp before before #[] starts hits []

theorem Hex.GraphIso.Nauty.Sparse.CountScan.sentinel {n stamp j : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) (hj : starts[j]! = n) : CountScan n stamp before marks touched starts hits (seen ++ [j])

theorem Hex.GraphIso.Nauty.Sparse.CountScan.repeated {n stamp j : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) (hj : j < n) (hk : starts[j]! < n) (hm : marks[starts[j]!]! = stamp + 1) : CountScan n stamp before marks touched starts (hits.setIfInBounds j (hits[j]! + 1)) (seen ++ [j])

theorem Hex.GraphIso.Nauty.Sparse.CountScan.fresh {n stamp j : Nat} {before marks touched starts hits cleared : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) (hj : j < n) (hk : starts[j]! < n) (hm : marks[starts[j]!]! ≠ stamp + 1) (hs : cleared.size = n) (hz : ∀ (v : Nat), v < n → cleared[v]! = if starts[v]! = starts[j]! then 0 else hits[v]!) : CountScan n stamp before (marks.setIfInBounds starts[j]! (stamp + 1)) (touched.push starts[j]!) starts (cleared.setIfInBounds j (cleared[j]! + 1)) (seen ++ [j])

theorem Hex.GraphIso.Nauty.Sparse.CountScan.sorted {n stamp : Nat} {before marks touched starts hits : Array Nat} {seen : List Nat} (h : CountScan n stamp before marks touched starts hits seen) : CountScan n stamp before marks (sortCells touched) starts hits seen