theorem Hex.GraphIso.Nauty.Max.Parent.scatter_cover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {p : Parent n} (h : Valid G ctx tcLevel p) {ref lab γ : Array Nat} {best : Option (Key n)} (hgsz : ctx.g.size = n) (href : ref.size = n) (hcheck : checkAutom ctx.g γ = true) (hfr : cellsPerm (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab ref) (hl : cellsPerm (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab lab) (hmap : ∀ (i : Nat), i < n → γ[ref[i]!]! = lab[i]!) (hchosen : lab[(Loop.prepare ctx tcLevel p.loop).snd.fst.toNat]! = p.chosen) (hcover : Generic.Covers (Loop.key ctx tcLevel p.loop ref[(Loop.prepare ctx tcLevel p.loop).snd.fst.toNat]!) best) : Generic.Covers (Frame.key ctx tcLevel (child ctx tcLevel p)) best

A scatter from a covered reference child covers the entire chosen child of the frozen parent, independently of the emitting leaf's depth.

theorem Hex.GraphIso.Nauty.Max.NodeInput.emit_out {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) : SearchOut G (f.level - 1) f.level f.entry (Frame.emit ctx tcLevel f).snd

The actual leaf action has the same ancestor partition effect as a node call, whether or not it changes the incumbent.

theorem Hex.GraphIso.Nauty.Max.NodeInput.emit_chosen {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) {t : Nat} {p : Parent n} (hp : parents t = some p) : (Frame.emit ctx tcLevel f).snd.lab[(Loop.prepare ctx tcLevel p.loop).snd.fst.toNat]! = p.chosen

A saved ancestor's chosen vertex is retained at every actual emitter.

theorem Hex.GraphIso.Nauty.Max.NodeInput.emit_parent {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) {t : Nat} {p : Parent n} (hp : parents t = some p) : cellsPerm (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab (Frame.emit ctx tcLevel f).snd.lab

The emitting leaf remains within every saved ancestor's cells.

theorem Hex.GraphIso.Nauty.Max.Frame.emit_first {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (f : Frame n) : (emit ctx tcLevel f).snd.firstlab = f.entry.firstlab ∧ (emit ctx tcLevel f).snd.gcaFirst = f.entry.gcaFirst

Leaf processing retains the first reference and its ancestor.

theorem Hex.GraphIso.Nauty.Max.NodeInput.first_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.autoFirst) : have out := (Frame.emit ctx tcLevel f).snd; checkAutom ctx.g out.workperm = true ∧ out.firstlab.size = n ∧ ∀ (i : Nat), i < n → out.workperm[out.firstlab[i]!]! = out.lab[i]!

The actual first-reference verdict supplies its checked scatter, expressed entirely in the emitting state's fields.

theorem Hex.GraphIso.Nauty.Max.NodeInput.first_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.autoFirst) {t : Nat} {p : Parent n} (hp : parents t = some p) (ht : f.entry.gcaFirst = 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 positive first-ancestor return covers that ancestor's entire chosen child from its saved first-reference coverage.

theorem Hex.GraphIso.Nauty.Max.first_exit {n : Nat} (level : Nat) (st : Search n) : (leafExit Generic.Leaf.autoFirst level st).fst = Generic.Exit.unwind (leafExit Generic.Leaf.autoFirst level st).snd.gcaFirst false

Code one returns to the first ancestor without requesting a short prune.

theorem Hex.GraphIso.Nauty.Max.auto_first {n k : Nat} (G : Colored n k) (tcLevel : Nat) : NodeRule G tcLevel false fun (level numcells : Nat) (st : Search n) => verdict G tcLevel level numcells st = Generic.Leaf.autoFirst

The actual first-reference emission satisfies its entire maximum rule, including returns across arbitrarily many intermediate sweeps.