theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.reference_frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{p : Parent n}
{out : State n}
{ref : Array Nat}
{ds : List Nat}
{cell : VSet n}
{tv : Nat}
{best : Option (Key n)}
(h : Valid G tcLevel p)
(hr : Ready G p.node.level (Frame.target G.graph tcLevel p.node).numcells out)
(he : FrameOut G p.node.level p.node.level p.state out)
(hc : Covers (key G.graph tcLevel p ref[p.tc]!) best)
(hp : cellsPerm p.state.ptn p.node.level p.state.lab ref)
:
Coverage of a reference child transfers to the actual recovered ordering together with reference containment in the parent cells.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.guide_frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{p : Parent n}
{out : State n}
{ds : List Nat}
{cell : VSet n}
{tv : Nat}
(h : Valid G tcLevel p)
(hr : Ready G p.node.level (Frame.target G.graph tcLevel p.node).numcells out)
(he : FrameOut G p.node.level p.node.level p.state out)
(hc : CanonGuide p.node.level p.tc p.state (key G.graph tcLevel p) (State.key G.graph ds out) out)
(hf :
out.gcaFirst = p.node.level →
Covers (key G.graph tcLevel p out.firstlab[p.tc]!) (State.key G.graph ds out) ∧ cellsPerm p.state.ptn p.node.level p.state.lab out.firstlab)
:
Recovered reference coverage in the frozen parent becomes the complete guide for whichever surviving vertex is suspended next.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.returned_frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel fuel : Nat}
{p : Parent n}
(h : Valid G tcLevel p)
(first : Bool)
:
have ch := Parent.child G.graph tcLevel p;
have raw := (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel ch.level ch.numcells ch.entry).snd;
have left :=
Generic.Policy.leaveChild p.chosen (if first = true then afterChildFirst p.node.level p.chosen raw else raw);
have out := Generic.Policy.recover (n + 2) p.node.level left;
Ready G p.node.level (Frame.target G.graph tcLevel p.node).numcells out ∧ FrameOut G p.node.level p.node.level p.state out
Either actual child call supplies a valid recovered parent and its native frame effect, including first-child bookkeeping and cache invalidation.