theorem
Hex.GraphIso.Nauty.Sparse.fixed_advance
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
{fuel cfuel : Nat}
{next : Generic.SweepFn (State n) n}
(hnext : (fixedContract G).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(st out : State n)
(exit : Generic.Exit)
(hl : 1 ≤ level)
(h : Ready G level numcells st)
(htarget : Generic.Target State.frame level tc cell st)
(hf : FixedCells level st.frame)
(hx : FrameOut G level level st out)
(he : out.fixedpts = st.fixedpts)
:
Every return arm retains the restored fixed set. A resumed sibling receives fixed singletons in the recovered equitable parent partition.
theorem
Hex.GraphIso.Nauty.Sparse.fixed_sweep
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel : Nat)
{fuel cfuel : Nat}
{next : Generic.SweepFn (State n) n}
(hd : (fixedContract G).nodeValid fuel (Generic.nodeCall (Graph.ofGraph G.graph) (n + 2) tcLevel fuel))
(hnext : (fixedContract G).sweepValid fuel cfuel next)
(first : Bool)
(level numcells tc tv1 tv index : Nat)
(cell : VSet n)
(st : State n)
(hl : 1 ≤ level)
(h : Ready G level numcells st)
(htarget : Generic.Target State.frame level tc cell st)
(hv : cell.mem tv = true)
(hf : FixedCells level st.frame)
:
(Generic.sweepStep (n + 2) (Generic.nodeCall (Graph.ofGraph G.graph) (n + 2) tcLevel fuel) next first level numcells tc
tv1 tv cell index st).snd.snd.fixedpts = st.fixedpts
A child call restores its enlarged fixed set by induction; removing its fresh temporary vertex restores exactly the parent's incoming set.