theorem
Hex.GraphIso.Nauty.Sparse.firstChild_stabilizes
{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)
(hw : st.workperm.size = n)
(he : st.genTrace = #[])
(htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel level numcells st).snd.snd.fst.nextElem none = some tv)
(path :
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;
TraceFrame G level r.snd.snd.snd.snd
(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
The actual first child initializes stabilization of its parent's prepared target partition. Its successful first path supplies the first reference; all subsequent child work is covered by the native recursion theorem, without a premise about the returned generators.
theorem
Hex.GraphIso.Nauty.Sparse.TraceFrame.skip_cover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel level numcells tc len tv : Nat}
{cs : List Nat}
{root st : State n}
{live : Nat → Prop}
{best : Option (Key n)}
{first : Bool}
(h : TraceFrame G level root st)
(hcover : CellCover G.graph tcLevel fuel level numcells tc len cs root live best)
(hr : Ready G level numcells root)
(ho : OrbitTrace G st)
(ht : TraceOk G st)
(hn : 0 < n)
(hl : 1 ≤ level)
(hc : IsCell root.ptn level tc len)
(hlen : 1 < len)
(hb : tc + len ≤ n)
(hf : n < fuel + (numcells + 1))
(hv : (windowSet n root.lab tc len).mem tv = true)
(hle : ∀ (v : Nat), live v → tv ≤ v)
(hskip : (!first || st.orbits[tv]! == tv) = false)
:
The frozen trace invariant discharges stabilization at the literal
orbit guard. Its first-child initialization and complete-call preservation
are supplied by firstChild_stabilizes and TraceFrame.sweep.