def Hex.GraphIso.Nauty.Sparse.Graph.context {n : Nat} (G : SparseGraph n) : Ctx n

A set-valued interpretation of native rows for the shared equitability predicates. It is used only in proofs, never by the sparse search.

Equations

• Hex.GraphIso.Nauty.Sparse.Graph.context G = { g := Array.ofFn fun (v : Fin n) => Hex.GraphIso.Nauty.VSet.ofList ((Hex.GraphIso.Nauty.Sparse.Graph.ofGraph G).row ↑v) }

theorem Hex.GraphIso.Nauty.Sparse.Graph.context_mem {n : Nat} (G : SparseGraph n) (u v : Fin n) : (context G).g[↑u]!.mem ↑v = G.adj u v

theorem Hex.GraphIso.Nauty.Sparse.cardInter_list {n : Nat} (s t : VSet n) (xs : List Nat) (hn : xs.Nodup) (hm : ∀ (v : Nat), s.mem v = true ↔ v ∈ xs) : s.cardInter t = (List.filter t.mem xs).length

Counting a set intersection can use any duplicate-free enumeration of the first set, independently of its packed representation.

theorem Hex.GraphIso.Nauty.Sparse.Graph.count_context {n : Nat} (G : SparseGraph n) (vertices : List Nat) (hb : ∀ (u : Nat), u ∈ vertices → u < n) (v : Fin n) : List.count (↑v) (List.flatMap (fun (u : Nat) => (ofGraph G).row u) vertices) = (List.filter (fun (u : Nat) => (context G).g[↑v]!.mem u) vertices).length

Native neighbour accumulation agrees with counting the adjacent vertices in the captured splitter list. Symmetry supplies the row orientation.

theorem Hex.GraphIso.Nauty.Sparse.segN_nodup {n first len : Nat} {lab : Array Nat} (hp : lab.toList.Perm (List.range n)) (hb : first + len ≤ n) : (segN lab first len).Nodup

A bounded interval of a labelling permutation has no repeated vertices.

theorem Hex.GraphIso.Nauty.Sparse.Graph.count_workset {n first last : Nat} (G : SparseGraph n) (lab : Array Nat) (hp : lab.toList.Perm (List.range n)) (hf : first ≤ last) (hb : last < n) (v : Fin n) : List.count (↑v) (List.flatMap (fun (q : Nat) => (ofGraph G).row lab[q]!) (List.range' first (last + 1 - first))) = (worksetOf n lab first last).cardInter (context G).g[↑v]!

Native accumulated counts into a captured label interval are exactly the shared equitability predicate's set-intersection cardinalities.

theorem Hex.GraphIso.Nauty.Sparse.Graph.constOn_workset {n first last a len : Nat} (G : SparseGraph n) (lab out : Array Nat) (hp : lab.toList.Perm (List.range n)) (hout : out.toList.Perm (List.range n)) (hf : first ≤ last) (hb : last < n) (ha : a + len ≤ n) (hc : ∀ (q r : Nat), a ≤ q → q < a + len → a ≤ r → r < a + len → List.count out[q]! (List.flatMap (fun (j : Nat) => (ofGraph G).row lab[j]!) (List.range' first (last + 1 - first))) = List.count out[r]! (List.flatMap (fun (j : Nat) => (ofGraph G).row lab[j]!) (List.range' first (last + 1 - first)))) : ConstOn (context G) (worksetOf n lab first last) (segN out a len)

Constant native counts imply the shared set-valued cell predicate.