Clique and odd-cycle surgery

Abstract

Rabern surgery colors a regular graph after deleting a maximal independent set whose induced complement exhibits a clique or an odd cycle.

In the formula, card denotes Fintype.card and ComplSubtype(A) is the subtype of vertices outside A. The quantified graph H in the induction hypothesis ranges over the same arbitrary vertex universe as G. Membership(A) denotes the predicate of belonging to A. IsContained is the native adjacency-preserving copy relation.

Theorem 1.1 (The surgery step).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)]\forall G\in \mathrm{SimpleGraph}\left(V\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall d\in \mathrm{Nat},\forall k\in \mathrm{Nat},\forall A\in \mathrm{Set}\left(V\right),[\mathrm{DecidablePred}\left(\mathrm{Membership}\left(A\right)\right)][\mathrm{Nonempty}\left(\mathrm{ComplSubtype}\left(A\right)\right)]\left(d=\mathrm{maxDegree}\left(G\right)\wedge \left(3\le d\wedge \left(\mathrm{CliqueFree}\left(G,d+1\right)\wedge \left(\left(\neg \mathrm{IsContained}\left(\mathrm{cliqueMinusEdge}\left(d-1\right),G\right)\right)\wedge \left(\mathrm{IsRegularOfDegree}\left(G,d\right)\wedge \left(\mathrm{Maximal}\left(\mathrm{IsIndepSet}\left(G\right),A\right)\wedge \left(\mathrm{maxDegree}\left(\mathrm{Induce}\left(G,\mathrm{Compl}\left(A\right)\right)\right)=d-1\wedge \left(\mathrm{card}\left(V\right)\le k+1\wedge \left(\mathrm{card}\left(\mathrm{ComplSubtype}\left(A\right)\right)\le k\wedge \left(\left(\left(\neg \mathrm{CliqueFree}\left(\mathrm{Induce}\left(G,\mathrm{Compl}\left(A\right)\right),d\right)\right)\vee \left(\mathrm{maxDegree}\left(\mathrm{Induce}\left(G,\mathrm{Compl}\left(A\right)\right)\right)=2\wedge \mathrm{HasOddCycle}\left(\mathrm{Induce}\left(G,\mathrm{Compl}\left(A\right)\right)\right)\right)\right)\wedge \left(\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)]\forall H\in \mathrm{SimpleGraph}\left(W\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(H\right)\right)]\mathrm{card}\left(W\right)\le k\Rightarrow \left(\mathrm{CliqueFree}\left(H,\mathrm{maxDegree}\left(H\right)+1\right)\Rightarrow \left(\left(\mathrm{maxDegree}\left(H\right)=2\Rightarrow \left(\neg \mathrm{HasOddCycle}\left(H\right)\right)\right)\Rightarrow \mathrm{Colorable}\left(H,\mathrm{maxDegree}\left(H\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{Colorable}\left(G,d\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/Brooks/Surgery.brooksSurgery (✓ std3). ∎

Citation. Landon Rabern (2023). Yet another proof of Brooks’ theorem. DOI: 10.1016/j.disc.2022.113261. URL: https://github.com/brianrabern/BrooksLean/tree/1d990050d881327fc79dd51e82ba4449b4e2467d.

Commentary.

Each vertex in the obstruction has one neighbor in the deleted independent set. Adjacent vertices with different such neighbors determine an edge to add to the smaller graph. Its coloring forces different colors at those two neighbors. A clique then admits a Hall coloring avoiding the prescribed colors. For a longer odd cycle, choose a spanning path, assign the first vertex the last outside-neighbor color, and extend along the path. At the final vertex two neighbors share a color, leaving a free color. A three-cycle uses the clique construction.

References

• Truth anchor: D5/S3/Combinatorics/Graph/Brooks/Surgery.brooksSurgery
• Dependency: D5/S3/Combinatorics/Graph/Brooks/CliqueExtension