theorem Hex.GraphIso.Nauty.Sparse.Max.canon_discrete {n : Nat} {g : Graph n} {level numcells : Nat} {st : State n} (h : (classify g level numcells st).fst = Generic.Leaf.autoCanon) : numcells = n

The native canonical automorphism verdict is necessarily discrete.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.emit_canon {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {f : Frame n} (ha : have p := prepareOther (Graph.ofGraph G) tcLevel f.level f.numcells f.entry; (classify (Graph.ofGraph G) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) : (emit G tcLevel f).snd.canonlab = f.entry.canonlab ∧ (emit G tcLevel f).snd.gcaCanon = f.entry.gcaCanon

The canonical verdict retains the reference and its ancestor through the actual preparation, native classifier, orbit update and leaf action.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.canon_scatter {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} (h : Valid G f) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (ha : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; (classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) : have out := (emit G.graph tcLevel f).snd; Automorphism G out.workperm ∧ out.canonlab.size = n ∧ ∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!

The actual canonical-reference emission retains its native checked scatter, including classification after a failed first-reference scan.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.auto_canon {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} {short : Bool} (h : Valid G f) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (hc : Comparison G.graph f.codes bs fs f.entry) (hs : Scope G tcLevel f bs f.entry parents) (hg : Guides G.graph tcLevel f.entry parents) (hpos : 0 < f.entry.gcaCanon) (hlt : f.entry.gcaCanon < f.level) (ha : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; (classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) (hexit : (emit G.graph tcLevel f).fst = Generic.Exit.unwind f.entry.gcaCanon short) : MaxResult (key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (emit G.graph tcLevel f).snd) (f.level - 1) (Max.Witness G tcLevel parents.frames) (emit G.graph tcLevel f).fst

A canonical automorphism returning to its canonical ancestor satisfies the full maximum contract for either short flag. The separate coset return to an earlier first ancestor has a different coverage argument.