theorem Hex.GraphIso.Nauty.Max.canon_discrete {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (h : (classify ctx level numcells st).fst = Generic.Leaf.autoCanon) : numcells = n

Code two occurs only after refinement reaches a discrete partition.

theorem Hex.GraphIso.Nauty.Max.Frame.emit_canon {n : Nat} {ctx : Ctx n} {tcLevel : Nat} {f : Frame n} (hauto : have p := prepareOther ctx tcLevel f.level f.numcells f.entry; (classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) : (emit ctx tcLevel f).snd.canonlab = f.entry.canonlab ∧ (emit ctx tcLevel f).snd.gcaCanon = f.entry.gcaCanon

A canonical admission retains its reference labelling and ancestor.

theorem Hex.GraphIso.Nauty.Max.NodeInput.canon_scatter {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel fuel false f bs fs parents) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hauto : have p := prepareOther ctx tcLevel f.level f.numcells f.entry; (classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) : have out := (Frame.emit ctx tcLevel f).snd; checkAutom ctx.g out.workperm = true ∧ out.canonlab.size = n ∧ ∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!

The actual canonical verdict supplies its checked scatter, including classification after a failed first-reference scan.

theorem Hex.GraphIso.Nauty.Max.NodeInput.canon_cover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G ctx tcLevel fuel false f bs fs parents) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hauto : have p := prepareOther ctx tcLevel f.level f.numcells f.entry; (classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) {t : Nat} {p : Parent n} (hp : parents t = some p) (ht : f.entry.gcaCanon = t) (hg : Generic.Grows (SearchState.key ctx bs f.entry) (SearchState.best ctx (Frame.emit ctx tcLevel f).snd)) : Generic.Covers (Frame.key ctx tcLevel (Parent.child ctx tcLevel p)) (SearchState.best ctx (Frame.emit ctx tcLevel f).snd)

A canonical-ancestor return covers the interrupted child using its already covered reference child and the actual emitting scatter.

theorem Hex.GraphIso.Nauty.Max.NodeInput.canon_return {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} {short : Bool} (h : NodeInput G ctx tcLevel fuel false f bs fs parents) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hauto : have p := prepareOther ctx tcLevel f.level f.numcells f.entry; (classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) (he : (Frame.emit ctx tcLevel f).fst = Generic.Exit.unwind f.entry.gcaCanon short) : Generic.Result (Frame.key ctx tcLevel f) (SearchState.key ctx bs f.entry) (SearchState.best ctx (Frame.emit ctx tcLevel f).snd) (f.level - 1) (Witness ctx tcLevel (Parents.frames ctx tcLevel parents)) (Frame.emit ctx tcLevel f).fst

Both short flags and both orbit-count outcomes are covered when code two selects the canonical ancestor as its return target.