theorem Hex.GraphIso.Nauty.Sparse.canonVerdict_canon {n : Nat} (G : SparseGraph n) {level : Nat} {st out : State n} {l c : Label n} (hauto : canonVerdict (Graph.ofGraph G) level 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) (hR : st.canong.Prefix (G.relabel c.perm) st.samerows) : G.relabel l.perm = G.relabel c.perm ∧ ∀ (v : Fin n), out.workperm[↑v]! = ↑((l.perm.comp c.perm.inv).get v)

A canonical tie uses equal native graphs and emits the forward map from the incumbent label to the current label.

theorem Hex.GraphIso.Nauty.Sparse.classify_canon {n : Nat} (G : SparseGraph n) {level numcells : Nat} {st out : State n} {l c : Label n} (hauto : classify (Graph.ofGraph G) 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) (hR : st.canong.Prefix (G.relabel c.perm) st.samerows) : G.relabel l.perm = G.relabel c.perm ∧ ∀ (v : Fin n), out.workperm[↑v]! = ↑((l.perm.comp c.perm.inv).get v)

Every native canonical-automorphism verdict has these semantics, including the path that first tried a scatter against the first leaf.

theorem Hex.GraphIso.Nauty.Sparse.classify_canon_adj {n : Nat} (G : SparseGraph n) {level numcells : Nat} {st out : State n} {l c : Label n} (hauto : classify (Graph.ofGraph G) 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) (hR : st.canong.Prefix (G.relabel c.perm) st.samerows) (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

Equality established by the canonical row scan implies adjacency preservation by the exact emitted permutation.