theorem Hex.GraphIso.Nauty.cellEnd_go_le {ptn : Array Nat} {level j : Nat} (hj : ptn[j]! ≤ level) (fuel i : Nat) : i ≤ j → j < i + fuel → cellEnd.go ptn level fuel i ≤ j

theorem Hex.GraphIso.Nauty.cellEnd_le {ptn : Array Nat} {level i j : Nat} (hij : i ≤ j) (hj : ptn[j]! ≤ level) (hjs : j < ptn.size) : cellEnd ptn level i ≤ j

theorem Hex.GraphIso.Nauty.segN_perm_tiled {ptnF : Array Nat} {levF : Nat} {lab1 lab2 : Array Nat} (hfine : cellsPerm ptnF levF lab1 lab2) (hendF : ptnF[ptnF.size - 1]! ≤ levF) (len a : Nat) : 0 < len → a + len ≤ ptnF.size → a = 0 ∨ ptnF[a - 1]! ≤ levF → ptnF[a + len - 1]! ≤ levF → (segN lab1 a len).Perm (segN lab2 a len)

Segments between fine boundaries split into fine cells, so cell-contents equivalence transfers to any coarser span.

theorem Hex.GraphIso.Nauty.cellsPerm_coarsen {ptnC ptnF : Array Nat} {levC levF : Nat} {lab1 lab2 : Array Nat} (hszp : ptnC.size = ptnF.size) (hs1 : lab1.size = ptnF.size) (hs2 : lab2.size = ptnF.size) (hfine : cellsPerm ptnF levF lab1 lab2) (hendF : ptnF[ptnF.size - 1]! ≤ levF) (hendC : ptnC[ptnC.size - 1]! ≤ levC) (hb : ∀ (q : Nat), ptnC[q]! ≤ levC → ptnF[q]! ≤ levF) : cellsPerm ptnC levC lab1 lab2

Cell-contents equivalence transfers from a finer partition (more boundaries, possibly at a later level) to a coarser one.

theorem Hex.GraphIso.Nauty.cellsPerm_of_confined {ptn : Array Nat} {level : Nat} {lab lab' : Array Nat} {A lenA c lenC : Nat} (hc : IsCell ptn level c lenC) (hcA : c ≤ A) (hAc : A + lenA ≤ c + lenC) (hperm : (segN lab A lenA).Perm (segN lab' A lenA)) (hout : ∀ (q : Nat), q < A ∨ A + lenA ≤ q → lab'[q]! = lab[q]!) : cellsPerm ptn level lab lab'

A labelling rewrite confined to a span of one cell, permuting its contents, preserves every cell's contents.

theorem Hex.GraphIso.Nauty.cellsPerm_refl (ptn : Array Nat) (level : Nat) (lab : Array Nat) : cellsPerm ptn level lab lab

theorem Hex.GraphIso.Nauty.cellsPerm_trans {ptn : Array Nat} {level : Nat} {lab1 lab2 lab3 : Array Nat} (h1 : cellsPerm ptn level lab1 lab2) (h2 : cellsPerm ptn level lab2 lab3) : cellsPerm ptn level lab1 lab3

structure Hex.GraphIso.Nauty.RefInv {n : Nat} (level : Nat) (lab0 ptn0 : Array Nat) (st : RefineSt n) : Prop

The state facts carried through refine relative to its input.

• labSize : st.lab.size = lab0.size
• ptnSize : st.ptn.size = ptn0.size
• grow (q : Nat) : ptn0[q]! ≤ level → st.ptn[q]! ≤ level
• perm : cellsPerm ptn0 level lab0 st.lab

theorem Hex.GraphIso.Nauty.RefInv.init {n : Nat} (level : Nat) (lab0 ptn0 : Array Nat) (active : VSet n) (numcells : Nat) : RefInv level lab0 ptn0 { lab := lab0, ptn := ptn0, active := active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }

theorem Hex.GraphIso.Nauty.RefInv.step {n level : Nat} {lab0 ptn0 : Array Nat} {st st' : RefineSt n} (h : RefInv level lab0 ptn0 st) (hls : st'.lab.size = st.lab.size) (hps : st'.ptn.size = st.ptn.size) (hpv : ∀ (q : Nat), st'.ptn[q]! = st.ptn[q]! ∨ st'.ptn[q]! = level) (hlab : cellsPerm ptn0 level st.lab st'.lab) : RefInv level lab0 ptn0 st'

theorem Hex.GraphIso.Nauty.subcell_of_grow {ptn0 ptnP : Array Nat} {level A lenA : Nat} (_hszp : ptn0.size = ptnP.size) (hcellP : IsCell ptnP level A lenA) (hend0 : ptn0[ptn0.size - 1]! ≤ level) (hb : ∀ (q : Nat), ptn0[q]! ≤ level → ptnP[q]! ≤ level) (hA0 : A < ptn0.size) (_hA : A + lenA ≤ ptn0.size) : ∃ (c : Nat), ∃ (lenC : Nat), IsCell ptn0 level c lenC ∧ c ≤ A ∧ A + lenA ≤ c + lenC

A cell of a boundary-richer partition sits inside a cell of the original.

theorem Hex.GraphIso.Nauty.splitCellLoop_region_perm {n : Nat} {gRow : VSet n} {lab : Array Nat} {cell1 cell2 : Nat} (h12 : cell1 ≤ cell2) (hsz : cell2 < lab.size) : (segN (splitCellLoop gRow (cell2 - cell1 + 2) lab (Int.ofNat cell1) (Int.ofNat cell2)).fst cell1 (cell2 + 1 - cell1)).Perm (segN lab cell1 (cell2 + 1 - cell1))

theorem Hex.GraphIso.Nauty.trivialSplit_lab {n : Nat} (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) : (trivialSplit level cell1 cell2 c1 c2 st).lab = st.lab

theorem Hex.GraphIso.Nauty.trivialSplit_ptn {n : Nat} (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) : (trivialSplit level cell1 cell2 c1 c2 st).ptn = st.ptn ∨ (trivialSplit level cell1 cell2 c1 c2 st).ptn = st.ptn.set! c2.toNat level

theorem Hex.GraphIso.Nauty.refInv_trivialCell {n level cell1 cell2 : Nat} {gRow : VSet n} {lab0 ptn0 : Array Nat} {st : RefineSt n} (hinv : RefInv level lab0 ptn0 st) {c lenC : Nat} (hc : IsCell ptn0 level c lenC) (hcA : c ≤ cell1) (hAc : cell2 + 1 ≤ c + lenC) (h12 : cell1 ≤ cell2) (hsz : cell2 < st.lab.size) : RefInv level lab0 ptn0 (trivialCell level gRow cell1 cell2 st)

theorem Hex.GraphIso.Nauty.mem_countValues {counts : List Nat} {v : Nat} (hlo : List.foldl Nat.min (counts.headD 0) counts ≤ v) (hhi : v ≤ List.foldl Nat.max (counts.headD 0) counts) : v ∈ countValues counts

theorem Hex.GraphIso.Nauty.segmentOf_perm {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) (_hsz : cell2 < lab.size) (_h12 : cell1 ≤ cell2) : (segmentOf lab cell1 (countsOf ctx lab workset cell1 cell2) (countValues (countsOf ctx lab workset cell1 cell2))).Perm (segN lab cell1 (cell2 + 1 - cell1))

theorem Hex.GraphIso.Nauty.nontrivialFix_lab {n : Nat} (cell1 : Nat) (st : RefineSt n) : (nontrivialFix cell1 st).lab = st.lab

theorem Hex.GraphIso.Nauty.nontrivialFix_ptn {n : Nat} (cell1 : Nat) (st : RefineSt n) : (nontrivialFix cell1 st).ptn = st.ptn

theorem Hex.GraphIso.Nauty.refInv_nontrivialCell {n : Nat} {ctx : Ctx n} {level cell1 cell2 : Nat} {workset : VSet n} {lab0 ptn0 : Array Nat} {st : RefineSt n} (hinv : RefInv level lab0 ptn0 st) {c lenC : Nat} (hc : IsCell ptn0 level c lenC) (hcA : c ≤ cell1) (hAc : cell2 + 1 ≤ c + lenC) (h12 : cell1 ≤ cell2) (hsz : cell2 < st.lab.size) : RefInv level lab0 ptn0 (nontrivialCell ctx level workset cell1 cell2 st)

theorem Hex.GraphIso.Nauty.refInv_cells_facts {n level : Nat} {lab0 ptn0 : Array Nat} {st : RefineSt n} (hinv : RefInv level lab0 ptn0 st) (hnn : n ≤ ptn0.size) (hs : lab0.size = ptn0.size) (hend0 : ptn0[ptn0.size - 1]! ≤ level) (p : Nat × Nat) : p ∈ cells st.ptn level n → p.fst ≤ p.snd ∧ p.snd < lab0.size ∧ ∃ (c : Nat), ∃ (lenC : Nat), IsCell ptn0 level c lenC ∧ c ≤ p.fst ∧ p.snd + 1 ≤ c + lenC

theorem Hex.GraphIso.Nauty.refInv_refineTrivial_go {n level : Nat} {gRow : VSet n} {lab0 ptn0 : Array Nat} (l : List (Nat × Nat)) (st : RefineSt n) : RefInv level lab0 ptn0 st → (∀ (p : Nat × Nat), p ∈ l → p.fst ≤ p.snd ∧ p.snd < lab0.size ∧ ∃ (c : Nat), ∃ (lenC : Nat), IsCell ptn0 level c lenC ∧ c ≤ p.fst ∧ p.snd + 1 ≤ c + lenC) → RefInv level lab0 ptn0 (refineTrivial.go level gRow l st)

theorem Hex.GraphIso.Nauty.refInv_refineNontrivial_go {n : Nat} {ctx : Ctx n} {level : Nat} {workset : VSet n} {lab0 ptn0 : Array Nat} (l : List (Nat × Nat)) (st : RefineSt n) : RefInv level lab0 ptn0 st → (∀ (p : Nat × Nat), p ∈ l → p.fst ≤ p.snd ∧ p.snd < lab0.size ∧ ∃ (c : Nat), ∃ (lenC : Nat), IsCell ptn0 level c lenC ∧ c ≤ p.fst ∧ p.snd + 1 ≤ c + lenC) → RefInv level lab0 ptn0 (refineNontrivial.go ctx level workset l st)

theorem Hex.GraphIso.Nauty.refInv_record {n level : Nat} {lab0 ptn0 : Array Nat} {st st' : RefineSt n} (hinv : RefInv level lab0 ptn0 st) (hl : st'.lab = st.lab) (hp : st'.ptn = st.ptn) : RefInv level lab0 ptn0 st'

theorem Hex.GraphIso.Nauty.refInv_refineStep {n : Nat} {ctx : Ctx n} {level split1 : Nat} {lab0 ptn0 : Array Nat} {st : RefineSt n} (hinv : RefInv level lab0 ptn0 st) (hnn : n ≤ ptn0.size) (hs : lab0.size = ptn0.size) (hend0 : ptn0[ptn0.size - 1]! ≤ level) : RefInv level lab0 ptn0 (refineStep ctx level split1 st)

theorem Hex.GraphIso.Nauty.refInv_refineLoop {n : Nat} {ctx : Ctx n} {level : Nat} {lab0 ptn0 : Array Nat} (hnn : n ≤ ptn0.size) (hs : lab0.size = ptn0.size) (hend0 : ptn0[ptn0.size - 1]! ≤ level) (fuel : Nat) (st : RefineSt n) : RefInv level lab0 ptn0 st → RefInv level lab0 ptn0 (refineLoop ctx level fuel st)

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

refine preserves labelling size and every input cell's contents, and only adds partition boundaries.

def Hex.GraphIso.Nauty.bcount (ptn : Array Nat) (level nn : Nat) : Nat

The number of positions carrying a boundary at level.

Equations

• Hex.GraphIso.Nauty.bcount ptn level nn = List.countP (fun (q : Nat) => decide (ptn[q]! ≤ level)) (List.range nn)

theorem Hex.GraphIso.Nauty.bcount_le (ptn : Array Nat) (level nn : Nat) : bcount ptn level nn ≤ nn

theorem Hex.GraphIso.Nauty.bcount_mono {ptn ptn' : Array Nat} {level level' nn : Nat} (h : ∀ (q : Nat), ptn[q]! ≤ level → ptn'[q]! ≤ level') : bcount ptn level nn ≤ bcount ptn' level' nn

theorem Hex.GraphIso.Nauty.countP_succ_le {p p' : Nat → Bool} (l : List Nat) : l.Nodup → (∀ (x : Nat), x ∈ l → p x = true → p' x = true) → ∀ (x0 : Nat), x0 ∈ l → p x0 = false → p' x0 = true → List.countP p l + 1 ≤ List.countP p' l

theorem Hex.GraphIso.Nauty.bcount_breakout {n : Nat} {ptn : Array Nat} {level tc nn : Nat} (_hvals : ∀ (q : Nat), ptn[q]! ≤ level ∨ ptn[q]! = n + 2) (_hlev : level + 1 < n + 2) (htc : ptn[tc]! > level) (htcn : tc < nn) (htcs : tc < ptn.size) : bcount ptn level nn + 1 ≤ bcount (ptn.set! tc (level + 1)) (level + 1) nn

Individualizing one vertex of a nontrivial cell adds a boundary.

theorem Hex.GraphIso.Nauty.bcount_pos_of_boundary {ptn : Array Nat} {level nn q : Nat} (hq : q < nn) (hv : ptn[q]! ≤ level) : 1 ≤ bcount ptn level nn

theorem Hex.GraphIso.Nauty.specNode_achieved {n : Nat} {ctx : Ctx n} (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : NodeOk n level lab ptn active → n + 1 ≤ level + fuel → level ≤ bcount ptn level n → ∃ (llab : Array Nat), llab.size = n ∧ cellsPerm ptn level lab llab ∧ (specNode ctx tcLevel fuel level lab ptn active numcells).rows = leafRows ctx llab

The key of a node has the leaf rows of a labelling that fills every cell of this node's partition with the same vertices.

theorem Hex.GraphIso.Nauty.segN_eq_toList {arr : Array Nat} {m : Nat} (hsz : arr.size = m) : segN arr 0 m = arr.toList

theorem Hex.GraphIso.Nauty.endsOf_append (l1 l2 : List (List Nat)) (s : Nat) : endsOf (l1 ++ l2) s = endsOf l1 s ++ endsOf l2 (s + totalOf l1)

theorem Hex.GraphIso.Nauty.pos_in_class (cls : List (List Nat)) (i : Nat) : i < totalOf cls → ∃ (pre : List (List Nat)), ∃ (cl : List Nat), ∃ (suf : List (List Nat)), cls = pre ++ cl :: suf ∧ totalOf pre ≤ i ∧ i < totalOf pre + cl.length

theorem Hex.GraphIso.Nauty.getElem!_append_block {l1 mid l2 : List Nat} {off : Nat} (hoff : off < mid.length) : (l1 ++ (mid ++ l2))[l1.length + off]! = mid[off]!

theorem Hex.GraphIso.Nauty.sortedColorSeq_at {n k : Nat} (G : Colored n k) {c : Nat} (hc : c < k) {off : Nat} (hoff : off < (colorClass G c).length) : (sortedColorSeq G)[totalOf (List.take c (List.map (colorClass G) (List.range k))) + off]! = c

Within its block, the sorted colour sequence is constant.

theorem Hex.GraphIso.Nauty.totalOf_append (l1 l2 : List (List Nat)) : totalOf (l1 ++ l2) = totalOf l1 + totalOf l2

theorem Hex.GraphIso.Nauty.interval_isCell {n k : Nat} (G : Colored n k) {pre suf : List (List Nat)} {cl : List Nat} (hsplit : List.map (colorClass G) (List.range k) = pre ++ cl :: suf) (hne : 0 < cl.length) : IsCell (initPtn n (n + 2) (initialPartition G).snd) 1 (totalOf pre) cl.length

Each nonempty class occupies one cell of the initial partition.

theorem Hex.GraphIso.Nauty.achieved_position_colors {n k : Nat} {G : Colored n k} {llab : Array Nat} (hcp : cellsPerm (initPtn n (n + 2) (initialPartition G).snd) 1 (initialPartition G).fst llab) (i : Nat) : i < n → ∃ (hv : llab[i]! < n), ↑G.coloring.cells[⟨llab[i]!, hv⟩] = (sortedColorSeq G)[i]!

Positions of any labelling that fills the initial cells with the initial contents carry the sorted colours.

theorem Hex.GraphIso.Nauty.achieved_perm_range {n k : Nat} {G : Colored n k} {llab : Array Nat} (hsz : llab.size = n) (hn0 : 0 < n) (hcp : cellsPerm (initPtn n (n + 2) (initialPartition G).snd) 1 (initialPartition G).fst llab) : llab.toList.Perm (List.range n)

theorem Hex.GraphIso.Nauty.label_of_perm_range {n : Nat} {llab : Array Nat} (hsz : llab.size = n) (hperm : llab.toList.Perm (List.range n)) : ∃ (l : Label n), ∀ (i : Nat) (hi : i < n), ↑(l.get ⟨i, hi⟩) = llab[i]!

theorem Hex.GraphIso.Nauty.form_eq_formOfKey {n k : Nat} {G F : Colored n k} {rows : List (VSet n)} (hrows : rowsOf F = rows.toArray) (hcols : ∀ (i : Nat) (hi : i < n), ↑F.coloring.cells[i] = (sortedColorSeq G)[i]!) : F = formOfKey G rows

A form with a key's rows and the sorted colours is the form of that key.

theorem Hex.GraphIso.Nauty.specCanon_iso {n k : Nat} (G : Colored n k) : Isomorphic G (specCanon G)

The total nauty-semantic canonical form is isomorphic to its input.

theorem Hex.GraphIso.Nauty.iso_iff_specCanon_eq {n k : Nat} {G H : Colored n k} : Isomorphic G H ↔ specCanon G = specCanon H

Isomorphism is equivalent to equality of the nauty-semantic canonical forms.