noncomputable def Hex.GraphIso.Nauty.Sparse.State.frame {n : Nat} (st : State n) : Search n

A proof projection exposing shared partition and bookkeeping fields. Its empty unused storage is never passed to an executable search or adjacency operation.

Equations

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

structure Hex.GraphIso.Nauty.Sparse.NodeInv {n k : Nat} (G : Sparse.Colored n k) (level numcells : Nat) (st : State n) : Prop

Entry to an actual sparse node: valid partition, exact depth/count, ordered-colour reachability, reference-label frame and bounded scratch.

• spec : SpecNode G.graph level st.lab st.ptn st.active numcells
• ok : SearchOk G.toDense level numcells st.frame
• scratch : Scratch.Bounded n st.canong.scratch

structure Hex.GraphIso.Nauty.Sparse.Ready {n k : Nat} (G : Sparse.Colored n k) (level numcells : Nat) (st : State n) : Prop

A refined or recovered parent is equitable. Its active set need not be reused: the next child installs its own singleton active splitter.

• ok : SearchOk G.toDense level numcells st.frame
• equitable : Equitable (Graph.context G.graph) level st.lab st.ptn
• scratch : Scratch.Valid n st.lab st.ptn level st.canong.scratch

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

The persistent result of a call, retaining the exact frame effect and scratch bounds also when the call unwinds past its caller.

• effect : SearchOut G.toDense base level st.frame out.frame
• scratch : Scratch.Bounded n out.canong.scratch

theorem Hex.GraphIso.Nauty.Sparse.FrameOut.refl {n k : Nat} {G : Sparse.Colored n k} {base level numcells : Nat} {st : State n} (h : NodeInv G level numcells st) : FrameOut G base level st st

theorem Hex.GraphIso.Nauty.Sparse.FrameOut.trans {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st mid out : State n} (h : FrameOut G level level st mid) (h' : FrameOut G level level mid out) : FrameOut G level level st out