theorem
Hex.GraphIso.Nauty.Max.SweepInput.unwind
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel inf : Nat}
{first short : Bool}
{level numcells tc tv1 tv index target : Nat}
{cell : VSet n}
{st out : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
{descend : Generic.NodeFn (Search n)}
{next : Generic.SweepFn (Search n) n}
(h : SweepInput G ctx tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hvisit : (!first || st.orbits[tv]! == tv) = true)
(hcall :
descend (first && tv == tv1) (level + 1) (numcells + 1) (child first level tc tv st) = (Generic.Exit.unwind target short, out))
(ht : target < level)
(hr :
have p := { loop := l, state := st, chosen := tv, bs := bs, fs := fs };
Generic.Result (Frame.key ctx tcLevel (Parent.child ctx tcLevel p))
(SearchState.key ctx bs (Parent.child ctx tcLevel p).entry) (SearchState.best ctx out) level
(Witness ctx tcLevel (Parents.frames ctx tcLevel (parents.push p))) (Generic.Exit.unwind target short))
:
have result := Generic.sweepStep inf descend next first level numcells tc tv1 tv cell index st;
Generic.Result (Loop.bound ctx tcLevel l) (SearchState.key ctx bs st) (SearchState.best ctx result.snd.snd) level
(Witness ctx tcLevel ((Parents.frames ctx tcLevel parents).insert l.node)) result.fst
An actual sweep propagates a child's nonlocal witness through first-child cleanup, with the same incumbent and the full chosen-cell upper bound.
theorem
Hex.GraphIso.Nauty.Max.Loop.receive
{n : Nat}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
{parents : Parents n}
{before after : Option (Key n)}
{short : Bool}
(hl : 1 ≤ l.node.level)
(h :
Generic.Result (bound ctx tcLevel l) before after l.node.level
(Witness ctx tcLevel ((Parents.frames ctx tcLevel parents).insert l.node))
(Generic.Exit.unwind (l.node.level - 1) short))
:
Generic.Covers (Frame.key ctx tcLevel l.node) after
At the cheap boundary's node, the returning sweep's witness becomes coverage of the node's full specification, independent of target hints.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.child_result
{n k : Nat}
{G : Colored n k}
{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 { g := rowsOf G } tcLevel fuel cfuel first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
:
have ctx := { g := rowsOf G };
have p := { loop := l, state := st, chosen := tv, bs := bs, fs := fs };
have result :=
Nauty.node (first && tv == tv1) ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st);
Generic.Result (Frame.key ctx tcLevel (Parent.child ctx tcLevel p))
(SearchState.key ctx bs (Parent.child ctx tcLevel p).entry) (SearchState.best ctx result.snd) level
(Witness ctx tcLevel (Parents.frames ctx tcLevel (parents.push p))) result.fst
Constructing the complete child input specializes the smaller-call contract to this sweep's actual descent and frozen ancestor table.
theorem
Hex.GraphIso.Nauty.Max.visit_unwind
{n k : Nat}
(G : Colored n k)
(tcLevel fuel cfuel : Nat)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
(first short : Bool)
(level numcells tc tv1 tv index target : Nat)
(cell : VSet n)
(st out : Search n)
(hvisit : (!first || st.orbits[tv]! == tv) = true)
(hcall :
node (first && tv == tv1) { g := rowsOf G } (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(child first level tc tv st) = (Generic.Exit.unwind target short, out))
(ht : target < level)
:
(keyContract G tcLevel).sweepPost fuel (cfuel + 1) first level numcells tc tv1 (some tv) cell index st
(Generic.sweepStep (n + 2) (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel)
(Generic.sweepCall { g := rowsOf G } (n + 2) tcLevel fuel cfuel) first level numcells tc tv1 tv cell index st)
An actual visited child returning past this sweep supplies the maximum contract directly from its smaller-call induction hypothesis.