def Hex.GraphIso.Nauty.incKey {n : Nat} (ctx : Ctx n) (bs : List Nat) (canonlab : Array Nat) : Key n

The incumbent's key: the ghost code list with the sentinel stamped, and the stored best leaf's rows.

Equations

• Hex.GraphIso.Nauty.incKey ctx bs canonlab = { codes := bs ++ [Hex.GraphIso.Nauty.codeSentinel], rows := Hex.GraphIso.Nauty.leafRows ctx canonlab }

def Hex.GraphIso.Nauty.pathLeafKey {n : Nat} (ctx : Ctx n) (cs : List Nat) (lab : Array Nat) : Key n

A leaf key of the current path.

Equations

• Hex.GraphIso.Nauty.pathLeafKey ctx cs lab = { codes := cs ++ [Hex.GraphIso.Nauty.codeSentinel], rows := Hex.GraphIso.Nauty.leafRows ctx lab }

theorem Hex.GraphIso.Nauty.codeInv_tied_le {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 0) : cs.length ≤ bs.length

Under full agreement the path is never deeper than the incumbent.

theorem Hex.GraphIso.Nauty.tied_short_keyCmp_gt {n nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 0) (hshort : cs.length < bs.length) (r1 r2 : List (VSet n)) : keyCmp { codes := cs ++ [codeSentinel], rows := r1 } { codes := bs ++ [codeSentinel], rows := r2 } = Ordering.gt

A code-tied leaf strictly above the incumbent's depth compares above it: the leaf's sentinel meets a real incumbent code.

theorem Hex.GraphIso.Nauty.tied_full_keyCmp {n nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 0) (hlen : cs.length = bs.length) (r1 r2 : List (VSet n)) : keyCmp { codes := cs ++ [codeSentinel], rows := r1 } { codes := bs ++ [codeSentinel], rows := r2 } = listCmp VSet.rowCmp r1 r2

A code-tied leaf at the incumbent's depth hands the comparison to the rows.

theorem Hex.GraphIso.Nauty.frozen_lt_keyCmp {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {lab canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) : keyCmp (pathLeafKey ctx cs lab) (incKey ctx bs canonlab) = Ordering.lt

The downward-frozen verdict at a leaf, in incumbent-key form.

theorem Hex.GraphIso.Nauty.frozen_gt_keyCmp {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {lab canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 1) : keyCmp (pathLeafKey ctx cs lab) (incKey ctx bs canonlab) = Ordering.gt

The upward-frozen verdict at a leaf, in incumbent-key form.

theorem Hex.GraphIso.Nauty.firstterminal_firstCodeInv {n : Nat} {κ : Type} {nn : Nat} {cs : List Nat} {st : SearchState n κ} (hsize : st.firstcode.size = nn + 2) (hLnn : cs.length ≤ nn) (hfc : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (hclt : ∀ (c : Nat), c ∈ cs → c < codeSentinel) : FirstCodeInv nn cs cs (firstterminal cs.length st).firstcode (firstterminal cs.length st).eqlevFirst

firstterminal seeds the first-path machine: the just-installed first leaf agrees with itself at full depth.

def Hex.GraphIso.Nauty.prefixKey {n : Nat} (cs : List Nat) (kk : Key n) : Key n

The absolute key of a spec subtree below the path codes cs.

Equations

• Hex.GraphIso.Nauty.prefixKey cs kk = { codes := cs ++ kk.codes, rows := kk.rows }

theorem Hex.GraphIso.Nauty.prefixKey_nil {n : Nat} (kk : Key n) : prefixKey [] kk = kk

theorem Hex.GraphIso.Nauty.prefixKey_keyMax {n : Nat} (cs : List Nat) (k1 k2 : Key n) : prefixKey cs (keyMax k1 k2) = keyMax (prefixKey cs k1) (prefixKey cs k2)

Prefixing by common path codes commutes with the key maximum.

theorem Hex.GraphIso.Nauty.prefixKey_cons {n : Nat} (cs : List Nat) (code : Nat) (K : Key n) : prefixKey cs { codes := code :: K.codes, rows := K.rows } = prefixKey (cs ++ [code]) K

Prefixing a common code moves it into the path.

theorem Hex.GraphIso.Nauty.prefixKey_keysMax {n : Nat} (l : List (Key n)) (b : Key n) (cs : List Nat) : prefixKey cs (keysMax b l) = keysMax (prefixKey cs b) (List.map (prefixKey cs) l)

Prefixing distributes over the seeded list maximum.

def Hex.GraphIso.Nauty.specChild {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells o : Nat) : Key n

One child key of a spec node: the subtree below individualizing the o-th target-cell vertex of the refined state.

Equations

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

theorem Hex.GraphIso.Nauty.specNode_internal {n : Nat} {ctx : Ctx n} {tcLevel fuel level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells len : Nat} (cs : List Nat) (hdisc : discreteAt (refine ctx level lab ptn active numcells).ptn level n = false) (hlen : (specMaketargetcell ctx (refine ctx level lab ptn active numcells).lab (refine ctx level lab ptn active numcells).ptn level tcLevel).snd.snd = len + 1) : prefixKey cs (specNode ctx tcLevel (fuel + 1) level lab ptn active numcells) = keysMax (prefixKey (cs ++ [(refine ctx level lab ptn active numcells).longcode]) (specChild ctx tcLevel fuel level lab ptn active numcells 0)) (List.map (fun (o : Nat) => prefixKey (cs ++ [(refine ctx level lab ptn active numcells).longcode]) (specChild ctx tcLevel fuel level lab ptn active numcells (o + 1))) (List.range len))

The internal arm of specNode, isolated: at a non-discrete node the subtree key under the path prefix is the maximum of the children's keys under the path extended by the node's own code.

theorem Hex.GraphIso.Nauty.discreteAt_iff_bcount {ptn : Array Nat} {level nn : Nat} (hnn : nn = ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) : discreteAt ptn level nn = true ↔ bcount ptn level nn = nn

Discreteness is exactly a full boundary count.

theorem Hex.GraphIso.Nauty.rows_eq_of_testcanlab_tie {n : Nat} {ctx : Ctx n} {st : Search n} (hinv : CanongInv ctx st.canong st.canonlab st.samerows) (h : (testcanlab ctx (updatecan ctx st.canong st.canonlab st.samerows) st.lab).fst = 0) : leafRows ctx st.canonlab = leafRows ctx st.lab

Equal canonical-row comparison identifies the two leaf-row lists.

theorem Hex.GraphIso.Nauty.labOk_of_reach {n k : Nat} {G : Colored n k} {lab : Array Nat} (hsz : lab.size = n) (h : CellsReach G lab) : LabOk lab n

A reached labelling lands in the vertex range.

theorem Hex.GraphIso.Nauty.labInj_of_reach {n k : Nat} {G : Colored n k} {lab : Array Nat} (hsz : lab.size = n) (hn0 : 0 < n) (h : CellsReach G lab) : LabInj lab n

A reached labelling is injective: it is a permutation of the vertex range, hence duplicate-free.

theorem Hex.GraphIso.Nauty.codeInv_take_listCmp_lt {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) {M : Nat} (hM : eqlevCanon.toNat < M) (hMcs : M ≤ cs.length) (ext : List Nat) : listCmp compare (List.take M cs ++ ext) (bs ++ [codeSentinel]) = Ordering.lt

The frozen divergence survives truncation: with the divergence recorded at level eqlevCanon + 1, the path prefix down to any level at or beyond it still compares below the incumbent, whatever comes after.

theorem Hex.GraphIso.Nauty.frozen_take_keyCmp_lt {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) {M : Nat} (hM : eqlevCanon.toNat < M) (hMcs : M ≤ cs.length) (K : Key n) : keyCmp (prefixKey (List.take M cs) K) (incKey ctx bs canonlab) = Ordering.lt

The key-level truncated verdict: every subtree hanging below the truncated path is dominated once the machine froze downward at or above the truncation level.

theorem Hex.GraphIso.Nauty.frozen_take_keyLe {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) {M : Nat} (hM : eqlevCanon.toNat < M) (hMcs : M ≤ cs.length) (K : Key n) : keyLe (prefixKey (List.take M cs) K) (incKey ctx bs canonlab)

frozen_take_keyCmp_lt in the keyLe form the absorption consumes.

theorem Hex.GraphIso.Nauty.frozen_keyLe {n nn : Nat} {cs bs : List Nat} {ctx : Ctx n} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} {canonlab : Array Nat} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) (K : Key n) : keyLe (prefixKey cs K) (incKey ctx bs canonlab)

The whole-path instance: with the machine frozen downward, every subtree below the current path is dominated.

theorem Hex.GraphIso.Nauty.childKey_of_carried {n : Nat} {ctx : Ctx n} (hgsz : ctx.g.size = n) {γ : Array Nat} (hAut : checkAutom ctx.g γ = true) (tcLevel fuel level : Nat) {rsLab rsPtn : Array Nat} {tc lenT numcells o o' : Nat} (hstab : 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 lenT) (hrange : tc + lenT ≤ n) (ho : o < lenT) (ho' : o' < lenT) (hlf : level + 1 + fuel ≤ n + 1) (hcarry : γ[rsLab[tc + o']!]! = rsLab[tc + o]!) : childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o = childKey ctx tcLevel fuel level rsLab rsPtn tc numcells o'

A checked automorphism stabilizing the refined node's cells and carrying one target-cell vertex onto another identifies the two children's subtree keys.