theorem
Hex.GraphIso.Nauty.Sparse.splitNontrivial_trace
{n : Nat}
(G : SparseGraph n)
(level split len : Nat)
(s : RefineSt n)
(hp : s.lab.toList.Perm (List.range n))
(hs : s.ptn.size = n)
(hend : s.ptn[n - 1]! ≤ level)
(hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend)
(hc : IsCell s.ptn level split len)
(hb : split + len ≤ n)
(hm : Scratch.Marks n s.stamp s.marks)
(hh : s.hits.size = n)
:
have seen :=
List.flatMap (fun (q : Nat) => (Graph.ofGraph G).row s.lab[q]!) (List.range' split (s.cellend[split]! + 1 - split));
have r :=
(have marks := s.marks;
have hits := s.hits;
have touched := #[];
do
let __s ←
forIn [split:s.cellend[split]! + 1] (marks, hits, touched)
fun (i : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have vertex := s.lab[i]!;
do
let __s ←
forIn [G.offsets[vertex]!:G.offsets[vertex + 1]!] (marks, hits, touched)
fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) =>
have marks := __s.fst;
have __s := __s.snd;
have hits := __s.fst;
have touched := __s.snd;
have j := (Graph.ofGraph G).neighbor e;
have k := s.cellstart[j]!;
if (k != n) = true then
have __do_jp := fun (__r : Unit) (marks hits touched : Array Nat) =>
have hits := hits.set! j (hits[j]! + 1);
pure (ForInStep.yield (marks, hits, touched));
if (marks[k]! != s.stamp + 1) = true then
have marks := marks.set! k (s.stamp + 1);
have touched := touched.push k;
do
let __s ←
forIn [k:s.cellend[k]! + 1] hits fun (l : Nat) (__s : Array Nat) =>
have hits := __s;
have hits := hits.set! s.lab[l]! 0;
pure (ForInStep.yield hits)
have hits : Array Nat := __s
__do_jp () marks hits touched
else __do_jp () marks hits touched
else pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (ForInStep.yield (marks, hits, touched))
have marks : Array Nat := __s.fst
have __s : Array Nat × Array Nat := __s.snd
have hits : Array Nat := __s.fst
have touched : Array Nat := __s.snd
pure (marks, sortCells touched, hits)).run;
have initial :=
{ lab := s.lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := s.cellstart, cellend := s.cellend,
indexed := s.indexed, hits := r.snd.snd, marks := r.fst, vmarks := s.vmarks, stamp := s.stamp + 1,
numcells := s.numcells, longcode := s.longcode }.hash
r.snd.fst.size;
CountTrace.Pass level false (fun (a : Nat) => List.count a seen) r.snd.fst.toList initial
(splitNontrivial (Graph.ofGraph G) level split s)
The complete production nontrivial pass admits its exact count-split trace. Native first-touch clearing derives the semantic count and local bound required at every processed cell.