theorem Hex.GraphIso.Nauty.Sparse.CellCut.left {ptn : Array Nat} {level first cut last : Nat} (h : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hb : cut - 1 < ptn.size) : IsCell (ptn.setIfInBounds (cut - 1) level) level first (cut - first)

theorem Hex.GraphIso.Nauty.Sparse.CellCut.right {ptn : Array Nat} {level first cut last : Nat} (h : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hb : cut - 1 < ptn.size) : IsCell (ptn.setIfInBounds (cut - 1) level) level cut (last - cut)

theorem Hex.GraphIso.Nauty.Sparse.CellCut.outside {ptn : Array Nat} {level first cut last a len : Nat} (h : IsCell (ptn.setIfInBounds (cut - 1) level) level a len) (hf : first < cut) (hl : cut < last) (ho : a + len ≤ first ∨ last ≤ a) : IsCell ptn level a len

A cut leaves every disjoint cell's boundary values unchanged.

theorem Hex.GraphIso.Nauty.Sparse.CellCut.preserve {ptn : Array Nat} {level first cut last a len : Nat} (h : IsCell ptn level a len) (hf : first < cut) (hl : cut < last) (ho : a + len ≤ first ∨ last ≤ a) : IsCell (ptn.setIfInBounds (cut - 1) level) level a len

A cut inside one cell preserves the partition contract of every disjoint cell, including its open interior and both closed endpoints.

theorem Hex.GraphIso.Nauty.Sparse.CellCut.cells {ptn : Array Nat} {level first cut last a len : Nat} (h : IsCell ptn level first (last - first)) (hf : first < cut) (hl : cut < last) (hb : cut - 1 < ptn.size) (ha : IsCell (ptn.setIfInBounds (cut - 1) level) level a len) : (a + len ≤ first ∨ last ≤ a) ∧ IsCell ptn level a len ∨ a = first ∧ len = cut - first ∨ a = cut ∧ len = last - cut

One boundary write replaces precisely its original cell by the two fragments; all other cells retain their original boundary contract.