theorem
Hex.GraphIso.Nauty.Max.Frame.emit_noncheap
{n : Nat}
(ctx : Ctx n)
(tcLevel : Nat)
(f : Frame n)
:
The emitting action retains the node entry's noncheap boundary.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.cheap_witness
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
{target : Nat}
{best : Option (Key n)}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
(hbelow : target < f.level - 1)
(hcheap : f.entry.noncheaplevel ≤ target + 1)
(hcover : Generic.Covers (Frame.key ctx tcLevel f) best)
(hgrows : Generic.Grows (SearchState.key ctx bs f.entry) best)
(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)
:
Witness ctx tcLevel (Parents.frames ctx tcLevel parents) target best
At any depth below a cheap boundary, coverage of the emitting node extends through the saved parents to the entire interrupted ancestor.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.cheap_leaf
{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)
(hd : (prepareOther ctx tcLevel f.level f.numcells f.entry).fst = n)
(hexit : (Frame.emit ctx tcLevel f).fst = Generic.Exit.unwind target short)
(hcheap : target = (Frame.emit ctx tcLevel f).snd.noncheaplevel - 1)
(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
An actual discrete emission returning to its cheap boundary satisfies the maximum contract at arbitrary depth, for either short-prune flag.