Reducible Configurations and Unavoidable Sets

The Two Tasks in a Four-Color Proof

The four-color theorem concerns coloring vertices so that adjacent vertices receive different colors. Its proof architecture is striking because it separates a global existence argument into two finite-looking tasks: show that some local configuration must occur, then show that each configuration on a specified list is incompatible with a smallest counterexample. Discharging addresses the first task; reducibility addresses the second.

A proper 4-coloring assigns each vertex one of four colors so that the endpoints of every edge have different colors. A graph is planar if it can be drawn in the plane without edge crossings; a particular crossing-free drawing is a plane graph. The drawing matters when we talk about the faces around a configuration, but the coloring condition is about the graph.

The four-color theorem is already known here as a result. The goal is to understand the structure behind its proof, not to reproduce the substantial finite verification required for the full theorem. The key logical pattern can nevertheless be stated and justified precisely.

Minimal Counterexamples and Reducibility

Suppose, for contradiction, that a loopless planar graph cannot be colored with four colors. Since it has finitely many vertices, among all such counterexamples choose one with the fewest vertices. This is a minimal counterexample. If a local part can be deleted, the remaining graph has fewer vertices and so must be 4-colorable. A reducibility argument shows that this coloring can be completed across the deleted part, contradicting the choice of the graph.

The boundary condition is important: after deleting the interior, the boundary vertices remain colored, and every edge from the interior to the outside must meet the boundary. To apply the definition, one must prove extension for every boundary coloring that can arise, not merely for a convenient coloring. In full four-color proofs, some configurations are treated by reducing or modifying the configuration before lifting a coloring back. The extension form captures the basic logic; it is not a claim that every technical reducibility check has this simplest form.

Proof. Suppose a minimal counterexample \(G\) contains such a configuration, and let \(I\) be its nonempty set of interior vertices. Delete \(I\), retaining the boundary and all vertices outside the configuration. The resulting graph is loopless and planar, and has fewer vertices than \(G\), so minimality says it has a proper 4-coloring. The colors on the boundary are one of the boundary colorings covered by reducibility. By the extension property, this coloring extends to the interior. Together the coloring outside and inside gives a proper 4-coloring of \(G\), contradicting that \(G\) is a counterexample. Hence no such configuration occurs. \(\square\)

The same argument works for a vertex with at most three neighbors in any graph: after deleting it, at most three colors are forbidden. It does not automatically work for four neighbors, since all four colors might appear around the deleted vertex.

Unavoidable Sets and Discharging

A triangulation is a plane graph in which every face is bounded by a triangle. The proof architecture reduces attention to triangulations: a simple planar graph can be augmented, by adding edges without adding vertices, to a maximal simple planar graph, and for at least three vertices a maximal simple planar graph is a triangulation. This is a standard fact about maximal planar graphs. A 4-coloring of the augmented graph also colors the original graph, since deleting the added edges cannot invalidate a coloring.

Unavoidability is established by discharging. Assign an initial numerical charge to vertices, faces, or both. Then prescribe local transfers of charge. Each transfer subtracts exactly what it adds elsewhere, so the total charge is preserved. The rules are chosen so that if none of the listed configurations occurs, the final charges would violate a bound or a local constraint. Therefore at least one listed configuration must occur.

For a triangulation with \(n\ge3\) vertices, Euler’s formula on the sphere is \(n-m+f=2\), where \(m\) is the number of edges and \(f\) the number of faces. Each face has three incident edges and each edge is incident with two face-sides, so \(3f=2m\). Substitution gives \(n-m+2m/3=2\), hence \(m=3n-6\). The handshake lemma gives \(\sum_{v\in V}\deg(v)=2m\). Consequently the vertex charges \(6-\deg(v)\) have total 12:

This fixed total is a starting point, not a complete discharging proof. A useful discharging argument specifies its rules, checks that the total remains 12, and then analyzes the final charge in the absence of each proposed local pattern. Merely knowing the total does not identify which configuration occurs.

A minimal counterexample cannot have a vertex of degree at most three, by the extension argument above. The charge identity also implies that some vertex has degree at most five: if every degree were at least six, then every charge \(6-\deg(v)\) would be nonpositive, contradicting the total charge 12. These observations restrict the local patterns that need attention, but they do not by themselves prove the four-color theorem. A degree-five vertex, for example, is not automatically reducible.

How the Two Parts Fit Together

The central logical implication can be expressed without performing the large finite checks. Suppose \(\mathcal{U}\) is an unavoidable set of configurations for the class containing every possible minimal counterexample, and suppose every member of \(\mathcal{U}\) is reducible in a way that rules out its occurrence in such a counterexample. Then no minimal counterexample exists.

Proof. Assume a counterexample exists, and choose one, \(G\), with the fewest vertices. Replacing each set of parallel edges by a single edge does not change which colorings are proper, so we may take \(G\) simple. Augment \(G\) to a maximal simple planar graph \(G^+\) on the same vertex set. Any proper 4-coloring of \(G^+\) is a proper 4-coloring of \(G\), so \(G^+\) is also not 4-colorable. It has the same number of vertices as \(G\), so it is also a counterexample with the fewest vertices. It is a triangulation, since \(G\) has at least four vertices (every graph on at most four vertices is 4-colorable). Hence \(G^+\) is a minimal counterexample belonging to the class for which \(\mathcal{U}\) is unavoidable, and it contains some member of \(\mathcal{U}\). By the assumed reducibility of that member, a minimal counterexample cannot contain it. These conclusions contradict one another. Hence no minimal counterexample exists, and every loopless planar graph is 4-colorable. \(\square\)

In the actual proof architecture, the unavoidability argument comes from discharging and the reducibility argument consists of separate local verifications. Neither part can be omitted: a list of reducible patterns is not enough unless every relevant triangulation contains one, and an unavoidable list is not enough unless each listed pattern can be excluded from a minimal counterexample. The next subject examines how computer-assisted proofs carry out extensive finite verification; no details of that verification are needed to understand this division of roles.

Common Pitfalls

Confusing “unavoidable” with “reducible.” Unavoidable means every graph in the chosen class contains at least one listed pattern. Reducible means that a pattern cannot occur in a minimal counterexample under the relevant extension or reduction argument. One property does not imply the other.

Using the degree-five conclusion as a proof. The charge identity forces positive charge somewhere and, in particular, a vertex of degree at most five. It does not say that every such vertex can be removed and recolored. Extra local structure is what configurations record.

Forgetting the loopless hypothesis. A loop cannot be properly colored under the usual definition, because its two endpoints are the same vertex. State the four-color theorem for loopless planar graphs, or restrict to simple planar graphs, rather than silently including graphs with loops.