theorem
Hex.GraphIso.Nauty.Sparse.chooseTarget_reference
{n : Nat}
(g : Graph n)
(tcLevel level numcells : Nat)
(st : State n)
:
SearchState.reference (chooseTarget false g tcLevel level numcells st).snd.snd.snd = SearchState.reference st
Off-path target selection may borrow scratch and update comparison controls, but retains all saved first-path reference fields.
theorem
Hex.GraphIso.Nauty.Sparse.classify_reference
{n : Nat}
(g : Graph n)
(level numcells : Nat)
(st : State n)
:
Native row comparisons and automorphism scattering preserve the saved first leaf, first codes and target hints.
theorem
Hex.GraphIso.Nauty.Sparse.referencePolicy
{n : Nat}
(g : Graph n)
(inf tcLevel : Nat)
:
Generic.ReferencePolicy g inf tcLevel SearchState.reference
All actual sparse off-path operations preserve the first reference. Common bookkeeping lemmas apply to arbitrary canonical storage.
theorem
Hex.GraphIso.Nauty.Sparse.node_reference
{n : Nat}
(g : Graph n)
(inf tcLevel fuel level numcells : Nat)
(st : State n)
:
SearchState.reference (Generic.node false g inf tcLevel fuel level numcells st).snd = SearchState.reference st
theorem
Hex.GraphIso.Nauty.Sparse.sweep_reference
{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)
:
SearchState.reference
(Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd = SearchState.reference st
theorem
Hex.GraphIso.Nauty.Sparse.firstPath_reference
{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)
:
SearchState.reference (Generic.node true g inf tcLevel fuel level numcells st).snd = (firstterminal last leaf).reference
The saved reference of the completed first-path call is exactly the reference installed at its actual first leaf.