theorem Hex.GraphIso.Nauty.Sparse.Graph.neighbor_mem {n : Nat} (G : SparseGraph n) (i v : Fin n) : ↑v ∈ List.map (ofGraph G).neighbor (List.range' G.offsets[↑i]! (G.offsets[↑i + 1]! - G.offsets[↑i]!)) ↔ G.adj i v = true

Packed neighbour-loop membership is native sparse adjacency.

theorem Hex.GraphIso.Nauty.Sparse.Index.Writes.marked {n : Nat} {before after : Array Nat} {seen : List Nat} {stamp v : Nat} (h : Writes n before after seen (stamp + 1)) (hb : Scratch.Marks n stamp before) (hv : v < n) : after[v]! = stamp + 1 ↔ v ∈ seen

A vertex marked in the new generation occurs in the executed scan.

theorem Hex.GraphIso.Nauty.Sparse.Index.Writes.count {n : Nat} {before after : Array Nat} {seen : List Nat} {stamp v w : Nat} (h : Writes n before after seen (stamp + 1)) (hb : Scratch.Marks n stamp before) (hn : seen.Nodup) (hv : v < n) (hw : w < n) (he : (after[v]! == stamp + 1) = (after[w]! == stamp + 1)) : List.count v seen = List.count w seen

For a simple graph row, equal mark predicates imply equal native counts.