theorem
Hex.GraphIso.Nauty.Sparse.Max.Guides.node
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs : List Nat}
{parents : Parents n}
(h : Guides G.graph tcLevel f.entry parents)
(hs : Scope G tcLevel f bs f.entry parents)
(hf : Frame.Valid G f)
(fuel : Nat)
:
The complete native off-path call retains every reference association with its suspended ancestors, including truncated calls and nonlocal exits.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Guides.emit
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs : List Nat}
{parents : Parents n}
(h : Guides G.graph tcLevel f.entry parents)
(hs : Scope G tcLevel f bs f.entry parents)
(hf : Frame.Valid G f)
(he : (Frame.emit G.graph tcLevel f).fst ≠ Generic.Exit.done)
:
Guides G.graph tcLevel (Frame.emit G.graph tcLevel f).snd parents
A terminal native dispatch inherits the full call's reference associations; its actual exit excludes any sibling continuation.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.recovered_canon
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel : Nat}
{p : Parent n}
(h : Valid G tcLevel p)
(first : Bool)
:
have ch := Parent.child G.graph tcLevel p;
have raw := (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd;
have left :=
Generic.Policy.leaveChild p.chosen (if first = true then afterChildFirst p.node.level p.chosen raw else raw);
have out := Generic.Policy.recover (n + 2) p.node.level left;
out.gcaCanon < p.node.level → out.gcaCanon = p.state.gcaCanon ∧ out.canonlab = p.state.canonlab
The actual returned child and native recovery retain an older canonical reference whenever the clamped ancestor still lies above this parent. This covers both first and off-path child calls.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Guides.back
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel : Nat}
{p : Parent n}
{parents : Parents n}
(h : Guides G.graph tcLevel p.state parents)
(hs : Scope G tcLevel p.node p.bs p.state parents)
(hp : Parent.Valid G tcLevel p)
:
Guides G.graph tcLevel (Parent.back G.graph tcLevel fuel p) parents
Recovery after an actual off-path child retains every covered reference belonging to an older suspended ancestor.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Guides.first_back
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel : Nat}
{p : Parent n}
{parents : Parents n}
(h : Guides G.graph tcLevel p.state parents)
(hs : Scope G tcLevel p.node p.bs p.state parents)
(hp : Parent.Valid G tcLevel p)
:
Guides G.graph tcLevel (Parent.firstBack G.graph tcLevel fuel p) parents
The first child's bookkeeping points the first reference to this parent. Its recovery still retains every older canonical association.