theorem Hex.GraphIso.Nauty.Sparse.Graph.row_eq {n : Nat} (G : SparseGraph n) (v : Fin n) : (ofGraph G).row ↑v = List.map Fin.val (G.nbrs v).toList

The executed native row scan retains exactly the packed neighbour order.

theorem Hex.GraphIso.Nauty.Sparse.Graph.row_nodup {n : Nat} (G : SparseGraph n) (v : Fin n) : ((ofGraph G).row ↑v).Nodup

Native simple graph rows cannot count a vertex twice.

theorem Hex.GraphIso.Nauty.Sparse.Graph.row_bound {n : Nat} (G : SparseGraph n) (v : Fin n) (j : Nat) : j ∈ (ofGraph G).row ↑v → j < n

theorem Hex.GraphIso.Nauty.Sparse.Graph.row_count {n : Nat} (G : SparseGraph n) (u v : Fin n) : List.count (↑v) ((ofGraph G).row ↑u) = if G.adj u v = true then 1 else 0

One native row contributes exactly its adjacency indicator.

theorem Hex.GraphIso.Nauty.Sparse.Graph.count_vertices {n : Nat} (G : SparseGraph n) (vertices : List (Fin n)) (v : Fin n) : List.count (↑v) (List.flatMap (fun (u : Fin n) => (ofGraph G).row ↑u) vertices) = (List.filter (fun (u : Fin n) => G.adj u v) vertices).length

Summing native row counts counts precisely the adjacent splitter vertices.

theorem Hex.GraphIso.Nauty.Sparse.Graph.count_rows {n : Nat} (G : SparseGraph n) (lab : Array Nat) (hp : lab.toList.Perm (List.range n)) (positions : List Nat) (hb : ∀ (q : Nat), q ∈ positions → q < n) (v : Nat) : List.count v (List.flatMap (fun (q : Nat) => (ofGraph G).row lab[q]!) positions) ≤ positions.length

Each splitter vertex contributes at most one to a neighbour's count.

theorem Hex.GraphIso.Nauty.Sparse.CountScan.cells {lab ptn starts ends before marks touched hits : Array Nat} {n stamp level : Nat} (G : SparseGraph n) (positions : List Nat) (h : CountScan n stamp before marks touched starts hits (List.flatMap (fun (q : Nat) => (Graph.ofGraph G).row lab[q]!) positions)) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Index.Valid n lab ptn level starts ends) (hb : ∀ (q : Nat), q ∈ positions → q < n) (a : Nat) : a ∈ touched.toList → IsCell ptn level a (ends[a]! + 1 - a) ∧ a < ends[a]! ∧ ends[a]! < n ∧ ∀ (q : Nat), a ≤ q → q ≤ ends[a]! → hits[lab[q]!]! ≤ positions.length

Every touched key names a complete original cell, and every count in that cell is bounded by the number of traversed splitter vertices.