structure Hex.GraphIso.Nauty.Sparse.TraceFrame {n k : Nat} (G : Sparse.Colored n k) (base : Nat) (root st : State n) : Prop

A suspended first-path partition contains the current and saved labels, and is stabilized by every emitted generator. The workspace bound justifies the literal reference scatters used to extend the trace.

• frame : FrameOut G base base root st
• first : st.firstlab.size = n ∧ cellsPerm root.ptn base root.lab st.firstlab
• canon : st.canonlab.size = n ∧ cellsPerm root.ptn base root.lab st.canonlab
• trace (gamma : Array Nat) : gamma ∈ st.genTrace → CellStab root.ptn base root.lab gamma
• work : st.workperm.size = n

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.label_perm {n k : Nat} {G : Sparse.Colored n k} {base numcells : Nat} {root : State n} (hroot : Ready G base numcells root) (hn : 0 < n) (hb : 1 ≤ base) {lab : Array Nat} (hs : lab.size = n) (hp : cellsPerm root.ptn base root.lab lab) : lab.toList.Perm (List.range n)

Cell membership in the frozen partition makes either saved reference a full permutation, supplying the precondition of the executed scatter.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.of_effect {n k : Nat} {G : Sparse.Colored n k} {base numcells : Nat} {root st out : State n} (h : TraceFrame G base root st) (hp : Ready G base numcells root) (he : FrameOut G base base st out) (ht : ∀ (gamma : Array Nat), gamma ∈ out.genTrace → CellStab root.ptn base root.lab gamma) (hw : out.workperm.size = n) : TraceFrame G base root out

An effect at the frozen level transports both reference-store alternatives. Only new trace entries require a separate stabilization proof.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.extend {n k : Nat} {G : Sparse.Colored n k} {base numcells : Nat} {root st out : State n} (h : TraceFrame G base root st) (hp : Ready G base numcells root) (hn : 0 < n) (hpos : 1 ≤ base) {bound level : Nat} (he : FrameOut G bound level st out) (hb : base ≤ bound) (hl : base ≤ level) (ht : ∀ (gamma : Array Nat), gamma ∈ out.genTrace → CellStab root.ptn base root.lab gamma) (hw : out.workperm.size = n) : TraceFrame G base root out

Effects below a suspended ancestor preserve its references as well as its frame, including complete calls and nonlocal returns.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.fields {n k : Nat} {G : Sparse.Colored n k} {base : Nat} {root st out : State n} (h : TraceFrame G base root st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) (hf : out.firstlab = st.firstlab) (hc : out.canonlab = st.canonlab) (ht : out.genTrace = st.genTrace) (hw : out.workperm.size = st.workperm.size) (hs : Scratch.Bounded n out.canong.scratch) : TraceFrame G base root out

Bookkeeping retaining labels, partition, trace and workspace transports the entire frozen-ancestor invariant. Scratch validity is supplied by its native operation contract.