def Hex.GraphIso.Nauty.Sparse.Compare.row {n : Nat} (G : SparseGraph n) (i : Nat) : List (Fin n)

A row of the canonical sparse key, with an empty default beyond its order.

Equations

• Hex.GraphIso.Nauty.Sparse.Compare.row G i = (Hex.GraphIso.Nauty.Sparse.graphRows G)[i]!

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.Compare.row_fin {n : Nat} (G : SparseGraph n) (i : Fin n) : row G ↑i = (G.nbrs i).toList

structure Hex.GraphIso.Nauty.Sparse.Compare.Result {n : Nat} (A B : SparseGraph n) (r : Int × Nat) : Prop

The comparison reports precisely the first differing row, or all rows when equal; its sign is the sparse row order at that position.

• bound : r.snd ≤ n
• agrees (i : Nat) : i < r.snd → row A i = row B i
• terminal : r.snd = n → r.fst = 0
• first (i : Nat) : i < n → i = r.snd → r.fst = ordInt (rowCmp (row A i) (row B i)) ∧ rowCmp (row A i) (row B i) ≠ Ordering.eq

theorem Hex.GraphIso.Nauty.Sparse.Compare.stop {n : Nat} {A B : SparseGraph n} {i : Nat} {c : Ordering} (hi : i < n) (hp : ∀ (j : Nat), j < i → row A j = row B j) (hc : rowCmp (row A i) (row B i) = c) (hn : c ≠ Ordering.eq) : Result A B (ordInt c, i)

theorem Hex.GraphIso.Nauty.Sparse.Compare.finish {n : Nat} {A B : SparseGraph n} (hp : ∀ (j : Nat), j < n → row A j = row B j) : Result A B (0, n)

theorem Hex.GraphIso.Nauty.Sparse.testcanlab_result {n : Nat} (G H : SparseGraph n) (R : Rows n) (lab : Array Nat) (l : Label n) (hl : Label.ofArray? n lab = some l) (hR : R.Prefix H n) : Compare.Result (G.relabel l.perm) H (testcanlab (Graph.ofGraph G) R lab)

The executed sparse comparison identifies the first unequal canonical row.