theorem
Hex.GraphIso.Nauty.Sparse.classify_pruned
{n : Nat}
{g : Graph n}
{level numcells : Nat}
{st : State n}
(hnc : numcells ≠ n)
(hbad : (classify g level numcells st).fst = Generic.Leaf.bad)
:
Rejection of a nondiscrete node happens before row comparison and leaves the state supplied to the native leaf exit unchanged.
theorem
Hex.GraphIso.Nauty.Sparse.Max.bad_target
{n level target : Nat}
{short : Bool}
{st : State n}
(he : (leafExit Generic.Leaf.bad level st).fst = Generic.Exit.unwind target short)
:
The native rejected exit chooses either a code-supported return or the explicit cheap boundary. This preserves both actual alternatives.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.prune_code
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel target : Nat}
{f : Frame n}
{frames : Frames n}
{bs fs : List Nat}
{short : Bool}
(h : Valid G f)
(hs : CodeScope G f.codes frames)
(hc : Comparison G.graph f.codes bs fs f.entry)
(hfirst : f.entry.gcaFirst < f.level)
(hcanon : f.entry.gcaCanon < f.level)
(hcheap : 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 →
p.snd.snd.snd.snd.snd.eqlevCanon.toNat ≤ target →
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 frames) (emit G.graph tcLevel f).fst
A code-supported native rejection satisfies the complete maximum return contract, even when it jumps past several intervening callers. The ancestor witness is derived from recorded entries and actual codes.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.prune_target
{n : Nat}
{G : SparseGraph n}
{tcLevel target : Nat}
{f : Frame n}
{short : Bool}
(hexit : (emit G tcLevel f).fst = Generic.Exit.unwind target short)
:
The actual nonterminal rejected dispatch exposes the precise split needed by the code-return and cheap-subtree proofs.