theorem Hex.GraphIso.Nauty.Sparse.array_slice (a : Array Nat) {lo hi : Nat} (hlo : lo ≤ hi) (hhi : hi ≤ a.size) : List.map (fun (e : Nat) => a[e]!) (List.range' lo (hi - lo)) = List.take (hi - lo) (List.drop lo a.toList)

Reading the bounded native interval gives exactly its list slice.

theorem Hex.GraphIso.Nauty.Sparse.Compact.hit_bound {before : Array Nat} {p : Nat → Bool} {first last : Nat} {seen : List Nat} {lab hit : Array Nat} {cut n : Nat} (h : Compact before p first last seen lab hit cut) (hv : ∀ (v : Nat), v ∈ seen → v < n) (v : Nat) : v ∈ hit.toList → v < n

The hit buffer inherits the original labelling's vertex bounds.

theorem Hex.GraphIso.Nauty.Sparse.Compact.scan_slice {before : Array Nat} {p : Nat → Bool} {first last : Nat} {lab hit : Array Nat} {cut : Nat} (h : Compact before p first (first + (last - first)) (List.map (fun (q : Nat) => before[q]!) (List.range' first (last - first))) lab hit cut) (hf : first ≤ last) : Compact before p first last (List.take (last - first) (List.drop first before.toList)) lab hit cut

A completed scan can be read directly as the original cell slice.

theorem Hex.GraphIso.Nauty.Sparse.Compact.preserve {before : Array Nat} {p : Nat → Bool} {first last : Nat} {seen : List Nat} {lab hit : Array Nat} {cut : Nat} {ptn : Array Nat} {level a len : Nat} (h : Compact before p first last seen lab hit cut) (hc : IsCell ptn level first (last - first)) (ha : IsCell ptn level a len) (hne : a ≠ first) : IsCell (if cut ≠ last ∧ cut ≠ first then ptn.setIfInBounds (cut - 1) level else ptn) level a len

Compaction and reinsertion preserve every other cell, independently of which singleton sentinel or activation branch follows the scan.