theorem
Hex.GraphIso.Nauty.Max.SweepInput.past_phase
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel true level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hpast : tv1 < tv)
:
SweepPre G ctx tcLevel true level numcells tc tv1 (some tv) cell st ∧ Comparison ctx (Loop.codes ctx l) bs fs st
Passing the guiding vertex selects the initialized sibling phase.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.cheap_visit
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel level numcells tc tv1 tv index : Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel true level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hpast : tv1 < tv)
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk ctx level R)
(hlab : R.lab = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn)
(hnc : R.numcells = numcells)
(href : Generation.HasLeaf ctx tcLevel level R targets key)
(hm : Generation.Matches ctx level st targets key)
(hg : st.gcaFirst = level)
(heq : st.eqlevFirst = level)
(hcheap : st.noncheaplevel ≤ level)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
:
Reordering a cheap receiving frame preserves the reference in every target child. Its actual off-path call therefore returns to this frame.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.visit_level
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel level numcells tc tv1 tv index target : Nat}
{short : Bool}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G ctx tcLevel fuel cfuel true level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hpast : tv1 < tv)
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk ctx level R)
(hlab : R.lab = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn)
(hnc : R.numcells = numcells)
(href : Generation.HasLeaf ctx tcLevel level R targets key)
(hm : Generation.Matches ctx level st targets key)
(hg : st.gcaFirst = level)
(heq : st.eqlevFirst = level)
(hsame : level < st.allsamelevel)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(he :
(Nauty.node false ctx (n + 2) tcLevel fuel (level + 1) (numcells + 1) (child true level tc tv st)).fst = Generic.Exit.unwind target short)
:
Every remaining first-path sibling returns to its receiver. The cheap case uses occurrence, while the other case uses the return bounds.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.tail_done
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel level numcells tc tv1 index : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G { g := rowsOf G } tcLevel fuel cfuel true level numcells tc tv1 cursor cell index st l bs fs parents)
(hn : (contract G tcLevel).nodeValid fuel (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel fuel))
(hpast : Generic.Past true tv1 cursor)
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk { g := rowsOf G } level R)
(hlab : R.lab = (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.ptn)
(hnc : R.numcells = numcells)
(href : Generation.HasLeaf { g := rowsOf G } tcLevel level R targets key)
(hm : Generation.Matches { g := rowsOf G } level st targets key)
(hg : st.gcaFirst = level)
(heq : st.eqlevFirst = level)
(hsame : level < st.allsamelevel)
:
The actual sibling suffix completes, including both short-prune flags. Recovery preserves the frozen reference and first agreement.