theorem Hex.GraphIso.Nauty.Sparse.splitCounts_trace {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) : CountTrace.Result distance first (s.cellend[first]! + 1) s (splitCounts level first distance s).lab (CountTrace.control (splitCounts level first distance s))

Every executed count split has its literal hash and queue trace. The only count bound is on the cell being divided; stale counts outside that cell and the other scratch fields are unrestricted.