def Hex.GraphIso.Nauty.SplitDone {n : Nat} (ctx : Ctx n) (lab : Array Nat) (workset : VSet n) (lo len : Nat) : Prop

The window of len positions from lo has constant neighbour counts into the vertex set workset.

Equations

• Hex.GraphIso.Nauty.SplitDone ctx lab workset lo len = ∀ (o o' : Nat), o < len → o' < len → workset.cardInter ctx.g[lab[lo + o]!]! = workset.cardInter ctx.g[lab[lo + o']!]!

def Hex.GraphIso.Nauty.Equitable {n : Nat} (ctx : Ctx n) (level : Nat) (lab ptn : Array Nat) : Prop

The partition at level is equitable: every cell has constant neighbour counts into every cell's vertex set.

Equations

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

theorem Hex.GraphIso.Nauty.SplitDone.sub {n : Nat} {ctx : Ctx n} {lab : Array Nat} {workset : VSet n} {lo len lo' len' : Nat} (h : SplitDone ctx lab workset lo len) (hlo : lo ≤ lo') (hhi : lo' + len' ≤ lo + len) : SplitDone ctx lab workset lo' len'

Constant counts restrict to any sub-window.

theorem Hex.GraphIso.Nauty.splitDone_of_le_one {n : Nat} {ctx : Ctx n} {lab : Array Nat} {workset : VSet n} {lo len : Nat} (h : len ≤ 1) : SplitDone ctx lab workset lo len

Windows with at most one position have constant counts.

theorem Hex.GraphIso.Nauty.SplitDone.congr {n : Nat} {ctx : Ctx n} {lab lab' : Array Nat} {workset : VSet n} {lo len : Nat} (h : SplitDone ctx lab workset lo len) (hagree : ∀ (o : Nat), o < len → lab'[lo + o]! = lab[lo + o]!) : SplitDone ctx lab' workset lo len

Constant counts transfer between labellings agreeing on the window.

theorem Hex.GraphIso.Nauty.equitable_of_singletons {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} (h : ∀ (cd : Nat × Nat), cd ∈ cells ptn level n → cd.snd = cd.fst) : Equitable ctx level lab ptn

A discrete partition is equitable.

theorem Hex.GraphIso.Nauty.splitDone_single_of_const {n : Nat} {ctx : Ctx n} {lab : Array Nat} {u lo len : Nat} {b : Bool} (hconst : ∀ (o : Nat), o < len → ctx.g[lab[lo + o]!]!.mem u = b) : SplitDone ctx lab (VSet.empty.insert u) lo len

Constant adjacency to a vertex on a window gives constant counts into its singleton set.

theorem Hex.GraphIso.Nauty.splitCellLoop_memConst {n : Nat} {gRow : VSet n} {lab : Array Nat} {cell1 cell2 : Nat} (h12 : cell1 ≤ cell2) (hsz : cell2 < lab.size) : (∀ (o : Nat), o < List.countP (fun (x : Nat) => gRow.mem x) (segN lab cell1 (cell2 + 1 - cell1)) → gRow.mem (splitCellLoop gRow (cell2 - cell1 + 2) lab (Int.ofNat cell1) (Int.ofNat cell2)).fst[cell1 + o]! = true) ∧ ∀ (o : Nat), List.countP (fun (x : Nat) => gRow.mem x) (segN lab cell1 (cell2 + 1 - cell1)) ≤ o → o < cell2 + 1 - cell1 → gRow.mem (splitCellLoop gRow (cell2 - cell1 + 2) lab (Int.ofNat cell1) (Int.ofNat cell2)).fst[cell1 + o]! = false

The two-pointer pass separates a window: the first cnt positions hold splitter-adjacent vertices and the remainder non-adjacent ones, where cnt is the window's adjacency count.

theorem Hex.GraphIso.Nauty.trivialCell_memConst {n level cell1 cell2 : Nat} {gRow : VSet n} {st : RefineSt n} (h12 : cell1 ≤ cell2) (hsz : cell2 < st.lab.size) : (trivialCell level gRow cell1 cell2 st).lab.size = st.lab.size ∧ (∀ (j : Nat), j < cell1 ∨ cell2 < j → (trivialCell level gRow cell1 cell2 st).lab[j]! = st.lab[j]!) ∧ (segN (trivialCell level gRow cell1 cell2 st).lab cell1 (cell2 + 1 - cell1)).Perm (segN st.lab cell1 (cell2 + 1 - cell1)) ∧ (∀ (o : Nat), o < List.countP (fun (x : Nat) => gRow.mem x) (segN st.lab cell1 (cell2 + 1 - cell1)) → gRow.mem (trivialCell level gRow cell1 cell2 st).lab[cell1 + o]! = true) ∧ ∀ (o : Nat), List.countP (fun (x : Nat) => gRow.mem x) (segN st.lab cell1 (cell2 + 1 - cell1)) ≤ o → o < cell2 + 1 - cell1 → gRow.mem (trivialCell level gRow cell1 cell2 st).lab[cell1 + o]! = false

A processed cell of the trivial-splitter pass: the labelling outside the cell is untouched, the cell keeps its contents as a multiset, and it is rearranged into the splitter-adjacent block followed by the non-adjacent block.

def Hex.GraphIso.Nauty.ConstOn {n : Nat} (ctx : Ctx n) (W : VSet n) (ms : List Nat) : Prop

Constant neighbour counts into W over a member list.

Equations

• Hex.GraphIso.Nauty.ConstOn ctx W ms = ∀ (x : Nat), x ∈ ms → ∀ (y : Nat), y ∈ ms → W.cardInter ctx.g[x]! = W.cardInter ctx.g[y]!

theorem Hex.GraphIso.Nauty.ConstOn.mono {n : Nat} {ctx : Ctx n} {W : VSet n} {ms ms' : List Nat} (h : ConstOn ctx W ms) (hsub : ∀ (x : Nat), x ∈ ms' → x ∈ ms) : ConstOn ctx W ms'

theorem Hex.GraphIso.Nauty.ConstOn.perm {n : Nat} {ctx : Ctx n} {W : VSet n} {ms ms' : List Nat} (h : ConstOn ctx W ms) (hp : ms'.Perm ms) : ConstOn ctx W ms'

theorem Hex.GraphIso.Nauty.splitDone_iff_constOn {n : Nat} {ctx : Ctx n} {lab : Array Nat} {W : VSet n} {lo len : Nat} : SplitDone ctx lab W lo len ↔ ConstOn ctx W (segN lab lo len)

theorem Hex.GraphIso.Nauty.ConstOn.or {n : Nat} {ctx : Ctx n} {a b : VSet n} {ms : List Nat} (hd : a.inter b = VSet.empty) (h1 : ConstOn ctx a ms) (h2 : ConstOn ctx b ms) : ConstOn ctx (a.union b) ms

Constancy into two disjoint sets gives constancy into the union.

theorem Hex.GraphIso.Nauty.ConstOn.of_or {n : Nat} {ctx : Ctx n} {a b : VSet n} {ms : List Nat} (hd : a.inter b = VSet.empty) (h1 : ConstOn ctx (a.union b) ms) (h2 : ConstOn ctx b ms) : ConstOn ctx a ms

Constancy into a disjoint union and into the right part gives constancy into the left part.

theorem Hex.GraphIso.Nauty.worksetOf_disjoint {n : Nat} {lab lab' : Array Nat} {lo hi lo' hi' : Nat} (h : ∀ (v : Nat), v ∈ segN lab lo (hi + 1 - lo) → v ∈ segN lab' lo' (hi' + 1 - lo') → False) : (worksetOf n lab lo hi).inter (worksetOf n lab' lo' hi') = VSet.empty

Splitter sets of member-disjoint segments are disjoint.

theorem Hex.GraphIso.Nauty.worksetOf_split {n : Nat} {lab : Array Nat} {lo j hi : Nat} (hlo : lo ≤ j) (hj : j < hi) : worksetOf n lab lo hi = (worksetOf n lab lo j).union (worksetOf n lab (j + 1) hi)

A splitter set splits at any interior junction of its window.

theorem Hex.GraphIso.Nauty.mem_worksetOf_iff {n : Nat} {lab : Array Nat} {lo hi v : Nat} : (worksetOf n lab lo hi).mem v = true ↔ v < n ∧ v ∈ segN lab lo (hi + 1 - lo)

Membership in a splitter set is membership of the segment (of a vertex).

theorem Hex.GraphIso.Nauty.constOn_single_of_adj {n : Nat} {ctx : Ctx n} {v : Nat} {ms : List Nat} {b : Bool} (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hv : v < n) (hms : ∀ (x : Nat), x ∈ ms → x < n) (hconst : ∀ (x : Nat), x ∈ ms → ctx.g[v]!.mem x = b) : ConstOn ctx (VSet.empty.insert v) ms

Adjacency to a vertex constant over a member list gives constant counts into its singleton set, through row symmetry.

theorem Hex.GraphIso.Nauty.trivialSplit_ptn_eq {n : Nat} (level cell1 cell2 : Nat) (c1 c2 : Int) (st : RefineSt n) : (trivialSplit level cell1 cell2 c1 c2 st).ptn = if c2 ≥ Int.ofNat cell1 ∧ c1 ≤ Int.ofNat cell2 then st.ptn.set! c2.toNat level else st.ptn

The split bookkeeping's partition effect: one boundary at the final c2 when the split is nontrivial, nothing otherwise.

theorem Hex.GraphIso.Nauty.trivialCell_effect {n level cell1 cell2 : Nat} {gRow : VSet n} {st : RefineSt n} (h12 : cell1 ≤ cell2) (hsz : cell2 < st.lab.size) : (trivialCell level gRow cell1 cell2 st).lab.size = st.lab.size ∧ (∀ (j : Nat), j < cell1 ∨ cell2 < j → (trivialCell level gRow cell1 cell2 st).lab[j]! = st.lab[j]!) ∧ (((trivialCell level gRow cell1 cell2 st).ptn = st.ptn ∧ ∃ (b : Bool), ∀ (p : Nat), cell1 ≤ p → p ≤ cell2 → gRow.mem (trivialCell level gRow cell1 cell2 st).lab[p]! = b) ∨ ∃ (j : Nat), cell1 ≤ j ∧ j < cell2 ∧ (trivialCell level gRow cell1 cell2 st).ptn = st.ptn.set! j level ∧ (∀ (p : Nat), cell1 ≤ p → p ≤ j → gRow.mem (trivialCell level gRow cell1 cell2 st).lab[p]! = true) ∧ ∀ (p : Nat), j < p → p ≤ cell2 → gRow.mem (trivialCell level gRow cell1 cell2 st).lab[p]! = false)

One processed cell of the trivial pass: sizes and the outside kept, and the window left as constant block(s) with the junction boundary written exactly in the two-block case.

theorem Hex.GraphIso.Nauty.refineTrivial_go_blocks {n level : Nat} {gRow : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : (∀ (p : Nat × Nat), p ∈ cs → p.fst ≤ p.snd ∧ p.snd < st.lab.size) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → st.ptn.size = st.lab.size → (refineTrivial.go level gRow cs st).lab.size = st.lab.size ∧ (∀ (j : Nat), (∀ (p : Nat × Nat), p ∈ cs → j < p.fst ∨ p.snd < j) → (refineTrivial.go level gRow cs st).lab[j]! = st.lab[j]!) ∧ (∀ (q : Nat), (∀ (p : Nat × Nat), p ∈ cs → q < p.fst ∨ p.snd ≤ q) → (refineTrivial.go level gRow cs st).ptn[q]! = st.ptn[q]!) ∧ (refineTrivial.go level gRow cs st).ptn.size = st.ptn.size ∧ ∀ (p : Nat × Nat), p ∈ cs → (∃ (b : Bool), ∀ (q : Nat), p.fst ≤ q → q ≤ p.snd → gRow.mem (refineTrivial.go level gRow cs st).lab[q]! = b) ∨ ∃ (j : Nat), p.fst ≤ j ∧ j < p.snd ∧ (refineTrivial.go level gRow cs st).ptn[j]! = level ∧ (∀ (q : Nat), p.fst ≤ q → q ≤ j → gRow.mem (refineTrivial.go level gRow cs st).lab[q]! = true) ∧ ∀ (q : Nat), j < q → q ≤ p.snd → gRow.mem (refineTrivial.go level gRow cs st).lab[q]! = false

The trivial pass over a window list: sizes kept, everything outside the windows kept, and every window left as constant block(s) with a surviving junction boundary in the two-block case.

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

With the last in-range position closed, cell ends stay in range.

theorem Hex.GraphIso.Nauty.refineTrivial_cell_adj {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (hpsz : st.ptn.size = n) (hlp : st.lab.size = st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (a len : Nat) : IsCell (refineTrivial ctx level split1 st).ptn level a len → a + len ≤ n → ∃ (b : Bool), ∀ (q : Nat), a ≤ q → q < a + len → ctx.g[st.lab[split1]!]!.mem (refineTrivial ctx level split1 st).lab[q]! = b

After the trivial pass, every cell of the result within range is adjacency-constant to the captured splitter row.

theorem Hex.GraphIso.Nauty.windowScan_junction {n level cell1 cell2 : Nat} {counts : List Nat} (vs : List Nat) (c1 : Nat) (maxcell : Int) (st : RefineSt n) : cell1 ≤ c1 → c1 + (List.map (multOf counts) vs).sum = cell2 + 1 → cell2 < st.ptn.size → (∀ (p : Nat), c1 ≤ p → p < cell2 → st.ptn[p]! > level) → ∀ (k : Nat), k < vs.length → 0 < multOf counts vs[k]! → c1 + (List.map (multOf counts) (List.take (k + 1) vs)).sum ≤ cell2 → (windowScan level cell1 cell2 counts vs c1 maxcell st).ptn[c1 + (List.map (multOf counts) (List.take (k + 1) vs)).sum - 1]! = level

The scan closes the junction after each nonempty group that ends inside the cell.

theorem Hex.GraphIso.Nauty.countsOf_getElem! {n : Nat} {ctx : Ctx n} {lab : Array Nat} {workset : VSet n} {cell1 cell2 j : Nat} (hj : j < cell2 + 1 - cell1) : (countsOf ctx lab workset cell1 cell2)[j]! = workset.cardInter ctx.g[lab[cell1 + j]!]!

theorem Hex.GraphIso.Nauty.nontrivialCell_effect {n : Nat} {ctx : Ctx n} {level cell1 cell2 : Nat} {workset : VSet n} {st : RefineSt n} (h12 : cell1 ≤ cell2) (hsz : cell2 < st.lab.size) (hlp : st.ptn.size = st.lab.size) (hfresh : ∀ (p : Nat), cell1 ≤ p → p < cell2 → st.ptn[p]! > level) : (nontrivialCell ctx level workset cell1 cell2 st).lab.size = st.lab.size ∧ (∀ (j : Nat), j < cell1 ∨ cell2 < j → (nontrivialCell ctx level workset cell1 cell2 st).lab[j]! = st.lab[j]!) ∧ (∀ (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 ∧ ∀ (q q' : Nat), cell1 ≤ q → q ≤ q' → q' ≤ cell2 → (∀ (i : Nat), q ≤ i → i < q' → (nontrivialCell ctx level workset cell1 cell2 st).ptn[i]! > level) → workset.cardInter ctx.g[(nontrivialCell ctx level workset cell1 cell2 st).lab[q]!]! = workset.cardInter ctx.g[(nontrivialCell ctx level workset cell1 cell2 st).lab[q']!]!

One processed cell of the nontrivial pass: sizes and the outside kept, and positions of the window connected by an open run of the result carry equal counts into the captured splitter set.

theorem Hex.GraphIso.Nauty.refineNontrivial_go_blocks {n : Nat} {ctx : Ctx n} {level : Nat} {workset : VSet n} (cs : List (Nat × Nat)) (st : RefineSt n) : (∀ (p : Nat × Nat), p ∈ cs → p.fst ≤ p.snd ∧ p.snd < st.lab.size) → List.Pairwise (fun (p q : Nat × Nat) => p.snd < q.fst) cs → st.ptn.size = st.lab.size → (∀ (p : Nat × Nat), p ∈ cs → ∀ (i : Nat), p.fst ≤ i → i < p.snd → st.ptn[i]! > level) → (refineNontrivial.go ctx level workset cs st).lab.size = st.lab.size ∧ (∀ (j : Nat), (∀ (p : Nat × Nat), p ∈ cs → j < p.fst ∨ p.snd < j) → (refineNontrivial.go ctx level workset cs st).lab[j]! = st.lab[j]!) ∧ (∀ (q : Nat), (∀ (p : Nat × Nat), p ∈ cs → q < p.fst ∨ p.snd ≤ q) → (refineNontrivial.go ctx level workset cs st).ptn[q]! = st.ptn[q]!) ∧ (refineNontrivial.go ctx level workset cs st).ptn.size = st.ptn.size ∧ ∀ (p : Nat × Nat), p ∈ cs → ∀ (q q' : Nat), p.fst ≤ q → q ≤ q' → q' ≤ p.snd → (∀ (i : Nat), q ≤ i → i < q' → (refineNontrivial.go ctx level workset cs st).ptn[i]! > level) → workset.cardInter ctx.g[(refineNontrivial.go ctx level workset cs st).lab[q]!]! = workset.cardInter ctx.g[(refineNontrivial.go ctx level workset cs st).lab[q']!]!

The nontrivial pass over a window list: sizes and the outside kept, and within every window, positions connected by an open run of the result carry equal counts into the captured splitter set.

theorem Hex.GraphIso.Nauty.refineNontrivial_cell_const {n : Nat} {ctx : Ctx n} {level split1 split2 : Nat} {st : RefineSt n} (hpsz : st.ptn.size = n) (hlp : st.lab.size = st.ptn.size) (hend : st.ptn[st.ptn.size - 1]! ≤ level) (a len : Nat) : IsCell (refineNontrivial ctx level split1 split2 st).ptn level a len → a + len ≤ n → ConstOn ctx (worksetOf n st.lab split1 split2) (segN (refineNontrivial ctx level split1 split2 st).lab a len)

After the nontrivial pass, every cell of the result within range has constant counts into the captured splitter set.

theorem Hex.GraphIso.Nauty.worksetOf_singleton {n : Nat} (lab : Array Nat) (lo : Nat) : worksetOf n lab lo lo = VSet.empty.insert lab[lo]!

theorem Hex.GraphIso.Nauty.refineStep_cell_const {n : Nat} {ctx : Ctx n} {level split1 : Nat} {st : RefineSt n} (hok : StOk n level st) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hs1 : split1 < n) (a len : Nat) : IsCell (refineStep ctx level split1 st).ptn level a len → a + len ≤ n → ConstOn ctx (worksetOf n st.lab split1 (cellEnd st.ptn level split1)) (segN (refineStep ctx level split1 st).lab a len)

After one refineStep, every cell of the result within range has constant counts into the retired splitter's captured vertex set.

def Hex.GraphIso.Nauty.activeUnion {n : Nat} (level : Nat) (st : RefineSt n) : VSet n

The union of the active cells' splitter sets.

Equations

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

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

Every cell's splitter set lies inside V or misses it.

Equations

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

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

The refinement loop's certificate invariant.

Equations

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

theorem Hex.GraphIso.Nauty.active_eq_empty_of_pickSplit_none {n : Nat} {active : VSet n} {hint : Nat} (h : pickSplit active hint = none) : active = VSet.empty

An exhausted pickSplit means an empty active set.

theorem Hex.GraphIso.Nauty.activeUnion_eq_empty {n level : Nat} {st : RefineSt n} (h : st.active = VSet.empty) : activeUnion level st = VSet.empty

With no active cells the active union vanishes.

theorem Hex.GraphIso.Nauty.equitable_of_certInv_exit {n : Nat} {ctx : Ctx n} {level : Nat} {st : RefineSt n} (hinv : CertInv ctx level st) (hact : st.active = VSet.empty) : Equitable ctx level st.lab st.ptn

At exit the certificate collapses and the invariant is equitability.