inductive Hex.GraphIso.Nauty.Sparse.CountTrace.Pass {n : Nat} (level : Nat) (distance : Bool) (key : Nat → Nat) : List Nat → RefineSt n → RefineSt n → Prop

A trace of executed count splits. The fixed key gives the semantic count only on cells that are actually processed, leaving other scratch entries unrestricted. The distance flag retains both production modes.

• nil {n level : Nat} {distance : Bool} {key : Nat → Nat} {s : RefineSt n} : Pass level distance key [] s s
• cons {n level : Nat} {distance : Bool} {key : Nat → Nat} {first : Nat} {rest : List Nat} {s u : RefineSt n} (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (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) (hv : ∀ (v : Nat), v ∈ segN s.lab first (s.cellend[first]! + 1 - first) → s.hits[v]! = key v) (ht : Pass level distance key rest (splitCounts level first distance s) u) : Pass level distance key (first :: rest) s u

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Pass.append {level : Nat} {distance : Bool} {key : Nat → Nat} {xs : List Nat} {n✝ : Nat} {s t : RefineSt n✝} {ys : List Nat} {u : RefineSt n✝} (h : Pass level distance key xs s t) : Pass level distance key ys t u → Pass level distance key (xs ++ ys) s u

Consecutive portions of a count-split loop compose.

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.split_valid {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (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) : have t := splitCounts level first distance s; t.lab.toList.Perm (List.range n) ∧ t.ptn.size = n ∧ Index.Valid n t.lab t.ptn level t.cellstart t.cellend

The structural facts needed at the next count split follow from the actual splitter's permutation, frame and cache theorems.

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Pass.valid {n level : Nat} {distance : Bool} {key : Nat → Nat} {xs : List Nat} {s t : RefineSt n} (h : Pass level distance key xs s t) : s.lab.toList.Perm (List.range n) → s.ptn.size = n → Index.Valid n s.lab s.ptn level s.cellstart s.cellend → t.lab.toList.Perm (List.range n) ∧ t.ptn.size = n ∧ Index.Valid n t.lab t.ptn level t.cellstart t.cellend

A completed trace preserves the labelling and valid partition index.