theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_controls
{n : Nat}
(first : Bool)
(g : Graph n)
(tcLevel level numcells : Nat)
(st : State n)
:
have out := (chooseTarget first g tcLevel level numcells st).snd.snd.snd;
out.gcaFirst = st.gcaFirst ∧ out.noncheaplevel = st.noncheaplevel
Actual target dispatch preserves the frozen ancestor and cheap boundary.
theorem
Hex.GraphIso.Nauty.Sparse.classify_controls
{n : Nat}
(g : Graph n)
(level numcells : Nat)
(st : State n)
:
have out := (classify g level numcells st).snd;
out.gcaFirst = st.gcaFirst ∧ out.noncheaplevel = st.noncheaplevel
theorem
Hex.GraphIso.Nauty.Sparse.gcaPolicy
{n : Nat}
(g : Graph n)
(inf tcLevel : Nat)
:
Generic.ReferencePolicy g inf tcLevel fun (st : State n) => st.gcaFirst
Outside the first descent the actual sparse engine retains its frozen first ancestor through every operation and every descendant call.
theorem
Hex.GraphIso.Nauty.Sparse.sweep_gca
{n : Nat}
(first : Bool)
(g : Graph n)
(inf tcLevel fuel cfuel level numcells tc tv1 index : Nat)
(cursor : Option Nat)
(cell : VSet n)
(st : State n)
(hpast : Generic.Past first tv1 cursor)
:
theorem
Hex.GraphIso.Nauty.Sparse.noncheapPolicy
{n : Nat}
(g : Graph n)
(inf tcLevel bound : Nat)
:
Generic.BoundedPolicy g inf tcLevel bound fun (st : State n) => bound < st.noncheaplevel
A failed guard at an ancestor remains failed below that ancestor, including the native cache invalidation and group-order accumulator updates.
theorem
Hex.GraphIso.Nauty.Sparse.node_noncheap
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells bound : Nat}
{st : State n}
(hl : bound < level)
(h : bound < st.noncheaplevel)
:
theorem
Hex.GraphIso.Nauty.Sparse.sweep_noncheap
{n : Nat}
{g : Graph n}
{first : Bool}
{inf tcLevel fuel cfuel level numcells tc tv1 index bound : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : State n}
(hpast : Generic.Past first tv1 cursor)
(hl : bound ≤ level)
(h : bound < st.noncheaplevel)
:
bound < (Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.noncheaplevel