theorem Hex.SparseGraph.offset_mono {n : Nat} (G : SparseGraph n) {i j : Nat} (hij : i ≤ j) (hj : j ≤ n) : G.offsets[i]! ≤ G.offsets[j]!

Consecutive packed rows have monotone offsets, including the terminal offset.

theorem Hex.SparseGraph.offset_le {n : Nat} (G : SparseGraph n) {i : Nat} (hi : i ≤ n) : G.offsets[i]! ≤ G.neighbors.size

theorem Hex.SparseGraph.edge_lt {n : Nat} (G : SparseGraph n) {i : Fin n} {e : Nat} (he : e < G.offsets[↑i + 1]!) : e < G.neighbors.size

An adjacency-loop cursor is inside the packed neighbour array.

theorem Hex.SparseGraph.edge_mem {n : Nat} (G : SparseGraph n) (i : Fin n) {e : Nat} (hlo : G.offsets[↑i]! ≤ e) (hhi : e < G.offsets[↑i + 1]!) : G.neighbors[e] ∈ G.nbrs i

Reading a packed entry in a row supplies an actual neighbour.

theorem Hex.SparseGraph.mem_edge {n : Nat} (G : SparseGraph n) {i v : Fin n} (hv : v ∈ G.nbrs i) : ∃ (e : Nat), G.offsets[↑i]! ≤ e ∧ e < G.offsets[↑i + 1]! ∧ G.neighbors[e]? = some v

Every row member is reached by a cursor of the adjacency loop.

def Hex.GraphIso.Nauty.Sparse.Graph.Valid {n : Nat} (g : Graph n) : Prop

Valid input views are precisely native simple sparse graphs.

Equations

• g.Valid = ∃ (G : Hex.SparseGraph n), g = Hex.GraphIso.Nauty.Sparse.Graph.ofGraph G

theorem Hex.GraphIso.Nauty.Sparse.Graph.valid_ofGraph {n : Nat} (G : SparseGraph n) : (ofGraph G).Valid

theorem Hex.GraphIso.Nauty.Sparse.Graph.neighbor_lt {n : Nat} (G : SparseGraph n) (i : Fin n) {e : Nat} (he : e < G.offsets[↑i + 1]!) : (ofGraph G).neighbor e < n

structure Hex.GraphIso.Nauty.Sparse.Rows.Prefix {n : Nat} (R : Rows n) (G : SparseGraph n) (count : Nat) : Prop

A partially installed canonical graph. Only its first count rows and their offsets describe G; the remaining entries are allocated scratch. Rows retain their unsorted nauty order, so row correctness is a permutation.

• count_le : count ≤ n
• offsets_size : R.offsets.size = n + 1
• neighbors_size : R.neighbors.size = G.neighbors.size
• offsets_eq (i : Nat) : i ≤ count → R.offsets[i]! = G.offsets[i]!
• rows_perm (i : Fin n) : ↑i < count → (SparseGraph.row R.offsets R.neighbors ↑i).toList.Perm (List.map Fin.val (G.nbrs i).toList)

theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.mono {n : Nat} {R : Rows n} {G : SparseGraph n} {count small : Nat} (h : R.Prefix G count) (hs : small ≤ count) : R.Prefix G small

theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.offset_le {n : Nat} {R : Rows n} {G : SparseGraph n} {count i : Nat} (h : R.Prefix G count) (hi : i ≤ count) : R.offsets[i]! ≤ R.neighbors.size

theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.degree_eq {n : Nat} {R : Rows n} {G : SparseGraph n} {count : Nat} (h : R.Prefix G count) (i : Fin n) (hi : ↑i < count) : R.degree ↑i = G.degree i

theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.mem_iff {n : Nat} {R : Rows n} {G : SparseGraph n} {count : Nat} (h : R.Prefix G count) (i v : Fin n) (hi : ↑i < count) : ↑v ∈ SparseGraph.row R.offsets R.neighbors ↑i ↔ G.adj i v = true

Membership in an installed row agrees with the canonical graph.

theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.entry_lt {n : Nat} {R : Rows n} {G : SparseGraph n} {count e : Nat} (h : R.Prefix G count) (i : Fin n) (hi : ↑i < count) (hlo : R.offsets[↑i]! ≤ e) (hhi : e < R.offsets[↑i + 1]!) : R.neighbors[e]! < n

An entry of an installed row is a vertex, even though the store is raw.

theorem Hex.GraphIso.Nauty.Sparse.Rows.Prefix.blank {n : Nat} (G : SparseGraph n) : (Graph.ofGraph G).blank.Prefix G 0