theorem Hex.GraphIso.Nauty.isCell_refine_one {n : Nat} {ctx : Ctx n} {level : Nat} {active : VSet n} {numcells a : Nat} {lab ptn : Array Nat} (hnn : n = ptn.size) (hls : lab.size = ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (hc : IsCell ptn level a 1) : IsCell (refine ctx level lab ptn active numcells).ptn level a 1

Refinement preserves an existing singleton cell.

theorem Hex.GraphIso.Nauty.isCell_set_miss {ptn : Array Nat} {level a tc len : Nat} (ha : IsCell ptn level a 1) (ht : IsCell ptn level tc len) (hlen : 2 ≤ len) : IsCell (ptn.set! tc (level + 1)) (level + 1) a 1

Splitting a different non-singleton cell preserves a singleton.

theorem Hex.GraphIso.Nauty.TrailOk.stateEq {n : Nat} {ctx : Ctx n} {level : Nat} {st st' : SearchSt n} {trail : FrameTrail} (h : TrailOk ctx level st trail) (hlab : st'.lab = st.lab) (hptn : st'.ptn = st.ptn) : TrailOk ctx level st' trail

Reindex frame reach across unchanged labelling and partition fields.

theorem Hex.GraphIso.Nauty.TrailOk.refine {n : Nat} {ctx : Ctx n} {level : Nat} {active : VSet n} {numcells : Nat} {st out : SearchSt n} {trail : FrameTrail} (h : TrailOk ctx level st trail) (hls : st.lab.size = n) (hps : st.ptn.size = n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hlab : out.lab = (Nauty.refine ctx level st.lab st.ptn active numcells).lab) (hptn : out.ptn = (Nauty.refine ctx level st.lab st.ptn active numcells).ptn) : TrailOk ctx level out trail

Refinement preserves reach from every active ancestor and leaves all of their closed boundaries untouched.

theorem Hex.GraphIso.Nauty.TrailOk.processnode {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} {trail : FrameTrail} (h : TrailOk ctx level st trail) : TrailOk ctx level (Nauty.processnode ctx level numcells st).snd trail

Leaf processing changes neither the current labelling nor partition.

theorem Hex.GraphIso.Nauty.TrailOk.recover {n : Nat} {ctx : Ctx n} {current level inf : Nat} {st : SearchSt n} {trail : FrameTrail} (h : TrailOk ctx current st trail) (hle : level ≤ current) : TrailOk ctx level (Nauty.recover n inf level st) trail

Reopening to an ancestor preserves every older active frame.

theorem Hex.GraphIso.Nauty.TrailOk.push {n : Nat} {ctx : Ctx n} {level specFuel numcells tc len o : Nat} {codes : List Nat} {st out : SearchSt n} {trail : FrameTrail} (h : TrailOk ctx level st trail) (hls : st.lab.size = n) (hps : st.ptn.size = n) (hinj : LabInj st.lab st.lab.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hlab : out.lab = (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst) (hptn : out.ptn = st.ptn.set! tc (level + 1)) : TrailOk ctx (level + 1) out (trail.push level { frame := sweepFrame specFuel codes st.lab st.ptn tc numcells, offset := o })

Individualization extends the active trail with the selected parent child while preserving reach from every older frame.

theorem Hex.GraphIso.Nauty.TrailOk.pushFrame {n : Nat} {ctx : Ctx n} {level specFuel numcells tc len offset currentOffset : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {st child : SearchSt n} {trail : FrameTrail} (h : TrailOk ctx level st trail) (hls : st.lab.size = n) (hps : st.ptn.size = n) (hinj : LabInj st.lab st.lab.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hrsLab : rsLab.size = n) (hrsPtn : rsPtn.size = n) (hrsEnd : rsPtn[rsPtn.size - 1]! ≤ level) (hperm : cellsPerm rsPtn level rsLab st.lab) (hptnEq : st.ptn = rsPtn) (hcell : IsCell rsPtn level tc len) (hcurrent : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (hoffset : offset < len) (hcurrentOffset : currentOffset < len) (hat : st.lab[tc + currentOffset]! = rsLab[tc + offset]!) (hlab : child.lab = (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + currentOffset]!).fst) (hptn : child.ptn = st.ptn.set! tc (level + 1)) : TrailOk ctx (level + 1) child (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset })

Individualizing a recovered parent records the frozen specification frame rather than the current within-cell permutation of that frame.

def Hex.GraphIso.Nauty.Guide.ofSweep {n : Nat} {ctx : Ctx n} {tcLevel specFuel level : Nat} {codes : List Nat} {rsLab rsPtn ref : Array Nat} {tc len numcells offset : Nat} {best : Option (Key n)} (hlevel : 1 ≤ level) (hdone : ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells best offset) (hls : rsLab.size = n) (hlab : LabOk rsLab n) (hps : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hcell : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hoff : offset < len) (hfuel : level + 1 + specFuel ≤ n + 1) (hat : ref[tc]! = rsLab[tc + offset]!) (hrefSize : ref.size = n) (hrefReach : cellsPerm rsPtn level rsLab ref) : Guide ctx tcLevel level best

Package one already-covered child of a frozen sweep as a generator guide. The reference labelling may be either the first leaf or the current canonical leaf.

Equations

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

theorem Hex.GraphIso.Nauty.GuideStore.pushSweep {n : Nat} {ctx : Ctx n} {tcLevel specFuel level numcells tc len activeOffset : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (h : GuideStore ctx tcLevel level st best trail) (hlevel : 1 ≤ level) (hls : rsLab.size = n) (hlab : LabOk rsLab n) (hps : rsPtn.size = n) (hend : rsPtn[rsPtn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), rsPtn[q]! ≤ level ∨ rsPtn[q]! = n + 2) (hcell : IsCell rsPtn level tc len) (hrange : tc + len ≤ n) (hfuel : level + 1 + specFuel ≤ n + 1) (hfirstSize : st.firstlab.size = n) (hcanonSize : st.canonlab.size = n) (hfirst : st.gcaFirst = level → ∃ (o : Nat), o < len ∧ ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells best o ∧ st.firstlab[tc]! = rsLab[tc + o]! ∧ cellsPerm rsPtn level rsLab st.firstlab) (hcanon : st.gcaCanon = level → ∃ (o : Nat), o < len ∧ ChildDone ctx tcLevel specFuel level codes rsLab rsPtn tc numcells best o ∧ st.canonlab[tc]! = rsLab[tc + o]! ∧ cellsPerm rsPtn level rsLab st.canonlab) : GuideStore ctx tcLevel (level + 1) st best (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := activeOffset })

Descending into a sweep child extends both guide ledgers. A guide whose control is the current level is supplied by an already-covered child of that sweep. Guides at shallower levels transport unchanged.

theorem Hex.GraphIso.Nauty.NodeResult.sound {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 cs st out numcells best outBest r) (hfuel : runFuel ≠ 0) : NodeSound ctx tcLevel specFuel level cs st numcells best outBest

Positive runtime fuel exposes the semantic soundness carried by every non-exhausted node result.

theorem Hex.GraphIso.Nauty.otherNode_leaf_receipt {n : Nat} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells target : Nat} {cs : List Nat} {st : SearchSt n} {best outBest : Option (Key n)} {trail : FrameTrail} (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) (payload : Unwind ctx tcLevel target (processnode ctx level n (otherLeafSt ctx level numcells st)).snd outBest) (hloc : Unwind.Located trail payload) : NodeReceipt trail 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 located leaf-event unwind lifts directly through otherNode.

theorem Hex.GraphIso.Nauty.Guide.firstLocated {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (g : Guide ctx tcLevel st.gcaFirst best) (href : g.ref = st.firstlab) (hloc : Located trail g) (htrail : TrailOk ctx level st trail) (hbelow : st.gcaFirst < level) (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) : ∃ (payload : Unwind ctx tcLevel st.gcaFirst (processnode ctx level numcells st).snd best), Unwind.Located trail payload

A code-one admission at a reached active child has a located direct unwind payload.

theorem Hex.GraphIso.Nauty.Guide.canonLocated {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (g : Guide ctx tcLevel st.gcaCanon best) (href : g.ref = st.canonlab) (hloc : Located trail g) (htrail : TrailOk ctx level st trail) (hbelow : st.gcaCanon < level) (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) : ∃ (payload : Unwind ctx tcLevel st.gcaCanon (processnode ctx level numcells st).snd best), Unwind.Located trail payload

A code-two admission at a reached active child has a located direct canonical unwind payload.

theorem Hex.GraphIso.Nauty.Guide.tiedLocated {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (g : Guide ctx tcLevel st.gcaCanon best) (href : g.ref = st.canonlab) (hloc : Located trail g) (htrail : TrailOk ctx level st trail) (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) (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 ∧ (target = (processnode ctx level numcells st).snd.gcaFirst ∨ target = (processnode ctx level numcells st).snd.gcaCanon) ∧ ∃ (payload : Unwind ctx tcLevel target (processnode ctx level numcells st).snd best), Unwind.Located trail payload

A row-tied code-two event carries location evidence in both return arms: the canonical arm uses its stored guide, while the first-ancestor arm is the loop-local orbit return.

theorem Hex.GraphIso.Nauty.GuideStore.firstUnwind {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hstore : GuideStore ctx tcLevel level st best trail) (htrail : TrailOk ctx level st trail) (hfirstPos : 0 < st.gcaFirst) (hbelow : st.gcaFirst < level) (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) : ∃ (payload : Unwind ctx tcLevel st.gcaFirst (processnode ctx level numcells st).snd best), Unwind.Located trail payload

The located guide store discharges a code-one leaf return.

theorem Hex.GraphIso.Nauty.GuideStore.tiedUnwind {n : Nat} {ctx : Ctx n} {tcLevel level numcells : Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hstore : GuideStore ctx tcLevel level st best trail) (htrail : TrailOk ctx level st trail) (hcanonPos : 0 < st.gcaCanon) (hcanonBelow : st.gcaCanon < level) (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) (hfirstPos : 1 ≤ st.gcaFirst) (hfirstBelow : st.gcaFirst < level) (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 ∧ (target = (processnode ctx level numcells st).snd.gcaFirst ∨ target = (processnode ctx level numcells st).snd.gcaCanon) ∧ ∃ (payload : Unwind ctx tcLevel target (processnode ctx level numcells st).snd best), Unwind.Located trail payload

The located guide store discharges either arm of a row-tied code-two leaf return.

theorem Hex.GraphIso.Nauty.otherNode_leaf_firstReceipt {n : Nat} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {cs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hstore : GuideStore ctx tcLevel level (otherLeafSt ctx level numcells st) best trail) (htrail : TrailOk ctx level (otherLeafSt ctx level numcells st) trail) (hfirstPos : 0 < (otherLeafSt ctx level numcells st).gcaFirst) (hbelow : (otherLeafSt ctx level numcells st).gcaFirst < level) (hgsz : ctx.g.size = n) (hfirstSize : (otherLeafSt ctx level numcells st).firstlab.size = 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) (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) : NodeReceipt trail ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best best (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A code-one leaf return is a located node receipt. Its incumbent is unchanged, so its NodeSound component needs no comparison with the first leaf.

theorem Hex.GraphIso.Nauty.otherNode_leaf_tiedReceipt {n : Nat} {ctx : Ctx n} {inf tcLevel specFuel fuel level numcells : Nat} {cs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hnum : (refine ctx level st.lab st.ptn st.active numcells).numcells = n) (hstore : GuideStore ctx tcLevel level (otherLeafSt ctx level numcells st) best trail) (htrail : TrailOk ctx level (otherLeafSt ctx level numcells st) trail) (hcanonPos : 0 < (otherLeafSt ctx level numcells st).gcaCanon) (hcanonBelow : (otherLeafSt ctx level numcells st).gcaCanon < level) (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)) (hrows : leafRows ctx (otherLeafSt ctx level numcells st).canonlab = leafRows ctx (otherLeafSt ctx level numcells st).lab) (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) (hfirstPos : 1 ≤ (otherLeafSt ctx level numcells st).gcaFirst) (hfirstBelow : (otherLeafSt ctx level numcells st).gcaFirst < level) (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) : NodeReceipt trail ctx tcLevel (specFuel + 1) (fuel + 1) level cs st (otherNode ctx inf tcLevel (fuel + 1) level numcells st).snd numcells best best (otherNode ctx inf tcLevel (fuel + 1) level numcells st).fst

A row-tied code-two leaf return is a located node receipt in both the canonical-guide and first-ancestor orbit arms.