theorem Hex.GraphIso.Nauty.Sparse.Target.Scan.next {n level used first : Nat} {ptn : Array Nat} {out : List Nat} (h : Scan n ptn level used first out) (hu : used < n) (hf : first < n) (ht : first < cellEnd ptn level first) : ∃ (rest : List Nat), nontrivial (cells ptn level n) = out ++ first :: rest

The next nontrivial cell follows exactly the already enumerated starts.

theorem Hex.GraphIso.Nauty.Sparse.Target.Scan.rank {n level used first : Nat} {ptn : Array Nat} {out : List Nat} (h : Scan n ptn level used first out) (hu : used < n) (hf : first < n) (ht : first < cellEnd ptn level first) : List.idxOf first (nontrivial (cells ptn level n)) = out.length

A newly enumerated cell's compact index is its rank in the complete list.

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

Compact cell indices fit in the same n-entry allocation as vertex indices.

theorem Hex.GraphIso.Nauty.Sparse.Target.get_rank {keys : List Nat} {k : Nat} (h : k ∈ keys) : keys[List.idxOf k keys]! = k

Index lookup recovers each listed key, also when other entries repeat.

theorem Hex.GraphIso.Nauty.Sparse.Target.rank_inj {keys : List Nat} {a b : Nat} (ha : a ∈ keys) (hb : b ∈ keys) (he : List.idxOf a keys = List.idxOf b keys) : a = b

Ranks distinguish listed cell starts.

theorem Hex.GraphIso.Nauty.Sparse.Target.rank_get {keys : List Nat} (hn : keys.Nodup) {i : Nat} (hi : i < keys.length) : List.idxOf keys[i]! keys = i