theorem Hex.GraphIso.Nauty.Sparse.perm_position {lab : Array Nat} {n v : Nat} (hp : lab.toList.Perm (List.range n)) (hv : v < n) : ∃ (q : Nat), q < n ∧ lab[q]! = v

Every vertex has a position in a labelling permutation.

theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.vertex_le {lab ptn starts ends : Array Nat} {n level v : Nat} (h : Valid n lab ptn level starts ends) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hp : lab.toList.Perm (List.range n)) (hv : v < n) : starts[v]! ≤ n

Native vertex lookup is bounded even when the caller has no inverse label array; the singleton sentinel is the only permitted value equal to n.

theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.vertex_cell {lab ptn starts ends : Array Nat} {n level v : Nat} (h : Valid n lab ptn level starts ends) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hp : lab.toList.Perm (List.range n)) (hv : v < n) (hne : starts[v]! ≠ n) : have a := starts[v]!; have b := ends[a]!; IsCell ptn level a (b + 1 - a) ∧ a < b ∧ b < n

Every nonsentinel native vertex lookup identifies a bounded nontrivial cell, providing the bounds used by first-touch clearing.