structure Hex.GraphIso.Nauty.Sparse.Touched (n stamp : Nat) (before marks touched : Array Nat) (seen : List Nat) : Prop

A generation-marked scan records each nonsentinel cell exactly once. seen includes all observed keys, including the singleton sentinel.

• initial : Scratch.Marks n stamp before
• writes : Index.Writes n before marks seen (stamp + 1)
• nodup : touched.toList.Nodup
• members (k : Nat) : k ∈ touched.toList ↔ k < n ∧ k ∈ seen

theorem Hex.GraphIso.Nauty.Sparse.Touched.empty {n stamp : Nat} {before : Array Nat} (h : Scratch.Marks n stamp before) : Touched n stamp before before #[] []

theorem Hex.GraphIso.Nauty.Sparse.Touched.marked {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) : marks[k]! = stamp + 1 ↔ k ∈ seen

A current-generation mark is equivalent to prior occurrence in the scan.

theorem Hex.GraphIso.Nauty.Sparse.Touched.present {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) : marks[k]! = stamp + 1 ↔ k ∈ touched.toList

theorem Hex.GraphIso.Nauty.Sparse.Touched.sentinel {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} (h : Touched n stamp before marks touched seen) : Touched n stamp before marks touched (seen ++ [n])

Singleton cells are skipped without touching generation marks.

theorem Hex.GraphIso.Nauty.Sparse.Touched.repeated {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) (hm : marks[k]! = stamp + 1) : Touched n stamp before marks touched (seen ++ [k])

Repeated neighbours of the same cell do not add duplicate work.

theorem Hex.GraphIso.Nauty.Sparse.Touched.fresh {n stamp : Nat} {before marks touched : Array Nat} {seen : List Nat} {k : Nat} (h : Touched n stamp before marks touched seen) (hk : k < n) (hm : marks[k]! ≠ stamp + 1) : Touched n stamp before (marks.setIfInBounds k (stamp + 1)) (touched.push k) (seen ++ [k])

First touch marks the cell and appends it exactly once.