theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.coarsen
{n k : Nat}
{G : Sparse.Colored n k}
{base bound level : Nat}
{st out : State n}
(h : FrameOut G bound level st out)
(hb : base ≤ bound)
(hl : base ≤ level)
(hsize : st.lab.size = n)
(hptn : st.ptn.size = n)
(hend : st.ptn[st.ptn.size - 1]! ≤ base)
:
FrameOut G base base st out
A descendant's actual effect also preserves each coarser ancestor level, including both reference-store alternatives. The final boundary is already closed at that ancestor, so every fine cell has a coarse owner.
theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.extend
{n k : Nat}
{G : Sparse.Colored n k}
{base bound level numcells : Nat}
{parent st out : State n}
(h : FrameOut G base base parent st)
(next : FrameOut G bound level st out)
(hp : Ready G base numcells parent)
(hn : 0 < n)
(hpos : 1 ≤ base)
(hb : base ≤ bound)
(hl : base ≤ level)
:
FrameOut G base base parent out
Compose a complete descendant call with a suspended ancestor frame. This transports its actual labels and saved references in one step.
theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.stab_below
{n k : Nat}
{G : Sparse.Colored n k}
{a b acells bcells : Nat}
{parent child out : State n}
{gamma : Array Nat}
(ha : FrameOut G a a parent out)
(hb : FrameOut G b b child out)
(hp : Ready G a acells parent)
(hc : Ready G b bcells child)
(hn : 0 < n)
(hapos : 1 ≤ a)
(hbpos : 1 ≤ b)
(hab : a ≤ b)
(hs : CellStab child.ptn b child.lab gamma)
:
A permutation stabilizing a suspended partition also stabilizes a coarser suspended ancestor. Their actual effects into the same current state supply both boundary inclusion and label transport.
theorem
Hex.GraphIso.Nauty.Sparse.FrameOut.scatter_stab
{n k : Nat}
{G : Sparse.Colored n k}
{level numcells : Nat}
{parent out : State n}
{reference gamma : Array Nat}
(h : FrameOut G level level parent out)
(hp : Ready G level numcells parent)
(hn : 0 < n)
(hl : 1 ≤ level)
(hs : reference.size = n)
(href : cellsPerm parent.ptn level parent.lab reference)
(hmap : ∀ (i : Nat), i < n → gamma[reference[i]!]! = out.lab[i]!)
:
A literal scatter between a retained reference and a descendant's current label stabilizes their common suspended ancestor cells.