structure Hex.GraphIso.Nauty.Sparse.Rows (n : Nat) : Type

Canonical rows retain nauty's unsorted neighbour order until the public result is constructed.

• offsets : Array Nat
• neighbors : Array Nat

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instInhabitedRows {a✝ : Nat} : Inhabited (Rows a✝)

Equations

• Hex.GraphIso.Nauty.Sparse.instInhabitedRows = { default := Hex.GraphIso.Nauty.Sparse.instInhabitedRows.default }

def Hex.GraphIso.Nauty.Sparse.instReprRows.repr {n✝ : Nat} : Rows n✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instReprRows {n✝ : Nat} : Repr (Rows n✝)

Equations

• Hex.GraphIso.Nauty.Sparse.instReprRows = { reprPrec := Hex.GraphIso.Nauty.Sparse.instReprRows.repr }

structure Hex.GraphIso.Nauty.Sparse.Graph (n : Nat) : Type

A view of native compressed adjacency, sharing its existing arrays.

• offsets : Array Nat
• neighbors : Array (Fin n)

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instInhabitedGraph {a✝ : Nat} : Inhabited (Graph a✝)

Equations

• Hex.GraphIso.Nauty.Sparse.instInhabitedGraph = { default := Hex.GraphIso.Nauty.Sparse.instInhabitedGraph.default }

def Hex.GraphIso.Nauty.Sparse.instReprGraph.repr {n✝ : Nat} : Graph n✝ → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instReprGraph {n✝ : Nat} : Repr (Graph n✝)

Equations

• Hex.GraphIso.Nauty.Sparse.instReprGraph = { reprPrec := Hex.GraphIso.Nauty.Sparse.instReprGraph.repr }

def Hex.GraphIso.Nauty.Sparse.Rows.degree {n : Nat} (G : Rows n) (v : Nat) : Nat

Equations

• G.degree v = G.offsets[v + 1]! - G.offsets[v]!

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

Equations

• Hex.GraphIso.Nauty.Sparse.Graph.ofGraph G = { offsets := G.offsets, neighbors := G.neighbors }

@[inline]

def Hex.GraphIso.Nauty.Sparse.Graph.neighbor {n : Nat} (G : Graph n) (i : Nat) : Nat

Fin proofs are erased; reading a native entry requires no converted adjacency array or runtime vertex wrapper.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.Graph.neighbor_ofGraph {n : Nat} (G : SparseGraph n) (i : Nat) (h : i < G.neighbors.size) : (ofGraph G).neighbor i = ↑G.neighbors[i]

def Hex.GraphIso.Nauty.Sparse.Graph.degree {n : Nat} (G : Graph n) (v : Nat) : Nat

Equations

• G.degree v = G.offsets[v + 1]! - G.offsets[v]!

def Hex.GraphIso.Nauty.Sparse.Graph.blank {n : Nat} (G : Graph n) : Rows n

Allocate the canonical store once, before the search.

Equations

• G.blank = { offsets := Array.replicate (n + 1) 0, neighbors := Array.replicate G.neighbors.size 0 }

def Hex.GraphIso.Nauty.Sparse.inverse (n : Nat) (lab : Array Nat) : Array Nat

nausparse's INVLAB scatter.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.isautom {n : Nat} (g : Graph n) (p : Array Nat) : Bool

isautom_sg: compare degrees and marked image neighbours, skipping fixed vertices in the undirected configuration.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.updatecan {n : Nat} (g : Graph n) (canong : Rows n) (lab : Array Nat) (samerows : Nat) : Rows n

updatecan_sg: retain the shared prefix and rewrite the remaining contiguous rows using inverse labels. No row sorting occurs in the search.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.testcanlab {n : Nat} (g : Graph n) (canong : Rows n) (lab : Array Nat) : Int × Nat

testcanlab_sg: smaller degree is preferred, then adjacency at the first differing vertex. Return the comparison and the equal row prefix.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.distvals {n : Nat} (g : Graph n) (root : Nat) : Array Nat

distvals: breadth-first distances, with n for unreachable vertices. The queue stores each vertex once, so n iterations suffice.

Equations

• One or more equations did not get rendered due to their size.