def Hex.GraphIso.Nauty.Sparse.LeafReturn {n : Nat} (target : Nat) (out : State 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.Sparse.shortPolicy {n : Nat} : Generic.ShortPolicy LeafReturn

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

theorem Hex.GraphIso.Nauty.Sparse.LeafReturn.admission {n target : Nat} {out : State 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.Sparse.node_origin {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel level numcells : Nat) (st : State n) {target : Nat} (he : (Generic.node first g inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target true) : LeafReturn target (Generic.node first g 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.Sparse.sweep_origin {n : Nat} (first : Bool) (g : Graph n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : State n) {target : Nat} (he : (Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).fst = Generic.Exit.unwind target true) : LeafReturn target (Generic.sweep first g 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.