def Hex.GraphIso.Nauty.EarlyReturn {n : Nat} (ctx : Ctx n) (target : Nat) (short : Bool) (out : Search n) : Prop

An off-path return retains its emitting classification and state until an enclosing sweep receives it. Only fixed-point cleanup intervenes.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.EarlyReturn.leave {n : Nat} {ctx : Ctx n} {target tv : Nat} {short : Bool} {st : Search n} (h : EarlyReturn ctx target short st) : EarlyReturn ctx target short { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts.erase tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm }

Removing an individualized point preserves the unconsumed emission.

theorem Hex.GraphIso.Nauty.node_early {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) {target : Nat} {short : Bool} (he : (node false ctx inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target short) (ht : target < level - 1) : EarlyReturn ctx target short (node false ctx inf tcLevel fuel level numcells st).snd

An off-path node returning past its immediate receiver supplies its actual leaf origin for either short-flag value.

theorem Hex.GraphIso.Nauty.node_short_early {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) {target : Nat} (he : (node false ctx inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target true) : EarlyReturn ctx target true (node false ctx inf tcLevel fuel level numcells st).snd

Every short off-path return retains its actual leaf origin, even when its immediate parent receives it. Exhausted sweeps return false.

theorem Hex.GraphIso.Nauty.node_same {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : (node false ctx inf tcLevel fuel level numcells st).snd.allsamelevel = st.allsamelevel

Off-path search preserves the all-same boundary exactly.

theorem Hex.GraphIso.Nauty.leafExit_floor {n : Nat} (leaf : Leaf) (level : Nat) (st : Search n) (bound target : Nat) (short : Bool) : have out := leafExit leaf level st; bound ≤ out.snd.gcaFirst → bound ≤ out.snd.gcaCanon → bound < out.snd.noncheaplevel → bound < out.snd.allsamelevel → out.fst = Generic.Exit.unwind target short → bound ≤ target

The two ancestor counters and two pruning boundaries bound every leaf return from below. The bounds are stated on the emitted state.

theorem Hex.GraphIso.Nauty.EarlyReturn.floor {n : Nat} {ctx : Ctx n} {target bound : Nat} {short : Bool} {out : Search n} (h : EarlyReturn ctx target short out) (hf : bound ≤ out.gcaFirst) (hc : bound ≤ out.gcaCanon) (hn : bound < out.noncheaplevel) (ha : bound < out.allsamelevel) : bound ≤ target

Above both pruning boundaries, an unconsumed return cannot cross either ancestor counter. This applies to short and non-short exits.

theorem Hex.GraphIso.Nauty.node_floor {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells bound target : Nat} {st : Search n} {short : Bool} (hb : bound < level) (hf : bound ≤ st.gcaFirst) (hc : bound ≤ st.gcaCanon) (hn : bound < st.noncheaplevel) (ha : bound < st.allsamelevel) (he : (node false ctx inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target short) : bound ≤ target

An actual off-path call cannot cross an ancestor above both pruning boundaries. All four output bounds follow from the call's entry state.

theorem Hex.GraphIso.Nauty.NodePre.return_eq {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel fuel level numcells target : Nat} {short : Bool} {st : Search n} (h : NodePre G ctx tcLevel level numcells st) (hf : level - 1 ≤ st.gcaFirst) (hc : level - 1 ≤ st.gcaCanon) (hn : level - 1 < st.noncheaplevel) (ha : level - 1 < st.allsamelevel) (he : (node false ctx inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target short) : target = level - 1

A valid visit below a first-path receiver returns to that receiver when it lies above the noncheap and all-same boundaries.