Orientation reversal preserves minimal counterexamples

For every finite hypermap $H$, if $H$ is a minimal counterexample, then its explicitly defined mirror is also a minimal counterexample. Preserve all admissibility conditions, noncolorability, and the same smaller-dart comparison class. Formalization note: direct source mirror theorem translated to the existing Lean minimality definition.

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.

The fixed catalogue $\mathcal C$ is the ordered list of all 633 literal configuration maps, boundary rings, and selected contracts, decoded from the pinned source. It is shared by reducibility and coverage; it is not an arbitrary or existentially chosen family. The table checker establishes array sizes, index bounds, and inverse/triangle identities only.

For a configuration $A$, let $R_A$ be its ordered boundary ring, $K_A$ the darts whose faces avoid that ring, and $S_A$ the list containing both darts of every selected contract edge. Geometric admissibility means that the map is planar, bridgeless, plain and connected; $R_A$ is a nonempty node cycle meeting each face at most once; off-ring nodes have arity three; ring faces have arity 3–6; and there is a kernel face having a common adjacent kernel face with every kernel face. Contract validity means that $S_A$ avoids $R_A$, its darts lie in pairwise distinct node orbits, the contract has 1–4 edges, and a four-edge contract has the source's kernel triad (more than two incident selected-face darts and not every selected face adjacent).

Colors are the Klein-four group $\{0,1,2,3\}$, with bitwise XOR as addition. A boundary trace records sums of consecutive face colors around the reversed ring, including the closing pair. Ordinary traces arise from proper face colorings. Contract traces arise from face-constant colorings with equal colors across exactly the edges selected by $S_A$. A trace set is Kempe-closed if it is closed under all permutations fixing zero and, for each member, contains every trace matching some compatible four-symbol noncrossing-chord word. The stack matcher rejects zero colors and requires an empty final stack. Coclosure of a set consists of traces whose every containing Kempe-closed set meets that set. C-reducibility means contract validity and inclusion of all contract traces in the coclosure of the ordinary traces.

An occurrence of $A$ in $H$ requires geometric admissibility of $A$ and a map of its darts into $H$ preserving face steps and exact face arities on $K_A$. Every kernel face must contain an edge-preserving dart; such darts obey the explicit ring-link path condition in the definition. A total injective map of all permutations is not required. Occurrence up to reflection means occurrence in $H$ or in its mirror, whose edge, node and face maps are respectively $f\circ p$, $p^{-1}$ and $f^{-1}$.

The concrete transfer $t_H(y)$ counts, with multiplicity, matches of the 71 symmetrized source patterns at $f^{-2}(y)$. Their 38 base entries include repeated entries implementing larger transfers. With $F_H(x)$ the face orbit of $x$ and $a_H(x)=|F_H(x)|$, the score is

All intervals are inclusive; a missing upper endpoint means no upper bound. Only the positive hub is eventually restricted to degrees 5–11. Neighboring faces are not silently restricted to those degrees.

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. 19, paragraph on PDF p. 19 giving the hypermap identity; Section 5.5, PDF pp. 44–48, configuration-matching and symmetry paragraphs. Relevant displays are unnumbered. Pinned executable reference: https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/hypermap.v#L366-L375; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/coloring.v#L369-L379; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/present.v#L167-L183.