theorem Hex.GraphIso.Nauty.Sparse.Index.Runs.valid {n first last : Nat} {lab hits starts ends : Array Nat} {level : Nat} {before ptn oldlab oldstarts oldends : Array Nat} (h : Runs n first last (last + 1) lab hits starts ends) (hp : CountPartition level first last lab hits before ptn) (hc : IsCell before level first (last + 1 - first)) (hi : Valid n oldlab before level oldstarts oldends) (he : ∀ (q : Nat), q < first ∨ last < q → ends[q]! = oldends[q]!) (hs : ∀ (q : Nat), q < n → q < first ∨ last < q → starts[lab[q]!]! = oldstarts[oldlab[q]!]!) : Valid n lab ptn level starts ends

Completed run entries and preservation outside the split establish full cache validity for the new partition.