theorem Hex.GraphIso.Nauty.windowStep_setLab {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) (X : Array Nat) : windowStep level cell1 cell2 v c1 c2 maxcell { lab := X, ptn := st.ptn, active := st.active, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode } = have __src := windowStep level cell1 cell2 v c1 c2 maxcell st; { lab := X, ptn := __src.ptn, active := __src.active, numcells := __src.numcells, hint := __src.hint, maxpos := __src.maxpos, longcode := __src.longcode }

The window-scan bookkeeping never reads the labelling.

theorem Hex.GraphIso.Nauty.windowScan_setLab {n : Nat} (level cell1 cell2 : Nat) (counts values : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) (X : Array Nat) : windowScan level cell1 cell2 counts values c1 maxcell { lab := X, ptn := st.ptn, active := st.active, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode } = have __src := windowScan level cell1 cell2 counts values c1 maxcell st; { lab := X, ptn := __src.ptn, active := __src.active, numcells := __src.numcells, hint := __src.hint, maxpos := __src.maxpos, longcode := __src.longcode }

theorem Hex.GraphIso.Nauty.windowScan_counts_congr {n : Nat} (level cell1 cell2 : Nat) {counts counts' : List Nat} (hm : ∀ (v : Nat), multOf counts v = multOf counts' v) (values : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : windowScan level cell1 cell2 counts values c1 maxcell st = windowScan level cell1 cell2 counts' values c1 maxcell st

The window scan reads the counts only through the multiplicities.

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

One window step's partition effect: the group end boundary, if it lies inside the cell.

theorem Hex.GraphIso.Nauty.segN_writeSegment (seg : List Nat) (lab : Array Nat) (lo : Nat) : lo + seg.length ≤ lab.size → segN (writeSegment lab lo seg) lo seg.length = seg

Writing a segment and reading it back.

theorem Hex.GraphIso.Nauty.isCell_split_right {ptn : Array Nat} {level A lenA c : Nat} (h : IsCell ptn level A lenA) (hc1 : A ≤ c) (hc2 : c + 1 < A + lenA) (hcs : c < ptn.size) : IsCell (ptn.set! c level) level (c + 1) (A + lenA - (c + 1))

theorem Hex.GraphIso.Nauty.flatMap_congr_mem {g g' : Nat → List Nat} (l : List Nat) : (∀ (a : Nat), a ∈ l → g a = g' a) → List.flatMap g l = List.flatMap g' l

theorem Hex.GraphIso.Nauty.flatMap_perm_of_pointwise {g g' : Nat → List Nat} (vs : List Nat) : (∀ (v : Nat), v ∈ vs → (g v).Perm (g' v)) → (List.flatMap g vs).Perm (List.flatMap g' vs)

theorem Hex.GraphIso.Nauty.zipIdx_filter_map_eq_filter (f : Nat → Nat) (v : Nat) (S : List Nat) (k : Nat) (get : Nat → Nat) : (∀ (j : Nat), j < S.length → get (k + j) = S[j]!) → List.map (fun (p : Nat × Nat) => get p.snd) (List.filter (fun (p : Nat × Nat) => p.fst == v) ((List.map f S).zipIdx k)) = List.filter (fun (x : Nat) => f x == v) S

theorem Hex.GraphIso.Nauty.segmentOf_eq_flatMap (lab : Array Nat) (cell1 : Nat) (S : List Nat) (f : Nat → Nat) (values : List Nat) (hS : ∀ (j : Nat), j < S.length → lab[cell1 + j]! = S[j]!) : segmentOf lab cell1 (List.map f S) values = List.flatMap (fun (v : Nat) => List.filter (fun (x : Nat) => f x == v) S) values

The stable counting redistribution groups the segment by count value: with counts read off the segment, segmentOf is the concatenation of the value filters.

theorem Hex.GraphIso.Nauty.segN_getElem! (lab : Array Nat) (lo len j : Nat) (hj : j < len) : (segN lab lo len)[j]! = lab[lo + j]!

theorem Hex.GraphIso.Nauty.filter_filter_ne {f : Nat → Nat} {u v : Nat} (huv : u ≠ v) (S : List Nat) : List.filter (fun (x : Nat) => f x == u) (List.filter (fun (x : Nat) => !f x == v) S) = List.filter (fun (x : Nat) => f x == u) S

theorem Hex.GraphIso.Nauty.flatMap_filters_perm {f : Nat → Nat} (values S : List Nat) : values.Nodup → (∀ (x : Nat), x ∈ S → f x ∈ values) → (List.flatMap (fun (v : Nat) => List.filter (fun (x : Nat) => f x == v) S) values).Perm S

Concatenating the value-filters over distinct values that cover the list recovers the list, as a multiset.

theorem Hex.GraphIso.Nauty.ptn_windowScan_outside {n : Nat} (level cell1 cell2 : Nat) (counts vs : List Nat) (c1acc : Nat) (maxcell : Int) (st : RefineSt n) : cell1 ≤ c1acc → ∀ (q : Nat), q < cell1 ∨ cell2 ≤ q → (windowScan level cell1 cell2 counts vs c1acc maxcell st).ptn[q]! = st.ptn[q]!

theorem Hex.GraphIso.Nauty.ptn_windowScan_size {n : Nat} (level cell1 cell2 : Nat) (counts vs : List Nat) (c1acc : Nat) (maxcell : Int) (st : RefineSt n) : (windowScan level cell1 cell2 counts vs c1acc maxcell st).ptn.size = st.ptn.size

theorem Hex.GraphIso.Nauty.windowScan_region_perm {n : Nat} (level cell1 cell2 : Nat) (counts : List Nat) {L L' : Array Nat} (gL gL' : Nat → List Nat) (hGperm : ∀ (v : Nat), (gL v).Perm (gL' v)) (hGlen : ∀ (v : Nat), (gL v).length = multOf counts v) (vs : List Nat) (start : Nat) (maxcell : Int) (st : RefineSt n) : (start ≤ cell2 → IsCell st.ptn level start (cell2 + 1 - start)) → cell2 < st.ptn.size → cellsPerm st.ptn level L L' → segN L start (cell2 + 1 - start) = List.flatMap gL vs → segN L' start (cell2 + 1 - start) = List.flatMap gL' vs → cellsPerm (windowScan level cell1 cell2 counts vs start maxcell st).ptn level L L'

The window scan's boundary writes preserve cell-contents equivalence of the final labellings: each nonempty group becomes a cell whose two contents are permutations of matching value filters.

theorem Hex.GraphIso.Nauty.nontrivialFix_setLab {n : Nat} (cell1 : Nat) (st : RefineSt n) (X : Array Nat) : nontrivialFix cell1 { lab := X, ptn := st.ptn, active := st.active, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode } = have __src := nontrivialFix cell1 st; { lab := X, ptn := __src.ptn, active := __src.active, numcells := __src.numcells, hint := __src.hint, maxpos := __src.maxpos, longcode := __src.longcode }

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

theorem Hex.GraphIso.Nauty.nontrivialCell_perm {n : Nat} {ctx : Ctx n} {level cell1 cell2 : Nat} {workset : VSet n} {st st' : RefineSt n} (h : StPerm level st st') (hcell : IsCell st.ptn level cell1 (cell2 + 1 - cell1)) (hc12 : cell1 ≤ cell2) (h2 : cell2 < st.lab.size) (hsz : st.ptn.size = st.lab.size) : StPerm level (nontrivialCell ctx level workset cell1 cell2 st) (nontrivialCell ctx level workset cell1 cell2 st') ∧ (∀ (q : Nat), q < cell1 ∨ cell2 ≤ q → (nontrivialCell ctx level workset cell1 cell2 st).ptn[q]! = st.ptn[q]!) ∧ (nontrivialCell ctx level workset cell1 cell2 st).ptn.size = st.ptn.size ∧ (nontrivialCell ctx level workset cell1 cell2 st).lab.size = st.lab.size

One nontrivial-splitter cell preserves cell-contents equivalence: the positional results agree and the labellings stay cell-equivalent for the result's partition, which changes only strictly inside the processed cell.

def Hex.GraphIso.Nauty.StartsOk {n : Nat} (level : Nat) (st : RefineSt n) : Prop

Every active position starts a cell of the partition at level.

Equations

• Hex.GraphIso.Nauty.StartsOk level st = ∀ (v : Nat), st.active.mem v = true → v = 0 ∨ st.ptn[v - 1]! ≤ level

theorem Hex.GraphIso.Nauty.getElem!_set!_cases (a : Array Nat) (i x q : Nat) : (a.set! i x)[q]! = a[q]! ∨ (a.set! i x)[q]! = x

theorem Hex.GraphIso.Nauty.starts_insert {n : Nat} {active : VSet n} {ptnQ : Array Nat} {level w : Nat} (hold : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptnQ[v - 1]! ≤ level) (hw : w = 0 ∨ ptnQ[w - 1]! ≤ level) (v : Nat) : (active.insert w).mem v = true → v = 0 ∨ ptnQ[v - 1]! ≤ level

theorem Hex.GraphIso.Nauty.trivialSplit_starts {n level cell1 cell2 : Nat} {c1 c2 : Int} {st : RefineSt n} (hst : StartsOk level st) (hcellstart : cell1 = 0 ∨ st.ptn[cell1 - 1]! ≤ level) (hc2eq : c2 = c1 - 1) (hc2s : cell2 < st.ptn.size) : StartsOk level (trivialSplit level cell1 cell2 c1 c2 st)

New actives after the trivial split start cells: the reused cell start, or the fresh boundary written one position earlier.

theorem Hex.GraphIso.Nauty.trivialCell_starts {n level cell1 cell2 : Nat} {gRow : VSet n} {st : RefineSt n} (hst : StartsOk level st) (hcellstart : cell1 = 0 ∨ st.ptn[cell1 - 1]! ≤ level) (hc12 : cell1 ≤ cell2) (hc2s : cell2 < st.ptn.size) (_h2 : cell2 < st.lab.size) : StartsOk level (trivialCell level gRow cell1 cell2 st)

theorem Hex.GraphIso.Nauty.active_windowStep_eq {n : Nat} (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) (st : RefineSt n) : (windowStep level cell1 cell2 v c1 c2 maxcell st).active = if (c1 != cell1) = true then st.active.insert c1 else st.active

theorem Hex.GraphIso.Nauty.windowScan_starts {n : Nat} (level cell1 cell2 : Nat) (counts vs : List Nat) (c1acc : Nat) (maxcell : Int) (st : RefineSt n) : StartsOk level st → c1acc = cell1 ∨ c1acc = 0 ∨ st.ptn[c1acc - 1]! ≤ level ∨ cell2 + 1 ≤ c1acc → c1acc + (List.map (multOf counts) vs).sum ≤ cell2 + 1 → cell2 < st.ptn.size → StartsOk level (windowScan level cell1 cell2 counts vs c1acc maxcell st)

Through the window scan, every active position keeps starting a cell: interior group starts follow the boundary written for the preceding group.

theorem Hex.GraphIso.Nauty.nontrivialFix_starts {n level cell1 : Nat} {st : RefineSt n} (hst : StartsOk level st) (hc : cell1 = 0 ∨ st.ptn[cell1 - 1]! ≤ level) : StartsOk level (nontrivialFix cell1 st)

theorem Hex.GraphIso.Nauty.nontrivialCell_starts {n : Nat} {ctx : Ctx n} {level cell1 cell2 : Nat} {workset : VSet n} {st : RefineSt n} (hst : StartsOk level st) (hcellstart : cell1 = 0 ∨ st.ptn[cell1 - 1]! ≤ level) (hc12 : cell1 ≤ cell2) (hc2s : cell2 < st.ptn.size) (_h2 : cell2 < st.lab.size) : StartsOk level (nontrivialCell ctx level workset cell1 cell2 st)

theorem Hex.GraphIso.Nauty.StPerm.refl {n : Nat} (level : Nat) (st : RefineSt n) : StPerm level st st

theorem Hex.GraphIso.Nauty.pickSplit_mem {n : Nat} {active : VSet n} {hint s : Nat} : pickSplit active hint = some s → active.mem s = true

theorem Hex.GraphIso.Nauty.starts_erase {n level : Nat} {st : RefineSt n} {w : Nat} (hst : StartsOk level st) : StartsOk level { lab := st.lab, ptn := st.ptn, active := st.active.erase w, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := st.longcode }

theorem Hex.GraphIso.Nauty.refineTrivial_go_starts {n level : Nat} {gRow : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : StartsOk level st → st.ptn.size = st.lab.size → (∀ (p : Nat × Nat), p ∈ cs → IsCell st.ptn level p.fst (p.snd + 1 - p.fst) ∧ p.snd < st.lab.size) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → StartsOk level (refineTrivial.go level gRow cs st)

theorem Hex.GraphIso.Nauty.refineTrivial_starts {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (hst : StartsOk level st) (hsz : st.ptn.size = st.lab.size) (hnn : n ≤ st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : StartsOk level (refineTrivial ctx level split1 st)

theorem Hex.GraphIso.Nauty.refineNontrivial_go_perm {n : Nat} {ctx : Ctx n} {level : Nat} {workset : VSet n} (cs : List (Nat × Nat)) (st st' : RefineSt n) : StPerm level st st' → st.ptn.size = st.lab.size → (∀ (p : Nat × Nat), p ∈ cs → IsCell st.ptn level p.fst (p.snd + 1 - p.fst) ∧ p.snd < st.lab.size) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → StPerm level (refineNontrivial.go ctx level workset cs st) (refineNontrivial.go ctx level workset cs st') ∧ (refineNontrivial.go ctx level workset cs st).lab.size = st.lab.size ∧ (refineNontrivial.go ctx level workset cs st).ptn.size = st.ptn.size

theorem Hex.GraphIso.Nauty.refineNontrivial_go_starts {n : Nat} {ctx : Ctx n} {level : Nat} {workset : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : StartsOk level st → st.ptn.size = st.lab.size → (∀ (p : Nat × Nat), p ∈ cs → IsCell st.ptn level p.fst (p.snd + 1 - p.fst) ∧ p.snd < st.lab.size) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → StartsOk level (refineNontrivial.go ctx level workset cs st)

theorem Hex.GraphIso.Nauty.refineNontrivial_perm {n : Nat} {ctx : Ctx n} {level split1 split2 : Nat} {st st' : RefineSt n} (h : StPerm level st st') (hsz : st.ptn.size = st.lab.size) (hnn : n ≤ st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (hsc : IsCell st.ptn level split1 (split2 + 1 - split1)) : StPerm level (refineNontrivial ctx level split1 split2 st) (refineNontrivial ctx level split1 split2 st')

theorem Hex.GraphIso.Nauty.refineNontrivial_starts {n : Nat} {ctx : Ctx n} {level split1 split2 : Nat} {st : RefineSt n} (hst : StartsOk level st) (hsz : st.ptn.size = st.lab.size) (hnn : n ≤ st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) : StartsOk level (refineNontrivial ctx level split1 split2 st)

theorem Hex.GraphIso.Nauty.refineStep_perm {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st st' : RefineSt n} (h : StPerm level st st') (hOk : StOk n level st) (hst : StartsOk level st) (hmem : st.active.mem split1 = true) : StPerm level (refineStep ctx level split1 st) (refineStep ctx level split1 st')

One active-cell iteration preserves cell-contents equivalence.

theorem Hex.GraphIso.Nauty.refineStep_starts {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (hOk : StOk n level st) (hst : StartsOk level st) : StartsOk level (refineStep ctx level split1 st)

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

The active-cell loop preserves cell-contents equivalence.

theorem Hex.GraphIso.Nauty.refine_perm {n : Nat} {ctx : Ctx n} {level : Nat} {lab lab' ptn : Array Nat} {active : VSet n} {numcells : Nat} (hcp : cellsPerm ptn level lab lab') (hls : lab'.size = lab.size) (hsl : lab.size = n) (hlab : LabOk lab n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hstarts : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) : StPerm level (refine ctx level lab ptn active numcells) (refine ctx level lab' ptn active numcells)

nauty's refine depends on the ordered partition only through the cell contents: cell-equivalent labellings refine to equal positions and codes with cell-equivalent labellings.

theorem Hex.GraphIso.Nauty.ptn_trivialSplit_vals {n : Nat} (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) (q : Nat) : (trivialSplit level cell1 cell2 c1 c2 st).ptn[q]! = st.ptn[q]! ∨ (trivialSplit level cell1 cell2 c1 c2 st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_trivialCell_vals {n : Nat} (level : Nat) (gRow : VSet n) (cell1 cell2 : Nat) (st : RefineSt n) (q : Nat) : (trivialCell level gRow cell1 cell2 st).ptn[q]! = st.ptn[q]! ∨ (trivialCell level gRow cell1 cell2 st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_windowScan_vals {n : Nat} (level cell1 cell2 : Nat) (counts vs : List Nat) (c1acc : Nat) (maxcell : Int) (st : RefineSt n) (q : Nat) : (windowScan level cell1 cell2 counts vs c1acc maxcell st).ptn[q]! = st.ptn[q]! ∨ (windowScan level cell1 cell2 counts vs c1acc maxcell st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_nontrivialCell_vals {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (cell1 cell2 : Nat) (st : RefineSt n) (q : Nat) : (nontrivialCell ctx level workset cell1 cell2 st).ptn[q]! = st.ptn[q]! ∨ (nontrivialCell ctx level workset cell1 cell2 st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_refineTrivial_go_vals {n : Nat} (level : Nat) (gRow : VSet n) (cs : List (Nat × Nat)) (st : RefineSt n) (q : Nat) : (refineTrivial.go level gRow cs st).ptn[q]! = st.ptn[q]! ∨ (refineTrivial.go level gRow cs st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_refineNontrivial_go_vals {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (cs : List (Nat × Nat)) (st : RefineSt n) (q : Nat) : (refineNontrivial.go ctx level workset cs st).ptn[q]! = st.ptn[q]! ∨ (refineNontrivial.go ctx level workset cs st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_refineStep_vals {n : Nat} (ctx : Ctx n) (level split1 : Nat) (st : RefineSt n) (q : Nat) : (refineStep ctx level split1 st).ptn[q]! = st.ptn[q]! ∨ (refineStep ctx level split1 st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_refineLoop_vals {n : Nat} (ctx : Ctx n) (level fuel : Nat) (st : RefineSt n) (q : Nat) : (refineLoop ctx level fuel st).ptn[q]! = st.ptn[q]! ∨ (refineLoop ctx level fuel st).ptn[q]! = level

theorem Hex.GraphIso.Nauty.ptn_refine_vals {n : Nat} (ctx : Ctx n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells q : Nat) : (refine ctx level lab ptn active numcells).ptn[q]! = ptn[q]! ∨ (refine ctx level lab ptn active numcells).ptn[q]! = level

Every partition write in refine carries the current level.

theorem Hex.GraphIso.Nauty.isCell_succ_iff {ptn : Array Nat} {level a len : Nat} (hvals : ∀ (q : Nat), ptn[q]! ≠ level + 1) : IsCell ptn (level + 1) a len ↔ IsCell ptn level a len

With no partition value exactly level + 1, runs at level and level + 1 coincide.

theorem Hex.GraphIso.Nauty.cellsPerm_succ {ptn : Array Nat} {level : Nat} {lab lab' : Array Nat} (hvals : ∀ (q : Nat), ptn[q]! ≠ level + 1) (h : cellsPerm ptn level lab lab') : cellsPerm ptn (level + 1) lab lab'

theorem Hex.GraphIso.Nauty.breakout_go_size {tv : Nat} (fuel : Nat) (lab : Array Nat) (i prev : Nat) : (breakout.go tv fuel lab i prev).size = lab.size

theorem Hex.GraphIso.Nauty.breakout_go_outside {tv : Nat} (fuel : Nat) (lab : Array Nat) (i prev q : Nat) : q < i → (breakout.go tv fuel lab i prev)[q]! = lab[q]!

theorem Hex.GraphIso.Nauty.breakout_go_outside_right {tv : Nat} (fuel len : Nat) (lab : Array Nat) (i prev : Nat) : (∃ (k : Nat), i ≤ k ∧ k < i + len ∧ k < lab.size ∧ lab[k]! = tv) → ∀ (q : Nat), i + len ≤ q → (breakout.go tv fuel lab i prev)[q]! = lab[q]!

theorem Hex.GraphIso.Nauty.breakout_go_seg {tv : Nat} (fuel len : Nat) (lab : Array Nat) (i prev : Nat) : (∃ (k : Nat), i ≤ k ∧ k < i + len ∧ k < lab.size ∧ lab[k]! = tv) → len ≤ fuel → i + len ≤ lab.size → segN (breakout.go tv fuel lab i prev) i len = prev :: (segN lab i len).erase tv

Individualization rotates the target vertex to the front of the segment: the result is the incoming vertex followed by the segment with its first occurrence of tv erased.