theorem Hex.GraphIso.Nauty.Sparse.Target.ordered (ptn : Array Nat) (level n : Nat) : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) (nontrivial (cells ptn level n))

The nontrivial-cell list is strictly increasing, so its order also fixes ties.

theorem Hex.GraphIso.Nauty.Sparse.Target.nodup (ptn : Array Nat) (level n : Nat) : (nontrivial (cells ptn level n)).Nodup

theorem Hex.GraphIso.Nauty.Sparse.Target.mem_iff {cs : List (Nat × Nat)} {a : Nat} : a ∈ nontrivial cs ↔ ∃ (b : Nat), (a, b) ∈ cs ∧ a < b

theorem Hex.GraphIso.Nauty.Sparse.Target.bound {ptn : Array Nat} {n level a : Nat} (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : a ∈ nontrivial (cells ptn level n)) : a < n

theorem Hex.GraphIso.Nauty.Sparse.Target.cell_mem {ptn : Array Nat} {n level a len : Nat} (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hc : IsCell ptn level a len) (hb : a + len ≤ n) : (a, a + len - 1) ∈ cells ptn level n

Every bounded maximal cell is one of the cells enumerated by the walk.

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

Every nonsentinel vertex index is an enumerated nontrivial cell start.

theorem Hex.GraphIso.Nauty.Sparse.Target.vertex_index {lab ptn starts ends : Array Nat} {n level : Nat} (h : Index.Valid n lab ptn level starts ends) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (l : Label n) (hl : Label.ofArray? n lab = some l) (v : Fin n) : starts[↑v]! = n ∨ starts[↑v]! ∈ nontrivial (cells ptn level n)

A checked labelling makes every native vertex lookup a cell start or the singleton sentinel; the count loops need no stronger scratch hypothesis.