theorem Hex.GraphIso.Nauty.pairOk_fmperm_of_reach {n k : Nat} {G : Colored n k} {ctx : Ctx n} {lab₁ lab₂ γ : Array Nat} (hn0 : 0 < n) (hs₁ : lab₁.size = n) (hr₁ : CellsReach G lab₁) (hr₂ : CellsReach G lab₂) (hsc : ∀ (i : Nat), i < n → γ[lab₁[i]!]! = lab₂[i]!) (hca : checkAutom ctx.g γ = true) : PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmperm γ n).fst (fmperm γ n).snd

A checked scatter between two reached labellings yields a valid explicit autos-ledger entry at the initial coloured partition.

def Hex.GraphIso.Nauty.renamingArray {n : Nat} (sigma : Renaming n) : Array Nat

The finite array represented by a vertex renaming.

Equations

• Hex.GraphIso.Nauty.renamingArray sigma = Array.ofFn fun (i : Fin n) => sigma.toFun ↑i

theorem Hex.GraphIso.Nauty.renamingArray_size {n : Nat} (sigma : Renaming n) : (renamingArray sigma).size = n

theorem Hex.GraphIso.Nauty.renamingArray_get {n : Nat} (sigma : Renaming n) {v : Nat} (hv : v < n) : (renamingArray sigma)[v]! = sigma.toFun v

theorem Hex.GraphIso.Nauty.checkAutom_renaming {n : Nat} {ctx : Ctx n} (sigma : Renaming n) (hrows : RowsMap sigma ctx.g ctx.g) : checkAutom ctx.g (renamingArray sigma) = true

A row-preserving renaming passes the concrete automorphism checker.

theorem Hex.GraphIso.Nauty.childKey_eq_of_subtree {n : Nat} {ctx : Ctx n} {st : RefineSt n} {tcLevel fuel level tc len numcells oU oV : Nat} (hS : SubtreeOk ctx level st) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (hoU : oU < len) (hoV : oV < len) (hfuel : level + 1 + fuel ≤ n + 1) : childKey ctx tcLevel fuel level st.lab st.ptn tc numcells oV = childKey ctx tcLevel fuel level st.lab st.ptn tc numcells oU

At a small-cell node, every two members of a non-singleton cell have equal semantic child subtrees. This packages the geometric flip as the concrete checked, cell-stabilizing array expected by childKey_of_carried.

theorem Hex.GraphIso.Nauty.nodeKey_eq_child_of_subtree {n : Nat} {ctx : Ctx n} {st : SearchSt n} {tcLevel fuel level numcells tc len o : Nat} {codes : List Nat} (hS : SubtreeOk ctx level (refine ctx level st.lab st.ptn st.active numcells)) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hdisc : discreteAt (refine ctx level st.lab st.ptn st.active numcells).ptn level n = false) (hsize : (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) (htc : (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 = tc) (hcell : IsCell (refine ctx level st.lab st.ptn st.active numcells).ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hfuel : level + 1 + fuel ≤ n + 1) : nodeKey ctx tcLevel (fuel + 1) level codes st numcells = sweepKey ctx tcLevel fuel level (codes ++ [(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 tc (refine ctx level st.lab st.ptn st.active numcells).numcells o

If refinement exposes a small-cell node, its unpruned maximum is the subtree below any chosen member of the specification target cell. The target is non-singleton, and the flip theorem makes every entry in its finite maximum equal.

theorem Hex.GraphIso.Nauty.pairOk_fmptn_of_subtree {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level : Nat} {r : RefineSt n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hS : SubtreeOk ctx level r) (hreach : CellsReach G r.lab) (hinit : ∀ (q : Nat), (initPtn n (n + 2) (initialPartition G).snd)[q]! ≤ 1 → r.ptn[q]! ≤ 1) : PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn r.lab r.ptn level n).fst (fmptn r.lab r.ptn level n).snd

The implicit pair recorded at a small-cell node is valid at the root partition. Its missing vertices are realized by the node's flip automorphisms, while singleton cells supply the fixed set.

theorem Hex.GraphIso.Nauty.CheapOk.nextOfSubtree {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level : Nat} {st : SearchSt n} {r : RefineSt n} (h : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) level st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hS : SubtreeOk ctx level r) (hreach : CellsReach G r.lab) (hinit : ∀ (q : Nat), (initPtn n (n + 2) (initialPartition G).snd)[q]! ≤ 1 → r.ptn[q]! ≤ 1) (hlab : st.lab = r.lab) (hptn : st.ptn = r.ptn) : CheapOk ctx (initialPartition G).fst (initPtn n (n + 2) (initialPartition G).snd) (level + 1) st

A guard-passing refined node supplies the pair needed to carry the cheap-boundary invariant into its children.

theorem Hex.GraphIso.Nauty.AutosOk.pushFmperm {n k : Nat} {ctx : Ctx n} {G : Colored n k} {st : SearchSt n} {lab₁ lab₂ gamma : Array Nat} (hn0 : 0 < n) (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (hs₁ : lab₁.size = n) (hr₁ : CellsReach G lab₁) (hr₂ : CellsReach G lab₂) (hsc : ∀ (i : Nat), i < n → gamma[lab₁[i]!]! = lab₂[i]!) (hca : checkAutom ctx.g gamma = true) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (pushAuto st (fmperm gamma n)).autos

Admitting a checked scatter between reached labellings preserves the root automorphism ledger.

theorem Hex.GraphIso.Nauty.AutosOk.pushFmptn {n k : Nat} {ctx : Ctx n} {G : Colored n k} {st : SearchSt n} {level : Nat} {r : RefineSt n} (hn0 : 0 < n) (hlevel : 1 ≤ level) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (hS : SubtreeOk ctx level r) (hreach : CellsReach G r.lab) (hinit : ∀ (q : Nat), (initPtn n (n + 2) (initialPartition G).snd)[q]! ≤ 1 → r.ptn[q]! ≤ 1) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (pushAuto st (fmptn r.lab r.ptn level n)).autos

Recording the scan-free pair justified by a small-cell subtree preserves the root automorphism ledger.

theorem Hex.GraphIso.Nauty.AutosOk.processnodeAuto {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level numcells : Nat} {st : SearchSt n} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (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) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (Nauty.processnode ctx level numcells st).snd.autos

A successful code-one admission preserves the root automorphism ledger.

theorem Hex.GraphIso.Nauty.AutosOk.processnodeRowTie {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level numcells : Nat} {st : SearchSt n} (hn0 : 0 < n) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hcanong : CanongInv ctx st.canong st.canonlab st.samerows) (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (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) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (Nauty.processnode ctx level numcells st).snd.autos

A successful code-two admission preserves the root automorphism ledger.

theorem Hex.GraphIso.Nauty.AutosOk.pruneAutos {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level : Nat} {st : SearchSt n} (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (hpair : level ≠ st.noncheaplevel → PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (Nauty.pruneAutos level st)

The shared code-three/code-four tail preserves the ledger whenever its optional implicit pair is valid.

theorem Hex.GraphIso.Nauty.WorkspaceOk.processAuto {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (h : WorkspaceOk st) (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) : WorkspaceOk (processnode ctx level numcells st).snd

A successful first-path generator admission preserves the bounded workspace.

theorem Hex.GraphIso.Nauty.WorkspaceOk.processOff {n : Nat} {ctx : Ctx n} {level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (h : WorkspaceOk st) (hcode : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hef : ¬(st.eqlevFirst == level) = true) : WorkspaceOk (processnode ctx level numcells st).snd

Off the first path, every comparison-machine leaf branch preserves the bounded workspace.

theorem Hex.GraphIso.Nauty.processnode_internal {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : SearchSt n} (hgate : ¬(st.eqlevFirst ≠ level ∧ st.compCanon < 0)) (hnc : ¬(numcells == n) = true) : processnode ctx level numcells st = (Int.ofNat level, st)

On a non-discrete node admitted to its child sweep, processnode performs no state update.

theorem Hex.GraphIso.Nauty.AutosOk.processnodeOff {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hn0 : 0 < n) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hcanong : CanongInv ctx st.canong st.canonlab st.samerows) (hcode : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (hpair : level ≠ st.noncheaplevel → PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) (hef : ¬(st.eqlevFirst == level) = true) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (Nauty.processnode ctx level numcells st).snd.autos

Off the first path, processnode preserves the root ledger in every comparison-machine outcome.

theorem Hex.GraphIso.Nauty.AutosOk.processnodeGateFail {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hn0 : 0 < n) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hcanong : CanongInv ctx st.canong st.canonlab st.samerows) (hcode : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (hpair : level ≠ st.noncheaplevel → PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) (heq : (st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (hfail : st.firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (Nauty.processnode ctx level numcells st).snd.autos

A failed first-path generator admission test reduces to the ordinary off-path ledger proof once canonical-labelling validity discharges the reused workspace overwrite.

theorem Hex.GraphIso.Nauty.AutosOk.processnode {n k : Nat} {ctx : Ctx n} {G : Colored n k} {level numcells : Nat} {cs bs : List Nat} {st : SearchSt n} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hok : SearchOk G level numcells st) (hrefs : LeafRefsOk G st) (hcanong : CanongInv ctx st.canong st.canonlab st.samerows) (hcode : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hprev : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 st.autos) (hpair : level ≠ st.noncheaplevel → PairOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (fmptn st.lab st.ptn st.noncheaplevel n).fst (fmptn st.lab st.ptn st.noncheaplevel n).snd) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (Nauty.processnode ctx level numcells st).snd.autos

processnode preserves the root automorphism ledger in every leaf, internal, generator, and comparison-prune outcome.

theorem Hex.GraphIso.Nauty.RunInv.processnodeAutos {n k : Nat} {ctx : Ctx n} {G : Colored n k} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (h : RunInv G ctx tcLevel level cs bs fs numcells st best trail) (hbound : st.noncheaplevel ≤ level) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (processnode ctx level numcells st).snd.autos

The stable search invariant discharges the one ledger premise of processnode that no other hypothesis supplies: the runtime bound selects the frozen pair carried by CheapOk.

theorem Hex.GraphIso.Nauty.RunPrep.processnodeAutos {n k : Nat} {ctx : Ctx n} {G : Colored n k} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (h : RunPrep G ctx tcLevel level cs bs fs numcells st best trail) (hbound : st.noncheaplevel ≤ level) : AutosOk ctx.g (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst 1 (processnode ctx level numcells st).snd.autos

The prepared state also discharges the root-ledger premise of a leaf event. Unlike RunInv, it permits the positive comparison sign produced by the immediately preceding code comparison.

theorem Hex.GraphIso.Nauty.RunPrep.leaf {n k : Nat} {ctx : Ctx n} {G : Colored n k} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = cs.length) (hbound : st.noncheaplevel ≤ level) (hef : ¬(st.eqlevFirst == level) = true) (hnc : (numcells == n) = true) (h : RunPrep G ctx tcLevel level cs bs fs numcells st best trail) : ∃ (bs' : List Nat), RunEvent G ctx tcLevel level cs bs' fs (processnode ctx level numcells st).snd (some (incKey ctx bs' (processnode ctx level numcells st).snd.canonlab)) trail ∧ incKey ctx bs' (processnode ctx level numcells st).snd.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ ((processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∨ (processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat cs.length) ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaCanon)

An ordinary off-first-path discrete leaf turns the prepared state into an event state whose incumbent is exactly the maximum of the incoming incumbent and that leaf. The return disjunction is retained for the node outcome split.

theorem Hex.GraphIso.Nauty.RunPrep.leafFirst {n k : Nat} {ctx : Ctx n} {G : Colored n k} {tcLevel level numcells : Nat} {cs bs fs : List Nat} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (hn0 : 0 < n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hlevel : 1 ≤ level) (hpath : level = cs.length) (hbound : st.noncheaplevel ≤ level) (heq : (st.eqlevFirst == level) = true) (hfail : st.firstcode[level + 1]! ≠ codeSentinel ∨ isautom ctx (firstScatter n st.firstlab st.lab) = false) (hnc : (numcells == n) = true) (h : RunPrep G ctx tcLevel level cs bs fs numcells st best trail) : ∃ (bs' : List Nat), RunEvent G ctx tcLevel level cs bs' fs (processnode ctx level numcells st).snd (some (incKey ctx bs' (processnode ctx level numcells st).snd.canonlab)) trail ∧ incKey ctx bs' (processnode ctx level numcells st).snd.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ ((processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel st.eqlevCanon ∨ (processnode ctx level numcells st).fst = pruneReturn st.noncheaplevel st.allsamelevel (Int.ofNat cs.length) ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaFirst ∨ (processnode ctx level numcells st).fst = Int.ofNat st.gcaCanon)

A first-path-agreeing leaf whose generator admission guard fails has the same exact event invariant as an ordinary compared leaf.