theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_state {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) (hcell : split + len ≤ n) (hm : Scratch.Marks n s.stamp s.marks) (hh : s.hits.size = n) : have t := splitNontrivial (Graph.ofGraph G) level split s; t.lab.toList.Perm (List.range n) ∧ t.ptn.size = n ∧ Index.Valid n t.lab t.ptn level t.cellstart t.cellend ∧ Cuts level n s.ptn t.ptn s.numcells t.numcells n ∧ cellsPerm s.ptn level t.lab s.lab ∧ (CellQueue s.ptn level s.active s.queue → CellQueue t.ptn level t.active t.queue) ∧ Pending n level (fun (a : Nat) => List.count a (List.flatMap (fun (q : Nat) => (Graph.ofGraph G).row s.lab[q]!) (List.range' split (s.cellend[split]! + 1 - split)))) s.cellend [] t.lab t.ptn ∧ Activation n level s.ptn t.ptn s.active t.active

The complete nontrivial pass preserves the labelling and partition cache. Native neighbour counting supplies the local hit bound for every count split, whose counter changes and inherited boundary values compose through the pass.

theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_index {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) (hcell : split + len ≤ n) (hm : Scratch.Marks n s.stamp s.marks) (hh : s.hits.size = n) : have t := splitNontrivial (Graph.ofGraph G) level split 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 complete nontrivial pass preserves a valid partition cache.

theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_constant {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) (hcell : 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 len); have t := splitNontrivial (Graph.ofGraph G) level split s; ∀ (a size : Nat), IsCell t.ptn level a size → a + size ≤ n → ∀ (q r : Nat), a ≤ q → q < a + size → a ≤ r → r < a + size → List.count t.lab[q]! seen = List.count t.lab[r]! seen

Every output cell has constant native neighbour count into the captured splitter cell, including cells that were never touched by the neighbour scan.

theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_active {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) (hcell : split + len ≤ n) (hm : Scratch.Marks n s.stamp s.marks) (hh : s.hits.size = n) : have t := splitNontrivial (Graph.ofGraph G) level split s; Activation n level s.ptn t.ptn s.active t.active

Every original cell satisfies sparse nauty's fragment-activation rule through the complete nontrivial pass, including largest-fragment replacement.