theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.emit_noncheap {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) : (emit G tcLevel f).snd.noncheaplevel = f.entry.noncheaplevel

The exact native preparation and leaf action retain the entry's cheap boundary, including code rejection and both automorphism exits.

theorem Hex.GraphIso.Nauty.Sparse.Max.Scope.cheap_witness {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {f : Frame n} {bs : List Nat} {st : State n} {parents : Parents n} {best : Option (Key n)} (h : Scope G tcLevel f bs st parents) (hbelow : target < f.level - 1) (hcheap : st.noncheaplevel ≤ target + 1) (hcover : Covers (Frame.key G.graph tcLevel f) best) (hgrows : Grows (State.key G.graph bs st) best) : Witness G tcLevel parents.frames target best

Coverage of the emitting node propagates across every interrupted cheap ancestor. Each step uses its actual selected child or a previously covered negative-comparison branch, with incumbent growth retaining that earlier coverage. The witness names the exact receiving ancestor.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.cheap_leaf {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} {short : Bool} (h : Valid G f) (hs : Scope G tcLevel f bs f.entry parents) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (hc : Comparison G.graph f.codes bs fs f.entry) (hd : (prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).fst = n) (hfirst : f.entry.gcaFirst < f.level) (hcanon : f.entry.gcaCanon < f.level) (hbound : f.entry.noncheaplevel ≤ f.level) (hexit : (emit G.graph tcLevel f).fst = Generic.Exit.unwind target short) (hcheap : target = (emit G.graph tcLevel f).snd.noncheaplevel - 1) : 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

An actual discrete emission returning to its cheap boundary satisfies the full maximum contract at arbitrary depth and for either short flag.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.prune {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} {short : Bool} (h : Valid G f) (hs : Scope G tcLevel f bs f.entry parents) (hc : Comparison G.graph f.codes bs fs f.entry) (hfirst : f.entry.gcaFirst < f.level) (hcanon : f.entry.gcaCanon < f.level) (hbound : f.entry.noncheaplevel ≤ f.level) (hexit : (emit G.graph tcLevel f).fst = Generic.Exit.unwind target short) : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; p.fst ≠ n → (classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.bad → 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

Every actual nondiscrete rejection satisfies the complete return contract. The return coordinate selects either the recorded code-prefix witness or coverage propagated across its interrupted cheap ancestors.