structure Hex.GraphIso.Nauty.DescentCodes {n : Nat} (nn : Nat) (cs : List Nat) (st : SearchSt n) : Prop

Code storage on the unique descent before the first leaf exists. Unlike FirstCodeInv, this phase has no stored first-leaf sentinel yet.

• firstSize : st.firstcode.size = nn + 2
• canonSize : st.canoncode.size = nn + 2
• bound : cs.length + 1 ≤ nn
• content (i : Nat) : 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!
• lt (c : Nat) : c ∈ cs → c < codeSentinel

theorem Hex.GraphIso.Nauty.DescentCodes.root {n : Nat} (lab : Array Nat) (cellEnds : List Nat) (hn0 : 0 < n) : DescentCodes n [] (rootSt n lab cellEnds)

The nonempty root begins the pre-incumbent descent with no codes.

theorem Hex.GraphIso.Nauty.DescentCodes.next {n nn : Nat} {cs : List Nat} {st st' : SearchSt n} {code : Nat} (h : DescentCodes nn cs st) (hfirst : st'.firstcode = st.firstcode.set! (cs.length + 1) code) (hcanon : st'.canoncode = st.canoncode) (hbound : cs.length + 2 ≤ nn) (hlt : code < codeSentinel) : DescentCodes nn (cs ++ [code]) st'

Writing one real refinement code advances the pre-incumbent descent to its child.

theorem Hex.GraphIso.Nauty.stInc_firstterminal {n : Nat} {ctx : Ctx n} {nn level : Nat} {cs : List Nat} {st : SearchSt n} (hlevel : level = cs.length) (hne : cs ≠ []) (hcanon : st.canoncode.size = nn + 2) (hbound : cs.length ≤ nn) (hcodes : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (hlt : ∀ (c : Nat), c ∈ cs → c < codeSentinel) : stInc ctx (firstterminal level st) = some (pathLeafKey ctx cs st.lab)

Once the first descent reaches a real leaf, firstterminal installs exactly that leaf as the semantic incumbent.

def Hex.GraphIso.Nauty.firstLeafSt {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : SearchSt n

The state immediately before the first-path leaf is installed.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.firstPath_discrete_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hdisc : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) : firstPathNode ctx inf tcLevel (fuel + 1) level numcells st = (Int.ofNat level - 1, firstterminal level (firstLeafSt ctx level numcells st))

The discrete arm of firstPathNode is exactly firstterminal on the refined leaf state.

theorem Hex.GraphIso.Nauty.refine_discrete_iff {n k : Nat} {G : Colored n k} {ctx : Ctx n} (hn0 : 0 < n) {level numcells : Nat} {st : SearchSt n} (hok : SearchOk G level numcells st) (hlevel : 1 ≤ level) : (refine ctx level st.lab st.ptn st.active numcells).numcells = n ↔ discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true

Under the search invariant, the transcription's refined cell-count guard agrees with the specification's discreteness guard.

theorem Hex.GraphIso.Nauty.firstLeafSt_codes {n : Nat} {ctx : Ctx n} {nn level numcells : Nat} {cs : List Nat} {st : SearchSt n} (hlevel : level = cs.length + 1) (hsize : st.firstcode.size = nn + 2) (hle : level ≤ nn) (hcodes : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (i : Nat) : 1 ≤ i → i ≤ (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]).length → (firstLeafSt ctx level numcells st).firstcode[i]! = (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode])[i - 1]!

Writing the current refinement code extends the stored first-path code sequence by one entry.

theorem Hex.GraphIso.Nauty.firstPath_discrete {n : Nat} {ctx : Ctx n} {nn inf tcLevel specFuel fuel level numcells : Nat} {cs : List Nat} {st : SearchSt n} (hlevel : level = cs.length + 1) (hfirstSize : st.firstcode.size = nn + 2) (hcanonSize : st.canoncode.size = nn + 2) (hle : level ≤ nn) (hcodes : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (hlt : ∀ (c : Nat), c ∈ cs → c < codeSentinel) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells none (some (nodeKey ctx tcLevel (specFuel + 1) level cs st numcells)) (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A discrete first-path node installs the exact specification leaf and returns ordinary completion. This is the phase transition from an absent incumbent to the stable off-path comparison state.

theorem Hex.GraphIso.Nauty.firstPath_discrete_of_ok {n k : Nat} {G : Colored n k} {ctx : Ctx n} (hn0 : 0 < n) {inf tcLevel specFuel fuel numcells : Nat} {cs : List Nat} {st : SearchSt n} (hok : SearchOk G (cs.length + 1) numcells st) (hcodes : DescentCodes n cs st) (hnum : (refine ctx (cs.length + 1) st.lab st.ptn st.active numcells).numcells = n) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) (cs.length + 1) cs st (firstPathNode ctx inf tcLevel (fuel + 1) (cs.length + 1) numcells st).snd numcells none (some (nodeKey ctx tcLevel (specFuel + 1) (cs.length + 1) cs st numcells)) (firstPathNode ctx inf tcLevel (fuel + 1) (cs.length + 1) numcells st).fst

The invariant-packaged first-path leaf rule: the search invariant supplies guard agreement and DescentCodes supplies the pre-incumbent code store.

theorem Hex.GraphIso.Nauty.root_result_of_discrete {n k : Nat} {G : Colored n k} (hn0 : 0 < n) (hnum : (refine { g := rowsOf G } 1 (rootSt n (initialPartition G).fst (initialPartition G).snd).lab (rootSt n (initialPartition G).fst (initialPartition G).snd).ptn (rootSt n (initialPartition G).fst (initialPartition G).snd).active (initialPartition G).snd.length).numcells = n) : NodeResult { g := rowsOf G } 100 n (n + 2) 1 [] (rootSt n (initialPartition G).fst (initialPartition G).snd) (rootOut n (rowsOf G) (initialPartition G).fst (initialPartition G).snd) (initialPartition G).snd.length none (some (nodeKey { g := rowsOf G } 100 n 1 [] (rootSt n (initialPartition G).fst (initialPartition G).snd) (initialPartition G).snd.length)) (firstPathNode { g := rowsOf G } (n + 2) 100 (n + 2) 1 (initialPartition G).snd.length (rootSt n (initialPartition G).fst (initialPartition G).snd)).fst

The root outcome is closed outright when root refinement is already discrete.

def Hex.GraphIso.Nauty.otherLeafSt {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : SearchSt n

The refined and compared state on entry to an off-path leaf event.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.otherLeafSt_short {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : SearchSt n) : (otherLeafSt ctx level numcells st).needshortprune = st.needshortprune

Refinement and comparison preparation do not alter the one-shot short-prune request carried into a leaf.

theorem Hex.GraphIso.Nauty.otherNode_leaf_early {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : otherNode ctx inf tcLevel (fuel + 1) level numcells st = processnode ctx level n (otherLeafSt ctx level numcells st)

If a discrete off-path leaf requests an early unwind, otherNode returns its processnode result verbatim.

def Hex.GraphIso.Nauty.leafFinish {n : Nat} (level : Nat) (st : SearchSt n) : SearchSt n

The comparison-blind cleanup performed when a leaf event does not request an early unwind.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.leafFinish_short {n : Nat} (level : Nat) (st : SearchSt n) : (leafFinish level st).needshortprune = false

Leaf cleanup always consumes a pending one-shot short-prune request.

theorem Hex.GraphIso.Nauty.otherNode_leaf_done_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdone : ¬(processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : otherNode ctx inf tcLevel (fuel + 1) level numcells st = (Int.ofNat level - 1, leafFinish level (processnode ctx level n (otherLeafSt ctx level numcells st)).snd)

A discrete off-path leaf that does not unwind runs the empty child sweep and returns ordinary node completion.

theorem Hex.GraphIso.Nauty.incKey_max_nonempty {n : Nat} {ctx : Ctx n} {bs cs bs' : List Nat} {canonlab canonlab' lab : Array Nat} (hbs : bs ≠ []) (hcs : cs ≠ []) (hmax : incKey ctx bs' canonlab' = keyMax (incKey ctx bs canonlab) (pathLeafKey ctx cs lab)) : bs' ≠ []

The maximum of two installed leaf keys still has a nonempty path.

theorem Hex.GraphIso.Nauty.processnode_leaf_read {n nn : Nat} {ctx : Ctx n} {cs bs : List Nat} {numcells : Nat} {st : SearchSt n} (hcinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hginv : CanongInv ctx st.canong st.canonlab st.samerows) (hcsn : cs.length ≤ nn) (hbs : bs ≠ []) (hcs : cs ≠ []) (hef : ¬(st.eqlevFirst == cs.length) = true) (hnc : (numcells == n) = true) : ∃ (bs' : List Nat), stInc ctx (processnode ctx cs.length numcells st).snd = some (keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab)) ∧ CanongInv ctx (processnode ctx cs.length numcells st).snd.canong (processnode ctx cs.length numcells st).snd.canonlab (processnode ctx cs.length numcells st).snd.samerows ∧ ((processnode ctx cs.length numcells st).snd.compCanon ≤ 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon (processnode ctx cs.length numcells st).snd.compCanon ∨ (processnode ctx cs.length numcells st).snd.compCanon < 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon 0) ∧ ((processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∨ (processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat cs.length) ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaCanon)

The faithful off-path leaf event can be read through stInc even in the row-rejection arm, where compCanon holds a row comparison result rather than a canonical one.

theorem Hex.GraphIso.Nauty.processnode_leafFirst_read {n nn : Nat} {ctx : Ctx n} {cs bs : List Nat} {numcells : Nat} {st : SearchSt n} (hcinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hginv : CanongInv ctx st.canong st.canonlab st.samerows) (hcsn : cs.length ≤ nn) (hbs : bs ≠ []) (hcs : cs ≠ []) (heq : (st.eqlevFirst == cs.length) = true) (hfail : st.firstcode[cs.length + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) (hnc : (numcells == n) = true) : ∃ (bs' : List Nat), stInc ctx (processnode ctx cs.length numcells st).snd = some (keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab)) ∧ CanongInv ctx (processnode ctx cs.length numcells st).snd.canong (processnode ctx cs.length numcells st).snd.canonlab (processnode ctx cs.length numcells st).snd.samerows ∧ ((processnode ctx cs.length numcells st).snd.compCanon ≤ 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon (processnode ctx cs.length numcells st).snd.compCanon ∨ (processnode ctx cs.length numcells st).snd.compCanon < 0 ∧ CodeCmpInv nn cs bs' (processnode ctx cs.length numcells st).snd.canoncode (processnode ctx cs.length numcells st).snd.canonlevel (processnode ctx cs.length numcells st).snd.eqlevCanon 0) ∧ ((processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∨ (processnode ctx cs.length numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat cs.length) ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx cs.length numcells st).fst = Int.ofNat st.gcaCanon)

The first-path-agreeing leaf whose guarded admission fails has the same exact incumbent read as the ordinary leaf comparison.

theorem Hex.GraphIso.Nauty.canonlevel_ne_zero_of_stInc {n : Nat} {ctx : Ctx n} {st : SearchSt n} {B : Key n} (h : stInc ctx st = some B) : st.canonlevel ≠ 0

Reading a present incumbent proves that a canonical leaf has been installed in the mutable state.

theorem Hex.GraphIso.Nauty.otherNode_leaf_pruned_of_read {n : Nat} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) (hread : stInc ctx (processnode ctx level n (otherLeafSt ctx level numcells st)).snd = some (keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab))) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells (some (incKey ctx bs st.canonlab)) (some (keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab))) (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

Any early off-path leaf event that exposes its exact incumbent read constructs the local pruned outcome. Event-specific comparison proofs only need to establish hread.

theorem Hex.GraphIso.Nauty.otherNode_leaf_unwind_of_event {n : Nat} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells target : Nat} {cs : List Nat} {st : SearchSt n} {best outBest : Option (Key n)} (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hreturn : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst = Int.ofNat target) (hbelow : target < level) (hsound : NodeSound ctx tcLevel (specFuel + 1) level cs st numcells best outBest) (hpayload : Unwind ctx tcLevel target (processnode ctx level n (otherLeafSt ctx level numcells st)).snd outBest) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A leaf event returning a generator carrier to a strict ancestor lifts directly to the node's explicit unwind outcome.

theorem Hex.GraphIso.Nauty.otherNode_leaf_firstAuto {n : Nat} {ctx : Ctx n} {nn inf tcLevel specFuel fuel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} (hlevel : level = cs.length + 1) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hfirstInv : FirstCodeInv nn (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) fs (otherLeafSt ctx level numcells st).firstcode (otherLeafSt ctx level numcells st).eqlevFirst) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hsent : (otherLeafSt ctx level numcells st).firstcode[level + 1]! = codeSentinel) (hpass : isautom ctx (firstScatter n (otherLeafSt ctx level numcells st).firstlab (otherLeafSt ctx level numcells st).lab) = true) (hgsz : ctx.g.size = n) (hfirstSize : (otherLeafSt ctx level numcells st).firstlab.size = n) (hfirstOk : LabOk (otherLeafSt ctx level numcells st).firstlab n) (hfirstPerm : (otherLeafSt ctx level numcells st).firstlab.toList.Perm (List.range n)) (hlabSize : (otherLeafSt ctx level numcells st).lab.size = n) (hlabPerm : (otherLeafSt ctx level numcells st).lab.toList.Perm (List.range n)) (hsymm : ∀ (i j : Nat), i < n → j < n → ctx.g[i]!.mem j = ctx.g[j]!.mem i) (hloop : ∀ (i : Nat), i < n → ctx.g[i]!.mem i = false) (hfirstKey : keyLe (pathLeafKey ctx fs (otherLeafSt ctx level numcells st).firstlab) (incKey ctx bs st.canonlab)) (hbelow : (otherLeafSt ctx level numcells st).gcaFirst < level) (g : Guide ctx tcLevel (otherLeafSt ctx level numcells st).gcaFirst (some (incKey ctx bs st.canonlab))) (href : g.ref = (otherLeafSt ctx level numcells st).firstlab) (hcurReach : cellsPerm g.rsPtn (otherLeafSt ctx level numcells st).gcaFirst g.rsLab (otherLeafSt ctx level numcells st).lab) {oCur : Nat} (hcur : oCur < g.len) (hatCur : (otherLeafSt ctx level numcells st).lab[g.tc]! = g.rsLab[g.tc + oCur]!) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells (some (incKey ctx bs st.canonlab)) (some (incKey ctx bs st.canonlab)) (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A successful code-one leaf is a genuine generator unwind: the sentinel identifies its path with the stored first path, the checked carrier identifies the leaf rows, and the first guide supplies the already-covered ancestor child.

theorem Hex.GraphIso.Nauty.otherNode_leaf_rowTie {n : Nat} {ctx : Ctx n} {nn inf tcLevel specFuel fuel level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hlevel : level = cs.length + 1) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hcinv : CodeCmpInv nn (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) bs (otherLeafSt ctx level numcells st).canoncode (otherLeafSt ctx level numcells st).canonlevel (otherLeafSt ctx level numcells st).eqlevCanon 0) (hginv : CanongInv ctx (otherLeafSt ctx level numcells st).canong (otherLeafSt ctx level numcells st).canonlab (otherLeafSt ctx level numcells st).samerows) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hcc : (otherLeafSt ctx level numcells st).compCanon = 0) (hge : ¬level < (otherLeafSt ctx level numcells st).canonlevel) (htie : (testcanlab ctx (updatecan ctx (otherLeafSt ctx level numcells st).canong (otherLeafSt ctx level numcells st).canonlab (otherLeafSt ctx level numcells st).samerows) (otherLeafSt ctx level numcells st).lab).fst = 0) (hgsz : ctx.g.size = n) (hcanonSize : (otherLeafSt ctx level numcells st).canonlab.size = n) (hcanonPerm : (otherLeafSt ctx level numcells st).canonlab.toList.Perm (List.range n)) (hlabSize : (otherLeafSt ctx level numcells st).lab.size = n) (hlabPerm : (otherLeafSt ctx level numcells st).lab.toList.Perm (List.range n)) (hcanonBelow : (otherLeafSt ctx level numcells st).gcaCanon < level) (hfirstPos : 1 ≤ (otherLeafSt ctx level numcells st).gcaFirst) (hfirstBelow : (otherLeafSt ctx level numcells st).gcaFirst < level) (g : Guide ctx tcLevel (otherLeafSt ctx level numcells st).gcaCanon (some (incKey ctx bs st.canonlab))) (href : g.ref = (otherLeafSt ctx level numcells st).canonlab) (hcurReach : cellsPerm g.rsPtn (otherLeafSt ctx level numcells st).gcaCanon g.rsLab (otherLeafSt ctx level numcells st).lab) {oCur : Nat} (hcur : oCur < g.len) (hatCur : (otherLeafSt ctx level numcells st).lab[g.tc]! = g.rsLab[g.tc + oCur]!) (hcoset : (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.cosetindex < n) (horbit : OrbSound (OrbConn (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.genTrace.toList n) (processnode ctx level n (otherLeafSt ctx level numcells st)).snd.orbits n) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells (some (incKey ctx bs st.canonlab)) (some (incKey ctx bs st.canonlab)) (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A row-tied code-two leaf becomes either the canonical-guide unwind or the explicitly distinguished first-ancestor orbit unwind.

theorem Hex.GraphIso.Nauty.otherNode_leaf_firstFail {n : Nat} {ctx : Ctx n} {nn inf tcLevel specFuel fuel level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hlevel : level = cs.length + 1) (hlevelN : level ≤ nn) (hbs : bs ≠ []) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hcinv : CodeCmpInv nn (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) bs (otherLeafSt ctx level numcells st).canoncode (otherLeafSt ctx level numcells st).canonlevel (otherLeafSt ctx level numcells st).eqlevCanon (otherLeafSt ctx level numcells st).compCanon) (hginv : CanongInv ctx (otherLeafSt ctx level numcells st).canong (otherLeafSt ctx level numcells st).canonlab (otherLeafSt ctx level numcells st).samerows) (heq : ((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hfail : (otherLeafSt ctx level numcells st).firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n (otherLeafSt ctx level numcells st).firstlab (otherLeafSt ctx level numcells st).lab) = false) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells (some (incKey ctx bs st.canonlab)) (some (keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab))) (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A first-path-agreeing leaf whose sentinel or automorphism guard fails falls through the ordinary leaf comparison and yields the same exact local prune outcome.

theorem Hex.GraphIso.Nauty.otherNode_leaf_pruned {n : Nat} {ctx : Ctx n} {nn inf tcLevel specFuel fuel level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hlevel : level = cs.length + 1) (hlevelN : level ≤ nn) (hbs : bs ≠ []) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hcinv : CodeCmpInv nn (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) bs (otherLeafSt ctx level numcells st).canoncode (otherLeafSt ctx level numcells st).canonlevel (otherLeafSt ctx level numcells st).eqlevCanon (otherLeafSt ctx level numcells st).compCanon) (hginv : CanongInv ctx (otherLeafSt ctx level numcells st).canong (otherLeafSt ctx level numcells st).canonlab (otherLeafSt ctx level numcells st).samerows) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hearly : (processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells (some (incKey ctx bs st.canonlab)) (some (keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab))) (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

An early non-first-path leaf return has already absorbed its whole (singleton) specification subtree. Its signed comparison return is a local prune outcome. The carrier and guide lemmas strengthen a generator return to unwind.

theorem Hex.GraphIso.Nauty.stInc_leafFinish {n : Nat} (ctx : Ctx n) (level : Nat) (st : SearchSt n) : stInc ctx (leafFinish level st) = stInc ctx st

Leaf cleanup changes no field used to read the incumbent.

def Hex.GraphIso.Nauty.firstFinish {n : Nat} (level tcellsize index : Nat) (st : SearchSt n) : SearchSt n

The sole state adjustment after a completed first-path child sweep.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.stInc_firstFinish {n : Nat} (ctx : Ctx n) (level tcellsize index : Nat) (st : SearchSt n) : stInc ctx (firstFinish level tcellsize index st) = stInc ctx st

First-path sweep cleanup does not alter the installed incumbent.

theorem Hex.GraphIso.Nauty.canonlevel_firstFinish {n : Nat} (level tcellsize index : Nat) (st : SearchSt n) : (firstFinish level tcellsize index st).canonlevel = st.canonlevel

First-path sweep cleanup does not uninstall an incumbent.

def Hex.GraphIso.Nauty.Unwind.firstFinish {n : Nat} {ctx : Ctx n} {tcLevel target level size index : Nat} {st : SearchSt n} {best : Option (Key n)} (h : Unwind ctx tcLevel target st best) : Unwind ctx tcLevel target (Nauty.firstFinish level size index st) best

A generator payload is insensitive to the first-path exit counter.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.NodeResult.firstFinish {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells size index : Nat} {cs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {r : Int} (hfuel : runFuel ≠ 0) (h : NodeResult ctx tcLevel specFuel runFuel level cs st out numcells best outBest r) : NodeResult ctx tcLevel specFuel runFuel level cs st (Nauty.firstFinish level size index out) numcells best outBest r

Every node outcome crosses the first-path exit counter update.

theorem Hex.GraphIso.Nauty.firstPath_internal_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (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 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; firstPathNode ctx inf tcLevel (fuel + 1) level numcells st = match L.fst with | some r => (r, L.snd.snd) | none => (Int.ofNat level - 1, firstFinish level mt.snd.snd L.snd.fst L.snd.snd)

A non-discrete first-path node is its explicit prefix state, one child loop, and the single exit-counter update.

theorem Hex.GraphIso.Nauty.firstPath_internal_of_loop {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel fuel level numcells tail : Nat) (cs : List Nat) (st : SearchSt n) (best outBest : Option (Key n)) (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; LoopResult ctx tcLevel specFuel fuel (n + 1) level (cs ++ [rs.longcode]) 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 L.fst → NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best outBest (firstPathNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A sound child-loop result supplies the complete outcome of a non-discrete first-path node. The theorem keeps the node's runtime fuel, the recursive node fuel, and the loop fuel separate.

theorem Hex.GraphIso.Nauty.otherNode_of_loop {n : Nat} {ctx : Ctx n} {inf tcLevel specFuel fuel level nodeNumcells loopNumcells tail : Nat} {nodeCs loopCs : List Nat} {nodeSt loopSt : SearchSt n} {rsLab rsPtn : Array Nat} {tc len : Nat} {tcell : VSet n} {best outBest : Option (Key n)} {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 : LoopResult ctx tcLevel specFuel fuel (n + 1) level loopCs rsLab rsPtn tc len loopNumcells tcell none (nodeKey ctx tcLevel (specFuel + 1) level nodeCs nodeSt nodeNumcells) loopSt L.snd best outBest L.fst) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level nodeCs nodeSt (otherNode ctx inf tcLevel (fuel + 1) level nodeNumcells nodeSt).snd nodeNumcells best outBest (otherNode ctx inf tcLevel (fuel + 1) level nodeNumcells nodeSt).fst

Once the imperative prefix has exposed an off-path child loop, either loop return constructs the corresponding node result.

theorem Hex.GraphIso.Nauty.otherNode_plain_state {n : Nat} (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : SearchSt n) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells < n) (hnonneg : have rs := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level rs.longcode { lab := rs.lab, ptn := rs.ptn, active := rs.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, needshortprune := st.needshortprune, numnodes := st.numnodes + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; pre.compCanon ≥ 0) (hshort : have rs := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level rs.longcode { lab := rs.lab, ptn := rs.ptn, active := rs.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, needshortprune := st.needshortprune, numnodes := st.numnodes + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have mt := maketargetcell ctx pre.lab pre.ptn level tcLevel (-1); have target := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; (processnode ctx level rs.numcells target).snd.needshortprune = false) (hcheap : have rs := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level rs.longcode { lab := rs.lab, ptn := rs.ptn, active := rs.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, needshortprune := st.needshortprune, numnodes := st.numnodes + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have mt := maketargetcell ctx pre.lab pre.ptn level tcLevel (-1); have target := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; cheapautom (processnode ctx level rs.numcells target).snd.ptn level n = true) : have rs := refine ctx level st.lab st.ptn st.active numcells; have pre := otherNodePrep level rs.longcode { lab := rs.lab, ptn := rs.ptn, active := rs.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, needshortprune := st.needshortprune, numnodes := st.numnodes + 1, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, genTrace := st.genTrace }; have mt := maketargetcell ctx pre.lab pre.ptn level tcLevel (-1); have target := { lab := pre.lab, ptn := pre.ptn, active := pre.active, orbits := pre.orbits, fixedpts := pre.fixedpts, autos := pre.autos, wsCap := pre.wsCap, firstcode := pre.firstcode, canoncode := pre.canoncode, firsttc := pre.firsttc, firstlab := pre.firstlab, canonlab := pre.canonlab, canong := pre.canong, samerows := pre.samerows, compCanon := pre.compCanon, eqlevFirst := pre.eqlevFirst, eqlevCanon := pre.eqlevCanon, gcaFirst := pre.gcaFirst, gcaCanon := pre.gcaCanon, canonlevel := pre.canonlevel, noncheaplevel := pre.noncheaplevel, allsamelevel := pre.allsamelevel, cosetindex := pre.cosetindex, stabvertex := pre.stabvertex, needshortprune := pre.needshortprune, numnodes := pre.numnodes, tctotal := pre.tctotal + mt.snd.snd, canupdates := pre.canupdates, numorbits := pre.numorbits, numgenerators := pre.numgenerators, numbadleaves := pre.numbadleaves, maxlevel := pre.maxlevel, genTrace := pre.genTrace }; have pr := processnode ctx level rs.numcells target; have L := otherChildLoop 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 pr.snd; otherNode ctx inf tcLevel (fuel + 1) level numcells st = if pr.fst < Int.ofNat level then pr else match L.fst with | some r => (r, L.snd) | none => (Int.ofNat level - 1, L.snd)

The ordinary off-path internal branch, with no pending short prune and a cheap refined partition, reaches its child loop without another state write.

theorem Hex.GraphIso.Nauty.otherNode_leaf_complete {n : Nat} {ctx : Ctx n} {nn inf tcLevel specFuel fuel level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hlevel : level = cs.length + 1) (hlevelN : level ≤ nn) (hbs : bs ≠ []) (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = true) (hcinv : CodeCmpInv nn (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) bs (otherLeafSt ctx level numcells st).canoncode (otherLeafSt ctx level numcells st).canonlevel (otherLeafSt ctx level numcells st).eqlevCanon (otherLeafSt ctx level numcells st).compCanon) (hginv : CanongInv ctx (otherLeafSt ctx level numcells st).canong (otherLeafSt ctx level numcells st).canonlab (otherLeafSt ctx level numcells st).samerows) (hef : ¬((otherLeafSt ctx level numcells st).eqlevFirst == level) = true) (hdone : ¬(processnode ctx level n (otherLeafSt ctx level numcells st)).fst < Int.ofNat level) : NodeResult ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells (some (incKey ctx bs st.canonlab)) (some (keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab))) (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

The complementary off-path leaf case completes after its empty child sweep, retaining the exact leaf maximum installed by processnode.

theorem Hex.GraphIso.Nauty.firstPath_zero {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel level numcells : Nat) (cs : List Nat) (st : SearchSt n) (best : Option (Key n)) : NodeResult ctx tcLevel specFuel 0 level cs st (firstPathNode ctx inf tcLevel 0 level numcells st).snd numcells best best (firstPathNode ctx inf tcLevel 0 level numcells st).fst

A first-path node with no runtime fuel reports exhaustion.

theorem Hex.GraphIso.Nauty.otherNode_zero {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel level numcells : Nat) (cs : List Nat) (st : SearchSt n) (best : Option (Key n)) : NodeResult ctx tcLevel specFuel 0 level cs st (otherNode ctx inf tcLevel 0 level numcells st).snd numcells best best (otherNode ctx inf tcLevel 0 level numcells st).fst

An off-path node with no runtime fuel reports exhaustion.

theorem Hex.GraphIso.Nauty.firstLoop_zero {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tv? cursor : Option Nat) (tcell : VSet n) (index : Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hcursor : ∀ (v : Nat), cursor = some v → v < n) : LoopResult ctx tcLevel specFuel runFuel 0 level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).snd.snd best best (firstChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell index st).fst

First-path child-loop fuel exhaustion is not completion.

theorem Hex.GraphIso.Nauty.otherLoop_zero {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tv? cursor : Option Nat) (tcell : VSet n) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hcursor : ∀ (v : Nat), cursor = some v → v < n) : LoopResult ctx tcLevel specFuel runFuel 0 level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).snd best best (otherChildLoop ctx inf tcLevel runFuel 0 level numcells tc tv1 tv? tcell st).fst

Off-path child-loop fuel exhaustion is not completion.

theorem Hex.GraphIso.Nauty.firstLoop_done {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (hinstalled : st.canonlevel ≠ 0) (hread : stInc ctx st = best) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = none) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell index st).snd.snd best best (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell index st).fst

With positive loop fuel, an absent next child completes the first-path sweep rather than exhausting it.

theorem Hex.GraphIso.Nauty.otherLoop_done {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (hinstalled : st.canonlevel ≠ 0) (hread : stInc ctx st = best) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = none) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell st).snd best best (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 none tcell st).fst

With positive loop fuel, an absent next child completes the off-path sweep rather than exhausting it.

theorem Hex.GraphIso.Nauty.otherLoop_childUnwind {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best outBest : Option (Key n)) (target : Nat) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } (numcells + 1) best outBest) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } (numcells + 1)) bound) (hreturn : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).fst = Int.ofNat target) (hbelow : target < level) (hpayload : Unwind ctx tcLevel target (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd outBest) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best outBest (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst

An off-path child generator unwind strictly past this loop returns immediately after removing the child's temporary fixed vertex.

theorem Hex.GraphIso.Nauty.otherLoop_next {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best mid outBest : Option (Key n)) (r : Int) (hnext : tcell.nextElem cursor = some tv) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } (numcells + 1) best mid) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 } (numcells + 1)) bound) (hreturn : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).fst = r) (hstay : ¬r < Int.ofNat level) (hshort : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.needshortprune = false) (hother : (tv == tv1) = false) (hrec : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound (recover n inf level (have __src := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace })) (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell (recover n inf level (have __src := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace }))).snd mid outBest (otherChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell (recover n inf level (have __src := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd; { lab := __src.lab, ptn := __src.ptn, active := __src.active, orbits := __src.orbits, fixedpts := (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 }).snd.fixedpts.erase tv, autos := __src.autos, wsCap := __src.wsCap, firstcode := __src.firstcode, canoncode := __src.canoncode, firsttc := __src.firsttc, firstlab := __src.firstlab, canonlab := __src.canonlab, canong := __src.canong, samerows := __src.samerows, compCanon := __src.compCanon, eqlevFirst := __src.eqlevFirst, eqlevCanon := __src.eqlevCanon, gcaFirst := __src.gcaFirst, gcaCanon := __src.gcaCanon, canonlevel := __src.canonlevel, noncheaplevel := __src.noncheaplevel, allsamelevel := __src.allsamelevel, cosetindex := __src.cosetindex, stabvertex := __src.stabvertex, needshortprune := __src.needshortprune, numnodes := __src.numnodes, tctotal := __src.tctotal, canupdates := __src.canupdates, numorbits := __src.numorbits, numgenerators := __src.numgenerators, numbadleaves := __src.numbadleaves, maxlevel := __src.maxlevel, genTrace := __src.genTrace }))).fst) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).snd best outBest (otherChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell st).fst

After an ordinary child completes without requesting either filter, the off-path loop recovers its parent frame and continues.

theorem Hex.GraphIso.Nauty.firstLoop_otherUnwind {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best outBest : Option (Key n)) (target : Nat) (hrep : (st.orbits[tv]! == tv) = true) (hother : (tv == tv1) = false) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 } (numcells + 1) best outBest) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 } (numcells + 1)) bound) (hreturn : (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 }).fst = Int.ofNat target) (hbelow : target < level) (hpayload : Unwind ctx tcLevel target (otherNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 }).snd outBest) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

An off-path child of the first-path loop that unwinds strictly past this loop returns immediately after removing its temporary fixed vertex.

theorem Hex.GraphIso.Nauty.firstLoop_guideUnwind {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best outBest : Option (Key n)) (target : Nat) (hrep : (st.orbits[tv]! == tv) = true) (hfirst : (tv == tv1) = true) (hsound : NodeSound ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 } (numcells + 1) best outBest) (hkey : keyLe (nodeKey ctx tcLevel specFuel (level + 1) cs { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 } (numcells + 1)) bound) (hreturn : (firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 }).fst = Int.ofNat target) (hbelow : target < level) (hpayload : Unwind ctx tcLevel target (firstPathNode ctx inf tcLevel runFuel (level + 1) (numcells + 1) { lab := (breakout n st.lab st.ptn (level + 1) tc tv).fst, ptn := (breakout n st.lab st.ptn (level + 1) tc tv).snd.fst, active := (breakout n st.lab st.ptn (level + 1) tc tv).snd.snd, orbits := st.orbits, fixedpts := st.fixedpts.insert tv, 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 := tv, 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 }).snd outBest) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best outBest (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

The guiding child of the first-path loop that unwinds strictly past this loop returns after installing the guide controls and removing its temporary fixed vertex.

theorem Hex.GraphIso.Nauty.firstLoop_orbitSkip {n : Nat} (ctx : Ctx n) (inf tcLevel specFuel runFuel loopFuel level numcells tc tv1 tv : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (len : Nat) (tcell : VSet n) (index o : Nat) (cursor : Option Nat) (bound : Key n) (st : SearchSt n) (best : Option (Key n)) (gens : List (Array Nat)) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = some tv) (ho : o < len) (htv : rsLab[tc + o]! = tv) (hgsz : ctx.g.size = n) (hv : ∀ (γ : Array Nat), γ ∈ gens → checkAutom ctx.g γ = true) (hstab : ∀ (γ : Array Nat), γ ∈ gens → CellStab rsPtn level rsLab γ) (hs : rsLab.size = n) (hinj : LabInj rsLab rsLab.size) (hok : LabOk rsLab n) (hsp : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hic : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hlf : level + 1 + specFuel ≤ n + 1) (hsound : OrbSound (OrbConn gens n) st.orbits n) (horbit : (st.orbits[tv]! == tv) = false) (hrec : ∀ (index' : Nat), SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell (some tv) best → LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound st (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' st).snd.snd best best (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem (some tv)) tcell index' st).fst) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).snd.snd best best (firstChildLoop ctx inf tcLevel runFuel (loopFuel + 1) level numcells tc tv1 (some tv) tcell index st).fst

A non-root orbit pointer skips the current first-path child and continues with ranked coverage advanced past that child.