theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Guided.canon_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {p : Parent n} {after : Option (Key n)} (h : Guided G.graph tcLevel p) (hp : Valid G tcLevel p) (first : Bool) (hb : p.state.gcaCanon ≤ p.node.level) (hg : Grows (State.key G.graph p.bs p.state) after) (hd : Covers (key G.graph tcLevel p p.chosen) after) : have ch := 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); CanonGuide p.node.level p.tc p.state (key G.graph tcLevel p) after (Generic.Policy.recover (n + 2) p.node.level left)

A completed native child supplies the canonical reference guide at recovery. Its coverage is the local induction premise; the reference's origin and containment follow from the executed child call.

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Guided.back {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel : Nat} {p : Parent n} {ds fs : List Nat} {cell : VSet n} {tv : Nat} (h : Guided G.graph tcLevel p) (hp : Valid G tcLevel p) (hb : p.state.gcaCanon ≤ p.node.level) (hg : Grows (State.key G.graph p.bs p.state) (State.key G.graph ds (Parent.back G.graph tcLevel fuel p))) (hr : have ch := child G.graph tcLevel p; ReturnCodes G.graph ch.codes ds fs (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd) (hd : have ch := child G.graph tcLevel p; Covers (Frame.key G.graph tcLevel ch) (State.best G.graph (Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd)) : Guided G.graph tcLevel (p.next (Parent.back G.graph tcLevel fuel p) ds cell tv)

Returning from an actual off-path child establishes the covered references for the next sibling in its recovered label ordering.