def Hex.GraphIso.Nauty.RowsMap {n : Nat} (σ : Renaming n) (g g' : Array (VSet n)) : Prop

g' holds the σ-images of the rows of g.

Equations

• Hex.GraphIso.Nauty.RowsMap σ g g' = (g.size = n ∧ g'.size = n ∧ ∀ (v : Nat), v < n → g'[σ.toFun v]! = Hex.GraphIso.Nauty.VSet.image σ.toFun g[v]!)

def Hex.GraphIso.Nauty.LabOk (lab : Array Nat) (n : Nat) : Prop

Every entry is a vertex.

Equations

• Hex.GraphIso.Nauty.LabOk lab n = ∀ (i : Nat), i < lab.size → lab[i]! < n

theorem Hex.GraphIso.Nauty.getElem!_map_of_lt (f : Nat → Nat) (a : Array Nat) {i : Nat} (hi : i < a.size) : (Array.map f a)[i]! = f a[i]!

theorem Hex.GraphIso.Nauty.map_set! (f : Nat → Nat) (a : Array Nat) (i x : Nat) : Array.map f (a.set! i x) = (Array.map f a).set! i (f x)

theorem Hex.GraphIso.Nauty.labOk_set! {n : Nat} {lab : Array Nat} (h : LabOk lab n) {x : Nat} (hx : x < n) (i : Nat) : LabOk (lab.set! i x) n

def Hex.GraphIso.Nauty.mapResult {n : Nat} (σ : Renaming n) (r : Array Nat × Int × Int) : Array Nat × Int × Int

Map a renaming over a loop result.

Equations

• Hex.GraphIso.Nauty.mapResult σ r = (Array.map σ.toFun r.fst, r.snd.fst, r.snd.snd)

theorem Hex.GraphIso.Nauty.splitCellLoop_map {n : Nat} (σ : Renaming n) {gRow : VSet n} (fuel : Nat) (lab : Array Nat) (c1 c2 : Int) : LabOk lab n → 0 ≤ c1 → c2 < ↑lab.size → splitCellLoop (VSet.image σ.toFun gRow) fuel (Array.map σ.toFun lab) c1 c2 = mapResult σ (splitCellLoop gRow fuel lab c1 c2)

theorem Hex.GraphIso.Nauty.splitCellLoop_ok {n : Nat} {gRow : VSet n} (fuel : Nat) (lab : Array Nat) (c1 c2 : Int) : LabOk lab n → 0 ≤ c1 → c2 < ↑lab.size → (splitCellLoop gRow fuel lab c1 c2).fst.size = lab.size ∧ LabOk (splitCellLoop gRow fuel lab c1 c2).fst n

The final labelling of the two-pointer partition keeps its size and its entries in range.

@[reducible]

def Hex.GraphIso.Nauty.mapSt {n : Nat} (σ : Renaming n) (st : RefineSt n) : RefineSt n

Apply a renaming to the labelling of a refinement state; every position-level field is untouched.

Equations

• Hex.GraphIso.Nauty.mapSt σ st = { lab := Array.map σ.toFun st.lab, ptn := st.ptn, active := st.active, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode }

theorem Hex.GraphIso.Nauty.trivialSplit_mapSt {n : Nat} (σ : Renaming n) (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) : trivialSplit level cell1 cell2 c1 c2 (mapSt σ st) = mapSt σ (trivialSplit level cell1 cell2 c1 c2 st)

The split bookkeeping reads and writes only position-level fields, so it commutes with the labelling transport.

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

The split bookkeeping leaves the labelling untouched.

theorem Hex.GraphIso.Nauty.trivialCell_map {n : Nat} (σ : Renaming n) (level : Nat) {gRow : VSet n} (cell1 cell2 : Nat) (st : RefineSt n) (hlab : LabOk st.lab n) (h2 : cell2 < st.lab.size) : trivialCell level (VSet.image σ.toFun gRow) cell1 cell2 (mapSt σ st) = mapSt σ (trivialCell level gRow cell1 cell2 st)

One trivial-splitter cell commutes with the labelling transport.

theorem Hex.GraphIso.Nauty.trivialCell_ok {n level cell1 cell2 : Nat} {gRow : VSet n} {st : RefineSt n} (hlab : LabOk st.lab n) (h2 : cell2 < st.lab.size) : (trivialCell level gRow cell1 cell2 st).lab.size = st.lab.size ∧ LabOk (trivialCell level gRow cell1 cell2 st).lab n

One trivial-splitter cell keeps the labelling's size and range.

theorem Hex.GraphIso.Nauty.cellEnd_go_lt {ptn : Array Nat} {level : Nat} (hend : ptn[ptn.size - 1]! ≤ level) (fuel j : Nat) : j < ptn.size → ptn.size ≤ fuel + j → cellEnd.go ptn level fuel j < ptn.size

With the partition's final position closed at level, a cell end found from an in-range start stays in range.

theorem Hex.GraphIso.Nauty.cellEnd_lt {ptn : Array Nat} {level i : Nat} (hi : i < ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) : cellEnd ptn level i < ptn.size

theorem Hex.GraphIso.Nauty.cells_go_bound {ptn : Array Nat} {level nn : Nat} (hn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (fuel c1 : Nat) (p : Nat × Nat) : p ∈ cells.go ptn level nn fuel c1 → p.snd < ptn.size

theorem Hex.GraphIso.Nauty.cells_bound {ptn : Array Nat} {level nn : Nat} (hn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (p : Nat × Nat) : p ∈ cells ptn level nn → p.snd < ptn.size

Every cell end of the partition at level is an in-range position.

theorem Hex.GraphIso.Nauty.refineTrivial_go_map {n : Nat} (σ : Renaming n) (level : Nat) {gRow : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : LabOk st.lab n → (∀ (p : Nat × Nat), p ∈ cs → p.snd < st.lab.size) → refineTrivial.go level (VSet.image σ.toFun gRow) cs (mapSt σ st) = mapSt σ (refineTrivial.go level gRow cs st)

theorem Hex.GraphIso.Nauty.refineTrivial_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (level split1 : Nat) (st : RefineSt n) (hlab : LabOk st.lab n) (hsl : st.lab.size = n) (hsp : st.ptn.size = n) (hs1 : split1 < n) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : refineTrivial ctx' level split1 (mapSt σ st) = mapSt σ (refineTrivial ctx level split1 st)

The trivial-splitter pass commutes with the labelling transport: on the renamed graph with the transported labelling it produces the transported state, with all position-level data unchanged.

theorem Hex.GraphIso.Nauty.foldl_insert_map {n : Nat} (σ : Renaming n) (lab : Array Nat) (hlab : LabOk lab n) (lo : Nat) (l : List Nat) (w : VSet n) : (∀ (o : Nat), o ∈ l → lo + o < lab.size) → List.foldl (fun (w : VSet n) (o : Nat) => w.insert (Array.map σ.toFun lab)[lo + o]!) (VSet.image σ.toFun w) l = VSet.image σ.toFun (List.foldl (fun (w : VSet n) (o : Nat) => w.insert lab[lo + o]!) w l)

theorem Hex.GraphIso.Nauty.worksetOf_map {n : Nat} (σ : Renaming n) {lab : Array Nat} (hlab : LabOk lab n) {lo hi : Nat} (hhi : hi < lab.size) : worksetOf n (Array.map σ.toFun lab) lo hi = VSet.image σ.toFun (worksetOf n lab lo hi)

The splitter cell's vertex set transports to its image.

theorem Hex.GraphIso.Nauty.countsOf_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab : Array Nat} (hlab : LabOk lab n) {workset : VSet n} {cell1 cell2 : Nat} (h2 : cell2 < lab.size) : countsOf ctx' (Array.map σ.toFun lab) (VSet.image σ.toFun workset) cell1 cell2 = countsOf ctx lab workset cell1 cell2

The neighbour counts into the splitter set are invariant under a renaming of graph, labelling, and splitter set.

theorem Hex.GraphIso.Nauty.windowStep_mapSt {n : Nat} (σ : Renaming n) (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : windowStep level cell1 cell2 v c1 c2 maxcell (mapSt σ st) = mapSt σ (windowStep level cell1 cell2 v c1 c2 maxcell st)

The window-scan bookkeeping reads and writes only position-level fields, so it commutes with the labelling transport.

theorem Hex.GraphIso.Nauty.lab_windowStep {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : (windowStep level cell1 cell2 v c1 c2 maxcell st).lab = st.lab

theorem Hex.GraphIso.Nauty.windowScan_map {n : Nat} (σ : Renaming n) (level cell1 cell2 : Nat) (counts values : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : windowScan level cell1 cell2 counts values c1 maxcell (mapSt σ st) = mapSt σ (windowScan level cell1 cell2 counts values c1 maxcell st)

theorem Hex.GraphIso.Nauty.lab_windowScan {n : Nat} (level cell1 cell2 : Nat) (counts values : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : (windowScan level cell1 cell2 counts values c1 maxcell st).lab = st.lab

The window scan touches no labelling data.

theorem Hex.GraphIso.Nauty.countsOf_length {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (cell1 cell2 : Nat) : (countsOf ctx lab workset cell1 cell2).length = cell2 + 1 - cell1

theorem Hex.GraphIso.Nauty.segmentOf_map {n : Nat} (σ : Renaming n) {lab : Array Nat} {cell1 : Nat} {counts : List Nat} (hlen : cell1 + counts.length ≤ lab.size) (values : List Nat) : segmentOf (Array.map σ.toFun lab) cell1 counts values = List.map σ.toFun (segmentOf lab cell1 counts values)

theorem Hex.GraphIso.Nauty.segmentOf_mem {n : Nat} {lab : Array Nat} (hlab : LabOk lab n) {cell1 : Nat} {counts : List Nat} (hlen : cell1 + counts.length ≤ lab.size) (values : List Nat) (x : Nat) : x ∈ segmentOf lab cell1 counts values → x < n

Segment entries are labelling entries, hence vertices.

theorem Hex.GraphIso.Nauty.writeSegment_map {n : Nat} (σ : Renaming n) (seg : List Nat) (lab : Array Nat) (c1 : Nat) : writeSegment (Array.map σ.toFun lab) c1 (List.map σ.toFun seg) = Array.map σ.toFun (writeSegment lab c1 seg)

theorem Hex.GraphIso.Nauty.writeSegment_ok {n : Nat} (seg : List Nat) (lab : Array Nat) (c1 : Nat) : LabOk lab n → (∀ (x : Nat), x ∈ seg → x < n) → (writeSegment lab c1 seg).size = lab.size ∧ LabOk (writeSegment lab c1 seg) n

theorem Hex.GraphIso.Nauty.nontrivialFix_mapSt {n : Nat} (σ : Renaming n) (cell1 : Nat) (st : RefineSt n) : nontrivialFix cell1 (mapSt σ st) = mapSt σ (nontrivialFix cell1 st)

The active-set fix reads and writes only position-level fields, so it commutes with the labelling transport.

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

theorem Hex.GraphIso.Nauty.nontrivialCell_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (level : Nat) {workset : VSet n} (cell1 cell2 : Nat) (st : RefineSt n) (hlab : LabOk st.lab n) (h2 : cell2 < st.lab.size) : nontrivialCell ctx' level (VSet.image σ.toFun workset) cell1 cell2 (mapSt σ st) = mapSt σ (nontrivialCell ctx level workset cell1 cell2 st)

One nontrivial-splitter cell commutes with the labelling transport.

theorem Hex.GraphIso.Nauty.nontrivialCell_ok {n : Nat} {ctx : Ctx n} {level cell1 cell2 : Nat} {workset : VSet n} {st : RefineSt n} (hlab : LabOk st.lab n) (h2 : cell2 < st.lab.size) : (nontrivialCell ctx level workset cell1 cell2 st).lab.size = st.lab.size ∧ LabOk (nontrivialCell ctx level workset cell1 cell2 st).lab n

One nontrivial-splitter cell keeps the labelling's size and range.

structure Hex.GraphIso.Nauty.StOk (n level : Nat) (st : RefineSt n) : Prop

The refinement-state invariant threaded through refine: labelling and partition are n-sized, labelling entries and active positions are in range, and the final partition position is closed at level.

• labSize : st.lab.size = n
• labOk : LabOk st.lab n
• ptnSize : st.ptn.size = n
• ptnEnd : st.ptn[st.ptn.size - 1]! ≤ level

theorem Hex.GraphIso.Nauty.ptnEnd_set! {ptn : Array Nat} {level i : Nat} (hend : ptn[ptn.size - 1]! ≤ level) : (ptn.set! i level)[(ptn.set! i level).size - 1]! ≤ level

Setting a partition position to the current level keeps the final position closed at that level.

theorem Hex.GraphIso.Nauty.pickSplit_lt {n : Nat} {active : VSet n} {hint s : Nat} : pickSplit active hint = some s → s < n

A splitter chosen from the active set is a position below n.

theorem Hex.GraphIso.Nauty.trivialSplit_stOk {n level cell1 cell2 : Nat} {c1 c2 : Int} {st : RefineSt n} (h : StOk n level st) : StOk n level (trivialSplit level cell1 cell2 c1 c2 st)

theorem Hex.GraphIso.Nauty.trivialCell_stOk {n level cell1 cell2 : Nat} {gRow : VSet n} {st : RefineSt n} (h : StOk n level st) (h2 : cell2 < n) : StOk n level (trivialCell level gRow cell1 cell2 st)

theorem Hex.GraphIso.Nauty.multOf_cons (x : Nat) (counts : List Nat) (v : Nat) : multOf (x :: counts) v = multOf counts v + if (x == v) = true then 1 else 0

theorem Hex.GraphIso.Nauty.sum_map_add (f g : Nat → Nat) (l : List Nat) : (List.map (fun (v : Nat) => f v + g v) l).sum = (List.map f l).sum + (List.map g l).sum

theorem Hex.GraphIso.Nauty.sum_map_ite_zero {x : Nat} {l : List Nat} : ¬x ∈ l → (List.map (fun (v : Nat) => if (x == v) = true then 1 else 0) l).sum = 0

theorem Hex.GraphIso.Nauty.sum_map_ite_le {x : Nat} {l : List Nat} : l.Nodup → (List.map (fun (v : Nat) => if (x == v) = true then 1 else 0) l).sum ≤ 1

theorem Hex.GraphIso.Nauty.sum_map_zero (l : List Nat) : (List.map (fun (x : Nat) => 0) l).sum = 0

theorem Hex.GraphIso.Nauty.sum_multOf_le {l : List Nat} (hl : l.Nodup) (counts : List Nat) : (List.map (multOf counts) l).sum ≤ counts.length

Over distinct count values, the group multiplicities sum to at most the cell size.

theorem Hex.GraphIso.Nauty.active_windowStep {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : (windowStep level cell1 cell2 v c1 c2 maxcell st).active = st.active ∨ (windowStep level cell1 cell2 v c1 c2 maxcell st).active = st.active.insert c1

theorem Hex.GraphIso.Nauty.ptn_windowStep {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : (windowStep level cell1 cell2 v c1 c2 maxcell st).ptn = st.ptn ∨ (windowStep level cell1 cell2 v c1 c2 maxcell st).ptn = st.ptn.set! (c2 - 1) level

theorem Hex.GraphIso.Nauty.windowStep_stOk {n level cell1 cell2 v c1 c2 : Nat} {maxcell : Int} {st : RefineSt n} (h : StOk n level st) : StOk n level (windowStep level cell1 cell2 v c1 c2 maxcell st)

theorem Hex.GraphIso.Nauty.windowScan_stOk {n level cell1 cell2 : Nat} {counts : List Nat} (hc2 : cell2 < n) (values : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : StOk n level st → c1 + (List.map (multOf counts) values).sum ≤ cell2 + 1 → StOk n level (windowScan level cell1 cell2 counts values c1 maxcell st)

theorem Hex.GraphIso.Nauty.nontrivialFix_stOk {n level cell1 : Nat} {st : RefineSt n} (h : StOk n level st) : StOk n level (nontrivialFix cell1 st)

theorem Hex.GraphIso.Nauty.nodup_range_map_add (b k : Nat) : (List.map (fun (x : Nat) => b + x) (List.range k)).Nodup

theorem Hex.GraphIso.Nauty.nontrivialCell_stOk {n : Nat} {ctx : Ctx n} {level cell1 cell2 : Nat} {workset : VSet n} {st : RefineSt n} (h : StOk n level st) (h2 : cell2 < n) : StOk n level (nontrivialCell ctx level workset cell1 cell2 st)

theorem Hex.GraphIso.Nauty.cellEnd_go_ge {ptn : Array Nat} {level : Nat} (fuel j : Nat) : j ≤ cellEnd.go ptn level fuel j

theorem Hex.GraphIso.Nauty.cellEnd_ge {ptn : Array Nat} {level i : Nat} : i ≤ cellEnd ptn level i

theorem Hex.GraphIso.Nauty.cells_go_le {ptn : Array Nat} {level nn : Nat} (fuel c1 : Nat) (p : Nat × Nat) : p ∈ cells.go ptn level nn fuel c1 → p.fst ≤ p.snd

theorem Hex.GraphIso.Nauty.cells_le {ptn : Array Nat} {level nn : Nat} (p : Nat × Nat) : p ∈ cells ptn level nn → p.fst ≤ p.snd

Every cell of the partition starts no later than it ends.

theorem Hex.GraphIso.Nauty.refineTrivial_go_stOk {n level : Nat} {gRow : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : StOk n level st → (∀ (p : Nat × Nat), p ∈ cs → p.fst < n ∧ p.snd < n) → StOk n level (refineTrivial.go level gRow cs st)

theorem Hex.GraphIso.Nauty.refineTrivial_stOk {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (h : StOk n level st) : StOk n level (refineTrivial ctx level split1 st)

theorem Hex.GraphIso.Nauty.refineNontrivial_go_stOk {n : Nat} {ctx : Ctx n} {level : Nat} {workset : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : StOk n level st → (∀ (p : Nat × Nat), p ∈ cs → p.fst < n ∧ p.snd < n) → StOk n level (refineNontrivial.go ctx level workset cs st)

theorem Hex.GraphIso.Nauty.refineNontrivial_stOk {n : Nat} {ctx : Ctx n} {level split1 split2 : Nat} {st : RefineSt n} (h : StOk n level st) : StOk n level (refineNontrivial ctx level split1 split2 st)

theorem Hex.GraphIso.Nauty.refineNontrivial_go_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (level : Nat) {workset : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : LabOk st.lab n → (∀ (p : Nat × Nat), p ∈ cs → p.snd < st.lab.size) → refineNontrivial.go ctx' level (VSet.image σ.toFun workset) cs (mapSt σ st) = mapSt σ (refineNontrivial.go ctx level workset cs st)

theorem Hex.GraphIso.Nauty.refineNontrivial_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (level split1 split2 : Nat) (st : RefineSt n) (h : StOk n level st) (hs2 : split2 < n) : refineNontrivial ctx' level split1 split2 (mapSt σ st) = mapSt σ (refineNontrivial ctx level split1 split2 st)

The nontrivial-splitter pass commutes with the labelling transport.

theorem Hex.GraphIso.Nauty.refineStep_stOk {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (h : StOk n level st) : StOk n level (refineStep ctx level split1 st)

theorem Hex.GraphIso.Nauty.refineStep_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (level split1 : Nat) (st : RefineSt n) (h : StOk n level st) (hs1 : split1 < n) : refineStep ctx' level split1 (mapSt σ st) = mapSt σ (refineStep ctx level split1 st)

One active-cell iteration commutes with the labelling transport.

theorem Hex.GraphIso.Nauty.refineLoop_stOk {n : Nat} {ctx : Ctx n} {level : Nat} (fuel : Nat) (st : RefineSt n) : StOk n level st → StOk n level (refineLoop ctx level fuel st)

theorem Hex.GraphIso.Nauty.refineLoop_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (level fuel : Nat) (st : RefineSt n) : StOk n level st → refineLoop ctx' level fuel (mapSt σ st) = mapSt σ (refineLoop ctx level fuel st)

The active-cell loop commutes with the labelling transport.

theorem Hex.GraphIso.Nauty.refine_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (hsl : lab.size = n) (hlab : LabOk lab n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : refine ctx' level (Array.map σ.toFun lab) ptn active numcells = mapSt σ (refine ctx level lab ptn active numcells)

nauty's refine commutes with a vertex renaming: on the renamed graph with the transported labelling it produces the transported state, with identical partition, active set, cell structure, and refinement code.

theorem Hex.GraphIso.Nauty.bestcellRow_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab startArr : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hstart : ∀ (v : Nat), startArr[v]! < n) {workset : VSet n} (v2 : Nat) (vs : List Nat) (bucket : Array Nat) : bestcellRow ctx' (Array.map σ.toFun lab) startArr (VSet.image σ.toFun workset) v2 vs bucket = bestcellRow ctx lab startArr workset v2 vs bucket

theorem Hex.GraphIso.Nauty.bestcellRows_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} {level : Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) {startArr : Array Nat} (hstart : ∀ (v : Nat), startArr[v]! < n) (vs : List Nat) (bucket : Array Nat) : bestcellRows ctx' (Array.map σ.toFun lab) ptn level startArr vs bucket = bestcellRows ctx lab ptn level startArr vs bucket

theorem Hex.GraphIso.Nauty.getElem!_list_lt {l : List Nat} {m : Nat} (hml : ∀ (x : Nat), x ∈ l → x < m) (hm0 : 0 < m) (v : Nat) : l.toArray[v]! < m

theorem Hex.GraphIso.Nauty.bestcell_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) {level : Nat} (hend : ptn[ptn.size - 1]! ≤ level) : bestcell ctx' (Array.map σ.toFun lab) ptn level = bestcell ctx lab ptn level

nauty's bestcell is position-valued and invariant under a renaming.

theorem Hex.GraphIso.Nauty.targetcell_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) {level tcLevel : Nat} {hint : Int} (hend : ptn[ptn.size - 1]! ≤ level) : targetcell ctx' (Array.map σ.toFun lab) ptn level tcLevel hint = targetcell ctx lab ptn level tcLevel hint

nauty's targetcell is position-valued and invariant under a renaming.

theorem Hex.GraphIso.Nauty.maketargetcell_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) {level tcLevel : Nat} {hint : Int} (hend : ptn[ptn.size - 1]! ≤ level) (hi : targetcell ctx lab ptn level tcLevel hint + 1 < n) : maketargetcell ctx' (Array.map σ.toFun lab) ptn level tcLevel hint = ((maketargetcell ctx lab ptn level tcLevel hint).fst, VSet.image σ.toFun (maketargetcell ctx lab ptn level tcLevel hint).snd.fst, (maketargetcell ctx lab ptn level tcLevel hint).snd.snd)

nauty's maketargetcell transports position and size unchanged and the target-cell set to its image.

theorem Hex.GraphIso.Nauty.breakout_go_map {n : Nat} (σ : Renaming n) {tv : Nat} (fuel : Nat) (lab : Array Nat) (i prev : Nat) : LabOk lab n → prev < n → (∃ (k : Nat), i ≤ k ∧ k < lab.size ∧ lab[k]! = tv) → breakout.go (σ.toFun tv) fuel (Array.map σ.toFun lab) i (σ.toFun prev) = Array.map σ.toFun (breakout.go tv fuel lab i prev)

theorem Hex.GraphIso.Nauty.breakout_map {n : Nat} (σ : Renaming n) {lab ptn : Array Nat} {level tc tv : Nat} (hlab : LabOk lab n) (hwit : ∃ (k : Nat), tc ≤ k ∧ k < lab.size ∧ lab[k]! = tv) : breakout n (Array.map σ.toFun lab) ptn level tc (σ.toFun tv) = (Array.map σ.toFun (breakout n lab ptn level tc tv).fst, (breakout n lab ptn level tc tv).snd.fst, (breakout n lab ptn level tc tv).snd.snd)

nauty's breakout commutes with a renaming: the labelling maps through, the partition and active set are position-level.

theorem Hex.GraphIso.Nauty.getElem!_replicate_zero (sz i : Nat) : (Array.replicate sz 0)[i]! = 0

theorem Hex.GraphIso.Nauty.invPerm_go_map {n : Nat} (σ : Renaming n) {lab : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (is : List Nat) (inv inv' : Array Nat) : inv'.size = n → inv.size = n → (∀ (v : Nat), v < n → inv'[σ.toFun v]! = inv[v]!) → (∀ (i : Nat), i ∈ is → i < lab.size) → ∀ (v : Nat), v < n → (invPerm.go (Array.map σ.toFun lab) is inv')[σ.toFun v]! = (invPerm.go lab is inv)[v]!

theorem Hex.GraphIso.Nauty.invPerm_map {n : Nat} (σ : Renaming n) {lab : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (v : Nat) : v < n → (invPerm (Array.map σ.toFun lab))[σ.toFun v]! = (invPerm lab)[v]!

The labelling inverse transports along a renaming.

theorem Hex.GraphIso.Nauty.permset_image {n : Nat} (σ : Renaming n) (s : VSet n) {perm perm' : Array Nat} (hp : ∀ (v : Nat), v < n → perm'[σ.toFun v]! = perm[v]!) : (VSet.image σ.toFun s).permset perm' = s.permset perm

permset of an image under the transported map recovers permset of the original set.

def Hex.GraphIso.Nauty.leafRows {n : Nat} (ctx : Ctx n) (lab : Array Nat) : List (VSet n)

The leaf key rows: g^lab in nauty's row order.

Equations

• Hex.GraphIso.Nauty.leafRows ctx lab = List.map (fun (i : Nat) => ctx.g[lab[i]!]!.permset (Hex.GraphIso.Nauty.invPerm lab)) (List.range n)

theorem Hex.GraphIso.Nauty.leafRows_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) : leafRows ctx' (Array.map σ.toFun lab) = leafRows ctx lab

The leaf key is invariant under a renaming: the transported labelling on the renamed graph induces the same adjacency rows.

theorem Hex.GraphIso.Nauty.refine_stOk {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} {active : VSet n} {numcells : Nat} (hsl : lab.size = n) (hlab : LabOk lab n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) : StOk n level (refine ctx level lab ptn active numcells)

theorem Hex.GraphIso.Nauty.argmaxLoop_lt {bucket : Array Nat} {bound : Nat} (is : List Nat) (v1 v2 : Nat) : v1 < bound → (∀ (i : Nat), i ∈ is → i < bound) → argmaxLoop bucket is v1 v2 < bound

theorem Hex.GraphIso.Nauty.argmax_start_mem {L : List Nat} (hlen : L.length ≠ 0) (B : Array Nat) (v2 : Nat) (is : List Nat) (his : ∀ (i : Nat), i ∈ is → i < L.length) : L.toArray[argmaxLoop B is 0 v2]! ∈ L

theorem Hex.GraphIso.Nauty.bestcell_mem {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hex : List.filter (fun (x : Nat × Nat) => match x with | (c1, c2) => decide (c1 ≠ c2)) (cells ptn level n) ≠ []) : bestcell ctx lab ptn level ∈ List.map (fun (x : Nat × Nat) => x.fst) (List.filter (fun (x : Nat × Nat) => match x with | (c1, c2) => decide (c1 ≠ c2)) (cells ptn level n))

With a nonsingleton cell present, bestcell returns one of the nonsingleton cell starts.

theorem Hex.GraphIso.Nauty.targetcell_nontrivial {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level tcLevel : Nat} (hex : ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ p.fst ≠ p.snd) : ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ p.fst ≠ p.snd ∧ targetcell ctx lab ptn level tcLevel (-1) = p.fst

With a nonsingleton cell present, the hint-free targetcell returns a nonsingleton cell start.

theorem Hex.GraphIso.Nauty.breakout_go_ok {n tv : Nat} (hn0 : 0 < n) (fuel : Nat) (lab : Array Nat) (i prev : Nat) : LabOk lab n → prev < n → (breakout.go tv fuel lab i prev).size = lab.size ∧ LabOk (breakout.go tv fuel lab i prev) n

theorem Hex.GraphIso.Nauty.breakout_ok {n : Nat} {lab ptn : Array Nat} {level tc tv : Nat} (hlab : LabOk lab n) (hn0 : 0 < n) (htv : tv < n) : (breakout n lab ptn level tc tv).fst.size = lab.size ∧ LabOk (breakout n lab ptn level tc tv).fst n