theorem Hex.GraphIso.Nauty.Sparse.child_canon_stab {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tc tv : Nat} {cell : VSet n} {base st : State n} {key : Nat → Key n} {best : Option (Key n)} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first childFirst : Bool) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hbase : Ready G level numcells base) (hframe : FrameOut G level level base st) (hguide : CanonGuide level tc base key best st) : have out := (Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd; out.gcaCanon = level → out.canonlab.size = n → (∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!) → CellStab base.ptn level base.lab out.workperm

The literal canonical scatter returned by a native child stabilizes the frozen parent cells. Both labels are related to those cells by the actual call's frame and canonical-reference provenance.

theorem Hex.GraphIso.Nauty.Sparse.child_canon_pair {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tc tv : Nat} {cell : VSet n} {base st : State n} {key : Nat → Key n} {best : Option (Key n)} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first childFirst : Bool) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hbase : Ready G level numcells base) (hframe : FrameOut G level level base st) (hguide : CanonGuide level tc base key best st) : have out := (Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd; out.gcaCanon = level → out.canonlab.size = n → Automorphism G out.workperm → (∀ (i : Nat), i < n → out.workperm[out.canonlab[i]!]! = out.lab[i]!) → PairOk (Graph.context G.graph).g base.ptn base.lab level (fmperm out.workperm n).fst (fmperm out.workperm n).snd

Native automorphism soundness and the actual returned scatter justify its explicit pair at the receiving parent's frozen partition.