theorem Hex.GraphIso.Nauty.NodePre.leaf_bound {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel level numcells target : Nat} {short : Bool} {st : Search n} (hin : NodePre G ctx tcLevel level numcells st) : have p := prepareOther ctx tcLevel level numcells st; have c := classify ctx level p.fst p.snd.snd.snd.snd.snd; (leafExit c.fst level c.snd).fst = Generic.Exit.unwind target short → target < level

The leaf action of an actual prepared node returns to a strict ancestor.

theorem Hex.GraphIso.Nauty.NodePre.node_bound {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells : Nat} {st : Search n} (hin : NodePre G ctx tcLevel level numcells st) (inf target : Nat) (short : Bool) : (node false ctx inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target short → target < level

An actual off-path node unwinds to a strict ancestor, including returns transported from any number of descendant sweeps.

theorem Hex.GraphIso.Nauty.first_node_bound {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) (hlevel : 1 ≤ level) (target : Nat) (short : Bool) : (node true ctx inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target short → target < level

A first-path node needs only a positive level to bound its unwind; its terminal return and its sweep both leave the node.

def Hex.GraphIso.Nauty.LeafReturn {n : Nat} (target : Nat) (out : Search n) : Prop

A short return retains its emitting leaf's state, apart from the fixed-point cleanup and first-path controls updated by enclosing loops.

Equations

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

theorem Hex.GraphIso.Nauty.shortPolicy {n : Nat} : Generic.ShortPolicy LeafReturn

The nauty cleanup operations retain the state of a short return's origin.

theorem Hex.GraphIso.Nauty.LeafReturn.admission {n target : Nat} {out : Search n} (h : LeafReturn target out) (hcap : 0 < out.wsCap) : out.autos.back? = some (fmperm out.workperm n) ∧ target = out.gcaCanon ∧ out.workperm ∈ out.genTrace ∧ (out.workperm.size = n → out.canonlab.size = n → out.canonlab.toList.Perm (List.range n) → ∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!) ∨ out.autos.back? = some (fmptn out.lab out.ptn out.noncheaplevel n) ∧ target ≤ out.noncheaplevel - 1

The receiving loop reads the emitting leaf's admitted pair in its own fields. Its target is the canonical ancestor for an explicit pair, and is bounded by the cheap boundary's parent for an implicit pair.

theorem Hex.GraphIso.Nauty.short_implicit_fix {n k : Nat} {G : Colored n k} {level numcells : Nat} {base out : Search n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hok : SearchOk G level numcells base) (hfixed : FixedCells level base) (hframe : SearchOut G level level base out) (hf : out.fixedpts = base.fixedpts) (hsaved : level ≤ out.noncheaplevel) : out.fixedpts.subset (fmptn out.lab out.ptn out.noncheaplevel n).fst = true

At a receiving loop, an implicit pair frozen below the parent fixes every vertex of the parent path, even before partition recovery.

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

A node's short-prune payload comes from an actual leaf emission, including when the return crosses several intermediate loops.

theorem Hex.GraphIso.Nauty.sweep_origin {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : Search n) {target : Nat} (he : (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).fst = Generic.Exit.unwind target true) : LeafReturn target (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

A sweep transports the emitting leaf's workspace and partition until the target loop consumes the short-prune request.