theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.prepare_closed
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{p : Parent n}
(h : Valid G tcLevel p)
{q : Nat}
(hq : p.node.entry.ptn[q]! ≤ p.node.level)
:
Native preparation and all completed sibling reorderings retain the incoming node's closed partition values literally.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.child_closed
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{p : Parent n}
(h : Valid G tcLevel p)
{q : Nat}
(hq : p.state.ptn[q]! ≤ p.node.level)
:
Individualization writes inside the selected nonsingleton cell and therefore leaves every already closed boundary unchanged.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Scope.closed
{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)
{t : Nat}
{p : Parent n}
(hp : parents t = some p)
{q : Nat}
(hq : p.node.entry.ptn[q]! ≤ p.node.level)
:
The actual ancestor chain retains every closed value from a suspended node's entry through the current entry, including new child singletons.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Scope.child_closed
{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)
{t : Nat}
{p : Parent n}
(hp : parents t = some p)
{q : Nat}
(hq : (Parent.child G.graph tcLevel p).entry.ptn[q]! ≤ p.node.level + 1)
:
The individualized child boundaries remain closed at every later entry, even when the selected child has since prepared and reordered siblings.