theorem
Hex.GraphIso.Nauty.Sparse.Ready.child
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{st : State n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(first : Bool)
{tc tv : Nat}
{cell : VSet n}
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
:
NodeInv G (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)
Every surviving target member establishes the complete production child entry invariant. The certificate is derived from parent equitability.
theorem
Hex.GraphIso.Nauty.Sparse.Ready.child_frame
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{st : State n}
(h : Ready G level numcells st)
(hn : 0 < n)
(hl : 1 ≤ level)
(first : Bool)
{tc tv : Nat}
{cell : VSet n}
{out : State n}
(ht : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hx : FrameOut G level (level + 1) (Generic.Policy.child first level tc tv st) out)
:
FrameOut G level level st out
A child's return composes with individualization to preserve the parent frame, including references installed anywhere below the child.