theorem
Hex.GraphIso.Nauty.Sparse.Touched.eq_of_order
{n stamp : Nat}
{before marks touched : Array Nat}
{seen : List Nat}
{next : Nat}
{old newmarks other : Array Nat}
{visits : List Nat}
(hs : Touched n stamp before marks touched seen)
(ht : Touched n next old newmarks other visits)
(ho : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) touched.toList)
(ho' : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) other.toList)
(hp : seen.Perm visits)
:
A sorted first-touch list is determined by the observed cell multiset, independently of the generation number and retained mark storage.
theorem
Hex.GraphIso.Nauty.Sparse.Touched.neighbors_eq
{n : Nat}
{lab ptn : Array Nat}
{level : Nat}
{starts ends out other final : Array Nat}
{stamp : Nat}
{before marks touched : Array Nat}
{next : Nat}
{old newmarks visits : Array Nat}
(G H : SparseGraph n)
(p : Perm n)
(hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v)
(vertex : Fin n)
(hi : Index.Valid n lab ptn level starts ends)
(hj : Index.Valid n out ptn level other final)
(hp : lab.toList.Perm (List.range n))
(hs : ptn.size = n)
(hend : ptn[n - 1]! ≤ level)
(hc : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab))
(hm : Touched n stamp before marks touched (List.map (fun (v : Nat) => starts[v]!) ((Graph.ofGraph G).row ↑vertex)))
(hn :
Touched n next old newmarks visits (List.map (fun (v : Nat) => other[v]!) ((Graph.ofGraph H).row ↑(p.get vertex))))
(ho : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) touched.toList)
(ho' : List.Pairwise (fun (x1 x2 : Nat) => x1 ≤ x2) visits.toList)
:
Native singleton marking records exactly the same sorted cell starts
under isomorphism, using the executed neighbour scan's Touched contract.