theorem
Hex.GraphIso.Nauty.Max.classify_eqlevCanon
{n : Nat}
(ctx : Ctx n)
(level numcells : Nat)
(st : Search n)
:
Row classification retains the frozen equal-code level.
theorem
Hex.GraphIso.Nauty.Max.bad_target
{n level target : Nat}
{short : Bool}
{st : Search n}
(he : (leafExit Generic.Leaf.bad level st).fst = Generic.Exit.unwind target short)
:
A rejected leaf retains the sharp choice between the code comparison and the cheap boundary in its actual return target.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.bad_bound
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel false f bs fs parents)
(hbad :
have p := prepareOther ctx tcLevel f.level f.numcells f.entry;
(classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.bad)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
:
Generic.Bounded (Frame.key ctx tcLevel f) (SearchState.key ctx bs f.entry)
(SearchState.best ctx (Frame.emit ctx tcLevel f).snd) ∧ Generic.Covers (Frame.key ctx tcLevel f) (SearchState.best ctx (Frame.emit ctx tcLevel f).snd)
An actual rejected node covers its own full subtree and retains the fragment upper bound, whether rejection happens before or at a leaf.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.bad_result
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
{target : Nat}
{short : Bool}
(h : NodeInput G ctx tcLevel fuel false f bs fs parents)
(hbad :
have p := prepareOther ctx tcLevel f.level f.numcells f.entry;
(classify ctx f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.bad)
(hexit : (Frame.emit ctx tcLevel f).fst = Generic.Exit.unwind target short)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
:
Generic.Result (Frame.key ctx tcLevel f) (SearchState.key ctx bs f.entry)
(SearchState.best ctx (Frame.emit ctx tcLevel f).snd) (f.level - 1)
(Witness ctx tcLevel (Parents.frames ctx tcLevel parents)) (Frame.emit ctx tcLevel f).fst
Both row rejection and nonterminal code rejection satisfy the complete emitting rule, with code-supported and cheap returns kept distinct.
The rejection rule discharges the whole node obligation, including row rejection, frozen code pruning, and arbitrary-depth cheap returns.