theorem
Hex.GraphIso.Nauty.Sparse.classify_first_map
{n : Nat}
{g : Graph n}
{level numcells : Nat}
{before out : State n}
(hc : classify g level numcells before = (Generic.Leaf.autoFirst, out))
(hw : out.workperm.size = n)
(hf : out.firstlab.size = n)
(hp : out.firstlab.toList.Perm (List.range n))
(i : Nat)
:
First-reference classification supplies the full scatter map from the returned native state, including its actual work-array allocation.
theorem
Hex.GraphIso.Nauty.Sparse.leaf_refReturn
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells target : Nat}
{before : State n}
{short : Bool}
(hn : 0 < n)
(ha :
(classify (Graph.ofGraph G.graph) level numcells before).fst = Generic.Leaf.autoFirst ∨ (classify (Graph.ofGraph G.graph) level numcells before).fst = Generic.Leaf.autoCanon)
(he :
(leafExit (classify (Graph.ofGraph G.graph) level numcells before).fst level
(classify (Graph.ofGraph G.graph) level numcells before).snd).fst = Generic.Exit.unwind target short)
(hs :
Saved G
(leafExit (classify (Graph.ofGraph G.graph) level numcells before).fst level
(classify (Graph.ofGraph G.graph) level numcells before).snd).snd)
(ht :
TraceOk G
(leafExit (classify (Graph.ofGraph G.graph) level numcells before).fst level
(classify (Graph.ofGraph G.graph) level numcells before).snd).snd)
:
RefReturn (Graph.context G.graph) target
(leafExit (classify (Graph.ofGraph G.graph) level numcells before).fst level
(classify (Graph.ofGraph G.graph) level numcells before).snd).snd
Every native automorphism verdict retains its emitted reference carrier or a strictly smaller orbit image, including canonical admissions that do not merge an orbit. The trace and label validity come from the executed call's already established soundness invariants.
theorem
Hex.GraphIso.Nauty.Sparse.EarlyReturn.reference
{n k : Nat}
{G : Sparse.Colored n k}
{target bound : Nat}
{short : Bool}
{out : State n}
(h : EarlyReturn (Graph.ofGraph G.graph) target short out)
(hn0 : 0 < n)
(hs : Saved G out)
(ht : TraceOk G out)
(hb : target < bound)
(hn : bound < out.noncheaplevel)
(ha : bound < out.allsamelevel)
:
RefReturn (Graph.context G.graph) target out
An unconsumed native return above both subtree boundaries retains the reference or orbit evidence through all fixed-point cleanup.
theorem
Hex.GraphIso.Nauty.Sparse.node_short_first
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells target : Nat}
{st : State n}
(hpos : 0 < target)
(he : (Generic.node false g inf tcLevel fuel level numcells st).fst = Generic.Exit.unwind target true)
:
The actual sparse off-path call never requests short pruning at its positive first ancestor. This includes arbitrarily deep emitted returns.