theorem Hex.GraphIso.Nauty.Sparse.canonVerdict_map {n : Nat} {g : Graph n} {level : Nat} {st : State n} (he : (canonVerdict g level st).fst = Generic.Leaf.autoCanon) (hw : st.workperm.size = n) (hs : st.canonlab.size = n) (hp : st.canonlab.toList.Perm (List.range n)) (i : Nat) : i < n → (canonVerdict g level st).snd.workperm[st.canonlab[i]!]! = st.lab[i]!

A canonical automorphism verdict stores the scatter from the canonical labelling to the current labelling.

theorem Hex.GraphIso.Nauty.Sparse.classify_canon_map {n : Nat} {g : Graph n} {level numcells : Nat} {st : State n} (he : (classify g level numcells st).fst = Generic.Leaf.autoCanon) (hw : st.workperm.size = n) (hs : st.canonlab.size = n) (hp : st.canonlab.toList.Perm (List.range n)) (i : Nat) : i < n → (classify g level numcells st).snd.workperm[st.canonlab[i]!]! = st.lab[i]!

The full classifier's canonical verdict has the same scatter relation, even when it first attempted an unsuccessful first-reference admission.

theorem Hex.GraphIso.Nauty.Sparse.classify_canon_out {n : Nat} {g : Graph n} {level numcells : Nat} {st : State n} (he : (classify g level numcells st).fst = Generic.Leaf.autoCanon) : have out := (classify g level numcells st).snd; out.workperm.size = n → out.canonlab.size = n → out.canonlab.toList.Perm (List.range n) → ∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!

The scatter relation is readable entirely from the classified state; its scratch allocation and canonical reference are the only size premises.