theorem
Hex.GraphIso.Nauty.Max.SweepInput.unwind_keeps
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel : 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}
(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))
(next : Generic.SweepFn (Search n) n)
(hvisit : (!first || st.orbits[tv]! == tv) = true)
(hcall :
Nauty.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)
:
A nonlocal child return preserves accumulated generators at exactly the older first frames that survive its unchanged exit.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.received_keeps
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel : Nat}
{first short : Bool}
{level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st out : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h :
SweepInput G { g := rowsOf G } tcLevel fuel (cfuel + 1) 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))
(hs : (contract G tcLevel).sweepValid fuel cfuel (Generic.sweepCall { g := rowsOf G } (n + 2) tcLevel fuel cfuel))
(hvisit : (!first || st.orbits[tv]! == tv) = true)
(hcall :
Nauty.node (first && tv == tv1) { g := rowsOf G } (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(child first level tc tv st) = (Generic.Exit.unwind level short, out))
:
Reception derives its generator inputs from the child contract and then preserves the entire trace returned by the actual resumed suffix.
theorem
Hex.GraphIso.Nauty.Max.sweep_trace
{n k : Nat}
(G : Colored n k)
(tcLevel : Nat)
:
SweepTraceRule G tcLevel
Both sweep branches preserve accumulated generators in the same induction as their maximum result, with no additional recursive premise.