structure
Hex.GraphIso.Nauty.RefTrail
{n : Nat}
(ctx : Ctx n)
(current : Nat)
(st : SearchSt n)
(trail : FrameTrail)
:
Every active frozen frame has the expected labelling size, and each installed leaf reference reaches all active frames no deeper than its current greatest-common-ancestor control.
Instances For
theorem
Hex.GraphIso.Nauty.RefTrail.otherLeaf_gcaFirst
{n : Nat}
(ctx : Ctx n)
(level numcells : Nat)
(st : SearchSt n)
:
The off-path comparison step leaves the first GCA control unchanged.
theorem
Hex.GraphIso.Nauty.RefTrail.otherLeaf_gcaCanon
{n : Nat}
(ctx : Ctx n)
(level numcells : Nat)
(st : SearchSt n)
:
The off-path comparison step leaves the canonical GCA control unchanged.
theorem
Hex.GraphIso.Nauty.RefTrail.otherLeaf_noncheaplevel
{n : Nat}
(ctx : Ctx n)
(level numcells : Nat)
(st : SearchSt n)
:
The off-path comparison step leaves the cheap-automorphism boundary unchanged.
theorem
Hex.GraphIso.Nauty.RefTrail.empty
{n : Nat}
(ctx : Ctx n)
(current : Nat)
(st : SearchSt n)
:
RefTrail ctx current st FrameTrail.empty
The empty trail imposes no reference history.
theorem
Hex.GraphIso.Nauty.RefTrail.firstterminal
{n : Nat}
{ctx : Ctx n}
{level : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(htrail : TrailOk ctx level st trail)
(hsize : ∀ (target : Nat) (entry : TrailEntry), target < level → trail target = some entry → entry.frame.rsLab.size = n)
:
RefTrail ctx level (Nauty.firstterminal level st) trail
Installing the first leaf seeds both reference histories from the current descent, while retaining the accumulated frozen-frame sizes.
theorem
Hex.GraphIso.Nauty.RefTrail.ofCurrent
{n : Nat}
{ctx : Ctx n}
{current : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(htrail : TrailOk ctx current st trail)
(hsize :
∀ (target : Nat) (entry : TrailEntry), target < current → trail target = some entry → entry.frame.rsLab.size = n)
(hfirst : st.firstlab = st.lab)
(hcanon : st.canonlab = st.lab)
:
RefTrail ctx current st trail
When both installed references are the current labelling, the active trail itself supplies their complete history.
theorem
Hex.GraphIso.Nauty.RefTrail.stateEq
{n : Nat}
{ctx : Ctx n}
{current : Nat}
{st st' : SearchSt n}
{trail : FrameTrail}
(h : RefTrail ctx current st trail)
(hfirstGca : st'.gcaFirst = st.gcaFirst)
(hfirst : st'.firstlab = st.firstlab)
(hcanonGca : st'.gcaCanon = st.gcaCanon)
(hcanon : st'.canonlab = st.canonlab)
:
RefTrail ctx current st' trail
Reference history depends only on the two references and their GCA controls.
theorem
Hex.GraphIso.Nauty.RefTrail.otherLeaf
{n : Nat}
{ctx : Ctx n}
{level numcells : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(h : RefTrail ctx level st trail)
:
RefTrail ctx level (otherLeafSt ctx level numcells st) trail
Refinement and the off-path comparison step retain both reference histories.
theorem
Hex.GraphIso.Nauty.RefTrail.recover
{n : Nat}
{ctx : Ctx n}
{current level inf : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(h : RefTrail ctx current st trail)
(hle : level ≤ current)
:
RefTrail ctx level (Nauty.recover n inf level st) trail
Recovering an ancestor preserves both reference histories. The canonical control may be clamped to the recovered level, which only weakens the reach it asserts.
theorem
Hex.GraphIso.Nauty.RefTrail.processnode
{n : Nat}
{ctx : Ctx n}
{level numcells : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(h : RefTrail ctx level st trail)
(htrail : TrailOk ctx level st trail)
:
RefTrail ctx level (Nauty.processnode ctx level numcells st).snd trail
A leaf event retains the first history. It either retains the canonical history as well or installs the current reached labelling as the new canonical reference.
theorem
Hex.GraphIso.Nauty.RefTrail.processnode_order
{n : Nat}
{ctx : Ctx n}
{level numcells : Nat}
{st : SearchSt n}
(horder : st.gcaFirst ≤ st.gcaCanon)
(hfirstBound : st.gcaFirst ≤ level)
:
(Nauty.processnode ctx level numcells st).snd.gcaFirst ≤ (Nauty.processnode ctx level numcells st).snd.gcaCanon
processnode preserves the ordering of the first and canonical GCA
controls. Installing a new canonical leaf parks its control at the
current level, above the bounded first control.
theorem
Hex.GraphIso.Nauty.RefTrail.leafFinish
{n : Nat}
{ctx : Ctx n}
{level current : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(h : RefTrail ctx current st trail)
:
RefTrail ctx current (Nauty.leafFinish level st) trail
Leaf cleanup changes neither installed reference nor its GCA control.
theorem
Hex.GraphIso.Nauty.RefTrail.push
{n : Nat}
{ctx : Ctx n}
{level : Nat}
{st : SearchSt n}
{trail : FrameTrail}
{entry : TrailEntry}
(h : RefTrail ctx level st trail)
(hfirstBound : st.gcaFirst ≤ level)
(hcanonBound : st.gcaCanon ≤ level)
(hsize : entry.frame.rsLab.size = n)
(hfirst : st.gcaFirst = level → cellsPerm entry.frame.rsPtn level entry.frame.rsLab st.firstlab)
(hcanon : st.gcaCanon = level → cellsPerm entry.frame.rsPtn level entry.frame.rsLab st.canonlab)
:
Pushing a child frame extends reference history. At the new frame, the loop's two reference receipts discharge the cases whose GCA control is exactly the parent level.
theorem
Hex.GraphIso.Nauty.RefTrail.LoopInv.childHistory
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel level numcells tc len : Nat}
{tcell : VSet n}
{coset : Nat}
{codes bs fs : List Nat}
{rsLab rsPtn : Array Nat}
{cursor : Option Nat}
{base st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len tcell cursor base st best trail)
(hhist : RefTrail ctx level st trail)
(offset currentOffset : Nat)
:
RefTrail ctx (level + 1)
{ lab := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst,
ptn := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.fst,
active := (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).snd.snd, orbits := st.orbits,
fixedpts := st.fixedpts.insert st.lab[tc + currentOffset]!, 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon,
canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel,
cosetindex := coset, stabvertex := st.stabvertex, needshortprune := st.needshortprune, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }
(trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })
The concrete child state created by a verified sweep inherits both
reference histories. FrameRefs supplies the new parent-frame case.
All shallower frames come directly from the incoming history.
theorem
Hex.GraphIso.Nauty.RefTrail.firstStab
{n : Nat}
{ctx : Ctx n}
{current : Nat}
{st : SearchSt n}
{trail : FrameTrail}
{gamma : Array Nat}
(h : RefTrail ctx current st trail)
(htrail : TrailOk ctx current st trail)
(hfirstSize : st.firstlab.size = n)
(hbelow : st.gcaFirst < current)
(hmap : ∀ (i : Nat), i < n → gamma[st.firstlab[i]!]! = st.lab[i]!)
(target : Nat)
(entry : TrailEntry)
:
A scatter from the first reference onto the current labelling
stabilizes every active frame to which gcaFirst permits a return.
theorem
Hex.GraphIso.Nauty.RefTrail.firstPushStab
{n : Nat}
{ctx : Ctx n}
{current : Nat}
{st out : SearchSt n}
{trail : FrameTrail}
{gamma : Array Nat}
(h : RefTrail ctx current st trail)
(htrail : TrailOk ctx current st trail)
(hfirstSize : st.firstlab.size = n)
(hbelow : st.gcaFirst < current)
(hprev : ReturnStab trail (Int.ofNat st.gcaFirst) st)
(hpush : out.genTrace = st.genTrace.push gamma)
(hmap : ∀ (i : Nat), i < n → gamma[st.firstlab[i]!]! = st.lab[i]!)
:
ReturnStab trail (Int.ofNat st.gcaFirst) out
Appending a first-reference scatter preserves complete return
stabilization at gcaFirst.
theorem
Hex.GraphIso.Nauty.RefTrail.canonStabTo
{n : Nat}
{ctx : Ctx n}
{current limit : Nat}
{st : SearchSt n}
{trail : FrameTrail}
{gamma : Array Nat}
(h : RefTrail ctx current st trail)
(htrail : TrailOk ctx current st trail)
(hcanonSize : st.canonlab.size = n)
(hle : limit ≤ st.gcaCanon)
(hbelow : limit < current)
(hmap : ∀ (i : Nat), i < n → gamma[st.canonlab[i]!]! = st.lab[i]!)
(target : Nat)
(entry : TrailEntry)
:
A scatter from the canonical reference onto the current labelling
stabilizes every active frame through any bound no deeper than
gcaCanon. The smaller bound is needed by code two's orbit return to
gcaFirst.
theorem
Hex.GraphIso.Nauty.RefTrail.canonPushStabTo
{n : Nat}
{ctx : Ctx n}
{current limit : Nat}
{st out : SearchSt n}
{trail : FrameTrail}
{gamma : Array Nat}
(h : RefTrail ctx current st trail)
(htrail : TrailOk ctx current st trail)
(hcanonSize : st.canonlab.size = n)
(hle : limit ≤ st.gcaCanon)
(hbelow : limit < current)
(hprev : ReturnStab trail (Int.ofNat limit) st)
(hpush : out.genTrace = st.genTrace.push gamma)
(hmap : ∀ (i : Nat), i < n → gamma[st.canonlab[i]!]! = st.lab[i]!)
:
ReturnStab trail (Int.ofNat limit) out
Appending a canonical-reference scatter preserves complete return stabilization through any resumable bound below its GCA.
theorem
Hex.GraphIso.Nauty.RefTrail.canonStab
{n : Nat}
{ctx : Ctx n}
{current : Nat}
{st : SearchSt n}
{trail : FrameTrail}
{gamma : Array Nat}
(h : RefTrail ctx current st trail)
(htrail : TrailOk ctx current st trail)
(hcanonSize : st.canonlab.size = n)
(hbelow : st.gcaCanon < current)
(hmap : ∀ (i : Nat), i < n → gamma[st.canonlab[i]!]! = st.lab[i]!)
(target : Nat)
(entry : TrailEntry)
:
The exact canonical-GCA instance of canonStabTo.
theorem
Hex.GraphIso.Nauty.RefTrail.processnodeFirstStab
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{level numcells : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(hn0 : 0 < n)
(h : RefTrail ctx level st trail)
(htrail : TrailOk ctx level st trail)
(hrefs : LeafRefsOk G st)
(hprev : ReturnStab trail (Int.ofNat st.gcaFirst) st)
(hbelow : st.gcaFirst < level)
(heq : (st.eqlevFirst == level) = true)
(hsent : st.firstcode[level + 1]! = codeSentinel)
(hnc : (numcells == n) = true)
(hpass : isautom ctx (firstScatter n st.firstlab st.lab) = true)
:
ReturnStab trail (Nauty.processnode ctx level numcells st).fst (Nauty.processnode ctx level numcells st).snd
A successful code-one admission extends the inherited ancestor stabilization and returns exactly to the first-reference GCA.
theorem
Hex.GraphIso.Nauty.RefTrail.processnodeTiedStab
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{level numcells : Nat}
{st : SearchSt n}
{trail : FrameTrail}
(hn0 : 0 < n)
(h : RefTrail ctx level st trail)
(htrail : TrailOk ctx level st trail)
(hrefs : LeafRefsOk G st)
(horder : st.gcaFirst ≤ st.gcaCanon)
(hprev : ReturnStab trail (Int.ofNat st.gcaFirst) st)
(hcanonBelow : st.gcaCanon < level)
(hef : ¬(st.eqlevFirst == level) = true)
(hnc : (numcells == n) = true)
(hcc : st.compCanon = 0)
(hge : ¬level < st.canonlevel)
(htie : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0)
:
ReturnStab trail (Int.ofNat st.gcaFirst) (Nauty.processnode ctx level numcells st).snd
A code-two admission stabilizes either advertised return: the direct
canonical return uses the full canonical history, while the special orbit
return uses gcaFirst ≤ gcaCanon.
theorem
Hex.GraphIso.Nauty.ReturnStab.otherLeaf
{n : Nat}
{ctx : Ctx n}
{level numcells : Nat}
{st : SearchSt n}
{trail : FrameTrail}
{r : Int}
(h : ReturnStab trail r st)
:
ReturnStab trail r (otherLeafSt ctx level numcells st)
Refinement and the off-path comparison step leave the generator store unchanged.
inductive
Hex.GraphIso.Nauty.EventOut
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel : Nat)
(stem fs : List Nat)
(out : SearchSt n)
(best : Option (Key n))
(trail : FrameTrail)
(r : Int)
:
A recursive result state with a faithful comparison path and every ancestor stabilization enabled by its returned level.
- intro {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {stem fs : List Nat} {out : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} {r : Int} (current : Nat) (codes bestCodes : List Nat) (event : RunEvent G ctx tcLevel current codes bestCodes fs out best trail) (depth : current = codes.length) (stemEq : List.take stem.length codes = stem) (past : stem.length < current) (returned : r ≤ Int.ofNat current) (stable : ReturnStab trail (min r (Int.ofNat out.gcaFirst)) out) (history : RefTrail ctx current out trail) : EventOut G ctx tcLevel stem fs out best trail r
Instances For
theorem
Hex.GraphIso.Nauty.RunEvent.read
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel current : Nat}
{cs bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : RunEvent G ctx tcLevel current cs bs fs st best trail)
:
Every event state reads back the semantic incumbent recorded by its comparison machine. The row-rejection arm uses its reset zero-sign machine.
theorem
Hex.GraphIso.Nauty.RunEvent.setFixed
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel current : Nat}
{cs bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : RunEvent G ctx tcLevel current cs bs fs st best trail)
(fixedpts : VSet n)
:
RunEvent G ctx tcLevel current cs bs fs
{ lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := 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 := st.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,
needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates,
numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves,
maxlevel := st.maxlevel, genTrace := st.genTrace }
best trail
Fixed-point bookkeeping changes none of an event state's logical fields.
theorem
Hex.GraphIso.Nauty.RunEvent.clearShort
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel current : Nat}
{cs bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : RunEvent G ctx tcLevel current cs bs fs st best trail)
:
RunEvent G ctx tcLevel current cs bs fs
{ 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 := st.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 := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }
best trail
Clearing the one-shot short-prune flag changes none of an event state's logical fields.
theorem
Hex.GraphIso.Nauty.RunEvent.setAllsame
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel current allsamelevel : Nat}
{cs bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : RunEvent G ctx tcLevel current cs bs fs st best trail)
:
RunEvent G ctx tcLevel current cs bs fs
{ 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex,
needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates,
numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves,
maxlevel := st.maxlevel, genTrace := st.genTrace }
best trail
Updating the first-path agreement counter changes none of an event state's logical fields.
theorem
Hex.GraphIso.Nauty.RunEvent.setFirst
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel current gcaFirst stabvertex : Nat}
{cs bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : RunEvent G ctx tcLevel current cs bs fs st best trail)
(hguides :
GuideStore ctx tcLevel current
{ 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := stabvertex,
needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates,
numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves,
maxlevel := st.maxlevel, genTrace := st.genTrace }
best trail)
(hpositive : 0 < gcaFirst)
(hbound : gcaFirst ≤ current)
:
RunEvent G ctx tcLevel current cs bs fs
{ 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := stabvertex,
needshortprune := st.needshortprune, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates,
numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves,
maxlevel := st.maxlevel, genTrace := st.genTrace }
best trail
Installing the first-path return controls preserves an event state once the caller supplies the new guide and numeric bounds.
theorem
Hex.GraphIso.Nauty.RunEvent.park
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel current boundary : Nat}
{cs bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : RunEvent G ctx tcLevel current cs bs fs st best trail)
(hpos : 0 < boundary)
(hcurrent : current ≤ boundary)
:
RunEvent G ctx tcLevel current cs bs fs
{ 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 := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := boundary, allsamelevel := st.allsamelevel,
cosetindex := st.cosetindex, stabvertex := st.stabvertex, needshortprune := st.needshortprune,
numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace }
best trail
Parking the cheap-automorphism boundary above the current event level preserves the event invariant.
theorem
Hex.GraphIso.Nauty.RunEvent.leafFinish
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level : Nat}
{cs bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
(h : RunEvent G ctx tcLevel level cs bs fs st best trail)
:
RunEvent G ctx tcLevel level cs bs fs (Nauty.leafFinish level st) best trail
The comparison-blind cleanup after an empty leaf sweep preserves an event state.
theorem
Hex.GraphIso.Nauty.ReturnStab.leafFinish
{n level : Nat}
{st : SearchSt n}
{trail : FrameTrail}
{r : Int}
(h : ReturnStab trail r st)
:
ReturnStab trail r (Nauty.leafFinish level st)
Leaf cleanup leaves the recorded-generator store unchanged.
theorem
Hex.GraphIso.Nauty.EventOut.read
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
:
A packaged event reads back its semantic incumbent.
theorem
Hex.GraphIso.Nauty.EventOut.canonSize
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
:
Every event output retains a full-size canonical reference.
theorem
Hex.GraphIso.Nauty.EventOut.autosOk
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
:
AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 out.autos
Every pair in a result workspace remains valid at the initial coloured partition.
theorem
Hex.GraphIso.Nauty.EventOut.returnStab
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
:
ReturnStab trail (min r (Int.ofNat out.gcaFirst)) out
Every event output exposes stabilization through the smaller of its return target and live first-reference GCA. Direct carrier returns need no stronger statement, while the orbit-return arm targets this GCA.
theorem
Hex.GraphIso.Nauty.EventOut.recoverRun
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level inf numcells : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
(hreturn : r = Int.ofNat level)
(hstem : stem.length = level)
(hlevel : 1 ≤ level)
(hinf : level < inf)
(hfirst : out.gcaFirst ≤ level)
(hok : SearchOk G level numcells (recover n inf level out))
:
Recovering an event that returned exactly to level produces the
stable parent-loop state and retains its generator stabilization.
theorem
Hex.GraphIso.Nauty.EventOut.ofRun
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel level numcells : Nat}
{stem codes bs fs : List Nat}
{st : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : RunInv G ctx tcLevel level codes bs fs numcells st best trail)
(hdepth : level = codes.length)
(hstem : List.take stem.length codes = stem)
(hpast : stem.length < level)
(hreturn : r ≤ Int.ofNat level)
(hnonpositive : st.compCanon ≤ 0)
(hstable : ReturnStab trail (min r (Int.ofNat st.gcaFirst)) st)
(hhistory : RefTrail ctx level st trail)
:
EventOut G ctx tcLevel stem fs st best trail r
A stable state with a nonpositive comparison sign is an event output at its own code depth.
theorem
Hex.GraphIso.Nauty.EventOut.lower
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r r' : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
(hle : r' ≤ r)
:
EventOut G ctx tcLevel stem fs out best trail r'
Weakening the returned level preserves an event output.
theorem
Hex.GraphIso.Nauty.EventOut.setFixed
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
(fixedpts : VSet n)
:
EventOut G ctx tcLevel stem fs
{ lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := fixedpts,
autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode,
firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong,
samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon,
gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel,
noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex,
stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes,
tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits,
numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel,
genTrace := out.genTrace }
best trail r
Fixed-point cleanup preserves the full result-side package.
theorem
Hex.GraphIso.Nauty.EventOut.clearShort
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
:
EventOut G ctx tcLevel stem fs
{ lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts,
autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode,
firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong,
samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon,
gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel,
noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex,
stabvertex := out.stabvertex, numnodes := out.numnodes, tctotal := out.tctotal, canupdates := out.canupdates,
numorbits := out.numorbits, numgenerators := out.numgenerators, numbadleaves := out.numbadleaves,
maxlevel := out.maxlevel, genTrace := out.genTrace }
best trail r
Clearing the short-prune request preserves the full result package.
theorem
Hex.GraphIso.Nauty.EventOut.setAllsame
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel allsamelevel : Nat}
{stem fs : List Nat}
{out : SearchSt n}
{best : Option (Key n)}
{trail : FrameTrail}
{r : Int}
(h : EventOut G ctx tcLevel stem fs out best trail r)
:
EventOut G ctx tcLevel stem fs
{ lab := out.lab, ptn := out.ptn, active := out.active, orbits := out.orbits, fixedpts := out.fixedpts,
autos := out.autos, wsCap := out.wsCap, firstcode := out.firstcode, canoncode := out.canoncode,
firsttc := out.firsttc, firstlab := out.firstlab, canonlab := out.canonlab, canong := out.canong,
samerows := out.samerows, compCanon := out.compCanon, eqlevFirst := out.eqlevFirst, eqlevCanon := out.eqlevCanon,
gcaFirst := out.gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel,
noncheaplevel := out.noncheaplevel, allsamelevel := allsamelevel, cosetindex := out.cosetindex,
stabvertex := out.stabvertex, needshortprune := out.needshortprune, numnodes := out.numnodes,
tctotal := out.tctotal, canupdates := out.canupdates, numorbits := out.numorbits,
numgenerators := out.numgenerators, numbadleaves := out.numbadleaves, maxlevel := out.maxlevel,
genTrace := out.genTrace }
best trail r
Updating the first-path agreement counter preserves the full result package.
An output trail retains every frame that was active on entry. A node may additionally replace deeper scratch entries used by its own recursive sweep.
Equations
- Hex.GraphIso.Nauty.TrailExt level before after = ∀ (target : Nat), target < level → after target = before target
Instances For
theorem
Hex.GraphIso.Nauty.TrailExt.refl
(level : Nat)
(trail : FrameTrail)
:
TrailExt level trail trail
theorem
Hex.GraphIso.Nauty.TrailExt.trans
{level : Nat}
{a b c : FrameTrail}
(hab : TrailExt level a b)
(hbc : TrailExt level b c)
:
TrailExt level a c
theorem
Hex.GraphIso.Nauty.TrailExt.ofPush
{level : Nat}
{trail out : FrameTrail}
{entry : TrailEntry}
(h : TrailExt (level + 1) (trail.push level entry) out)
:
TrailExt level trail out
Retaining a pushed child trail retains every older parent frame.
theorem
Hex.GraphIso.Nauty.TrailExt.pushAt
{level : Nat}
{trail out : FrameTrail}
{entry : TrailEntry}
(h : TrailExt (level + 1) (trail.push level entry) out)
:
Retaining a pushed child trail keeps the newly active parent frame at its exact level.
theorem
Hex.GraphIso.Nauty.Unwind.Located.retrail
{n : Nat}
{ctx : Ctx n}
{tcLevel target : Nat}
{out : SearchSt n}
{best : Option (Key n)}
{source dest : FrameTrail}
{payload : Unwind ctx tcLevel target out best}
(h : Located source payload)
(heq : source target = dest target)
:
Located dest payload
Location evidence can be moved between trails that agree at the unwind target.
theorem
Hex.GraphIso.Nauty.LoopReceipt.retrail
{n : Nat}
{ctx : Ctx n}
{tcLevel specFuel runFuel loopFuel level : Nat}
{cs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len numcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{source dest : FrameTrail}
{r : Option Int}
(htrail : TrailExt level dest source)
(h :
LoopReceipt source ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st
out best outBest r)
:
LoopReceipt dest ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out
best outBest r
A loop receipt depends on its trail only below the loop level.
structure
Hex.GraphIso.Nauty.NodeOutcome
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel specFuel runFuel level : Nat)
(cs fs : List Nat)
(st out : SearchSt n)
(numcells : Nat)
(best outBest : Option (Key n))
(receiptTrail eventTrail : FrameTrail)
(r : Int)
:
The semantic node receipt and the concrete result state produced by one recursive node call.
- receipt : NodeReceipt receiptTrail ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
- event : EventOut G ctx tcLevel cs fs out outBest eventTrail r
- preserved : TrailExt level receiptTrail eventTrail
Instances For
theorem
Hex.GraphIso.Nauty.NodeOutcome.toResult
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells : Nat}
{cs fs : List Nat}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(h : NodeOutcome G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r)
:
NodeResult ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
Forgetting the concrete result invariant recovers the semantic node result consumed by the root reduction.
theorem
Hex.GraphIso.Nauty.NodeOutcome.parentReturn
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells : Nat}
{cs fs : List Nat}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{r : Int}
{trail eventTrail : FrameTrail}
{entry : TrailEntry}
(h :
NodeOutcome G ctx tcLevel specFuel runFuel (level + 1) cs fs st out numcells best outBest (trail.push level entry)
eventTrail r)
(hfuel : runFuel ≠ 0)
(hstay : ¬r < Int.ofNat level)
:
At a parent boundary, a child outcome either supplies its exact subtree maximum or a located unwind whose generator store stabilizes the receiving frozen frame.
theorem
Hex.GraphIso.Nauty.NodeOutcome.parentEq
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells : Nat}
{cs fs : List Nat}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{r : Int}
{receiptTrail eventTrail : FrameTrail}
(h :
NodeOutcome G ctx tcLevel specFuel runFuel (level + 1) cs fs st out numcells best outBest receiptTrail eventTrail r)
(hfuel : runFuel ≠ 0)
(hstay : ¬r < Int.ofNat level)
:
A positive-fuel child that does not unwind past its parent returns exactly to that parent level.
structure
Hex.GraphIso.Nauty.OtherOutcome
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel specFuel runFuel level : Nat)
(cs fs : List Nat)
(st out : SearchSt n)
(numcells : Nat)
(best outBest : Option (Key n))
(receiptTrail eventTrail : FrameTrail)
(r : Int)
:
An off-path node additionally leaves the first-path guide unchanged.
It also preserves live guide ordering. Unlike a first-path node, it never
raises gcaFirst while returning through its child loop. These are the
facts its parent needs before recovering a completed child.
- node : NodeOutcome G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r
Instances For
The integer return represented by a loop result. Exhausting the sweep completes its parent node one level up.
Equations
- Hex.GraphIso.Nauty.loopReturn level (some r) = r
- Hex.GraphIso.Nauty.loopReturn level none = Int.ofNat level - 1
Instances For
structure
Hex.GraphIso.Nauty.LoopOutcome
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel specFuel runFuel loopFuel level : Nat)
(stem codes fs : List Nat)
(rsLab rsPtn : Array Nat)
(tc len numcells : Nat)
(tcell : VSet n)
(cursor : Option Nat)
(bound : Key n)
(st out : SearchSt n)
(best outBest : Option (Key n))
(receiptTrail eventTrail : FrameTrail)
(r : Option Int)
:
A loop receipt coupled to the concrete result invariant ultimately
returned by its parent node. stem is the parent node's entry prefix.
The loop's own codes include that node's refinement code.
- receipt : LoopReceipt receiptTrail ctx tcLevel specFuel runFuel loopFuel level codes rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r
- event : EventOut G ctx tcLevel stem fs out outBest eventTrail (loopReturn level r)
- preserved : TrailExt level receiptTrail eventTrail
Instances For
theorem
Hex.GraphIso.Nauty.LoopOutcome.toNodeSome
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat}
{nodeCs loopCs fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCs nodeSt nodeNumcells)
(h :
LoopOutcome G ctx tcLevel loopSpecFuel runFuel loopFuel level nodeCs loopCs fs rsLab rsPtn tc len loopNumcells tcell
cursor bound loopSt out best outBest receiptTrail eventTrail (some r))
:
NodeOutcome G ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCs fs nodeSt out nodeNumcells best outBest receiptTrail
eventTrail r
A loop that returns an integer supplies its parent node outcome.
theorem
Hex.GraphIso.Nauty.LoopOutcome.toNodeNone
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel nodeRunFuel runFuel loopFuel level tail : Nat}
{nodeCs loopCs fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len nodeNumcells loopNumcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{nodeSt loopSt out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
(hbound : bound = nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells)
(hchildren :
nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells = keysMax (sweepKey ctx tcLevel specFuel level loopCs rsLab rsPtn tc loopNumcells 0)
(List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level loopCs rsLab rsPtn tc loopNumcells (o + 1))
(List.range tail)))
(hlen : len = tail + 1)
(hfuel : n < cursorRank cursor + loopFuel)
(h :
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level nodeCs loopCs fs rsLab rsPtn tc len loopNumcells tcell
cursor bound loopSt out best outBest receiptTrail eventTrail none)
:
NodeOutcome G ctx tcLevel (specFuel + 1) nodeRunFuel level nodeCs fs nodeSt out nodeNumcells best outBest receiptTrail
eventTrail (Int.ofNat level - 1)
A completed loop with sufficient cursor fuel supplies its parent node's completed outcome.
theorem
Hex.GraphIso.Nauty.LoopOutcome.prefix
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel loopFuel level : Nat}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len numcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{st recSt out : SearchSt n}
{best mid outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(hpre : LoopSound ctx bound best mid)
(h :
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound
recSt out mid outBest receiptTrail eventTrail r)
:
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound
st out best outBest receiptTrail eventTrail r
Prepending a semantic loop fragment leaves the concrete result package unchanged.
theorem
Hex.GraphIso.Nauty.LoopOutcome.reindexSet
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel loopFuel level : Nat}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len numcells : Nat}
{tcell tcell' : VSet n}
{cursor : Option Nat}
{bound : Key n}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(h :
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound
st out best outBest receiptTrail eventTrail r)
:
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell' cursor bound
st out best outBest receiptTrail eventTrail r
Changing the mutable entry workset does not affect a completed loop outcome.
theorem
Hex.GraphIso.Nauty.LoopOutcome.step
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel loopFuel level tv : Nat}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len numcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Option Int}
(ha : After cursor tv)
(h :
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell (some tv)
bound st out best outBest receiptTrail eventTrail r)
:
LoopOutcome G ctx tcLevel specFuel runFuel (loopFuel + 1) level stem codes fs rsLab rsPtn tc len numcells tcell cursor
bound st out best outBest receiptTrail eventTrail r
One successful cursor step preserves the coupled loop outcome.
theorem
Hex.GraphIso.Nauty.LoopOutcome.retrail
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel loopFuel level : Nat}
{stem codes fs : List Nat}
{rsLab rsPtn : Array Nat}
{tc len numcells : Nat}
{tcell : VSet n}
{cursor : Option Nat}
{bound : Key n}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{source dest eventTrail : FrameTrail}
{r : Option Int}
(htrail : TrailExt level dest source)
(h :
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound
st out best outBest source eventTrail r)
:
LoopOutcome G ctx tcLevel specFuel runFuel loopFuel level stem codes fs rsLab rsPtn tc len numcells tcell cursor bound
st out best outBest dest eventTrail r
A coupled loop outcome can be rebased onto an entry trail that agrees below the loop level.
theorem
Hex.GraphIso.Nauty.NodeOutcome.firstFinish
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells size index : Nat}
{cs fs : List Nat}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(hfuel : runFuel ≠ 0)
(h : NodeOutcome G ctx tcLevel specFuel runFuel level cs fs st out numcells best outBest receiptTrail eventTrail r)
:
NodeOutcome G ctx tcLevel specFuel runFuel level cs fs st (Nauty.firstFinish level size index out) numcells best outBest
receiptTrail eventTrail r
First-path exit bookkeeping preserves a node outcome.
theorem
Hex.GraphIso.Nauty.FirstInv.terminalOutcome
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel fuel level numcells : Nat}
{cs : List Nat}
{st : SearchSt n}
{trail : FrameTrail}
(hn0 : 0 < n)
(hlevel : level = cs.length + 1)
(h : FirstInv G ctx level cs numcells st trail)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have full := cs ++ [rs.longcode];
have out := firstPathNode ctx inf tcLevel (fuel + 1) level numcells st;
NodeOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level cs full st out.snd numcells none
(some (pathLeafKey ctx full rs.lab)) trail trail out.fst
The first discrete leaf closes the result package. Its generator store is still empty, so every return-frame stabilization holds vacuously.
theorem
Hex.GraphIso.Nauty.firstPath_internal_outcome
{n k : Nat}
{G : Colored n k}
(ctx : Ctx n)
(inf tcLevel specFuel fuel level numcells tail : Nat)
(cs fs : List Nat)
(st : SearchSt n)
(best outBest : Option (Key n))
(trail outTrail : FrameTrail)
(hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells ≠ n)
(hchildren :
nodeKey ctx tcLevel (specFuel + 1) level cs st numcells = have rs := refine ctx level st.lab st.ptn st.active numcells;
have mt := maketargetcell ctx rs.lab rs.ptn level tcLevel (-1);
keysMax (sweepKey ctx tcLevel specFuel level (cs ++ [rs.longcode]) rs.lab rs.ptn mt.fst rs.numcells 0)
(List.map
(fun (o : Nat) =>
sweepKey ctx tcLevel specFuel level (cs ++ [rs.longcode]) rs.lab rs.ptn mt.fst rs.numcells (o + 1))
(List.range tail)))
(hlen :
(maketargetcell ctx (refine ctx level st.lab st.ptn st.active numcells).lab
(refine ctx level st.lab st.ptn st.active numcells).ptn level tcLevel (-1)).snd.snd = tail + 1)
:
have rs := refine ctx level st.lab st.ptn st.active numcells;
have mt := maketargetcell ctx rs.lab rs.ptn level tcLevel (-1);
have pre0 :=
{ lab := rs.lab, ptn := rs.ptn, active := rs.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode.set! level rs.longcode, canoncode := st.canoncode,
firsttc := st.firsttc.set! level (Int.ofNat mt.fst), firstlab := st.firstlab, canonlab := st.canonlab,
canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.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, needshortprune := st.needshortprune, numnodes := st.numnodes + 1,
tctotal := st.tctotal + mt.snd.snd, canupdates := st.canupdates, numorbits := st.numorbits,
numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel,
genTrace := st.genTrace };
have pre :=
if pre0.noncheaplevel ≥ level ∧ ¬cheapautom pre0.ptn level n = true then
{ lab := pre0.lab, ptn := pre0.ptn, active := pre0.active, orbits := pre0.orbits, fixedpts := pre0.fixedpts,
autos := pre0.autos, wsCap := pre0.wsCap, firstcode := pre0.firstcode, canoncode := pre0.canoncode,
firsttc := pre0.firsttc, firstlab := pre0.firstlab, canonlab := pre0.canonlab, canong := pre0.canong,
samerows := pre0.samerows, compCanon := pre0.compCanon, eqlevFirst := pre0.eqlevFirst,
eqlevCanon := pre0.eqlevCanon, gcaFirst := pre0.gcaFirst, gcaCanon := pre0.gcaCanon,
canonlevel := pre0.canonlevel, noncheaplevel := level + 1, allsamelevel := pre0.allsamelevel,
cosetindex := pre0.cosetindex, stabvertex := pre0.stabvertex, needshortprune := pre0.needshortprune,
numnodes := pre0.numnodes, tctotal := pre0.tctotal, canupdates := pre0.canupdates, numorbits := pre0.numorbits,
numgenerators := pre0.numgenerators, numbadleaves := pre0.numbadleaves, maxlevel := pre0.maxlevel,
genTrace := pre0.genTrace }
else pre0;
have L :=
firstChildLoop ctx inf tcLevel fuel (n + 1) level rs.numcells mt.fst ((mt.snd.fst.nextElem none).getD 0)
(mt.snd.fst.nextElem none) mt.snd.fst 0 pre;
LoopOutcome G ctx tcLevel specFuel fuel (n + 1) level cs (cs ++ [rs.longcode]) fs rs.lab rs.ptn mt.fst mt.snd.snd
rs.numcells mt.snd.fst none (nodeKey ctx tcLevel (specFuel + 1) level cs st numcells) pre L.snd.snd best outBest
trail outTrail L.fst →
NodeOutcome G ctx tcLevel (specFuel + 1) (fuel + 1) level cs fs st
(firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest trail outTrail
(firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).fst
A coupled child-loop outcome supplies the complete outcome of a non-discrete first-path node.
theorem
Hex.GraphIso.Nauty.otherNode_outcome
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel fuel level nodeNumcells loopNumcells tail : Nat}
{nodeCs loopCs fs : List Nat}
{nodeSt loopSt : SearchSt n}
{rsLab rsPtn : Array Nat}
{tc len : Nat}
{tcell : VSet n}
{best outBest : Option (Key n)}
{trail outTrail : FrameTrail}
{L : Option Int × SearchSt n}
(hchildren :
nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells = keysMax (sweepKey ctx tcLevel specFuel level loopCs rsLab rsPtn tc loopNumcells 0)
(List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level loopCs rsLab rsPtn tc loopNumcells (o + 1))
(List.range tail)))
(hlen : len = tail + 1)
(hstate :
otherNode ctx inf tcLevel (fuel + 1) level nodeNumcells nodeSt = match L.fst with
| some r => (r, L.snd)
| none => (Int.ofNat level - 1, L.snd))
(hloop :
LoopOutcome G ctx tcLevel specFuel fuel (n + 1) level nodeCs loopCs fs rsLab rsPtn tc len loopNumcells tcell none
(nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells) loopSt L.snd best outBest trail outTrail
L.fst)
:
Once the imperative prefix exposes an off-path child loop, its coupled outcome constructs the corresponding node outcome.