theorem Hex.GraphIso.Nauty.Sparse.scatter_perm {n : Nat} {ref : Array Nat} {st : State n} {c l : Label n} (hw : st.workperm.size = n) (hc : Label.ofArray? n ref = some c) (hl : Label.ofArray? n st.lab = some l) (v : Fin n) : (scatter ref st).workperm[↑v]! = ↑((l.perm.comp c.perm.inv).get v)

The reusable scatter stores the forward map from the reference leaf to the current leaf. Every old workspace entry is overwritten.

theorem Hex.GraphIso.Nauty.Sparse.scatter_isautom {n : Nat} (G : SparseGraph n) {ref : Array Nat} {st : State n} {c l : Label n} (hw : st.workperm.size = n) (hc : Label.ofArray? n ref = some c) (hl : Label.ofArray? n st.lab = some l) (ha : isautom (Graph.ofGraph G) (scatter ref st).workperm = true) (i j : Fin n) : G.adj ((l.perm.comp c.perm.inv).get i) ((l.perm.comp c.perm.inv).get j) = G.adj i j

An explicit native scan on this workspace establishes adjacency preservation by precisely the permutation emitted by the scatter.