theorem
Hex.GraphIso.Nauty.Sparse.Comparison.leaf_bounded
{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), ∃ (label : Label n), Label.ofArray? n st.lab = some label ∧ ReturnCodes G.graph cs bs' fs out ∧ Bounded { codes := cs ++ [codeSentinel], graph := G.graph.relabel label.perm } (State.key G.graph bs st)
(State.key G.graph bs' out) ∧ Covers { codes := cs ++ [codeSentinel], graph := G.graph.relabel label.perm } (State.key G.graph bs' out)
The actual discrete classifier and exit satisfy both native fragment bounds: they cover the candidate and install exactly the maximum permitted by that candidate and the incoming incumbent.
theorem
Hex.GraphIso.Nauty.Sparse.Comparison.prune_bounded
{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)
(bound : Key n)
:
A nonterminal code rejection leaves the actual incumbent unchanged, so it satisfies the upper invariant for any enclosing subtree bound.