theorem
Hex.GraphIso.Nauty.Max.NodeInput.boundary
{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}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
:
have out := (node first ctx (n + 2) tcLevel fuel f.level f.numcells f.entry).snd;
out.noncheaplevel = f.entry.noncheaplevel ∨ f.level ≤ out.noncheaplevel
An actual call retains its entry boundary or replaces it by a boundary at least as deep as the call, including on the initial descent.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.boundaries
{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}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
:
Every captured ancestor retains its cheap-boundary alternative after the actual node call. No maximum or leaf-coverage premise is required.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.child_boundaries
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
:
have p := { loop := l, state := st, chosen := tv, bs := bs, fs := fs };
have ch := (Parent.child ctx tcLevel p).entry;
∀ (t : Nat) (q : Parent n),
parents.push p t = some q → ch.noncheaplevel = q.state.noncheaplevel ∨ t + 1 ≤ ch.noncheaplevel
Suspending a parent initializes its boundary equality; the actual individualization preserves every older ancestor's boundary alternative.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.recovered_boundaries
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel level : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel first f bs fs parents)
:
Clamping at a resumed sweep preserves the alternative at every strictly older saved parent, even if the child created a deeper boundary.