theorem Hex.GraphIso.Nauty.LabInj.eq {lab : Array Nat} {nn i j : Nat} (h : LabInj lab nn) (hi : i < nn) (hj : j < nn) (heq : lab[i]! = lab[j]!) : i = j

Public eliminator for injective labellings in downstream outcome modules, where the defining predicate is opaque.

def Hex.GraphIso.Nauty.LabelCarrier {n : Nat} (ctx : Ctx n) (ref cur : Array Nat) (store : Array (Array Nat)) : Prop

A checked generator maps one labelling pointwise onto another.

Equations

• Hex.GraphIso.Nauty.LabelCarrier ctx ref cur store = ∃ (γ : Array Nat), γ ∈ store ∧ Hex.GraphIso.Nauty.checkAutom ctx.g γ = true ∧ ∀ (i : Nat), i < n → γ[ref[i]!]! = cur[i]!

def Hex.GraphIso.Nauty.CellCarrier {n : Nat} (ctx : Ctx n) (ptn : Array Nat) (level : Nat) (base ref cur : Array Nat) (store : Array (Array Nat)) : Prop

A checked carrier whose witnessing generator stabilizes one ancestor frame. Direct generator unwinds need only this witness. Requiring every recorded generator to stabilize the frame is stronger, and it fails away from the first-path loop that consumes an orbit closure.

Equations

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

theorem Hex.GraphIso.Nauty.CellCarrier.toLabel {n : Nat} {ctx : Ctx n} {ptn : Array Nat} {level : Nat} {base ref cur : Array Nat} {store : Array (Array Nat)} (h : CellCarrier ctx ptn level base ref cur store) : LabelCarrier ctx ref cur store

theorem Hex.GraphIso.Nauty.LabelCarrier.leafRows {n : Nat} {ctx : Ctx n} {ref cur : Array Nat} {store : Array (Array Nat)} (h : LabelCarrier ctx ref cur store) (hgsz : ctx.g.size = n) (hrefsz : ref.size = n) (hrefok : LabOk ref n) (hcursz : cur.size = n) : Nauty.leafRows ctx cur = Nauty.leafRows ctx ref

A checked carrier identifies the relabelled leaf rows of its two permutation labellings.

theorem Hex.GraphIso.Nauty.processnode_labelCarrier {n k : Nat} {G : Colored n k} {ctx : Ctx n} {rlab rptn : Array Nat} {cs bs fs : List Nat} {numcells level nc : Nat} {st : SearchSt n} (hn0 : 0 < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hdom : DomOk G ctx rlab rptn cs bs fs numcells st) (hfsz : st.firstlab.size = n) (hfre : CellsReach G st.firstlab) (hcsz : st.canonlab.size = n) (hcre : CellsReach G st.canonlab) : (processnode ctx level nc st).snd.genTrace = st.genTrace ∨ LabelCarrier ctx st.firstlab st.lab (processnode ctx level nc st).snd.genTrace ∨ LabelCarrier ctx st.canonlab st.lab (processnode ctx level nc st).snd.genTrace

At a valid leaf event, either no generator is recorded or the output store contains a checked carrier from the first or incumbent leaf.

theorem Hex.GraphIso.Nauty.processnode_firstLabelCarrier {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hsz₁ : st.firstlab.size = n) (hp₁ : st.firstlab.toList.Perm (List.range n)) (hsz₂ : st.lab.size = n) (hp₂ : 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) (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) : LabelCarrier ctx st.firstlab st.lab (processnode ctx level numcells st).snd.genTrace

The guarded code-one event yields the first-reference carrier directly, without routing through the event-wide carrier disjunction.

theorem Hex.GraphIso.Nauty.processnode_canonLabelCarrier {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hsz₁ : st.canonlab.size = n) (hp₁ : st.canonlab.toList.Perm (List.range n)) (hsz₂ : st.lab.size = n) (hp₂ : st.lab.toList.Perm (List.range n)) (hrows : leafRows ctx st.canonlab = leafRows ctx st.lab) (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) : LabelCarrier ctx st.canonlab st.lab (processnode ctx level numcells st).snd.genTrace

The guarded code-two event yields the incumbent-reference carrier directly, independently of its chosen return ancestor.

def Hex.GraphIso.Nauty.After (cursor : Option Nat) (v : Nat) : Prop

Vertices strictly after the loop cursor.

Equations

• Hex.GraphIso.Nauty.After none v = True
• Hex.GraphIso.Nauty.After (some u) v = (u < v)

def Hex.GraphIso.Nauty.cursorRank : Option Nat → Nat

Numeric rank used to count strict cursor progress.

Equations

• Hex.GraphIso.Nauty.cursorRank none = 0
• Hex.GraphIso.Nauty.cursorRank (some u) = u + 1

theorem Hex.GraphIso.Nauty.cursorRank_step {cursor : Option Nat} {v : Nat} (h : After cursor v) : cursorRank cursor + 1 ≤ cursorRank (some v)

Moving to a vertex after the cursor increases its rank.

theorem Hex.GraphIso.Nauty.cursorFuel_step {cursor : Option Nat} {v fuel n : Nat} (hnext : After cursor v) (hfuel : n < cursorRank cursor + (fuel + 1)) : n < cursorRank (some v) + fuel

Consuming one cursor step preserves the strict remaining-fuel bound used to rule out loop exhaustion.

theorem Hex.GraphIso.Nauty.cursorRank_le {cursor : Option Nat} {n : Nat} (h : ∀ (v : Nat), cursor = some v → v < n) : cursorRank cursor ≤ n

A bounded cursor has rank at most the vertex count.

theorem Hex.GraphIso.Nauty.LoopResult.exhaustion_false {n : Nat} {cursor finalCursor : Option Nat} {loopFuel : Nat} (hfuel : n < cursorRank cursor + loopFuel) (hprogress : cursorRank cursor + loopFuel ≤ cursorRank finalCursor) (hbounded : ∀ (v : Nat), finalCursor = some v → v < n) : False

A loop cannot consume more fuel than the remaining bounded cursor range. This is the contradiction used to rule out the exhaustion outcome of the executable root sweeps.

def Hex.GraphIso.Nauty.sweepKey {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (tc numcells o : Nat) : Key n

The prefixed specification key of offset o in a refined target cell.

Equations

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

theorem Hex.GraphIso.Nauty.sweepKey_of_cellCarrier {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {ref cur : Array Nat} {store : Array (Array Nat)} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells oRef oCur : Nat} (hcarrier : CellCarrier ctx rsPtn level rsLab ref cur store) (hs : rsLab.size = n) (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) (href : oRef < len) (hcur : oCur < len) (hlf : level + 1 + specFuel ≤ n + 1) (hatRef : ref[tc]! = rsLab[tc + oRef]!) (hatCur : cur[tc]! = rsLab[tc + oCur]!) : sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells oCur = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells oRef

A checked label carrier identifies the two children selected at an ancestor, once the two leaf labellings are known at that ancestor's individualized position.

theorem Hex.GraphIso.Nauty.sweepKey_of_carrier {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {ref cur : Array Nat} {store : Array (Array Nat)} (hcarrier : LabelCarrier ctx ref cur store) {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells oRef oCur : Nat} (hstab : ∀ (γ : Array Nat), γ ∈ store → CellStab rsPtn level rsLab γ) (hs : rsLab.size = n) (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) (href : oRef < len) (hcur : oCur < len) (hlf : level + 1 + specFuel ≤ n + 1) (hatRef : ref[tc]! = rsLab[tc + oRef]!) (hatCur : cur[tc]! = rsLab[tc + oCur]!) : sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells oCur = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells oRef

The store-wide stabilization form used by orbit-local callers.

theorem Hex.GraphIso.Nauty.nodeKey_children {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells len : Nat} {cs : List Nat} {st : SearchSt n} (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = false) (hlen : (specMaketargetcell 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).snd.snd = len + 1) : nodeKey ctx tcLevel (fuel + 1) level cs st numcells = keysMax (sweepKey ctx tcLevel fuel level (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn (specMaketargetcell 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).fst (refine ctx level st.lab st.ptn st.active numcells).numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel fuel level (cs ++ [(refine ctx level st.lab st.ptn st.active numcells).longcode]) (refine ctx level st.lab st.ptn st.active numcells).lab (refine ctx level st.lab st.ptn st.active numcells).ptn (specMaketargetcell 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).fst (refine ctx level st.lab st.ptn st.active numcells).numcells (o + 1)) (List.range len))

The key of a non-discrete node is the maximum of the keys swept by its child loop. The loop prefix contains the node's refinement code.

def Hex.GraphIso.Nauty.ChildDone {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (tc numcells : Nat) (best : Option (Key n)) (o : Nat) : Prop

Offset o has been absorbed by the semantic incumbent. This is explicit rather than read from SearchSt n: during an upward code comparison the executable overwrites canoncode before it installs the new leaf, so the state temporarily contains no faithful incumbent key.

Equations

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

def Hex.GraphIso.Nauty.ChildLive {n : Nat} (rsLab : Array Nat) (tc len : Nat) (tcell : VSet n) (cursor : Option Nat) (o : Nat) : Prop

Offset o is still eligible after the loop cursor.

Equations

• Hex.GraphIso.Nauty.ChildLive rsLab tc len tcell cursor o = (o < len ∧ tcell.mem rsLab[tc + o]! = true ∧ Hex.GraphIso.Nauty.After cursor rsLab[tc + o]!)

structure Hex.GraphIso.Nauty.SweepCover {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (tc len numcells : Nat) (tcell : VSet n) (cursor : Option Nat) (best : Option (Key n)) : Prop

The evolving invariant of a mutable target-cell sweep.

cover follows removed children transitively to the current live suffix. past records the ordering fact needed when a pruning automorphism carries a live vertex backwards: every retained vertex at or before the cursor has already been absorbed.

• cover : ChildCover (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells) (fun (o : Nat) => rsLab[tc + o]!) (fun (o : Nat) => o < len) (ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best) (ChildLive rsLab tc len tcell cursor)
• past (o : Nat) : o < len → tcell.mem rsLab[tc + o]! = true → ¬After cursor rsLab[tc + o]! → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best o

theorem Hex.GraphIso.Nauty.sweepCover_init {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (cs : List Nat) (rsLab rsPtn : Array Nat) (tc len numcells : Nat) (best : Option (Key n)) (hok : ∀ (o : Nat), o < len → rsLab[tc + o]! < n) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells (windowSet n rsLab tc len) none best

Before the first iteration, the whole target-cell window is live.

theorem Hex.GraphIso.Nauty.SweepCover.step {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor cursor' : Option Nat} {best best' : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hs : ∀ (o : Nat), ChildLive rsLab tc len tcell cursor o → (∀ (j : Nat), sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells j = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best' j) ∨ ∃ (j : Nat), ChildLive rsLab tc len tcell' cursor' j ∧ sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells j ∧ rsLab[tc + j]! ≤ rsLab[tc + o]!) (hd : ∀ (o : Nat), ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best o → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best' o) (hpast : ∀ (o : Nat), o < len → tcell'.mem rsLab[tc + o]! = true → ¬After cursor' rsLab[tc + o]! → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best' o) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell' cursor' best'

Coverage crosses an arbitrary loop step once old covered children stay covered and every old survivor is either covered or replaced by a key-equivalent new survivor.

theorem Hex.GraphIso.Nauty.ChildDone.mono {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells o : Nat} {best best' : Option (Key n)} (h : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best o) (hinc : ∀ (b : Key n), best = some b → ∃ (b' : Key n), best' = some b' ∧ keyLe b b') : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best' o

Previously covered children remain covered when the incumbent grows.

theorem Hex.GraphIso.Nauty.SweepCover.grow {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best best' : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hinc : ∀ (b : Key n), best = some b → ∃ (b' : Key n), best' = some b' ∧ keyLe b b') : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best'

The evolving sweep remains valid when the semantic incumbent grows.

theorem Hex.GraphIso.Nauty.ChildDone.ofEq {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells oRef oCur : Nat} {best : Option (Key n)} (h : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best oRef) (heq : sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells oCur = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells oRef) : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best oCur

Coverage transfers across equality of two child keys.

theorem Hex.GraphIso.Nauty.SweepCover.filter {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hs : ∀ (o : Nat), ChildLive rsLab tc len tcell cursor o → (∀ (j : Nat), sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells j = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best j) ∨ ∃ (j : Nat), ChildLive rsLab tc len tcell' cursor j ∧ sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells j ∧ rsLab[tc + j]! ≤ rsLab[tc + o]!) (hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell' cursor best

A filter preserves sweep coverage when every old live child is either absorbed or carried to a key-equivalent new survivor, and filtering adds no vertices. A carried survivor before the cursor is discharged through past. It need not remain in the live suffix.

theorem Hex.GraphIso.Nauty.after_or_not (cursor : Option Nat) (v : Nat) : After cursor v ∨ ¬After cursor v

Cursor eligibility is decidable without asking typeclass search to reduce the opaque After definition.

theorem Hex.GraphIso.Nauty.SweepCover.filterCarried {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hs : ∀ (o : Nat), ChildLive rsLab tc len tcell cursor o → ∃ (j : Nat), j < len ∧ tcell'.mem rsLab[tc + j]! = true ∧ sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells j ∧ rsLab[tc + j]! ≤ rsLab[tc + o]!) (hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell' cursor best

A filter's natural preservation rule: every old live child is carried to a key-equivalent member of the filtered set. The member may lie before the cursor, and past converts that case to completed coverage.

theorem Hex.GraphIso.Nauty.SweepCover.filterDesc {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hs : ∀ (o : Nat), ChildLive rsLab tc len tcell cursor o → tcell'.mem rsLab[tc + o]! = true ∨ ∃ (j : Nat), j < len ∧ sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells j ∧ rsLab[tc + j]! < rsLab[tc + o]!) (hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell' cursor best

The form used by executable prune filters. A current live child either survives unchanged or is carried to a strictly smaller child of the full target cell. Ranked coverage follows the latter through any earlier filters until it reaches an already-covered child or a new survivor.

theorem Hex.GraphIso.Nauty.SweepCover.filterAutom {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hgsz : ctx.g.size = n) (hs : rsLab.size = n) (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) (hdrop : ∀ (o : Nat), ChildLive rsLab tc len tcell cursor o → tcell'.mem rsLab[tc + o]! = false → ∃ (γ : Array Nat), checkAutom ctx.g γ = true ∧ CellStab rsPtn level rsLab γ ∧ γ[rsLab[tc + o]!]! < rsLab[tc + o]!) (hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell' cursor best

Cell-stabilizing downward automorphism carriers discharge the abstract descending-filter rule.

theorem Hex.GraphIso.Nauty.SweepCover.longprune {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {fixedpts : VSet n} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} {out : SearchSt n} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hgsz : ctx.g.size = n) (hs : rsLab.size = n) (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) (haut : ∀ (p : VSet n × VSet n), p ∈ out.autos.toList → fixedpts.subset p.fst = true → PairOk ctx.g rsPtn rsLab level p.fst p.snd) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells (Nauty.longprune tcell fixedpts out.autos) cursor best

longprune preserves the evolving sweep under the autos ledger.

theorem Hex.GraphIso.Nauty.SweepCover.shortprune {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} {out : SearchSt n} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hgsz : ctx.g.size = n) (hs : rsLab.size = n) (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) (hlast : ∀ (fix mcr : VSet n), out.autos.back? = some (fix, mcr) → PairOk ctx.g rsPtn rsLab level fix mcr) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells (Nauty.shortprune tcell out) cursor best

shortprune preserves the evolving sweep under the last-pair ledger.

theorem Hex.GraphIso.Nauty.SweepCover.finish {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hempty : ∀ (o : Nat), ¬ChildLive rsLab tc len tcell cursor o) (o : Nat) : o < len → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best o

At loop completion the evolving coverage invariant says that every offset in the original target cell has been absorbed.

theorem Hex.GraphIso.Nauty.SweepCover.maxLe {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tail : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc (tail + 1) numcells tcell cursor best) (hempty : ∀ (o : Nat), ¬ChildLive rsLab tc (tail + 1) tcell cursor o) {b : Key n} (hout : best = some b) : keyLe (keysMax (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells (o + 1)) (List.range tail))) b

Completed child coverage bounds the maximum over the whole original target cell, not merely the final filtered set.

theorem Hex.GraphIso.Nauty.SweepCover.maxLeLive {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tail : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} {b : Key n} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc (tail + 1) numcells tcell cursor best) (hout : best = some b) (hlive : ∀ (o : Nat), ChildLive rsLab tc (tail + 1) tcell cursor o → keyLe (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o) b) : keyLe (keysMax (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells (o + 1)) (List.range tail))) b

A partially explored sweep has the same maximum bound when every remaining live representative is already dominated by the installed incumbent.

theorem Hex.GraphIso.Nauty.no_child_after {n : Nat} {s : VSet n} {cursor : Option Nat} (hnext : s.nextElem cursor = none) (v : Nat) : s.mem v = true → After cursor v → False

A none cursor result means that no set member remains after the cursor.

theorem Hex.GraphIso.Nauty.nextElem_after {n : Nat} {s : VSet n} {v : Nat} {cursor : Option Nat} (hnext : s.nextElem cursor = some v) : After cursor v

A successful nextElem lies strictly after its cursor.

theorem Hex.GraphIso.Nauty.nextElem_le {n : Nat} {s : VSet n} {v w : Nat} {cursor : Option Nat} (hnext : s.nextElem cursor = some v) (hw : s.mem w = true) (ha : After cursor w) : v ≤ w

nextElem returns the least set member strictly after its cursor.

theorem Hex.GraphIso.Nauty.SweepCover.advance {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells tv : Nat} {tcell : VSet n} {cursor : Option Nat} {best best' : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = some tv) (hcur : ∀ (o : Nat), o < len → rsLab[tc + o]! = tv → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best' o) (hd : ∀ (o : Nat), ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best o → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best' o) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell (some tv) best'

Advancing to the least remaining vertex preserves sweep coverage once that vertex's child is absorbed. The hcur premise identifies every offset carrying the chosen vertex. Callers normally discharge it from labelling injectivity.

theorem Hex.GraphIso.Nauty.SweepCover.done_of_smaller {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells tv o j : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = some tv) (hj : j < len) (hkey : sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o = sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells j) (hrank : rsLab[tc + j]! < tv) : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best o

A child whose key is carried to a strictly smaller target-cell vertex is already covered when the loop is about to visit the least eligible vertex. Any live witness supplied by ranked coverage would be both below and at least that least vertex, a contradiction.

theorem Hex.GraphIso.Nauty.SweepCover.orbitSkip {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tv o : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} {out : SearchSt n} {gens : List (Array Nat)} (h : 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) out.orbits n) (hne : out.orbits[tv]! ≠ tv) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell (some tv) best

The non-root arm of the first-path orbit test is a covered skip. Orbit soundness supplies a smaller word-connected pointer target. Cell stabilization keeps that target in the sibling cell, and ranked coverage shows it was already absorbed.

theorem Hex.GraphIso.Nauty.SweepCover.finish_of_nextElem {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = none) (o : Nat) : o < len → ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells best o

The executable loop terminator discharges the live-set premise of SweepCover.finish.

structure Hex.GraphIso.Nauty.Anchor {n : Nat} (ctx : Ctx n) (tcLevel target : Nat) (best : Option (Key n)) : Type

A child at an ancestor has already been absorbed. The arrays and offset are stored explicitly because neither gcaFirst nor gcaCanon retains this path history.

• positive : 1 ≤ target
• specFuel : Nat
• codes : List Nat
• rsLab : Array Nat
• rsPtn : Array Nat
• tc : Nat
• numcells : Nat
• offset : Nat
• done : ChildDone ctx tcLevel self.specFuel target self.codes self.rsLab self.rsPtn self.tc self.numcells best self.offset

def Hex.GraphIso.Nauty.Anchor.ofCellCarrier {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {tcLevel level specFuel : Nat} {codes : List Nat} {rsLab rsPtn ref cur : Array Nat} {store : Array (Array Nat)} {tc len numcells oRef oCur : Nat} {best : Option (Key n)} (hpos : 1 ≤ level) (hdone : ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells best oRef) (hcarrier : CellCarrier ctx rsPtn level rsLab ref cur store) (hs : rsLab.size = n) (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) (href : oRef < len) (hcur : oCur < len) (hlf : level + 1 + specFuel ≤ n + 1) (hatRef : ref[tc]! = rsLab[tc + oRef]!) (hatCur : cur[tc]! = rsLab[tc + oCur]!) : Anchor ctx tcLevel level best

Turn an already-covered reference child into the current child's unwind anchor using a checked carrier between their leaf labellings.

Equations

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

def Hex.GraphIso.Nauty.Anchor.ofCarrier {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {tcLevel level specFuel : Nat} {codes : List Nat} {rsLab rsPtn ref cur : Array Nat} {store : Array (Array Nat)} {tc len numcells oRef oCur : Nat} {best : Option (Key n)} (hpos : 1 ≤ level) (hdone : ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells best oRef) (hcarrier : LabelCarrier ctx ref cur store) (hstab : ∀ (γ : Array Nat), γ ∈ store → CellStab rsPtn level rsLab γ) (hs : rsLab.size = n) (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) (href : oRef < len) (hcur : oCur < len) (hlf : level + 1 + specFuel ≤ n + 1) (hatRef : ref[tc]! = rsLab[tc + oRef]!) (hatCur : cur[tc]! = rsLab[tc + oCur]!) : Anchor ctx tcLevel level best

Store-wide stabilization implies the witness-local form.

Equations

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

structure Hex.GraphIso.Nauty.OrbitUnwind {n : Nat} (ctx : Ctx n) (target : Nat) (out : SearchSt n) : Prop

A code-two return to gcaFirst is justified by the updated orbit pointer rather than by the direct canonical carrier. The receiving loop uses this sound pointer together with its own coverage frame.

• positive : 1 ≤ target
• bound : target ≤ out.gcaFirst
• currentLt : out.cosetindex < n
• smaller : out.orbits[out.cosetindex]! < out.cosetindex
• sound : OrbSound (OrbConn out.genTrace.toList n) out.orbits n

inductive Hex.GraphIso.Nauty.Unwind {n : Nat} (ctx : Ctx n) (tcLevel target : Nat) (out : SearchSt n) (best : Option (Key n)) : Type

The evidence carried by a generator unwind. Code one and the ordinary code-two return retain their different reference labellings. The canonical constructor also retains its exact return guide. Code two's special gcaFirst return retains the sound orbit pointer that selected an earlier child. Non-generator pruning instead returns a locally complete maximum and therefore has its own result constructor.

• first {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (anchor : Anchor ctx tcLevel target best) (carrier : LabelCarrier ctx out.firstlab out.lab out.genTrace) (atFirst : target ≤ out.gcaFirst) : Unwind ctx tcLevel target out best
• canon {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (anchor : Anchor ctx tcLevel target best) (carrier : LabelCarrier ctx out.canonlab out.lab out.genTrace) (atCanon : target = out.gcaCanon) : Unwind ctx tcLevel target out best
• orbit {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (payload : OrbitUnwind ctx target out) : Unwind ctx tcLevel target out best

def Hex.GraphIso.Nauty.Unwind.setFirst {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (h : Unwind ctx tcLevel target out best) (gcaFirst stabvertex : Nat) (hbound : target ≤ gcaFirst) : Unwind ctx tcLevel target { 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 := gcaFirst, gcaCanon := out.gcaCanon, canonlevel := out.canonlevel, noncheaplevel := out.noncheaplevel, allsamelevel := out.allsamelevel, cosetindex := out.cosetindex, stabvertex := 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

Updating the first-path return controls changes none of the fields carried by a generator unwind.

Equations

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

def Hex.GraphIso.Nauty.Unwind.setFixed {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {out : SearchSt n} {best : Option (Key n)} (h : Unwind ctx tcLevel target out best) (fixedpts : VSet n) : Unwind ctx tcLevel target { 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

Removing a loop's temporary fixed vertex changes none of the fields carried by a generator unwind.

Equations

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

def Hex.GraphIso.Nauty.IncGrows {n : Nat} (best out : Option (Key n)) : Prop

A semantic incumbent can only improve across a search fragment.

Equations

• Hex.GraphIso.Nauty.IncGrows best out = ∀ (b : Hex.GraphIso.Nauty.Key n), best = some b → ∃ (b' : Hex.GraphIso.Nauty.Key n), out = some b' ∧ Hex.GraphIso.Nauty.keyLe b b'

structure Hex.GraphIso.Nauty.Guide {n : Nat} (ctx : Ctx n) (tcLevel target : Nat) (best : Option (Key n)) : Type

A previously explored child together with the ancestor geometry needed to reuse it as a generator guide. Unlike gcaFirst and gcaCanon, this keeps the reference labelling and the exact target-cell frame.

• positive : 1 ≤ target
• specFuel : Nat
• codes : List Nat
• rsLab : Array Nat
• rsPtn : Array Nat
• ref : Array Nat
• tc : Nat
• len : Nat
• numcells : Nat
• offset : Nat
• done : ChildDone ctx tcLevel self.specFuel target self.codes self.rsLab self.rsPtn self.tc self.numcells best self.offset
• labSize : self.rsLab.size = n
• labOk : LabOk self.rsLab n
• ptnSize : self.rsPtn.size = n
• endClosed : self.rsPtn[self.rsPtn.size - 1]! ≤ target
• values (q : Nat) : self.rsPtn[q]! ≤ target ∨ self.rsPtn[q]! = n + 2
• cell : IsCell self.rsPtn target self.tc self.len
• range : self.tc + self.len ≤ n
• offsetLt : self.offset < self.len
• fuelBound : target + 1 + self.specFuel ≤ n + 1
• atRef : self.ref[self.tc]! = self.rsLab[self.tc + self.offset]!
• refSize : self.ref.size = n
• refReach : cellsPerm self.rsPtn target self.rsLab self.ref

def Hex.GraphIso.Nauty.Guide.anchor {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {best best' : Option (Key n)} (g : Guide ctx tcLevel target best) (hgsz : ctx.g.size = n) (hinc : IncGrows best best') {cur : Array Nat} {store : Array (Array Nat)} {oCur : Nat} (hcarrier : LabelCarrier ctx g.ref cur store) (hstab : ∀ (γ : Array Nat), γ ∈ store → CellStab g.rsPtn target g.rsLab γ) (hcur : oCur < g.len) (hatCur : cur[g.tc]! = g.rsLab[g.tc + oCur]!) : Anchor ctx tcLevel target best'

A guide remains usable after the incumbent grows. Cell stabilization of the current generator store and the current child's ancestor position are the only facts that must be supplied at the leaf event.

Equations

• g.anchor hgsz hinc hcarrier hstab hcur hatCur = Hex.GraphIso.Nauty.Anchor.ofCarrier hgsz ⋯ ⋯ hcarrier hstab ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ hcur ⋯ ⋯ hatCur

def Hex.GraphIso.Nauty.Guide.anchorCell {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {best best' : Option (Key n)} (g : Guide ctx tcLevel target best) (hgsz : ctx.g.size = n) (hinc : IncGrows best best') {cur : Array Nat} {store : Array (Array Nat)} {oCur : Nat} (hcarrier : CellCarrier ctx g.rsPtn target g.rsLab g.ref cur store) (hcur : oCur < g.len) (hatCur : cur[g.tc]! = g.rsLab[g.tc + oCur]!) : Anchor ctx tcLevel target best'

A witness-local carrier is enough for a direct generator unwind.

Equations

• g.anchorCell hgsz hinc hcarrier hcur hatCur = Hex.GraphIso.Nauty.Anchor.ofCellCarrier hgsz ⋯ ⋯ hcarrier ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ hcur ⋯ ⋯ hatCur

theorem Hex.GraphIso.Nauty.Guide.firstUnwind {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} (g : Guide ctx tcLevel st.gcaFirst best) (href : g.ref = st.firstlab) (hgsz : ctx.g.size = n) (hsz₁ : st.firstlab.size = n) (hp₁ : st.firstlab.toList.Perm (List.range n)) (hsz₂ : st.lab.size = n) (hp₂ : 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) (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) (hcurReach : cellsPerm g.rsPtn st.gcaFirst g.rsLab st.lab) {oCur : Nat} (hcur : oCur < g.len) (hatCur : st.lab[g.tc]! = g.rsLab[g.tc + oCur]!) : Nonempty (Unwind ctx tcLevel st.gcaFirst (processnode ctx level numcells st).snd best)

A successful code-one leaf admission, paired with its concrete first-path guide, produces the corresponding generator unwind payload.

theorem Hex.GraphIso.Nauty.Guide.canonUnwind {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} (g : Guide ctx tcLevel st.gcaCanon best) (href : g.ref = st.canonlab) (hgsz : ctx.g.size = n) (hsz₁ : st.canonlab.size = n) (hp₁ : st.canonlab.toList.Perm (List.range n)) (hsz₂ : st.lab.size = n) (hp₂ : st.lab.toList.Perm (List.range n)) (hrows : leafRows ctx st.canonlab = leafRows ctx st.lab) (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) (hcurReach : cellsPerm g.rsPtn st.gcaCanon g.rsLab st.lab) {oCur : Nat} (hcur : oCur < g.len) (hatCur : st.lab[g.tc]! = g.rsLab[g.tc + oCur]!) : Nonempty (Unwind ctx tcLevel st.gcaCanon (processnode ctx level numcells st).snd best)

A successful code-two leaf admission, paired with the selected canonical guide, produces the corresponding generator unwind payload.

theorem Hex.GraphIso.Nauty.Guide.tiedUnwind {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} (g : Guide ctx tcLevel st.gcaCanon best) (href : g.ref = st.canonlab) (hgsz : ctx.g.size = n) (hsz₁ : st.canonlab.size = n) (hp₁ : st.canonlab.toList.Perm (List.range n)) (hsz₂ : st.lab.size = n) (hp₂ : st.lab.toList.Perm (List.range n)) (hrows : leafRows ctx st.canonlab = leafRows ctx st.lab) (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) (hcanonBelow : st.gcaCanon < level) (hfirstPos : 1 ≤ st.gcaFirst) (hfirstBelow : st.gcaFirst < level) (hcurReach : cellsPerm g.rsPtn st.gcaCanon g.rsLab st.lab) {oCur : Nat} (hcur : oCur < g.len) (hatCur : st.lab[g.tc]! = g.rsLab[g.tc + oCur]!) (hcoset : (processnode ctx level numcells st).snd.cosetindex < n) (horbit : OrbSound (OrbConn (processnode ctx level numcells st).snd.genTrace.toList n) (processnode ctx level numcells st).snd.orbits n) : ∃ (target : Nat), (processnode ctx level numcells st).fst = Int.ofNat target ∧ target < level ∧ Nonempty (Unwind ctx tcLevel target (processnode ctx level numcells st).snd best)

A row-tied code-two event is either the direct canonical-guide unwind, or the special first-ancestor orbit unwind selected by a smaller pointer.

def Hex.GraphIso.Nauty.Guide.mono {n : Nat} {ctx : Ctx n} {tcLevel target : Nat} {best best' : Option (Key n)} (g : Guide ctx tcLevel target best) (hinc : IncGrows best best') : Guide ctx tcLevel target best'

A guide's covered child remains covered when the incumbent grows.

Equations

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

structure Hex.GraphIso.Nauty.Guides {n : Nat} (ctx : Ctx n) (tcLevel level : Nat) (st : SearchSt n) (best : Option (Key n)) : Prop

The first and canonical generator guides that are live strictly above the current node. A guide at the current level is not required: leaf installation temporarily sets a gca to the leaf level, and the parent loop replaces it with a concrete explored-child guide.

• first : 0 < st.gcaFirst → st.gcaFirst < level → ∃ (g : Guide ctx tcLevel st.gcaFirst best), g.ref = st.firstlab
• canon : 0 < st.gcaCanon → st.gcaCanon < level → ∃ (g : Guide ctx tcLevel st.gcaCanon best), g.ref = st.canonlab

theorem Hex.GraphIso.Nauty.Guides.grow {n : Nat} {ctx : Ctx n} {tcLevel level : Nat} {st : SearchSt n} {best best' : Option (Key n)} (h : Guides ctx tcLevel level st best) (hinc : IncGrows best best') : Guides ctx tcLevel level st best'

Both guide ledgers survive an incumbent increase.

theorem Hex.GraphIso.Nauty.Guides.root {n : Nat} (g : Array (VSet n)) (lab : Array Nat) (cellEnds : List Nat) (tcLevel : Nat) (best : Option (Key n)) : Guides { g := g } tcLevel 1 (rootSt n lab cellEnds) best

The root has no live generator guide.

structure Hex.GraphIso.Nauty.NodeSound {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (cs : List Nat) (st : SearchSt n) (numcells : Nat) (best out : Option (Key n)) : Prop

Every installed output came from the incoming incumbent or this node's specification subtree, and the incoming incumbent was not lost.

• upper (b : Key n) : out = some b → keyLe b (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))
• grows : IncGrows best out

structure Hex.GraphIso.Nauty.LoopSound {n : Nat} (ctx : Ctx n) (bound : Key n) (best out : Option (Key n)) : Prop

The state component common to both successful loop outcomes. The loop may stop early, but every incumbent it installs is still bounded by the incoming incumbent and the whole parent subtree.

• upper (b : Key n) : out = some b → keyLe b (incMax best bound)
• grows : IncGrows best out

theorem Hex.GraphIso.Nauty.IncGrows.refl {n : Nat} (best : Option (Key n)) : IncGrows best best

theorem Hex.GraphIso.Nauty.IncGrows.incMax {n : Nat} (best : Option (Key n)) (K : Key n) : IncGrows best (some (Nauty.incMax best K))

Folding one key into an incumbent preserves the incoming incumbent.

theorem Hex.GraphIso.Nauty.NodeSound.refl {n : Nat} (ctx : Ctx n) (tcLevel specFuel level : Nat) (cs : List Nat) (st : SearchSt n) (numcells : Nat) (best : Option (Key n)) : NodeSound ctx tcLevel specFuel level cs st numcells best best

theorem Hex.GraphIso.Nauty.NodeSound.ofExact {n : Nat} {ctx : Ctx n} {tcLevel specFuel level numcells : Nat} {cs : List Nat} {st : SearchSt n} {best out : Option (Key n)} (h : out = some (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))) : NodeSound ctx tcLevel specFuel level cs st numcells best out

An exact node maximum supplies both clauses of NodeSound.

theorem Hex.GraphIso.Nauty.LoopSound.refl {n : Nat} (ctx : Ctx n) (bound : Key n) (best : Option (Key n)) : LoopSound ctx bound best best

theorem Hex.GraphIso.Nauty.LoopSound.ofExact {n : Nat} {ctx : Ctx n} {bound : Key n} {best out : Option (Key n)} (h : out = some (incMax best bound)) : LoopSound ctx bound best out

An exact loop maximum supplies both clauses of LoopSound.

theorem Hex.GraphIso.Nauty.keyMax_le_of_le {n : Nat} {a b c : Key n} (ha : keyLe a c) (hb : keyLe b c) : keyLe (keyMax a b) c

theorem Hex.GraphIso.Nauty.keyLe_incMax_right {n : Nat} (inc : Option (Key n)) (b : Key n) : keyLe b (incMax inc b)

theorem Hex.GraphIso.Nauty.ChildDone.ofExact {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells o : Nat} {child : SearchSt n} {best out : Option (Key n)} (hfull : out = some (incMax best (nodeKey ctx tcLevel specFuel (level + 1) cs child (numcells + 1)))) (hlab : child.lab = (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).fst) (hptn : child.ptn = (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).snd.fst) (hactive : child.active = (breakout n rsLab rsPtn (level + 1) tc rsLab[tc + o]!).snd.snd) : ChildDone ctx tcLevel specFuel level cs rsLab rsPtn tc numcells out o

An exactly completed child is covered in its parent sweep. The three field equations identify the executable state after breakout with the specification child used by sweepKey.

theorem Hex.GraphIso.Nauty.SweepCover.advanceExact {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc len numcells tv : Nat} {tcell : VSet n} {cursor : Option Nat} {child : SearchSt n} {best out : Option (Key n)} (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell cursor best) (hnext : tcell.nextElem cursor = some tv) (hfull : out = some (incMax best (nodeKey ctx tcLevel specFuel (level + 1) cs child (numcells + 1)))) (hlab : child.lab = (breakout n rsLab rsPtn (level + 1) tc tv).fst) (hptn : child.ptn = (breakout n rsLab rsPtn (level + 1) tc tv).snd.fst) (hactive : child.active = (breakout n rsLab rsPtn (level + 1) tc tv).snd.snd) : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells tcell (some tv) out

Exact completion of the selected child advances the mutable sweep cursor and preserves all earlier coverage.

theorem Hex.GraphIso.Nauty.incMax_mono_right {n : Nat} (inc : Option (Key n)) {a b : Key n} (h : keyLe a b) : keyLe (incMax inc a) (incMax inc b)

theorem Hex.GraphIso.Nauty.IncGrows.trans {n : Nat} {best mid out : Option (Key n)} (h₁ : IncGrows best mid) (h₂ : IncGrows mid out) : IncGrows best out

theorem Hex.GraphIso.Nauty.LoopSound.ofNode {n : Nat} {ctx : Ctx n} {tcLevel specFuel level numcells : Nat} {cs : List Nat} {st : SearchSt n} {bound : Key n} {best out : Option (Key n)} (h : NodeSound ctx tcLevel specFuel level cs st numcells best out) (hle : keyLe (nodeKey ctx tcLevel specFuel level cs st numcells) bound) : LoopSound ctx bound best out

A sound child step is sound against any larger fixed loop bound.

theorem Hex.GraphIso.Nauty.LoopSound.trans {n : Nat} {ctx : Ctx n} {bound : Key n} {best mid out : Option (Key n)} (h₁ : LoopSound ctx bound best mid) (h₂ : LoopSound ctx bound mid out) : LoopSound ctx bound best out

Consecutive fragments with the same fixed bound compose.

theorem Hex.GraphIso.Nauty.LoopSound.exact {n : Nat} {ctx : Ctx n} {bound b : Key n} {best out : Option (Key n)} (h : LoopSound ctx bound best out) (hout : out = some b) (hlower : keyLe bound b) : out = some (incMax best bound)

Matching upper and lower bounds turn loop soundness into the exact incumbent equation required when a parent node completes.

theorem Hex.GraphIso.Nauty.SweepCover.exactLive {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tail : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound b : Key n} {best out : Option (Key n)} (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (h : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc (tail + 1) numcells tcell cursor out) (hsound : LoopSound ctx bound best out) (hout : out = some b) (hlive : ∀ (o : Nat), ChildLive rsLab tc (tail + 1) tcell cursor o → keyLe (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells o) b) : out = some (incMax best bound)

Loop soundness plus domination of every live suffix recovers the exact fixed bound without pretending that the executable loop completed.

theorem Hex.GraphIso.Nauty.SweepCover.exact {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tail : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {best out : Option (Key n)} {b : Key n} (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc (tail + 1) numcells tcell cursor out) (hempty : ∀ (o : Nat), ¬ChildLive rsLab tc (tail + 1) tcell cursor o) (hsound : LoopSound ctx (keysMax (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells (o + 1)) (List.range tail))) best out) (hout : out = some b) : out = some (incMax best (keysMax (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells (o + 1)) (List.range tail))))

A completed sweep whose fixed loop bound is the maximum of its original children recovers the exact final incumbent.

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

An installed mutable incumbent always has a concrete key.

theorem Hex.GraphIso.Nauty.SweepCover.exact_of_read {n : Nat} {ctx : Ctx n} {tcLevel specFuel level tail : Nat} {cs : List Nat} {rsLab rsPtn : Array Nat} {tc numcells : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} {st : SearchSt n} {best out : Option (Key n)} (hbound : bound = keysMax (sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells 0) (List.map (fun (o : Nat) => sweepKey ctx tcLevel specFuel level cs rsLab rsPtn tc numcells (o + 1)) (List.range tail))) (hcover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc (tail + 1) numcells tcell cursor out) (hempty : ∀ (o : Nat), ¬ChildLive rsLab tc (tail + 1) tcell cursor o) (hsound : LoopSound ctx bound best out) (hinstalled : st.canonlevel ≠ 0) (hread : stInc ctx st = out) : out = some (incMax best bound)

A completed covered sweep with a readable installed state has exactly folded its fixed child maximum into the incoming incumbent.

inductive Hex.GraphIso.Nauty.NodeResult {n : Nat} (ctx : Ctx n) (tcLevel specFuel runFuel level : Nat) (cs : List Nat) (st out : SearchSt n) (numcells : Nat) (best outBest : Option (Key n)) (r : Int) : Prop

The result of a node call, with logical and runtime fuel separated.

complete and unwind may have the same return integer. The latter is therefore a constructor, not an inequality side condition.

• complete {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (sound : NodeSound ctx tcLevel specFuel level cs st numcells best outBest) (returned : r = Int.ofNat level - 1) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (full : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))) : NodeResult ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
• unwind {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (sound : NodeSound ctx tcLevel specFuel level cs st numcells best outBest) (target : Nat) (returned : r = Int.ofNat target) (below : target < level) (payload : Unwind ctx tcLevel target out outBest) : NodeResult ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
• pruned {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (sound : NodeSound ctx tcLevel specFuel level cs st numcells best outBest) (target : Int) (returned : r = target) (below : target < Int.ofNat level) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (full : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))) : NodeResult ctx tcLevel specFuel runFuel level cs st out numcells best outBest r
• exhausted {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level : Nat} {cs : List Nat} {st out : SearchSt n} {numcells : Nat} {best outBest : Option (Key n)} {r : Int} (empty : runFuel = 0) (returned : r = 0) (unchanged : out = st) (bestUnchanged : outBest = best) : NodeResult ctx tcLevel specFuel runFuel level cs st out numcells best outBest r

theorem Hex.GraphIso.Nauty.NodeResult.parentReturn {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells : Nat} {cs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {r : Int} (h : NodeResult ctx tcLevel specFuel runFuel (level + 1) cs st out numcells best outBest r) (hfuel : runFuel ≠ 0) (hstay : ¬r < Int.ofNat level) : outBest = some (incMax best (nodeKey ctx tcLevel specFuel (level + 1) cs st numcells)) ∨ Nonempty (Unwind ctx tcLevel level out outBest)

When a child does not return past its parent, it either completed its whole subtree (including a local comparison prune), or its generator payload is addressed exactly to that parent.

inductive Hex.GraphIso.Nauty.LoopResult {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)) (r : Option Int) : Prop

The result of a child-loop call. Exhaustion is distinct from a completed empty remainder, so a general theorem cannot accidentally treat the cfuel = 0 arm as coverage of every child.

• complete {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)} {r : Option Int} (returned : r = none) (sound : LoopSound ctx bound best outBest) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (finalSet : VSet n) (finalCursor : Option Nat) (cover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells finalSet finalCursor outBest) (empty : ∀ (o : Nat), ¬ChildLive rsLab tc len finalSet finalCursor o) : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r
• unwind {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)} {r : Option Int} (sound : LoopSound ctx bound best outBest) (target : Nat) (returned : r = some (Int.ofNat target)) (below : target < level) (payload : Unwind ctx tcLevel target out outBest) : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r
• pruned {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)} {r : Option Int} (target : Int) (returned : r = some target) (below : target < Int.ofNat level) (sound : LoopSound ctx bound best outBest) (installed : out.canonlevel ≠ 0) (read : stInc ctx out = outBest) (full : outBest = some (incMax best bound)) : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r
• exhausted {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)} {r : Option Int} (returned : r = none) (sound : LoopSound ctx bound best outBest) (finalSet : VSet n) (finalCursor : Option Nat) (cover : SweepCover ctx tcLevel specFuel level cs rsLab rsPtn tc len numcells finalSet finalCursor outBest) (progress : cursorRank cursor + loopFuel ≤ cursorRank finalCursor) (bounded : ∀ (v : Nat), finalCursor = some v → v < n) : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r

theorem Hex.GraphIso.Nauty.LoopResult.ofChildUnwind {n : Nat} {ctx : Ctx n} {tcLevel childFuel childRunFuel parentFuel loopFuel level : Nat} {childCs loopCs : List Nat} {childNumcells loopNumcells : Nat} {childSt loopSt out : SearchSt n} {best outBest : Option (Key n)} {target : Nat} {fixedpts : VSet n} {rsLab rsPtn : Array Nat} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} {bound : Key n} (hsound : NodeSound ctx tcLevel childFuel (level + 1) childCs childSt childNumcells best outBest) (hkey : keyLe (nodeKey ctx tcLevel childFuel (level + 1) childCs childSt childNumcells) bound) (hbelow : target < level) (hpayload : Unwind ctx tcLevel target out outBest) : LoopResult ctx tcLevel parentFuel childRunFuel loopFuel level loopCs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt { 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 outBest (some (Int.ofNat target))

A child generator unwind strictly past its parent lifts through the parent loop's temporary fixed-vertex cleanup.

theorem Hex.GraphIso.Nauty.NodeResult.complete_of_sweep {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level nodeNumcells loopNumcells tail : Nat} {nodeCs loopCs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {r : Int} {rsLab rsPtn : Array Nat} {tc : Nat} {tcell : VSet n} {cursor : Option Nat} (hchildren : nodeKey ctx tcLevel (specFuel + 1) level nodeCs st 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))) (hsound : LoopSound ctx (nodeKey ctx tcLevel (specFuel + 1) level nodeCs st nodeNumcells) best outBest) (hinstalled : out.canonlevel ≠ 0) (hread : stInc ctx out = outBest) (hcover : SweepCover ctx tcLevel specFuel level loopCs rsLab rsPtn tc (tail + 1) loopNumcells tcell cursor outBest) (hempty : ∀ (o : Nat), ¬ChildLive rsLab tc (tail + 1) tcell cursor o) (hreturn : r = Int.ofNat level - 1) : NodeResult ctx tcLevel (specFuel + 1) runFuel level nodeCs st out nodeNumcells best outBest r

A readable completed child sweep constructs ordinary node completion once the specification identifies that sweep's fixed bound with the node subtree.

theorem Hex.GraphIso.Nauty.NodeResult.pruned_of_loop {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel level numcells : Nat} {cs : List Nat} {st out : SearchSt n} {best outBest : Option (Key n)} {r target : Int} (hinstalled : out.canonlevel ≠ 0) (hread : stInc ctx out = outBest) (hfull : outBest = some (incMax best (nodeKey ctx tcLevel specFuel level cs st numcells))) (hreturn : r = target) (hbelow : target < Int.ofNat level) : NodeResult ctx tcLevel specFuel runFuel level cs st out numcells best outBest r

A loop that has already absorbed its fixed child bound constructs the corresponding pruned node outcome when that bound is the node subtree.

theorem Hex.GraphIso.Nauty.NodeResult.of_loop_some {n : Nat} {ctx : Ctx n} {tcLevel nodeSpecFuel loopSpecFuel nodeRunFuel runFuel loopFuel level : Nat} {nodeCs loopCs : 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)} {r : Int} (hbound : bound = nodeKey ctx tcLevel nodeSpecFuel level nodeCs nodeSt nodeNumcells) (h : LoopResult ctx tcLevel loopSpecFuel runFuel loopFuel level loopCs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out best outBest (some r)) : NodeResult ctx tcLevel nodeSpecFuel nodeRunFuel level nodeCs nodeSt out nodeNumcells best outBest r

A loop return carrying an integer lifts directly through its parent node. The impossible completed and exhausted constructors are excluded by the loop's return option itself.

theorem Hex.GraphIso.Nauty.NodeResult.of_loop_none {n : Nat} {ctx : Ctx n} {tcLevel specFuel nodeRunFuel runFuel loopFuel level tail : Nat} {nodeCs loopCs : 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)} (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 : LoopResult ctx tcLevel specFuel runFuel loopFuel level loopCs rsLab rsPtn tc len loopNumcells tcell cursor bound loopSt out best outBest none) : NodeResult ctx tcLevel (specFuel + 1) nodeRunFuel level nodeCs nodeSt out nodeNumcells best outBest (Int.ofNat level - 1)

A completed loop with enough ranked cursor fuel lifts to ordinary node completion. Cursor exhaustion is ruled out by the same finite-range bound used by the executable root search.

theorem Hex.GraphIso.Nauty.LoopResult.prefix {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 recSt out : SearchSt n} {best mid outBest : Option (Key n)} {r : Option Int} (hpre : LoopSound ctx bound best mid) (h : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound recSt out mid outBest r) : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r

Prepending a sound child fragment transports every recursive loop outcome. In the prune case, the recursive exact incumbent and the composed upper bound recover exactness relative to the original incumbent.

theorem Hex.GraphIso.Nauty.LoopResult.reindexSet {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level : Nat} {cs : 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)} {r : Option Int} (h : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r) : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell' cursor bound st out best outBest r

The entry set only describes where the call begins. Every constructor records the final set, so the result can cross a filter exposed in the caller.

theorem Hex.GraphIso.Nauty.LoopResult.step {n : Nat} {ctx : Ctx n} {tcLevel specFuel runFuel loopFuel level tv : 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)} {r : Option Int} (ha : After cursor tv) (h : LoopResult ctx tcLevel specFuel runFuel loopFuel level cs rsLab rsPtn tc len numcells tcell (some tv) bound st out best outBest r) : LoopResult ctx tcLevel specFuel runFuel (loopFuel + 1) level cs rsLab rsPtn tc len numcells tcell cursor bound st out best outBest r

One successful cursor step transports every recursive loop outcome. For exhaustion, its rank certificate accounts for the fuel consumed by the exposed iteration.