theorem Hex.GraphIso.Nauty.Sparse.Target.row_encode {n : Nat} (G : SparseGraph n) (lab : Array Nat) (s : Scratch) (keys : List Nat) (raw : Array Nat) (h : MapPrefix n lab s.cellstart keys n raw) (l : Label n) (hl : Label.ofArray? n lab = some l) (first : Nat) (hf : first < n) : List.map (fun (e : Nat) => raw[(Graph.ofGraph G).neighbor e]!) (List.range' G.offsets[lab[first]!]! (G.offsets[lab[first]! + 1]! - G.offsets[lab[first]!]!)) = List.map (encode keys n) (row (Graph.ofGraph G) lab s first)

The packed neighbour scan observes precisely the compact encoding of its cached cell-index row.

theorem Hex.GraphIso.Nauty.Sparse.Target.sizes_get {sizes : Array Nat} {keys : List Nat} {degree : Nat → Nat} (h : sizes.toList = List.map degree keys) {i : Nat} (hi : i < keys.length) : sizes[i]! = degree keys[i]!

The parallel size array gives the size of the cell at each compact index.

theorem Hex.GraphIso.Nauty.Sparse.Target.select_map (f left right : Nat → Nat) (state : Nat × Nat) (i : Nat) (h : left i = right (f i)) : Prod.map f id (select left state i) = select right (Prod.map f id state) (f i)

Translating compact indices commutes with each strict score comparison.

theorem Hex.GraphIso.Nauty.Sparse.Target.fold_map (f left right : Nat → Nat) (xs : List Nat) (state : Nat × Nat) (h : ∀ (i : Nat), i ∈ xs → left i = right (f i)) : Prod.map f id (List.foldl (select left) state xs) = List.foldl (select right) (Prod.map f id state) (List.map f xs)

The translated best-so-far state follows the same ordered score fold.

theorem Hex.GraphIso.Nauty.Sparse.Target.row_entries {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level : Nat) (s : Scratch) (hidx : Index.Valid n lab ptn level s.cellstart s.cellend) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (l : Label n) (hl : Label.ofArray? n lab = some l) (first : Nat) (hf : first < n) (k : Nat) : k ∈ row (Graph.ofGraph G) lab s first → k = n ∨ k ∈ nontrivial (cells ptn level n)

Every cell index read from a valid native row is listed or is the singleton sentinel.

theorem Hex.GraphIso.Nauty.Sparse.Target.encoded_score {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level : Nat) (s : Scratch) (hidx : Index.Valid n lab ptn level s.cellstart s.cellend) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (l : Label n) (hl : Label.ofArray? n lab = some l) (first : Nat) (hf : first < n) : have keys := nontrivial (cells ptn level n); List.countP (Join.qualifies (List.map (encode keys n) (row (Graph.ofGraph G) lab s first)) fun (i : Nat) => s.cellend[keys[i]!]! - keys[i]! + 1) (List.range keys.length) = score (Graph.ofGraph G) lab s keys first

Computing scores with compact ranks gives the same native partial-join score.