theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.rebase {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {root st : State n} (h : TraceFrame G level root st) (hr : Ready G level numcells root) (hs : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) : TraceFrame G level st st

Reordering a recovered equitable parent changes neither reference containment nor stabilization of its cells. This supplies the exact current ordering used when the next sibling is suspended.

theorem Hex.GraphIso.Nauty.Sparse.TraceFrame.freeze {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {root st : State n} (h : TraceFrame G level st st) (he : FrameOut G level level root st) (hr : Ready G level numcells root) (hs : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) : TraceFrame G level root st

The current first-sweep trace also stabilizes its original frozen cell ordering. Recovery permutes labels only within those cells.

def Hex.GraphIso.Nauty.Sparse.Max.Traces {n k : Nat} (G : Sparse.Colored n k) (st : State n) (parents : Parents n) : Prop

Every suspended first sweep contains both saved labels and is stabilized by the complete emitted trace in the current native state.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.Sparse.Max.Traces.root {n k : Nat} (G : Sparse.Colored n k) (st : State n) : Traces G st fun (x : Nat) => none

theorem Hex.GraphIso.Nauty.Sparse.Max.Traces.first_node {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel last : Nat} {f : Frame n} {bs : List Nat} {st leaf : State n} {parents : Parents n} (hs : Scope G tcLevel f bs st parents) (hf : Frame.Valid G f) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf) (hw : f.entry.workperm.size = n) (he : f.entry.genTrace = #[]) : Traces G (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd parents

The actual first call establishes every older first ancestor's reference containment and stabilization directly from its first leaf. The native parent chain supplies all required incoming frame effects.

theorem Hex.GraphIso.Nauty.Sparse.Max.Traces.node {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs : List Nat} {st : State n} {parents : Parents n} (h : Traces G f.entry parents) (hs : Scope G tcLevel f bs st parents) (hf : Frame.Valid G f) (first : Bool) (fuel : Nat) : Traces G (Generic.node first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd parents

Complete descendant calls retain every suspended first ancestor's native trace frame, including nonlocal returns and truncated calls.

theorem Hex.GraphIso.Nauty.Sparse.Max.Traces.prepare {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs : List Nat} {parents : Parents n} (h : Traces G f.entry parents) (hs : Scope G tcLevel f bs f.entry parents) (hf : Frame.Valid G f) (tv : Nat) : Traces G (Frame.otherParent G.graph tcLevel f bs tv).state parents

theorem Hex.GraphIso.Nauty.Sparse.Max.Traces.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} {parents : Parents n} (h : Traces G p.state parents) (hs : Scope G tcLevel p.node p.bs p.state parents) (hp : Parent.Valid G tcLevel p) (hself : p.first = true → TraceFrame G p.node.level p.state p.state) : Traces G (Parent.child G.graph tcLevel p).entry (parents.push p)

Suspending a first sweep adds its own current trace frame. Native individualization transports every older frame into the selected child.

theorem Hex.GraphIso.Nauty.Sparse.Max.Traces.recovered {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} {parents : Parents n} {raw : State n} (h : Traces G raw (parents.push p)) (hs : Scope G tcLevel p.node p.bs p.state parents) (hp : Parent.Valid G tcLevel p) (first : Bool) : have left := Generic.Policy.leaveChild p.chosen (if first = true then afterChildFirst p.node.level p.chosen raw else raw); Traces G (Generic.Policy.recover (n + 2) p.node.level left) (parents.push p)

Both actual return paths preserve the trace frames of the receiving parent and all older suspended first sweeps, through fixed-point cleanup and native partition recovery.

theorem Hex.GraphIso.Nauty.Sparse.Max.Traces.pop {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {p : Parent n} {parents : Parents n} {st : State n} (h : Traces G st (parents.push p)) (hs : Scope G tcLevel p.node p.bs p.state parents) : Traces G st parents