theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_state {n : Nat} (G : SparseGraph n) (level split : Nat) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hend : s.ptn[n - 1]! ≤ level) (hsp : split < n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hm : Scratch.Marks n s.stamp s.marks) (hv : Scratch.Marks n s.stamp s.vmarks) : have t := splitSingleton (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 ∧ (CellQueue s.ptn level s.active s.queue → CellQueue t.ptn level t.active t.queue) ∧ cellsPerm s.ptn level t.lab s.lab ∧ Pending n level (fun (a : Nat) => List.count a ((Graph.ofGraph G).row s.lab[split]!)) s.cellend [] t.lab t.ptn ∧ Activation n level s.ptn t.ptn s.active t.active

The complete singleton pass preserves the labelling permutation and partition cache, including all touched cells and uniform-cell returns. Every new boundary is charged once, and inherited closed values are retained literally.

theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_constant {n : Nat} (G : SparseGraph n) (level split : Nat) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hend : s.ptn[n - 1]! ≤ level) (hsp : split < n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hm : Scratch.Marks n s.stamp s.marks) (hv : Scratch.Marks n s.stamp s.vmarks) : have t := splitSingleton (Graph.ofGraph G) level split s; ∀ (a len : Nat), IsCell t.ptn level a len → a + len ≤ n → ∀ (q r : Nat), a ≤ q → q < a + len → a ≤ r → r < a + len → List.count t.lab[q]! ((Graph.ofGraph G).row s.lab[split]!) = List.count t.lab[r]! ((Graph.ofGraph G).row s.lab[split]!)

Every output cell has constant native neighbour count into the captured singleton splitter, including untouched cells and uniform compaction returns.

theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_active {n : Nat} (G : SparseGraph n) (level split : Nat) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hend : s.ptn[n - 1]! ≤ level) (hsp : split < n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hm : Scratch.Marks n s.stamp s.marks) (hv : Scratch.Marks n s.stamp s.vmarks) : have t := splitSingleton (Graph.ofGraph G) level split s; Activation n level s.ptn t.ptn s.active t.active

The full singleton pass satisfies the fragment-activation rule for every original cell, including cells absent from the touched list.

theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_index {n : Nat} (G : SparseGraph n) (level split : Nat) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hend : s.ptn[n - 1]! ≤ level) (hsp : split < n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hm : Scratch.Marks n s.stamp s.marks) (hv : Scratch.Marks n s.stamp s.vmarks) : have t := splitSingleton (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 singleton pass preserves a valid partition cache.