theorem Hex.GraphIso.Nauty.Sparse.CountSort.finish_trace {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (lab : Array Nat) (w1 v2 w2 v3 : Nat) (hm : Minima.Permuted s.lab lab s.hits first last v2 v3 last w1 w2 (n + 2)) (hn : ∃ (q : Nat), first ≤ q ∧ q < last ∧ s.hits[s.lab[q]!]! ≠ s.hits[s.lab[first]!]!) : have t := finish level first last distance (have __src := s.hash first; { lab := lab, ptn := __src.ptn, active := __src.active, queue := __src.queue, cellstart := __src.cellstart, cellend := __src.cellend, indexed := __src.indexed, hits := __src.hits, marks := __src.marks, vmarks := __src.vmarks, stamp := __src.stamp, numcells := __src.numcells, longcode := __src.longcode }) w1 v2 w2 v3; CountTrace.Result distance first last s t.lab (CountTrace.control t)

The fragment installer emits the count-run control trace, including both hash conventions and the final largest-fragment replacement.

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.