@[macro_inline]

def Hex.GraphIso.Nauty.Sparse.CountSort.firstRun (lab hits : Array Nat) (first last : Nat) : Nat

End of the initial run having the first vertex's count.

Equations

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

@[macro_inline]

def Hex.GraphIso.Nauty.Sparse.CountSort.minima (lab hits : Array Nat) (cap first last begin : Nat) : Nat × Nat × Nat × Nat × Array Nat

Partition the cell around its two smallest counts using nauty's exact three-way insertion. Return the two counts, their run boundaries, and labels.

Equations

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

@[inline]

def Hex.GraphIso.Nauty.Sparse.CountSort.finish {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (w1 v2 w2 v3 : Nat) : RefineSt n

Install the first two count fragments, sort the larger-count tail, and activate all but the largest inactive fragment. Distance splitting has its own hash updates but uses the same ordering and activation rules.

Equations

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

def Hex.GraphIso.Nauty.Sparse.splitCounts {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) : RefineSt n

Divide one cell by counts or distances. The first two minimum fragments use nauty's three-way insertion; later fragments use its exact indirect sort. distance selects the distinct distance-branch code updates.

Equations

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