theorem Hex.GraphIso.Nauty.SweepPre.child_target {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 tv target : Nat} {first : Bool} {cell : VSet n} {st : Search n} (h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st) (hn0 : 0 < n) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (he : (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).fst = Generic.Exit.unwind target true) (hreceive : level ≤ target) : target = level

A short return received from a child targets exactly this sweep. The node bound rules out a target strictly between adjacent levels.

theorem Hex.GraphIso.Nauty.return_pair {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv target : Nat} {first childFirst : Bool} {cell : VSet n} {st : Search n} {key : Nat → Key n} {best : Option (Key n)} (h : SearchOk G level numcells st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hpath : PathInv G ctx level st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) (hbound : target < level + 1) (he : (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).fst = Generic.Exit.unwind target true) (hi : RunInv G ctx (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd) (hreceive : level ≤ target) (hguide : CanonGuide level tc st key best st) : have raw := (node childFirst ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child first level tc tv st)).snd; have out := { lab := raw.lab, ptn := raw.ptn, active := raw.active, orbits := raw.orbits, fixedpts := raw.fixedpts.erase tv, autos := raw.autos, wsCap := raw.wsCap, firstcode := raw.firstcode, canoncode := raw.canoncode, firsttc := raw.firsttc, firstlab := raw.firstlab, canonlab := raw.canonlab, canong := raw.canong, samerows := raw.samerows, compCanon := raw.compCanon, eqlevFirst := raw.eqlevFirst, eqlevCanon := raw.eqlevCanon, gcaFirst := raw.gcaFirst, gcaCanon := raw.gcaCanon, canonlevel := raw.canonlevel, noncheaplevel := raw.noncheaplevel, allsamelevel := raw.allsamelevel, cosetindex := raw.cosetindex, stabvertex := raw.stabvertex, numnodes := raw.numnodes, tctotal := raw.tctotal, canupdates := raw.canupdates, numorbits := raw.numorbits, numgenerators := raw.numgenerators, numbadleaves := raw.numbadleaves, maxlevel := raw.maxlevel, order := raw.order, genTrace := raw.genTrace, workperm := raw.workperm }; ∀ (pair : VSet n × VSet n), out.autos.back? = some pair → PairOk ctx.g st.ptn st.lab level pair.fst pair.snd

The actual short-return pair is valid at its receiving parent. Canonical scatters use the parent's covered reference; implicit pairs fix the parent path and use its root-stabilization invariant.

theorem Hex.GraphIso.Nauty.SweepPre.return_pair {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 tv target : Nat} {first : Bool} {cell : VSet n} {st : Search n} {key : Nat → Key n} {best : Option (Key n)} (h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st) (hn0 : 0 < n) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (he : (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).fst = Generic.Exit.unwind target true) (hi : RunInv G ctx (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd) (hreceive : level ≤ target) (hguide : CanonGuide level tc st key best st) : have raw := (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd; have out := { lab := raw.lab, ptn := raw.ptn, active := raw.active, orbits := raw.orbits, fixedpts := raw.fixedpts.erase tv, autos := raw.autos, wsCap := raw.wsCap, firstcode := raw.firstcode, canoncode := raw.canoncode, firsttc := raw.firsttc, firstlab := raw.firstlab, canonlab := raw.canonlab, canong := raw.canong, samerows := raw.samerows, compCanon := raw.compCanon, eqlevFirst := raw.eqlevFirst, eqlevCanon := raw.eqlevCanon, gcaFirst := raw.gcaFirst, gcaCanon := raw.gcaCanon, canonlevel := raw.canonlevel, noncheaplevel := raw.noncheaplevel, allsamelevel := raw.allsamelevel, cosetindex := raw.cosetindex, stabvertex := raw.stabvertex, numnodes := raw.numnodes, tctotal := raw.tctotal, canupdates := raw.canupdates, numorbits := raw.numorbits, numgenerators := raw.numgenerators, numbadleaves := raw.numbadleaves, maxlevel := raw.maxlevel, order := raw.order, genTrace := raw.genTrace, workperm := raw.workperm }; ∀ (pair : VSet n × VSet n), out.autos.back? = some pair → PairOk ctx.g st.ptn st.lab level pair.fst pair.snd

Later siblings obtain the target bound from their actual node precondition.

theorem Hex.GraphIso.Nauty.first_return_pair {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv target : Nat} {cell : VSet n} {st : Search n} {key : Nat → Key n} {best : Option (Key n)} (h : SearchOk G level numcells st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hpath : PathInv G ctx level st) (htarget : Generic.Target (fun (st : Search n) => st) level tc cell st) (htv : cell.mem tv = true) (he : (node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).fst = Generic.Exit.unwind target true) (hi : RunInv G ctx (node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).snd) (hreceive : level ≤ target) (hguide : CanonGuide level tc st key best st) : have raw := (node true ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).snd; have out := have __src := afterChildFirst level tv raw; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := raw.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, order := __src.order, genTrace := __src.genTrace, workperm := __src.workperm }; ∀ (pair : VSet n × VSet n), out.autos.back? = some pair → PairOk ctx.g st.ptn st.lab level pair.fst pair.snd

The leftmost first-path child has the same local pair guarantee after its first-path controls and fixed points are cleaned up. No later-sibling precondition is needed at this first entry.

theorem Hex.GraphIso.Nauty.SweepPre.return_cover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel specFuel level numcells tc tv1 tv target len : Nat} {first : Bool} {cell : VSet n} {st : Search n} {key : Nat → Key n} {best : Option (Key n)} {cs : List Nat} {live : Nat → Prop} (h : SweepPre G ctx tcLevel first level numcells tc tv1 (some tv) cell st) (hn0 : 0 < n) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (he : (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).fst = Generic.Exit.unwind target true) (hi : RunInv G ctx (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd) (hreceive : level ≤ target) (hguide : CanonGuide level tc st key best st) (hc : IsCell st.ptn level tc len) (hr : tc + len ≤ n) (hfuel : level + 1 + specFuel ≤ n + 1) (hcover : CellCover ctx tcLevel specFuel level numcells tc len cs st live best) (hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true) (hmem : ∀ (v : Nat), live v → cell.mem v = true) : have raw := (node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Nauty.child first level tc tv st)).snd; have out := { lab := raw.lab, ptn := raw.ptn, active := raw.active, orbits := raw.orbits, fixedpts := raw.fixedpts.erase tv, autos := raw.autos, wsCap := raw.wsCap, firstcode := raw.firstcode, canoncode := raw.canoncode, firsttc := raw.firsttc, firstlab := raw.firstlab, canonlab := raw.canonlab, canong := raw.canong, samerows := raw.samerows, compCanon := raw.compCanon, eqlevFirst := raw.eqlevFirst, eqlevCanon := raw.eqlevCanon, gcaFirst := raw.gcaFirst, gcaCanon := raw.gcaCanon, canonlevel := raw.canonlevel, noncheaplevel := raw.noncheaplevel, allsamelevel := raw.allsamelevel, cosetindex := raw.cosetindex, stabvertex := raw.stabvertex, numnodes := raw.numnodes, tctotal := raw.tctotal, canupdates := raw.canupdates, numorbits := raw.numorbits, numgenerators := raw.numgenerators, numbadleaves := raw.numbadleaves, maxlevel := raw.maxlevel, order := raw.order, genTrace := raw.genTrace, workperm := raw.workperm }; CellCover ctx tcLevel specFuel level numcells tc len cs st (fun (v : Nat) => live v ∧ (shortprune cell out).mem v = true) best

Applying a received short return preserves coverage of the parent's original target cell, using the pair justified by that actual child call.