def Hex.GraphIso.Nauty.bitCnt {n : Nat} (r : VSet n) (v : Nat) : Nat

The adjacency bit as a count.

Equations

• Hex.GraphIso.Nauty.bitCnt r v = if r.mem v = true then 1 else 0

theorem Hex.GraphIso.Nauty.bitCnt_le_one {n : Nat} (r : VSet n) (v : Nat) : bitCnt r v ≤ 1

theorem Hex.GraphIso.Nauty.bitCnt_eq_zero {n : Nat} {r : VSet n} {v : Nat} : bitCnt r v = 0 ↔ r.mem v = false

theorem Hex.GraphIso.Nauty.bitCnt_eq_one {n : Nat} {r : VSet n} {v : Nat} : bitCnt r v = 1 ↔ r.mem v = true

theorem Hex.GraphIso.Nauty.bitCnt_inj {n : Nat} {r r' : VSet n} {v v' : Nat} : bitCnt r v = bitCnt r' v' ↔ r.mem v = r'.mem v'

theorem Hex.GraphIso.Nauty.cardInter_workset {n : Nat} {lab : Array Nat} (r : VSet n) (len lo : Nat) : (∀ (o o' : Nat), o ≤ len → o' ≤ len → o ≠ o' → lab[lo + o]! ≠ lab[lo + o']!) → (worksetOf n lab lo (lo + len)).cardInter r = (List.map (fun (o : Nat) => bitCnt r lab[lo + o]!) (List.range (len + 1))).sum

The count into a window's splitter set expands into the sum of the adjacency bits at the window's members.

theorem Hex.GraphIso.Nauty.bitCnt_symm {n : Nat} {ctx : Ctx n} (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) {u w : Nat} (hu : u < n) (hw : w < n) : bitCnt ctx.g[u]! w = bitCnt ctx.g[w]! u

Adjacency-bit counts are symmetric between vertices.

theorem Hex.GraphIso.Nauty.count_into_cell {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) {d e : Nat} (hD : (d, e) ∈ cells ptn level n) {u : Nat} : (worksetOf n lab d e).cardInter ctx.g[u]! = (List.map (fun (o : Nat) => bitCnt ctx.g[u]! lab[d + o]!) (List.range (e + 1 - d))).sum

The count of a vertex into a cell's splitter set is the sum of its adjacency bits at the cell's members.

theorem Hex.GraphIso.Nauty.countP_balance {α : Type} (p q : α → Bool) (l : List α) : List.countP p l + List.countP (fun (x : α) => q x && !p x) l = List.countP q l + List.countP (fun (x : α) => p x && !q x) l

Equal Boolean counts balance the two directions of disagreement.

theorem Hex.GraphIso.Nauty.countP_bits {n : Nat} (r : VSet n) (l : List Nat) : List.countP r.mem l = (List.map (bitCnt r) l).sum

The count into a list is the sum of its adjacency bits.

theorem Hex.GraphIso.Nauty.countP_cell {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level d e u : Nat} (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hD : (d, e) ∈ cells ptn level n) : List.countP (fun (o : Nat) => ctx.g[u]!.mem lab[d + o]!) (List.range (e + 1 - d)) = (worksetOf n lab d e).cardInter ctx.g[u]!

Counting adjacent cell members agrees with the splitter-set count.

theorem Hex.GraphIso.Nauty.differ_balance {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level c e d de u v : Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hC : (c, e) ∈ cells ptn level n) (hD : (d, de) ∈ cells ptn level n) (hu : u < e + 1 - c) (hv : v < e + 1 - c) : List.countP (fun (w : Nat) => ctx.g[lab[c + u]!]!.mem w && !ctx.g[lab[c + v]!]!.mem w) (segN lab d (de + 1 - d)) = List.countP (fun (w : Nat) => ctx.g[lab[c + v]!]!.mem w && !ctx.g[lab[c + u]!]!.mem w) (segN lab d (de + 1 - d))

Equitability balances the two directions of disagreement in each cell.

theorem Hex.GraphIso.Nauty.bits_eq_of_short {n : Nat} {r s : VSet n} {l : List Nat} (hlen : l.length ≤ 1) (he : (List.map (bitCnt r) l).sum = (List.map (bitCnt s) l).sum) (w : Nat) : w ∈ l → r.mem w = s.mem w

On a list of at most one vertex, equal neighbour counts force pointwise equal adjacency.

theorem Hex.GraphIso.Nauty.countP_unique {α : Type} {p : α → Bool} {l : List α} (hc : List.countP p l ≤ 1) {a b : α} (ha : a ∈ l) (hb : b ∈ l) (hpa : p a = true) (hpb : p b = true) : a = b

A predicate counted at most once selects at most one distinct element.

theorem Hex.GraphIso.Nauty.countP_differ_le {α : Type} (p q : α → Bool) (l : List α) : List.countP (fun (x : α) => p x && !q x) l + List.countP (fun (x : α) => q x && !p x) l ≤ l.length

Disagreement in either direction uses at most the whole list.

theorem Hex.GraphIso.Nauty.differ_pair {α : Type} (p q : α → Bool) {l : List α} (hlen : l.length ≤ 3) (he : List.countP p l = List.countP q l) : (∀ (w : α), w ∈ l → p w = q w) ∨ ∃ (a : α), a ∈ l ∧ ∃ (b : α), b ∈ l ∧ a ≠ b ∧ p a = true ∧ q a = false ∧ p b = false ∧ q b = true ∧ ∀ (w : α), w ∈ l → w ≠ a → w ≠ b → p w = q w

Equal counts on at most three vertices give either identical bits or a single pair distinguishing the two rows in opposite directions.

theorem Hex.GraphIso.Nauty.pair_swap_eq {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlb : ∀ (i : Nat), i < n → lab[i]! < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) {c d : Nat} (hP : (c, c + 1) ∈ cells ptn level n) (hQ : (d, d + 1) ∈ cells ptn level n) : ctx.g[lab[c]!]!.mem lab[d]! = ctx.g[lab[c + 1]!]!.mem lab[d + 1]! ∧ ctx.g[lab[c]!]!.mem lab[d + 1]! = ctx.g[lab[c + 1]!]!.mem lab[d]!

Swapping both pairs preserves adjacency: the bits between two pair cells of an equitable partition satisfy the two cross equalities, in every configuration (empty, complete, or either matching).

def Hex.GraphIso.Nauty.PairMatch {n : Nat} (g : Array (VSet n)) (x y z t : Nat) : Prop

The matching configuration between two pair cells: each member of one pair is adjacent to exactly one member of the other, in one of the two consistent ways.

Equations

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

theorem Hex.GraphIso.Nauty.pair_eq_of_not_match {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlb : ∀ (i : Nat), i < n → lab[i]! < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) {c d : Nat} (hP : (c, c + 1) ∈ cells ptn level n) (hQ : (d, d + 1) ∈ cells ptn level n) (hnm : ¬PairMatch ctx.g lab[c]! lab[c + 1]! lab[d]! lab[d + 1]!) : ctx.g[lab[c]!]!.mem lab[d]! = ctx.g[lab[c + 1]!]!.mem lab[d]! ∧ ctx.g[lab[c]!]!.mem lab[d + 1]! = ctx.g[lab[c + 1]!]!.mem lab[d + 1]!

Between two non-matching pair cells of an equitable partition the bits are insensitive to swapping either pair alone.

theorem Hex.GraphIso.Nauty.pair_odd_eq {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlb : ∀ (i : Nat), i < n → lab[i]! < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) {c d e : Nat} (hP : (c, c + 1) ∈ cells ptn level n) (hD : (d, e) ∈ cells ptn level n) (hodd : (e + 1 - d) % 2 = 1) (o : Nat) : o < e + 1 - d → ctx.g[lab[c]!]!.mem lab[d + o]! = ctx.g[lab[c + 1]!]!.mem lab[d + o]!

The members of a pair cell have identical bits at every member of a cell of odd size: parity forces the count between them to be empty or complete.

theorem Hex.GraphIso.Nauty.reg4_comp {e01 e02 e03 e12 e13 e23 : Nat} (h01 : e01 + e02 + e03 = e01 + e12 + e13) (h02 : e01 + e02 + e03 = e02 + e12 + e23) (h03 : e01 + e02 + e03 = e03 + e13 + e23) : e01 = e23 ∧ e02 = e13 ∧ e03 = e12

Equal internal degrees in a four-element cell make complementary pairs equally adjacent.

theorem Hex.GraphIso.Nauty.perm_of_nodup_subset (l₁ l₂ : List Nat) : l₁.Nodup → (∀ (x : Nat), x ∈ l₁ → x ∈ l₂) → l₂.length ≤ l₁.length → l₁.Perm l₂

A duplicate-free list included in a list of no greater length is a permutation of it.

theorem Hex.GraphIso.Nauty.sum_of_perm {l₁ l₂ : List Nat} (h : l₁.Perm l₂) : l₁.sum = l₂.sum

Sums are invariant under permutation.

theorem Hex.GraphIso.Nauty.range_perm_of_distinct {l : List Nat} {k : Nat} (hlen : l.length = k) (hnd : l.Nodup) (hbd : ∀ (x : Nat), x ∈ l → x < k) : l.Perm (List.range k)

A permutation of range k from k distinct bounded values.

theorem Hex.GraphIso.Nauty.sum_range_of_distinct {l : List Nat} {k : Nat} (F : Nat → Nat) (hlen : l.length = k) (hnd : l.Nodup) (hbd : ∀ (x : Nat), x ∈ l → x < k) : (List.map F (List.range k)).sum = (List.map F l).sum

A sum over range k rewritten through k distinct bounded indices.

theorem Hex.GraphIso.Nauty.triple_const {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlb : ∀ (i : Nat), i < n → lab[i]! < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) {d : Nat} (hT : (d, d + 2) ∈ cells ptn level n) {c ce : Nat} (hC : (c, ce) ∈ cells ptn level n) (hsz : ce + 1 - c ≤ 2) {o o' w : Nat} (ho : o < 3) (ho' : o' < 3) (hw : w < ce + 1 - c) : ctx.g[lab[d + o]!]!.mem lab[c + w]! = ctx.g[lab[d + o']!]!.mem lab[c + w]!

Members of the triple cell have identical bits at every member of any other cell of size at most two.

theorem Hex.GraphIso.Nauty.triple_internal {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlb : ∀ (i : Nat), i < n → lab[i]! < n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) {d : Nat} (hT : (d, d + 2) ∈ cells ptn level n) (o o' u u' : Nat) : o < 3 → o' < 3 → u < 3 → u' < 3 → o ≠ o' → u ≠ u' → ctx.g[lab[d + o]!]!.mem lab[d + o']! = ctx.g[lab[d + u]!]!.mem lab[d + u']!

All off-diagonal internal bits of the triple agree.

theorem Hex.GraphIso.Nauty.mem_erase_nodup {l : List Nat} : l.Nodup → ∀ (a w : Nat), w ∈ l.erase a ↔ w ∈ l ∧ w ≠ a

theorem Hex.GraphIso.Nauty.cell_const_into_singleton {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hE : Equitable ctx level lab ptn) {tc te : Nat} (hC : (tc, te) ∈ cells ptn level n) {s : Nat} (hS : (s, s) ∈ cells ptn level n) {o o' : Nat} (ho : o ≤ te - tc) (ho' : o' ≤ te - tc) : ctx.g[lab[tc + o]!]!.mem lab[s]! = ctx.g[lab[tc + o']!]!.mem lab[s]!

The count of one row into a singleton cell is its bit there, so equitability makes the bits of all members of a cell agree at every singleton-cell vertex.

theorem Hex.GraphIso.Nauty.nodup_erase {l : List Nat} : l.Nodup → ∀ (a : Nat), (l.erase a).Nodup

theorem Hex.GraphIso.Nauty.nodup_subset_length (l r : List Nat) : l.Nodup → (∀ (x : Nat), x ∈ l → x ∈ r) → l.length ≤ r.length

theorem Hex.GraphIso.Nauty.sum3_eq_of_cover {f : Nat → Nat} {a b c : Nat} (ha : a ≤ 2) (hb : b ≤ 2) (hc : c ≤ 2) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : f 0 + f 1 + f 2 = f a + f b + f c

theorem Hex.GraphIso.Nauty.other_two {p q : Nat} (hp : p ≤ 3) (hq : q ≤ 3) (hpq : p ≠ q) : ∃ (r : Nat), ∃ (s : Nat), r ≤ 3 ∧ s ≤ 3 ∧ p ≠ r ∧ p ≠ s ∧ q ≠ r ∧ q ≠ s ∧ r ≠ s

Two distinct offsets below four leave two more.

theorem Hex.GraphIso.Nauty.differ_five {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc te oU oV wa wb wf : Nat} (hIt : IterOk ctx level st) (hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z) (hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false) (hE : Equitable ctx level st.lab st.ptn) (hC : (tc, te) ∈ cells st.ptn level n) (hm : te + 1 - tc = 5) (hoU : oU ≤ te - tc) (hoV : oV ≤ te - tc) (hne : oU ≠ oV) (hwa : wa ≤ te - tc) (hwb : wb ≤ te - tc) (hwf : wf ≤ te - tc) (hab : wa ≠ wb) (haf : wa ≠ wf) (hbf : wb ≠ wf) (hau : wa ≠ oU) (hav : wa ≠ oV) (hbu : wb ≠ oU) (hbv : wb ≠ oV) (hfu : wf ≠ oU) (hfv : wf ≠ oV) (htau : ctx.g[st.lab[tc + wa]!]!.mem st.lab[tc + oU]! = true) (htav : ctx.g[st.lab[tc + wa]!]!.mem st.lab[tc + oV]! = false) (htbu : ctx.g[st.lab[tc + wb]!]!.mem st.lab[tc + oU]! = false) (htbv : ctx.g[st.lab[tc + wb]!]!.mem st.lab[tc + oV]! = true) : ctx.g[st.lab[tc + wf]!]!.mem st.lab[tc + wa]! = ctx.g[st.lab[tc + wf]!]!.mem st.lab[tc + wb]!

In a five-member window, the member outside a crossed pair has equal bits at the pair: the pair's two row sums expand over the five named offsets, the crossed types cancel, and the shared internal bit cancels by symmetry.

theorem Hex.GraphIso.Nauty.fourCell_comp {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc oU oV w1 w2 : Nat} (hIt : IterOk ctx level st) (hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z) (hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false) (hE : Equitable ctx level st.lab st.ptn) (hC : (tc, tc + 3) ∈ cells st.ptn level n) (hoU : oU ≤ 3) (hoV : oV ≤ 3) (hw1 : w1 ≤ 3) (hw2 : w2 ≤ 3) (hnd : [oU, oV, w1, w2].Nodup) : ctx.g[st.lab[tc + oU]!]!.mem st.lab[tc + w1]! = ctx.g[st.lab[tc + oV]!]!.mem st.lab[tc + w2]! ∧ ctx.g[st.lab[tc + oU]!]!.mem st.lab[tc + w2]! = ctx.g[st.lab[tc + oV]!]!.mem st.lab[tc + w1]! ∧ ctx.g[st.lab[tc + oU]!]!.mem st.lab[tc + oV]! = ctx.g[st.lab[tc + w1]!]!.mem st.lab[tc + w2]!

Complementary pairs of a four-cell are equally adjacent.