def Hex.GraphIso.Nauty.Sparse.DescentAt {n : Nat} (G : SparseGraph n) (store : Array Int) (base : Nat) (root : RefineSt n) (level numcells : Nat) (st : State n) : Prop

A frozen equitable witness represents the current production partition and count, with its saved-target descent modulo within-cell label order. Its active set belongs to the witness; child calls install their own splitter.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.DescentAt.congr {n : Nat} {G : SparseGraph n} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st out : State n} (h : DescentAt G store base root level numcells st) (hl : out.lab = st.lab) (hp : out.ptn = st.ptn) : DescentAt G store base root level numcells out

theorem Hex.GraphIso.Nauty.Sparse.DescentAt.reorder {n : Nat} {G : SparseGraph n} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st out : State n} (h : DescentAt G store base root level numcells st) (hl : out.lab.size = st.lab.size) (hp : out.ptn = st.ptn) (hc : cellsPerm st.ptn level out.lab st.lab) : DescentAt G store base root level numcells out

Restoring a parent retains its descent while adopting the returned label order, preserving the witness's complete refinement certificate.

theorem Hex.GraphIso.Nauty.Sparse.DescentAt.child {n : Nat} {G : SparseGraph n} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st : State n} (h : DescentAt G store base root level numcells st) (hr : RefineSt.Ready G base root) (first : Bool) {tc len o : Nat} (hc : IsCell st.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ho : o < len) (htc : store[level]! = Int.ofNat tc) (hs : Scratch.Bounded n st.canong.scratch) : have next := Generic.Policy.child first level tc st.lab[tc + o]! st; have r := visit (Graph.ofGraph G) (level + 1) (numcells + 1) next; DescentAt G store base root (level + 1) r.fst r.snd.snd

Every native individualization followed by its actual cached visit extends the current saved-target descent.

theorem Hex.GraphIso.Nauty.Sparse.DescentAt.recover {n k : Nat} {G : Sparse.Colored n k} {store : Array Int} {base level numcells : Nat} {root : RefineSt n} {st out : State n} (h : DescentAt G.graph store base root level numcells st) (hok : SearchOk G.toDense level numcells st.frame) (hout : FrameOut G level level st out) : DescentAt G.graph store base root level numcells (Generic.Policy.recover (n + 2) level out)

The established native frame effect restores the parent history through the literal recovery and cache invalidation operation.