theorem Hex.GraphIso.Nauty.Sparse.Activation.counts {n : Nat} {before : Array Nat} {active : VSet n} (level first : Nat) (distance : Bool) (s : RefineSt n) (h : Activation n level before s.ptn active s.active) (hc : IsCell before level first (s.cellend[first]! + 1 - first)) (ht : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) : have t := splitCounts level first distance s; Activation n level before t.ptn active t.active

A complete native count split composes the per-cell activation rule through the touched-cell fold and the distance-cell fold.