Residue

The residue of a graph is the number of zeros remaining after iteratively applying the Havel-Hakimi algorithm to the degree sequence until all remaining degrees are zero.

def SimpleGraph.havelHakimiStep (s : List ℕ) : List ℕ

Helper function: Performs one step of the Havel-Hakimi reduction on a degree sequence. Assumes the input list s is sorted descending. Removes the first element d, decrements the next d elements by 1, and re-sorts the list descending.

Note: when s is the list of vertices arising from a simple graph, if the first index is s then the degree list always has length at least s+1 so this makes sense.

Equations

• One or more equations did not get rendered due to their size.
• SimpleGraph.havelHakimiStep [] = []

theorem SimpleGraph.havelHakimiStep_length_cons (d : ℕ) (rest : List ℕ) : (havelHakimiStep (d :: rest)).length = rest.length

havelHakimiStep drops the list length by exactly one on a nonempty list: (havelHakimiStep (d :: rest)).length = rest.length. splitAt partitions rest, and map, ++, and mergeSort all preserve the total length while the head d is dropped. This is the termination measure for the well-founded residueAux below.

@[irreducible]

def SimpleGraph.residueAux : List ℕ → ℕ

Auxiliary function to calculate the residue recursively. Applies Havel-Hakimi steps until the sequence consists only of zeros or is empty. Defined by well-founded recursion on the list length (via havelHakimiStep_length_cons), so that it admits equational and inductive reasoning.

Equations

• SimpleGraph.residueAux [] = 0
• SimpleGraph.residueAux (0 :: s) = 1 + s.length
• SimpleGraph.residueAux (d :: rest) = SimpleGraph.residueAux (SimpleGraph.havelHakimiStep (d :: rest))

noncomputable def SimpleGraph.residue {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℕ

Computes the residue of a graph G, i.e. the number of zeros remaining after iteratively applying the Havel-Hakimi algorithm to the degree sequence until all remaining degrees are zero. Starts with the descending degree sequence and applies the Havel-Hakimi process.

Equations

• G.residue = SimpleGraph.residueAux ((Multiset.map (fun (v : α) => G.degree v) Finset.univ.val).sort fun (x1 x2 : ℕ) => x1 ≥ x2)