theorem
Hex.GraphIso.Nauty.Sparse.Comparison.leaf_returned
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G.graph cs bs fs st)
(hh : RouteHistory G.graph tcLevel cs.length cs.length n st)
(hi : TraceReady G tcLevel cs.length n st)
(hn : 0 < n)
(hl : 1 ≤ cs.length)
:
have verdict := classify (Graph.ofGraph G.graph) cs.length n st;
have out := (leafExit verdict.fst cs.length verdict.snd).snd;
∃ (bs' : List Nat), ∃ (l : Label n), ∃ (c : Label n), Label.ofArray? n st.lab = some l ∧ Label.ofArray? n st.canonlab = some c ∧ ReturnCodes G.graph cs bs' fs out ∧ State.key G.graph bs' out = some
({ codes := bs ++ [codeSentinel], graph := G.graph.relabel c.perm }.max
{ codes := cs ++ [codeSentinel], graph := G.graph.relabel l.perm })
The actual discrete exit returns settled comparisons and the exact local maximum. First-reference admission obtains its full key from the retained selected and guided histories, including the terminal sentinel.
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.prune_returned
{n : Nat}
{G : SparseGraph n}
{numcells : Nat}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G cs bs fs st)
(hnc : numcells ≠ n)
(hbad : (classify (Graph.ofGraph G) cs.length numcells st).fst = Generic.Leaf.bad)
:
A nonterminal code rejection returns settled machines and leaves the actual incumbent unchanged.
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.exit_returned
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel numcells : Nat}
{cs bs fs : List Nat}
{st : State n}
(h : Comparison G.graph cs bs fs st)
(hh : RouteHistory G.graph tcLevel cs.length cs.length numcells st)
(hi : TraceReady G tcLevel cs.length numcells st)
(hn : 0 < n)
(hl : 1 ≤ cs.length)
(hexit : (classify (Graph.ofGraph G.graph) cs.length numcells st).fst ≠ Generic.Leaf.internal)
:
Every terminal native classification returns recoverable comparisons and preserves or increases the incumbent, including internal code rejection.