Section 5.1 — Sixfold cubic normalization

Proved

FourColor.cubic_normalization

by Minghui · Sep 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

four-color-theoremgraph-theory

For every finite hypermap $H$ on $n$ darts, there is a hypermap $Q$ on exactly $6n$ darts that is plain and cubic, such that

\operatorname{Planar}(Q)\iff\operatorname{Planar}(H),\qquad \operatorname{Bridgeless}(Q)\iff\operatorname{Bridgeless}(H),

and every existence proof of a four-coloring of $Q$ gives a four-coloring of $H$ . No planarity or bridgelessness assumption is needed to construct $Q$ ; these properties are preserved in both directions. The case $n=0$ is included.

Formalization note: source-derived existential interface to the actual six-tag cubification construction, corresponding to plain_cube, cubic_cube, planar_cube, bridgeless_cube and cube_colorable. The internal data structure may be Lean-native, but the count and preservation conclusions are fixed.

Notation: $D=\{0,\ldots,n-1\}$ is the dart set, $n = |D|$ its size, and $p = \nu_H$ is the node permutation. Write $e,f$ for the edge and face permutations, with $p(f(e(d)))=d$ . Edge, node and face counts $E,N,F$ are numbers of permutation orbits, including singleton orbits. The component count $C$ uses the equivalence generated by all three permutations. Planarity means the exact Euler equality $E+N+F=n+2C$ , and connectedness means $C=1$ .

A plain hypermap has a fixed-point-free involution $e$ . Cubic means every node orbit has size three; precubic means every node orbit has size at most three. Bridgeless means $d$ and $e(d)$ never lie in the same face orbit. A $k$ -coloring is a map $D\to\{0,\ldots,k-1\}$ constant on face orbits and different across each edge step. No requirement uses all available colors. The empty dart set has zero components, is planar, and is colorable, but is not connected.

An admissible hypermap is planar, bridgeless, plain and precubic. A minimal counterexample is a non-four-colorable admissible hypermap such that every admissible hypermap with fewer darts is four-colorable. Minimality includes all finite carriers through their enumeration by $\operatorname{Fin}(m)$ ; cubicity, connectedness and lower face-degree bounds are not assumed.

Source: Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem (2005), https://www.microsoft.com/en-us/research/wp-content/uploads/2012/10/4colproof.pdf; Section 5.1, PDF p. 26, paragraph on PDF p. 26 describing cubification; Section 3, PDF p. 6, cubic-map reduction. Relevant displays are unnumbered. Pinned executable reference: https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/cube.v#L44; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/cube.v#L89.

Preamble

import Definitions.Def_FourColor_Hypermap

Formal statement

namespace FourColor
universe u
theorem cubic_normalization :
  ∀ (n : ℕ) (H : Hypermap n), ∃ K : Hypermap (6 * n),
    K.Plain ∧ K.Cubic ∧ (K.Planar ↔ H.Planar) ∧
      (K.Bridgeless ↔ H.Bridgeless) ∧ (K.FourColorable → H.FourColorable) := by sorry
end FourColor

Source

Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem (2005), https://www.microsoft.com/en-us/research/wp-content/uploads/2012/10/4colproof.pdf; Section 5.1, PDF p. 26, paragraph on PDF p. 26 describing cubification; Section 3, PDF p. 6, cubic-map reduction. Relevant displays are unnumbered. Pinned executable reference: https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/cube.v#L44; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/cube.v#L89.

Read-back

What the Lean code literally says, in plain math · gpt-6

CubicNormalization. Let $n\in\mathbb N$ , $D_n=\{0,\ldots,n-1\}$ (empty if $n=0$ ), and let $H=(e,\nu,\phi)$ be three permutations of $D_n$ with $\nu(\phi(e(x)))=x$ for every $x\in D_n$ . The proposition asserts the existence of permutations $e_K,\nu_K,\phi_K$ of $D_{6n}=\{0,\ldots,6n-1\}$ with $\nu_K(\phi_K(e_K(x)))=x$ for all $x$ , such that all of the following hold. Every $x\in D_{6n}$ satisfies $e_K(e_K(x))=x$ and $e_K(x)\ne x$ , and every $\nu_K$ -cycle has exactly three elements. For each triple $J=H,K$ , set $d_H=n$ , $d_K=6n$ ; let $E_J,N_J,F_J$ count its edge, node, and face cycles, where a $\sigma$ -cycle uses $\exists j\in\mathbb Z,\ \sigma^j(x)=y$ ; and let $C_J$ count the classes of the equivalence relation generated by its edge, node, and face permutation steps. Then $E_K+N_K+F_K=6n+2C_K$ if and only if $E_H+N_H+F_H=n+2C_H$ . Also $(\forall x\in D_{6n},\ \neg\exists j\in\mathbb Z,\ \phi_K^j(x)=e_K(x))$ if and only if $(\forall x\in D_n,\ \neg\exists j\in\mathbb Z,\ \phi^j(x)=e(x))$ . Finally, if there exists $c_K:D_{6n}\to\{0,1,2,3\}$ constant on each $\phi_K$ -cycle with $c_K(e_K(x))\ne c_K(x)$ for every $x$ , then there exists $c_H:D_n\to\{0,1,2,3\}$ constant on each $\phi$ -cycle with $c_H(e(x))\ne c_H(x)$ for every $x$ . There is no converse coloring implication, no requirement to use all four colors, and no map between the two dart sets is specified. There is no additional hypothesis on the input triple. Negative powers use inverses, and generated equivalence allows reflexivity, symmetry, and transitivity. If $n=0$ , both dart sets are empty, all counts are zero, the universal dart conditions are vacuous, and empty colorings exist.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph