theorem Hex.GraphIso.Nauty.Sparse.classify_canon_iso {n k : Nat} (G : Sparse.Colored n k) {level numcells : Nat} {st out : State n} {l c : Label n} (hauto : classify (Graph.ofGraph G.graph) level numcells st = (Generic.Leaf.autoCanon, out)) (hw : st.workperm.size = n) (hl : Label.ofArray? n st.lab = some l) (hc : Label.ofArray? n st.canonlab = some c) (hrl : CellsReach G.toDense st.lab) (hrc : CellsReach G.toDense st.canonlab) (hR : st.canong.Prefix (G.graph.relabel c.perm) st.samerows) : Sparse.IsIso G G (l.perm.comp c.perm.inv) ∧ ∀ (v : Fin n), out.workperm[↑v]! = ↑((l.perm.comp c.perm.inv).get v)

The canonical-row admission emits a colour-preserving automorphism. The statement identifies every entry of the actual emitted workspace.

theorem Hex.GraphIso.Nauty.Sparse.classify_first_scan {n k : Nat} (G : Sparse.Colored n k) {level numcells : Nat} {st out : State n} {l f : Label n} (hauto : classify (Graph.ofGraph G.graph) level numcells st = (Generic.Leaf.autoFirst, out)) (hnc : st.gcaFirst < st.noncheaplevel) (hw : st.workperm.size = n) (hl : Label.ofArray? n st.lab = some l) (hf : Label.ofArray? n st.firstlab = some f) (hrl : CellsReach G.toDense st.lab) (hrf : CellsReach G.toDense st.firstlab) : Sparse.IsIso G G (l.perm.comp f.perm.inv) ∧ ∀ (v : Fin n), out.workperm[↑v]! = ↑((l.perm.comp f.perm.inv).get v)

When the cheap boundary is unavailable, first-reference admission executes the native scan. Its exact scatter is a coloured automorphism.