theorem
Hex.GraphIso.Nauty.Max.SweepInput.skip_phase
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{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 first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hskip : (!first || st.orbits[tv]! == tv) = false)
:
An orbit skip occurs only after the first leaf has initialized the persistent state and settled the comparison.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.skip_carrier
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{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 first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hskip : (!first || st.orbits[tv]! == tv) = false)
:
The consulted orbit pointer has a checked carrier stabilizing the frozen target partition, with a strictly smaller endpoint.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.skip_cover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{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 first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hgsz : ctx.g.size = n)
(hskip : (!first || st.orbits[tv]! == tv) = false)
:
CellCover ctx tcLevel (n - level) level numcells tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst (Loop.codes ctx l)
(Loop.prepare ctx tcLevel l).snd.snd.snd.snd (Remaining (cell.nextElem (some tv)) cell) (SearchState.key ctx bs st)
The carrier supplied by the actual orbit test removes the current vertex from ranked coverage, even after earlier filters.
theorem
Hex.GraphIso.Nauty.Max.SweepInput.skip_input
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel cfuel : Nat}
{first : Bool}
{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 + 1) first level numcells tc tv1 (some tv) cell index st l bs fs parents)
(hgsz : ctx.g.size = n)
(hskip : (!first || st.orbits[tv]! == tv) = false)
:
Advancing past an orbit skip supplies the complete unchanged-state input to the smaller suffix contract.