theorem Hex.GraphIso.Nauty.Sparse.Index.cover {ptn : Array Nat} {n level i : Nat} (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : i < n) : ∃ (a : Nat), ∃ (len : Nat), IsCell ptn level a len ∧ a + len ≤ n ∧ a ≤ i ∧ i < a + len

Every position of a closed partition belongs to a bounded maximal cell.

theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.end_eq {lab ptn starts ends : Array Nat} {n level a : Nat} (h : Valid n lab ptn level starts ends) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : a < n) (hstart : a = 0 ∨ ptn[a - 1]! ≤ level) : ends[a]! = cellEnd ptn level a

A valid cache's endpoint agrees with the independent partition walk.

theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.start_le {lab ptn starts ends : Array Nat} {n level i : Nat} (h : Valid n lab ptn level starts ends) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : i < n) : starts[lab[i]!]! ≤ n

Vertex indices are either bounded cell starts or the singleton sentinel.

theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.nontrivial {lab ptn starts ends : Array Nat} {n level i : Nat} (h : Valid n lab ptn level starts ends) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : i < n) (hne : starts[lab[i]!]! ≠ n) : have a := starts[lab[i]!]!; have b := ends[a]!; IsCell ptn level a (b + 1 - a) ∧ a < b ∧ b < n ∧ a ≤ i ∧ i ≤ b

A nonsentinel index identifies the complete nontrivial cell containing that labelled vertex, including all bounds for subsequent array accesses.