structure Hex.GraphIso.Nauty.Sparse.RowRep {n : Nat} (read : Nat → Nat) (lo hi : Nat) (row : List (Fin n)) : Prop

A packed interval enumerates one normalized row, in arbitrary order.

• le : lo ≤ hi
• perm : (List.map read (List.range' lo (hi - lo))).Perm (List.map Fin.val row)

theorem Hex.GraphIso.Nauty.Sparse.RowRep.length {n : Nat} {read : Nat → Nat} {lo hi : Nat} {row : List (Fin n)} (h : RowRep read lo hi row) : row.length = hi - lo

theorem Hex.GraphIso.Nauty.Sparse.RowRep.mem_iff {n : Nat} {read : Nat → Nat} {lo hi : Nat} {row : List (Fin n)} (h : RowRep read lo hi row) (v : Nat) : (∃ (e : Nat), lo ≤ e ∧ e < hi ∧ read e = v) ↔ v ∈ List.map Fin.val row

theorem Hex.GraphIso.Nauty.Sparse.RowRep.bound {n : Nat} {read : Nat → Nat} {lo hi : Nat} {row : List (Fin n)} (h : RowRep read lo hi row) {e : Nat} (hlo : lo ≤ e) (hhi : e < hi) : read e < n

theorem Hex.GraphIso.Nauty.Sparse.RowRep.injective {n : Nat} {read : Nat → Nat} {lo hi : Nat} {row : List (Fin n)} (h : RowRep read lo hi row) (hs : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) row) {a b : Nat} (ha : lo ≤ a) (ha' : a < hi) (hb : lo ≤ b) (hb' : b < hi) (he : read a = read b) : a = b

theorem Hex.GraphIso.Nauty.Sparse.RowRep.stored {n : Nat} {R : Rows n} {H : SparseGraph n} (h : R.Prefix H n) (i : Fin n) : RowRep (fun (e : Nat) => R.neighbors[e]!) R.offsets[↑i]! R.offsets[↑i + 1]! (H.nbrs i).toList

The canonical store's raw row has the represented row's members and degree.

theorem Hex.GraphIso.Nauty.Sparse.RowRep.candidate {n : Nat} (G : SparseGraph n) {lab : Array Nat} {l : Label n} (hl : Label.ofArray? n lab = some l) (i : Fin n) : RowRep (fun (e : Nat) => (inverse n lab)[(Graph.ofGraph G).neighbor e]!) G.offsets[lab[↑i]!]! G.offsets[lab[↑i]! + 1]! ((G.relabel l.perm).nbrs i).toList

The candidate scan enumerates exactly its native relabelled row.