theorem
Hex.GraphIso.Nauty.Sparse.Rows.Prefix.congr
{n : Nat}
{R S : Rows n}
{H : SparseGraph n}
{count : Nat}
(h : R.Prefix H count)
(ho : S.offsets.size = R.offsets.size)
(hn : S.neighbors.size = R.neighbors.size)
(he : ∀ (i : Nat), i ≤ count → S.offsets[i]! = R.offsets[i]!)
(hv : ∀ (e : Nat), e < H.offsets[count]! → S.neighbors[e]! = R.neighbors[e]!)
:
S.Prefix H count
Changing uninstalled entries does not change the installed rows.
theorem
Hex.GraphIso.Nauty.Sparse.updatecan_prefix
{n : Nat}
(g : Graph n)
(H : SparseGraph n)
(R : Rows n)
(lab : Array Nat)
(same : Nat)
(hR : R.Prefix H same)
(hrow :
∀ (i : Fin n),
(List.map (fun (e : Nat) => (inverse n lab)[g.neighbor e]!)
(List.range' g.offsets[lab[↑i]!]! (g.offsets[lab[↑i]! + 1]! - g.offsets[lab[↑i]!]!))).Perm
(List.map Fin.val (H.nbrs i).toList))
:
Install the remaining rows when each source row, after inverse scatter, is a permutation of the corresponding normalized target row.
theorem
Hex.GraphIso.Nauty.Sparse.source_row
{n : Nat}
(G : SparseGraph n)
(lab : Array Nat)
(l : Label n)
(hl : Label.ofArray? n lab = some l)
(i : Fin n)
:
The executed source-row scan emits inverse-labelled neighbours.
theorem
Hex.GraphIso.Nauty.Sparse.updatecan_relabel
{n : Nat}
(G : SparseGraph n)
(R : Rows n)
(lab : Array Nat)
(l : Label n)
(same : Nat)
(hl : Label.ofArray? n lab = some l)
(hR : R.Prefix (G.relabel l.perm) same)
:
(updatecan (Graph.ofGraph G) R lab same).Prefix (G.relabel l.perm) n
The exact canonical installation represents native relabelling, even when its retained prefix and copied rows use different neighbour orders.
theorem
Hex.GraphIso.Nauty.Sparse.updatecan_blank
{n : Nat}
(G : SparseGraph n)
(lab : Array Nat)
(l : Label n)
(hl : Label.ofArray? n lab = some l)
:
(updatecan (Graph.ofGraph G) (Graph.ofGraph G).blank lab 0).Prefix (G.relabel l.perm) n
The initial canonical allocation suffices for every checked label.