theorem Hex.GraphIso.Nauty.Max.SweepInput.received_result {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)) : have ctx := { g := rowsOf G }; have middle := if (first && tv == tv1) = true then afterChildFirst level tv1 out else out; have left := { lab := middle.lab, ptn := middle.ptn, active := middle.active, orbits := middle.orbits, fixedpts := middle.fixedpts.erase tv, autos := middle.autos, wsCap := middle.wsCap, firstcode := middle.firstcode, canoncode := middle.canoncode, firsttc := middle.firsttc, firstlab := middle.firstlab, canonlab := middle.canonlab, canong := middle.canong, samerows := middle.samerows, compCanon := middle.compCanon, eqlevFirst := middle.eqlevFirst, eqlevCanon := middle.eqlevCanon, gcaFirst := middle.gcaFirst, gcaCanon := middle.gcaCanon, canonlevel := middle.canonlevel, noncheaplevel := middle.noncheaplevel, allsamelevel := middle.allsamelevel, cosetindex := middle.cosetindex, stabvertex := middle.stabvertex, numnodes := middle.numnodes, tctotal := middle.tctotal, canupdates := middle.canupdates, numorbits := middle.numorbits, numgenerators := middle.numgenerators, numbadleaves := middle.numbadleaves, maxlevel := middle.maxlevel, order := middle.order, genTrace := middle.genTrace, workperm := middle.workperm }; have ready := recover (n + 2) level left; (first = true → ∀ (γ : Array Nat), γ ∈ ready.genTrace → CellStab (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab γ) → (∀ (t : Nat) (p : Parent n), parents t = some p → p.loop.first = true → ∀ (γ : Array Nat), γ ∈ ready.genTrace → CellStab p.state.ptn t p.state.lab γ) → have result := Generic.sweepStep (n + 2) (Generic.nodeCall ctx (n + 2) tcLevel fuel) (Generic.sweepCall ctx (n + 2) tcLevel fuel cfuel) 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

The actual received child and suffix compose with the identical semantic incumbent at recovery, including incumbent installation.

theorem Hex.GraphIso.Nauty.Max.SweepInput.visit {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 + 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) (hreturn : ∀ (short : Bool) (out : Search n), 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) → have ctx := { g := rowsOf G }; have middle := if (first && tv == tv1) = true then afterChildFirst level tv1 out else out; have left := { lab := middle.lab, ptn := middle.ptn, active := middle.active, orbits := middle.orbits, fixedpts := middle.fixedpts.erase tv, autos := middle.autos, wsCap := middle.wsCap, firstcode := middle.firstcode, canoncode := middle.canoncode, firsttc := middle.firsttc, firstlab := middle.firstlab, canonlab := middle.canonlab, canong := middle.canong, samerows := middle.samerows, compCanon := middle.compCanon, eqlevFirst := middle.eqlevFirst, eqlevCanon := middle.eqlevCanon, gcaFirst := middle.gcaFirst, gcaCanon := middle.gcaCanon, canonlevel := middle.canonlevel, noncheaplevel := middle.noncheaplevel, allsamelevel := middle.allsamelevel, cosetindex := middle.cosetindex, stabvertex := middle.stabvertex, numnodes := middle.numnodes, tctotal := middle.tctotal, canupdates := middle.canupdates, numorbits := middle.numorbits, numgenerators := middle.numgenerators, numbadleaves := middle.numbadleaves, maxlevel := middle.maxlevel, order := middle.order, genTrace := middle.genTrace, workperm := middle.workperm }; have ready := recover (n + 2) level left; (first = true → ∀ (γ : Array Nat), γ ∈ ready.genTrace → CellStab (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab γ) ∧ ∀ (t : Nat) (p : Parent n), parents t = some p → p.loop.first = true → ∀ (γ : Array Nat), γ ∈ ready.genTrace → CellStab p.state.ptn t p.state.lab γ) : have ctx := { g := rowsOf G }; have result := Generic.sweepStep (n + 2) (Generic.nodeCall ctx (n + 2) tcLevel fuel) (Generic.sweepCall ctx (n + 2) tcLevel fuel cfuel) 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

Every actual visiting branch satisfies the maximum contract once received generators stabilize the current and suspended first frames.