theorem
Hex.GraphIso.Nauty.Sparse.firstChild_history
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tv last : Nat}
{st leaf : State n}
(hn : 0 < n)
(hl : 1 ≤ level)
(hok : NodeInv G level numcells st)
(hshape : FirstShape G.graph level numcells st)
(htsize : n < st.firsttc.size)
(hcsize : n + 1 < st.firstcode.size)
(hopen : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).fst ≠ n)
(htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.fst.nextElem none = some tv)
(horbit :
(cheapCheck true level
(Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.snd.snd).orbits[tv]! = tv)
(hpath :
have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st;
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) last leaf)
:
have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st;
have out :=
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))).snd;
have result := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv (afterChildFirst level tv out));
CheapHistory G.graph tcLevel level level r.fst result
Completion of the actual first child installs its native saved history at the recovered parent. The parent witness, cheap shape and current descent are derived from entry invariants and the executed first path.
theorem
Hex.GraphIso.Nauty.Sparse.firstChild_target
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tv last : Nat}
{st leaf : State n}
(hn : 0 < n)
(hl : 1 ≤ level)
(hok : NodeInv G level numcells st)
(htsize : n < st.firsttc.size)
(hopen : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).fst ≠ n)
(hpath :
have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st;
Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) last leaf)
:
have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st;
have out :=
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd))).snd;
have result := Generic.Policy.recover (n + 2) level (Generic.Policy.leaveChild tv (afterChildFirst level tv out));
result.firsttc[level]! = Int.ofNat r.snd.fst.toNat
The first child's saved target survives its terminal sentinel write, all later siblings, and the actual parent recovery.