theorem
Hex.GraphIso.Nauty.Sparse.Ready.child_chosen
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv : Nat}
{st : State n}
{cell : VSet 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)
:
(Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd.lab[tc]! = tv
The returned native child retains its individualized vertex at the selected position before parent partition recovery.
theorem
Hex.GraphIso.Nauty.Sparse.Ready.canon_earlier
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv : Nat}
{st : State n}
{cell : VSet 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)
{previous : Option Nat}
(hp : Generation.CanonPast level tc previous st)
(hnext : cell.nextElem previous = some tv)
:
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[tc]! < tv
A canonical return to the receiving parent retains its earlier canonical source, which lies strictly before the current live cursor.
theorem
Hex.GraphIso.Nauty.Sparse.Ready.canon_past
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc tv : Nat}
{st : State n}
{cell : VSet 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)
{previous : Option Nat}
(hp : Generation.CanonPast level tc previous st)
(hnext : cell.nextElem previous = some tv)
:
have raw :=
(Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1)
(Generic.Policy.child first level tc tv st)).snd;
have middle := if childFirst = true then afterChildFirst level tv raw else raw;
have left := Generic.Policy.leaveChild tv middle;
Generation.CanonPast level tc (some tv) (Generic.Policy.recover (n + 2) level left)
Receiving either kind of native child keeps every local canonical source behind the next cursor, whether the child retained or installed the reference. This includes cache invalidation during recovery.