theorem
Hex.GraphIso.Nauty.Sparse.firstChild_trace
{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)
(hi : NodeInv G level numcells st)
(hshape : FirstShape G.graph level numcells st)
(ht : n < st.firsttc.size)
(hc : n + 1 < st.firstcode.size)
(hb : st.canong.toRows = (Graph.ofGraph G.graph).blank)
(hw : st.workperm.size = n)
(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)
(htrace :
have r := Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st;
TraceOk G
(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 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));
TraceReady G tcLevel level r.fst result ∧ CheapRecorded level r.snd.fst.toNat result
A sound first-child trace establishes every invariant for the actual recovered parent and all later siblings, using its executed first path.
theorem
Hex.GraphIso.Nauty.Sparse.trace_advance
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel fuel cfuel level numcells tc tv1 tv index : Nat)
(first : Bool)
(cell : VSet n)
(st : State n)
(exit : Generic.Exit)
(hl : 1 ≤ level)
(htrace : TraceOk G st)
(h : TraceReady G tcLevel level numcells (Generic.Policy.recover (n + 2) level st))
(ht : Generic.Target State.frame level tc cell (Generic.Policy.recover (n + 2) level st))
(hrecord : CheapRecorded level tc (Generic.Policy.recover (n + 2) level st))
(hpast : ∀ (smaller : VSet n), Generic.Past first tv1 (smaller.nextElem (some tv)))
:
TraceOk G
(Generic.advance (n + 2)
(fun (first : Bool) (level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat)
(st : State n) =>
Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index
st)
first level numcells tc tv1 tv cell index st exit).snd.snd
A sound child trace and a proved recovered sweep frame suffice for every resume or nonlocal exit, including short and long target filtering.
theorem
Hex.GraphIso.Nauty.Sparse.firstPath_trace
{n k : Nat}
{G : Sparse.Colored n k}
(hn : 0 < n)
{tcLevel fuel level numcells last : Nat}
{st leaf : State n}
(path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf)
(hl : 1 ≤ level)
(hi : NodeInv G level numcells st)
(hshape : FirstShape G.graph level numcells st)
(htsize : n < st.firsttc.size)
(hcsize : n + 1 < st.firstcode.size)
(hblank : st.canong.toRows = (Graph.ofGraph G.graph).blank)
(hwork : st.workperm.size = n)
(htrace : TraceOk G st)
:
TraceOk G (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd
The first descent seeds every later sibling's admission history, so its full production call preserves trace soundness without any generator validity premise for work performed by descendants.