theorem
Hex.GraphIso.Nauty.chooseTarget_unhinted
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hnc : numcells < n)
(hcomp : 0 ≤ st.compCanon)
(heq : Equitable ctx level st.lab st.ptn)
(hlab : LabOk st.lab n)
(hlsz : st.lab.size = n)
(hpsz : st.ptn.size = n)
(hend : st.ptn[st.ptn.size - 1]! ≤ level)
:
(chooseTarget false ctx tcLevel level numcells st).fst = Int.ofNat (specTargetcell ctx st.lab st.ptn level tcLevel)
A nonnegative canonical comparison uses the specification's unhinted target on an equitable partition.
theorem
Hex.GraphIso.Nauty.chooseTarget_hinted
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hnc : numcells < n)
(hlevel : 0 < level)
(heq : st.eqlevFirst = level)
(hcomp : st.compCanon < 0)
(hkeep : (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd.eqlevFirst = level)
:
In the hinted arm, retaining first-code agreement forces the selected position to be the recorded first-path target.
theorem
Hex.GraphIso.Nauty.chooseTarget_match
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hnc : numcells < n)
(hlevel : 0 < level)
(heq : st.eqlevFirst = level)
(hkeep : (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd.eqlevFirst = level)
(hchoice : Int.ofNat (specTargetcell ctx st.lab st.ptn level tcLevel) = st.firsttc[level]!)
(hequitable : Equitable ctx level st.lab st.ptn)
(hlab : LabOk st.lab n)
(hlsz : st.lab.size = n)
(hpsz : st.ptn.size = n)
(hend : st.ptn[st.ptn.size - 1]! ≤ level)
:
Both target-selection arms follow the stored position while first-code agreement survives, provided the unhinted choice follows the reference.
theorem
Hex.GraphIso.Nauty.chooseTarget_fields
{n : Nat}
(ctx : Ctx n)
(tcLevel level numcells : Nat)
(st : Search n)
:
have out := (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd;
out = { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc,
firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows,
compCanon := st.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes,
tctotal := out.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace,
workperm := st.workperm }
Off-path target selection changes only first-code agreement and the target-size counter; in particular the reference target history is frozen.
theorem
Hex.GraphIso.Nauty.chooseTarget_cast
{n : Nat}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{st : Search n}
(hnc : numcells < n)
(heq : st.eqlevFirst = level)
:
Int.ofNat (chooseTarget false ctx tcLevel level numcells st).fst.toNat = (chooseTarget false ctx tcLevel level numcells st).fst
Selecting an active target returns a nonnegative position.