structure
Hex.GraphIso.Nauty.FirstRun
{n k : Nat}
(G : Colored n k)
(ctx : Ctx n)
(tcLevel specFuel runFuel level : Nat)
(codes fs : List Nat)
(st out : SearchSt n)
(numcells : Nat)
(outBest : Option (Key n))
(receiptTrail eventTrail : FrameTrail)
(r : Int)
:
A first-path result with both its reference histories and the reason for its return.
- proof : FirstProof G ctx tcLevel specFuel runFuel level codes fs st out numcells outBest receiptTrail eventTrail r
- short : out.needshortprune = true → ShortSource G ctx out eventTrail r
Instances For
theorem
Hex.GraphIso.Nauty.FirstRun.firstFinish
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells size index : Nat}
{codes fs : List Nat}
{st out : SearchSt n}
{outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(hfuel : runFuel ≠ 0)
(h : FirstRun G ctx tcLevel specFuel runFuel level codes fs st out numcells outBest receiptTrail eventTrail r)
:
FirstRun G ctx tcLevel specFuel runFuel level codes fs st (Nauty.firstFinish level size index out) numcells outBest
receiptTrail eventTrail r
The final first-path counter adjustment preserves the complete first-node result.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.toNodeSome
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat}
{nodeCodes loopCodes 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}
{outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCodes nodeSt nodeNumcells)
(hprefix : List.take nodeCodes.length loopCodes = nodeCodes)
(hfixed : loopSt.fixedpts = nodeSt.fixedpts)
(h :
FirstLoopRun G ctx tcLevel loopSpecFuel runFuel loopFuel level nodeCodes loopCodes fs rsLab rsPtn tc len loopNumcells
tcell cursor bound loopSt out none outBest receiptTrail eventTrail (some r))
:
FirstRun G ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCodes fs nodeSt out nodeNumcells outBest receiptTrail
eventTrail r
An early integer-valued first-path sweep becomes its enclosing node.
theorem
Hex.GraphIso.Nauty.FirstLoopRun.toNodeNone
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel nodeRunFuel runFuel loopFuel level tail : Nat}
{nodeCodes loopCodes 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}
{outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
(hbound : bound = nodeKey ctx tcLevel (specFuel + 1) level nodeCodes nodeSt nodeNumcells)
(hchildren :
nodeKey ctx tcLevel (specFuel + 1) level nodeCodes nodeSt nodeNumcells = keysMax (sweepKey ctx tcLevel specFuel level loopCodes rsLab rsPtn tc loopNumcells 0)
(List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level loopCodes rsLab rsPtn tc loopNumcells (o + 1))
(List.range tail)))
(hlen : len = tail + 1)
(hfuel : n < cursorRank cursor + loopFuel)
(hfixed : loopSt.fixedpts = nodeSt.fixedpts)
(h :
FirstLoopRun G ctx tcLevel specFuel runFuel loopFuel level nodeCodes loopCodes fs rsLab rsPtn tc len loopNumcells
tcell cursor bound loopSt out none outBest receiptTrail eventTrail none)
:
A sufficiently fuelled none sweep is genuine completion and becomes
the enclosing first-path node's ordinary return.
theorem
Hex.GraphIso.Nauty.FirstInv.terminalRun
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{inf tcLevel specFuel fuel level numcells : Nat}
{codes : List Nat}
{st : SearchSt n}
{trail : FrameTrail}
(hn0 : 0 < n)
(hlevel : level = codes.length + 1)
(h : FirstInv G ctx level codes 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 := codes ++ [rs.longcode];
have out := firstPathNode ctx inf tcLevel (fuel + 1) level numcells st;
FirstRun G ctx tcLevel (specFuel + 1) (fuel + 1) level codes full st out.snd numcells
(some (pathLeafKey ctx full rs.lab)) trail trail out.fst
The first discrete leaf is an ordinary exact return in the exit classification.
theorem
Hex.GraphIso.Nauty.dominated_of_firstRun
{n k : Nat}
{G : Colored n k}
(hn0 : n ≠ 0)
{fs : List Nat}
{best : Option (Key n)}
(hroot :
FirstRun G { g := rowsOf G } 100 n (n + 2) 1 [] fs (rootSt n (initialPartition G).fst (initialPartition G).snd)
(rootOut n (rowsOf G) (initialPartition G).fst (initialPartition G).snd) (initialPartition G).snd.length best
FrameTrail.empty FrameTrail.empty
(firstPathNode { g := rowsOf G } (n + 2) 100 (n + 2) 1 (initialPartition G).snd.length
(rootSt n (initialPartition G).fst (initialPartition G).snd)).fst)
:
The first-path root result proves equality between the unpruned specification key and the key installed by the transcription.
theorem
Hex.GraphIso.Nauty.recover_noncheaplevel
(n inf level : Nat)
(st : SearchSt n)
:
(recover n inf level st).noncheaplevel = if level < st.noncheaplevel then level + 1 else st.noncheaplevel
theorem
Hex.GraphIso.Nauty.processnode_noncheaplevel'
{n : Nat}
(ctx : Ctx n)
(level numcells : Nat)
(st : SearchSt n)
:
theorem
Hex.GraphIso.Nauty.processnode_genOrb
{n : Nat}
(ctx : Ctx n)
(level numcells : Nat)
(st : SearchSt n)
:
processnode either leaves both the generator store and the orbit
array alone, or appends one generator and joins the orbits by it.
theorem
Hex.GraphIso.Nauty.processnode_orbSound
{n : Nat}
{ctx : Ctx n}
{level numcells : Nat}
{st : SearchSt n}
(hsound : OrbSound (OrbConn st.genTrace.toList n) st.orbits n)
(hcheck : ∀ (γ : Array Nat), γ ∈ (processnode ctx level numcells st).snd.genTrace → checkAutom ctx.g γ = true)
:
OrbSound (OrbConn (processnode ctx level numcells st).snd.genTrace.toList n)
(processnode ctx level numcells st).snd.orbits n
The orbit array stays sound across a leaf event whose appended generator, if any, is checked.
theorem
Hex.GraphIso.Nauty.SubtreeOk.ofCellsPerm
{n : Nat}
{ctx : Ctx n}
{level : Nat}
{r : RefineSt n}
{lab' : Array Nat}
(h : SubtreeOk ctx level r)
(hperm : cellsPerm r.ptn level r.lab lab')
(hsz : lab'.size = n)
(hok : LabOk lab' n)
(hinj : LabInj lab' n)
:
The small-cell subtree facts depend on the labelling only through its cell contents.
theorem
Hex.GraphIso.Nauty.GuideRel.transRefine
{n level : Nat}
{a b c : SearchSt n}
(hab : GuideRel level a b)
(hbc : GuideRel level b c)
(hsz : a.ptn.size = b.ptn.size)
(hlb : b.lab.size = b.ptn.size)
(hlc : c.canonlab.size = b.ptn.size)
(hendB : b.ptn[b.ptn.size - 1]! ≤ level)
(hendA : a.ptn[a.ptn.size - 1]! ≤ level)
(hgrow : ∀ (q : Nat), a.ptn[q]! ≤ level → b.ptn[q]! ≤ level)
(hperm : cellsPerm a.ptn level a.lab b.lab)
:
GuideRel level a c
Compose a guide relation whose second leg is stated over the refined frame of the first leg's endpoint. Refinement only closes more cell boundaries, so a within-cell permutation of the refined frame is one of the coarser frame.
theorem
Hex.GraphIso.Nauty.EventOut.nonpositive
{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 packaged event leaves the comparison sign nonpositive.
theorem
Hex.GraphIso.Nauty.CodeCmpInv.neg_eq
{nn : Nat}
{cs bs : List Nat}
{canoncode : Array Nat}
{canonlevel : Nat}
{eqlevCanon compCanon : Int}
(h : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon compCanon)
(hneg : compCanon < 0)
:
A negative comparison sign is exactly the frozen downward machine.
theorem
Hex.GraphIso.Nauty.CodeCmpInv.frozenBound
{n nn : Nat}
{cs bs : List Nat}
{ctx : Ctx n}
{canoncode : Array Nat}
{canonlevel : Nat}
{eqlevCanon compCanon : Int}
{canonlab : Array Nat}
(h : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon compCanon)
(hneg : compCanon < 0)
(K : Key n)
:
With the machine frozen downward, every key below the current path is dominated by the incumbent.
theorem
Hex.GraphIso.Nauty.OtherRun.grows
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel specFuel runFuel level numcells : Nat}
{codes fs : List Nat}
{st out : SearchSt n}
{best outBest : Option (Key n)}
{receiptTrail eventTrail : FrameTrail}
{r : Int}
(h : OtherRun G ctx tcLevel specFuel runFuel level codes fs st out numcells best outBest receiptTrail eventTrail r)
(hfuel : runFuel ≠ 0)
:
IncGrows best outBest
Every off-path run only improves the incumbent.