theorem Hex.GraphIso.Nauty.Sparse.bad_nonpos {n : Nat} {g : Graph n} {level numcells : Nat} {st : State n} (h : (classify g level numcells st).fst = Generic.Leaf.bad) : st.compCanon ≤ 0

A native bad verdict cannot follow a positive code comparison.

theorem Hex.GraphIso.Nauty.Sparse.classify_eqlevCanon {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : (classify g level numcells st).snd.eqlevCanon = st.eqlevCanon

Native row classification retains the first divergent code level.

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

A better native verdict occurs only at a discrete leaf.

theorem Hex.GraphIso.Nauty.Sparse.Max.better_target {n level sr target : Nat} {short : Bool} {st : State n} (he : (leafExit (Generic.Leaf.better sr) level st).fst = Generic.Exit.unwind target short) (ht : target < level) : target = st.noncheaplevel - 1

Installing a better leaf resets code agreement to its depth; any strict-ancestor return therefore names the actual cheap boundary.

theorem Hex.GraphIso.Nauty.Sparse.Max.NodeInput.bad {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} {short : Bool} (h : NodeInput G tcLevel f bs fs parents) (hbad : 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.bad) (hexit : (Frame.emit G.graph tcLevel f).fst = Generic.Exit.unwind target short) : MaxResult (Frame.key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (Frame.emit G.graph tcLevel f).snd) (f.level - 1) (Witness G tcLevel parents.frames) (Frame.emit G.graph tcLevel f).fst

Native rejection satisfies the full return contract at discrete and nondiscrete nodes. A nonlocal code return carries a negative prefix; every other nonlocal return propagates coverage through cheap ancestors.

theorem Hex.GraphIso.Nauty.Sparse.Max.NodeInput.better {n k : Nat} {G : Sparse.Colored n k} {tcLevel target sr : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} {short : Bool} (h : NodeInput G tcLevel f bs fs parents) (hbetter : 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.better sr) (hexit : (Frame.emit G.graph tcLevel f).fst = Generic.Exit.unwind target short) : MaxResult (Frame.key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (Frame.emit G.graph tcLevel f).snd) (f.level - 1) (Witness G tcLevel parents.frames) (Frame.emit G.graph tcLevel f).fst

A better native leaf satisfies the full maximum return contract, including its nonlocal cheap-boundary return.

theorem Hex.GraphIso.Nauty.Sparse.Max.NodeInput.emit {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : NodeInput G tcLevel f bs fs parents) (he : (Frame.emit G.graph tcLevel f).fst ≠ Generic.Exit.done) : MaxResult (Frame.key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (Frame.emit G.graph tcLevel f).snd) (f.level - 1) (Witness G tcLevel parents.frames) (Frame.emit G.graph tcLevel f).fst

Every terminal native classifier branch now discharges the complete node return rule under the single assembled traversal context.