theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.return_frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{p : Parent n}
{out : State n}
(h : Valid G tcLevel p)
(hx : FrameOut G p.node.level (p.node.level + 1) (Parent.child G.graph tcLevel p).entry out)
:
A returned effect inside the actual selected child composes with its native individualization to retain the suspended parent.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Scope.child_frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs : List Nat}
{st : State n}
{parents : Parents n}
(h : Scope G tcLevel f bs st parents)
(hf : Frame.Valid G f)
{t : Nat}
{p : Parent n}
(hp : parents t = some p)
:
The established ancestor chain determines the current entry's effect inside every suspended selected child. No separate ancestor-frame premise is needed in the maximum-coverage recursion.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Scope.frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs : List Nat}
{st : State n}
{parents : Parents n}
(h : Scope G tcLevel f bs st parents)
(hf : Frame.Valid G f)
{t : Nat}
{p : Parent n}
(hp : parents t = some p)
:
Every suspended parent's cells contain the current entry, as a consequence of its actual child chain and native frame effects.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.emit_frame
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
(h : Valid G f)
:
The native leaf dispatcher preserves the current node's complete entry frame, including either reference-store alternative.