def Hex.GraphIso.Nauty.Sparse.Max.Parent.next {n : Nat} (p : Parent n) (st : State n) (bs : List Nat) (cell : VSet n) (tv : Nat) : Parent n

The same frozen parent selects another vertex after native recovery and filtering. The suspended entry and its target coordinate are retained.

Equations

• p.next st bs cell tv = { node := p.node, first := p.first, state := st, tc := p.tc, cell := cell, chosen := tv, bs := bs }

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.Valid.next {n k : Nat} {G : Sparse.Colored n k} {tcLevel tv : Nat} {p : Parent n} {out : State n} {ds : List Nat} {cell : VSet n} (h : Valid G tcLevel p) (hr : Ready G p.node.level (Frame.target G.graph tcLevel p.node).numcells out) (he : FrameOut G p.node.level p.node.level p.state out) (hg : Grows (State.key G.graph p.bs p.state) (State.key G.graph ds out)) (hb : out.noncheaplevel = p.state.noncheaplevel ∨ p.node.level < out.noncheaplevel) (ht : Generic.Target State.frame p.node.level p.tc cell out) (hm : cell.mem tv = true) : Valid G tcLevel (p.next out ds cell tv)

Recovered parent geometry, incumbent growth and the literal boundary alternative preserve the invariant for any next surviving target vertex.

theorem Hex.GraphIso.Nauty.Sparse.Max.recover_boundary {n level inf : Nat} {before out : State n} (h : out.noncheaplevel = before.noncheaplevel ∨ level + 1 ≤ out.noncheaplevel) : (Generic.Policy.recover inf level out).noncheaplevel = before.noncheaplevel ∨ level < (Generic.Policy.recover inf level out).noncheaplevel

Recovering the returned child cannot turn a failed parent guard into a passing one. This follows the exact clamp written by recoverLevels.

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.child_boundary {n : Nat} (G : SparseGraph n) (tcLevel fuel : Nat) (p : Parent n) : have out := (Generic.node false (Graph.ofGraph G) (n + 2) tcLevel fuel (child G tcLevel p).level (child G tcLevel p).numcells (child G tcLevel p).entry).snd; have back := Generic.Policy.recover (n + 2) p.node.level (Generic.Policy.leaveChild p.chosen out); back.noncheaplevel = p.state.noncheaplevel ∨ p.node.level < back.noncheaplevel

The native off-path child supplies the precise boundary alternative needed when its parent recovers and chooses another surviving vertex.

theorem Hex.GraphIso.Nauty.Sparse.Max.Parent.first_boundary {n : Nat} {G : SparseGraph n} {tcLevel fuel last : Nat} {p : Parent n} {leaf : State n} (path : Generic.FirstPath (Graph.ofGraph G) tcLevel fuel (child G tcLevel p).level (child G tcLevel p).numcells (child G tcLevel p).entry last leaf) : have out := (Generic.node true (Graph.ofGraph G) (n + 2) tcLevel fuel (child G tcLevel p).level (child G tcLevel p).numcells (child G tcLevel p).entry).snd; have back := Generic.Policy.recover (n + 2) p.node.level (Generic.Policy.leaveChild p.chosen (afterChildFirst p.node.level p.chosen out)); back.noncheaplevel = p.state.noncheaplevel ∨ p.node.level < back.noncheaplevel

The first-path child has the same recovery guarantee, including all later siblings traversed before its actual return.