theorem Hex.GraphIso.Nauty.refine_longcode_lt {n : Nat} (ctx : Ctx n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : (refine ctx level lab ptn active numcells).longcode < codeSentinel

Every refinement code is strictly below the sentinel.

def Hex.GraphIso.Nauty.bcode (bs : List Nat) (i : Nat) : Nat

The incumbent's code at level i (1-indexed): the stored codes, then the sentinel at every deeper level.

Equations

• Hex.GraphIso.Nauty.bcode bs i = if i - 1 < bs.length then bs[i - 1]! else Hex.GraphIso.Nauty.codeSentinel

theorem Hex.GraphIso.Nauty.bcode_of_le {bs : List Nat} {i : Nat} (h1 : 1 ≤ i) (h2 : i ≤ bs.length) : bcode bs i = bs[i - 1]!

theorem Hex.GraphIso.Nauty.bcode_sentinel {bs : List Nat} {i : Nat} (h : bs.length < i) : bcode bs i = codeSentinel

theorem Hex.GraphIso.Nauty.bcode_lt {bs : List Nat} {i : Nat} (hblt : ∀ (b : Nat), b ∈ bs → b < codeSentinel) (h1 : 1 ≤ i) (h2 : i ≤ bs.length) : bcode bs i < codeSentinel

theorem Hex.GraphIso.Nauty.getElem!_append_sentinel {bs : List Nat} {i : Nat} (h : i ≤ bs.length) : (bs ++ [codeSentinel])[i]! = bcode bs (i + 1)

The extended incumbent list bs ++ [codeSentinel] reads as bcode at every position up to and including the sentinel.

theorem Hex.GraphIso.Nauty.listCmp_lt_of_prefix (p : Nat) (xs ys : List Nat) : p < xs.length → p < ys.length → (∀ (i : Nat), i < p → xs[i]! = ys[i]!) → xs[p]! < ys[p]! → listCmp compare xs ys = Ordering.lt

A strict drop at position p after agreement below it decides the lexicographic comparison downward.

theorem Hex.GraphIso.Nauty.listCmp_gt_of_prefix (p : Nat) (xs ys : List Nat) : p < xs.length → p < ys.length → (∀ (i : Nat), i < p → xs[i]! = ys[i]!) → ys[p]! < xs[p]! → listCmp compare xs ys = Ordering.gt

A strict rise at position p after agreement below it decides the lexicographic comparison upward.

structure Hex.GraphIso.Nauty.CodeCmpInv (nn : Nat) (cs bs : List Nat) (canoncode : Array Nat) (canonlevel : Nat) (eqlevCanon compCanon : Int) : Prop

The lazily threaded code comparison state, relative to the current path's codes cs (levels 1 .. cs.length) and the incumbent's codes bs (levels 1 .. bs.length, sentinel beyond).

• size : canoncode.size = nn + 2

  The code store always has nn + 2 slots.

• blen : canonlevel = bs.length

  canonlevel counts the incumbent's codes.

• bbound : bs.length ≤ nn

  The incumbent's leaf is at a real level.

• blt (b : Nat) : b ∈ bs → b < codeSentinel

  Stored incumbent codes are real codes.

• clt (c : Nat) : c ∈ cs → c < codeSentinel

  Path codes are real codes.

• tri : (compCanon = 0 ∧ eqlevCanon = Int.ofNat cs.length ∧ cs.length ≤ bs.length ∧ ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → cs[i - 1]! = bcode bs i) ∨ ∃ (j : Nat), 1 ≤ j ∧ j ≤ cs.length ∧ j ≤ bs.length + 1 ∧ eqlevCanon = Int.ofNat (j - 1) ∧ (∀ (i : Nat), 1 ≤ i → i < j → cs[i - 1]! = bcode bs i) ∧ (compCanon = -1 ∧ cs[j - 1]! < bcode bs j ∨ compCanon = 1 ∧ j ≤ bs.length ∧ bcode bs j < cs[j - 1]!)

  The comparison trichotomy: full agreement, or a frozen divergence at level j with matched prefix below it.

• content (i : Nat) : 1 ≤ i → i ≤ bs.length + 1 → (compCanon = 1 → i ≤ eqlevCanon.toNat ∨ cs.length < i) → canoncode[i]! = bcode bs i

  Outside the upward-divergence overwrite window, the store holds the incumbent's codes (sentinel at bs.length + 1).

• over : compCanon = 1 → ∀ (i : Nat), eqlevCanon.toNat < i → i ≤ cs.length → canoncode[i]! = cs[i - 1]!

  Inside the overwrite window, the store holds the path's codes.

theorem Hex.GraphIso.Nauty.codeInv_listCmp_lt {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) (ext : List Nat) : listCmp compare (cs ++ ext) (bs ++ [codeSentinel]) = Ordering.lt

With compCanon = -1, every leaf below the node compares below the incumbent on codes, whatever the deeper codes are.

theorem Hex.GraphIso.Nauty.codeInv_listCmp_gt {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon 1) (ext : List Nat) : listCmp compare (cs ++ ext) (bs ++ [codeSentinel]) = Ordering.gt

With compCanon = 1, every leaf below the node compares above the incumbent on codes, whatever the deeper codes are.

theorem Hex.GraphIso.Nauty.codeInv_keyCmp_lt {n nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon (-1)) (ext : List Nat) (r1 r2 : List (VSet n)) : keyCmp { codes := cs ++ ext, rows := r1 } { codes := bs ++ [codeSentinel], rows := r2 } = Ordering.lt

The key-level form of codeInv_listCmp_lt.

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

The key-level form of codeInv_listCmp_gt.

theorem Hex.GraphIso.Nauty.codeInv_eq_of_tied {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) : cs = bs

With compCanon = 0 and the path at the incumbent's depth, the code lists are equal outright: the tied-leaf case hands the key comparison to the rows (keyCmp_codes_eq).

theorem Hex.GraphIso.Nauty.otherNodePrep_codeInv {n nn : Nat} {cs bs : List Nat} {st : SearchSt n} {code : Nat} (hinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hcode : code < codeSentinel) (hLnn : cs.length + 1 ≤ nn + 1) : CodeCmpInv nn (cs ++ [code]) bs (otherNodePrep (cs.length + 1) code st).canoncode (otherNodePrep (cs.length + 1) code st).canonlevel (otherNodePrep (cs.length + 1) code st).eqlevCanon (otherNodePrep (cs.length + 1) code st).compCanon

One otherNodePrep step at level cs.length + 1 with fresh code code extends the comparison invariant by one level.

theorem Hex.GraphIso.Nauty.recover_codeInv {nn N inf : Nat} {cs bs : List Nat} {st : SearchSt N} {lvl : Nat} (hinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon) (hcc : st.compCanon ≤ 0) (hlvl : lvl ≤ cs.length) : CodeCmpInv nn (List.take lvl cs) bs (recover N inf lvl st).canoncode (recover N inf lvl st).canonlevel (recover N inf lvl st).eqlevCanon (recover N inf lvl st).compCanon

recover under a live (non-overwriting) comparison: unwinding to lvl truncates the path and restores full agreement when the match reached lvl.

theorem Hex.GraphIso.Nauty.recover_codeInv_reset {nn N inf : Nat} {cs bs : List Nat} {st : SearchSt N} {lvl : Nat} (hinv : CodeCmpInv nn cs bs st.canoncode st.canonlevel st.eqlevCanon 0) (hlvl : lvl ≤ cs.length) : CodeCmpInv nn (List.take lvl cs) bs (recover N inf lvl st).canoncode (recover N inf lvl st).canonlevel (recover N inf lvl st).eqlevCanon (recover N inf lvl st).compCanon

recover after a leaf event that repurposed compCanon for the row comparison: the pre-leaf state matched through the whole path (compCanon = 0 invariant), so unwinding to any lvl within the path resets to full agreement whatever compCanon currently holds.

theorem Hex.GraphIso.Nauty.firstterminal_codeInv {n nn : Nat} {cs : List Nat} {st : SearchSt n} (hsize : st.canoncode.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) : CodeCmpInv nn cs cs (firstterminal cs.length st).canoncode (firstterminal cs.length st).canonlevel (firstterminal cs.length st).eqlevCanon (firstterminal cs.length st).compCanon

firstterminal seeds the comparison invariant: the first leaf's codes become the incumbent with full agreement recorded.

theorem Hex.GraphIso.Nauty.install_codeInv {nn : Nat} {cs bs : List Nat} {canoncode : Array Nat} {canonlevel : Nat} {eqlevCanon compCanon : Int} (hinv : CodeCmpInv nn cs bs canoncode canonlevel eqlevCanon compCanon) (hne : compCanon ≠ -1) (hLnn : cs.length ≤ nn) : CodeCmpInv nn cs cs (canoncode.set! (cs.length + 1) codeSentinel) cs.length (Int.ofNat cs.length) 0

Installing the current path as the new incumbent (the pure part of the code-3 arm): after a non-downward comparison, the store already holds the path's codes, so recording the path as incumbent with the sentinel stamped re-seeds the invariant at full agreement.

structure Hex.GraphIso.Nauty.FirstCodeInv (nn : Nat) (cs fs : List Nat) (firstcode : Array Nat) (eqlevFirst : Nat) : Prop

The first-path comparison state: the current path's codes cs agree with the first leaf's codes fs through level eqlevFirst, and firstcode stores fs with the sentinel stamped above.

• size : firstcode.size = nn + 2

  The code store always has nn + 2 slots.

• fbound : fs.length ≤ nn

  The first leaf is at a real level.

• flt (f : Nat) : f ∈ fs → f < codeSentinel

  First-path codes are real codes.

• fcontent (i : Nat) : 1 ≤ i → i ≤ fs.length → firstcode[i]! = fs[i - 1]!

  The store holds the first leaf's codes.

• fsent : firstcode[fs.length + 1]! = codeSentinel

  The sentinel is stamped above the first leaf's codes.

• elev_le : eqlevFirst ≤ cs.length

  The agreement depth is within the current path.

• elev_fs : eqlevFirst ≤ fs.length

  The agreement depth is within the first path.

• agree (i : Nat) : 1 ≤ i → i ≤ eqlevFirst → cs[i - 1]! = fs[i - 1]!

  Recorded agreement is code-prefix agreement.

theorem Hex.GraphIso.Nauty.firstCodeInv_mono {nn : Nat} {cs fs : List Nat} {firstcode : Array Nat} {eqlevFirst e' : Nat} (hinv : FirstCodeInv nn cs fs firstcode eqlevFirst) (he : e' ≤ eqlevFirst) : FirstCodeInv nn cs fs firstcode e'

Lowering the agreement depth preserves the invariant: the clause for othernode's target-cell demotion and any other clamp.

theorem Hex.GraphIso.Nauty.firstCodeInv_take {nn : Nat} {cs fs : List Nat} {firstcode : Array Nat} {eqlevFirst lvl : Nat} (hinv : FirstCodeInv nn cs fs firstcode eqlevFirst) (hlvl : lvl ≤ cs.length) : FirstCodeInv nn (List.take lvl cs) fs firstcode (min lvl eqlevFirst)

Truncating the path above the agreement depth preserves the invariant: the clause for recover's unwind together with its clamp.

theorem Hex.GraphIso.Nauty.firstCodeInv_eq_of_tied {nn : Nat} {cs fs : List Nat} {firstcode : Array Nat} (hinv : FirstCodeInv nn cs fs firstcode cs.length) (hlen : cs.length = fs.length) : cs = fs

With the agreement depth at the full length of both paths, the code lists are equal outright: the code-1 leaf case.

theorem Hex.GraphIso.Nauty.firstCodeInv_len_of_sentinel {nn : Nat} {cs fs : List Nat} {firstcode : Array Nat} (hinv : FirstCodeInv nn cs fs firstcode cs.length) (hsent : firstcode[cs.length + 1]! = codeSentinel) : cs.length = fs.length

The first-path store decides where the first leaf sits: every position within the first path holds a real code, so the sentinel appearing just above the current path forces the two paths to end at the same level.

This is what the length premise of firstCodeInv_eq_of_tied reduces to. It cannot be read off the refinement codes: mash masks its accumulator to fifteen bits, so agreeing codes do not determine the partition, let alone its cell count. The store's sentinel position does determine it.

theorem Hex.GraphIso.Nauty.firstCodeInv_listCmp_gt_of_lt {nn : Nat} {cs fs : List Nat} {firstcode : Array Nat} (hinv : FirstCodeInv nn cs fs firstcode cs.length) (hlt : cs.length < fs.length) : listCmp compare (cs ++ [codeSentinel]) (fs ++ [codeSentinel]) = Ordering.gt

The sentinel hypothesis above cannot be dropped. Where the first-path comparison is still live and the path is strictly shorter than the first path, the current leaf's key strictly exceeds the first leaf's, because the sentinel outranks every real code, so the code-1 skip would discard a candidate above the incumbent.

theorem Hex.GraphIso.Nauty.firstCodeInv_eq_of_live {nn : Nat} {cs fs : List Nat} {firstcode : Array Nat} (hinv : FirstCodeInv nn cs fs firstcode cs.length) (hsent : firstcode[cs.length + 1]! = codeSentinel) : cs = fs

The code-1 leaf case in the form the induction applies: where the first-path comparison is still live and the first-path store shows the sentinel just above the current level, the two code paths are equal outright.

theorem Hex.GraphIso.Nauty.otherNodePrep_firstCodeInv {n nn : Nat} {cs fs : List Nat} {st : SearchSt n} {code : Nat} (hinv : FirstCodeInv nn cs fs st.firstcode st.eqlevFirst) (hcode : code < codeSentinel) : FirstCodeInv nn (cs ++ [code]) fs (otherNodePrep (cs.length + 1) code st).firstcode (otherNodePrep (cs.length + 1) code st).eqlevFirst

One otherNodePrep step at level cs.length + 1 with fresh code code extends the first-path agreement by one level exactly when the depth had reached the path and the code matches the first path's next code.

theorem Hex.GraphIso.Nauty.recover_firstCodeInv {nn N inf : Nat} {cs fs : List Nat} {st : SearchSt N} {lvl : Nat} (hinv : FirstCodeInv nn cs fs st.firstcode st.eqlevFirst) (hlvl : lvl ≤ cs.length) : FirstCodeInv nn (List.take lvl cs) fs (recover N inf lvl st).firstcode (recover N inf lvl st).eqlevFirst

recover clamps the agreement depth to the unwind level.