theorem
Hex.GraphIso.Nauty.Sparse.refineWith_code_lt
{n : Nat}
(g : Graph n)
(level : Nat)
(lab ptn : Array Nat)
(active : VSet n)
(numcells : Nat)
(scratch : Scratch)
:
Both refinement exits clean the actual accumulated code below the terminal sentinel, regardless of input scratch or partition validity.
theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_le
{n : Nat}
(g : Graph n)
(tcLevel level numcells : Nat)
(st : State n)
:
A mismatching native target can only lower first-code agreement.
theorem
Hex.GraphIso.Nauty.Sparse.classify_eqlev
{n : Nat}
(g : Graph n)
(level numcells : Nat)
(st : State n)
:
theorem
Hex.GraphIso.Nauty.Sparse.depthPolicy
{n : Nat}
(g : Graph n)
(inf tcLevel last : Nat)
:
Generic.StablePolicy g inf tcLevel (Depth last) fun (code : Nat) => code < codeSentinel
The real sparse off-path dispatch retains the terminal sentinel and cannot extend first-code agreement below that saved leaf.
theorem
Hex.GraphIso.Nauty.Sparse.sweep_depth
{n : Nat}
{g : Graph n}
{first : Bool}
{inf tcLevel fuel cfuel level numcells tc tv1 index last : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : State n}
(h : Depth last st)
(hpast : Generic.Past first tv1 cursor)
:
Depth last (Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd
theorem
Hex.GraphIso.Nauty.Sparse.firstPath_depth
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells last : Nat}
{st leaf : State n}
(path : Generic.FirstPath g tcLevel fuel level numcells st last leaf)
(hs : last + 1 < st.firstcode.size)
:
Depth last (Generic.node true g inf tcLevel fuel level numcells st).snd
The actual first-path call retains its installed sentinel and depth bound through every later branch of the production search.