Section 3 — Euler charge conservation and a positive face

Proved

FourColor.charge_conservation

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

four-color-theoremgraph-theory

Let $H$ be planar, plain and cubic. For any rational dart-transfer function $w:D\to\mathbb Q$ , define the charge of the face containing $d$ by

q_w(d)=60-10a(d)+\sum_{y\sim_f d}\bigl(w(e(y))-w(y)\bigr).

Then, with $C$ the number of components,

\sum_{d\in D}\frac{q_w(d)}{a(d)}=120C.

If $H$ is connected, some dart lies on a positive-charge face:

\exists d\in D,\quad 0<q_w(d).

Each face orbit contains its own dart, so $a(d)>0$ . The weighted dart sum counts each face charge once, avoiding arbitrary representative choices. The empty hypermap has total charge zero and fails the connectedness premise.

Formalization note: source-derived generalization of integer rule-count conservation to arbitrary rational transfers and disconnected maps. It proves conservation only; no claim about the adequacy of any fixed discharge rules or the occurrence of a reducible configuration is hidden in it.

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 3, PDF p. 9, paragraph on PDF p. 9 defining discharging and its unnumbered charge formula; Section 5.5, PDF pp. 44–48. Relevant displays are unnumbered. Pinned executable reference: https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/geometry.v#L617; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/discharge.v#L167; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/discharge.v#L201.

Preamble

import Definitions.Def_FourColor_Discharging

Formal statement

namespace FourColor
universe u
theorem charge_conservation :
  ∀ (n : ℕ) (H : Hypermap n), H.Planar → H.Plain → H.Cubic →
    ∀ transfer : Fin n → ℚ,
      H.totalFaceCharge transfer = 120 * (H.componentCount : ℚ) ∧
        (H.Connected → ∃ x : Fin n, 0 < H.faceCharge transfer x) := 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 3, PDF p. 9, paragraph on PDF p. 9 defining discharging and its unnumbered charge formula; Section 5.5, PDF pp. 44–48. Relevant displays are unnumbered. Pinned executable reference: https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/geometry.v#L617; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/discharge.v#L167; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/discharge.v#L201.

Read-back

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

ChargeConservation. 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$ . For a permutation $\sigma$ , a cycle is a class for $x\sim_\sigma y\iff\exists j\in\mathbb Z,\ \sigma^j(x)=y$ , using inverse powers for negative $j$ . Let $E,N,F$ count the cycles of $e,\nu,\phi$ , and let $C$ count the classes of the equivalence relation generated by $(x,e(x))$ , $(x,\nu(x))$ , and $(x,\phi(x))$ , allowing reflexivity, symmetry, and transitivity. Write $F_x=\{y\in D_n:\exists j\in\mathbb Z,\ \phi^j(x)=y\}$ and $a_x=|F_x|$ , using inverse powers for negative $j$ . The proposition says that if $E+N+F=n+2C$ , every $x\in D_n$ satisfies $e(e(x))=x$ and $e(x)\ne x$ , and every $\nu$ -cycle has exactly three elements, then for every function $t:D_n\to\mathbb Q$ the following conjunction holds. Set $q_t(x)=60-10a_x+\sum_{y\in F_x}(t(e(y))-t(y))$ , with $a_x$ converted to a rational number. Then $\sum_{x\in D_n}q_t(x)/a_x=120C$ , with $a_x$ and $C$ converted to rational numbers; and, if $C=1$ , there exists $x\in D_n$ with $q_t(x)>0$ . The values of $t$ have no sign or size restriction. There is no hypothesis excluding a dart and its edge image from sharing a face cycle, and connectedness is required only in the conditional second conclusion. Each denominator in an existing summand is positive because $x\in F_x$ . For $n=0$ all premises hold, the sum and $120C$ are zero, and the conditional positive-charge conclusion has false antecedent $C=1$ .

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