Théorème des quatre couleurs · 633 configurations · preuve lisible

Les 633 configurations,
une à une et toutes ensemble

Toute carte se colorie avec quatre couleurs sans que deux pays voisins se ressemblent. La preuve de ce théorème repose sur 633 petits morceaux de carte, vérifiés un à un par ordinateur. Cet atlas montre, morceau par morceau, pourquoi chacun fonctionne — et jusqu’où ces raisons se lisent à la main.

Visite guidée : prouver un morceau de carte à la main

On suit le plus petit morceau du corpus, 0.7322, de la question posée jusqu’à sa preuve complète. À chaque étape, « Montrer dans l’atlas » règle l’explorateur ci-dessous sur ce qu’il faut regarder.

Petit lexique : les mots de l’atlas

Sommet: Un pays. Un trait entre deux sommets signifie que les deux pays ont une frontière commune.
Configuration: Un petit morceau de carte : un anneau de pays qui entoure quelques pays intérieurs.
Coloriage du bord: Les couleurs des pays du bord, écrites dans l’ordre (par exemple ababcb), à renommage des couleurs près.
Remplissage direct: Un coloriage des pays intérieurs compatible avec le coloriage du bord.
Mot bloqué, noyau: Un coloriage sans remplissage direct ; le noyau est un petit groupe de pays intérieurs qui, à lui seul, rend le coloriage impossible.
Échange (de Kempe), chaîne: Recolorier une partie de l’extérieur en permutant deux paires de couleurs le long d’une chaîne de pays, qui relie deux arêtes de l’anneau. Le coloriage reste correct ; le coloriage du bord change.
Rang: Le nombre de coups dans l’ordre de preuve : 0 pour un coloriage qui se remplit directement, puis chaque échange mène à un coloriage de rang plus petit.
Réductible (D ou C): Un morceau qui ne peut pas figurer dans la plus petite carte impossible à colorier. D : tous les coloriages se résolvent par échanges. C : il faut en plus une contraction, qui colle quelques pays entre eux.
Inévitabilité: Le fait que toute carte contienne l’un des 633 morceaux. C’est un résultat historique, cité ici, non refait.

Explorer les 633 morceaux de carte

Choisissez une configuration (ou « morceau ») dans la liste. Le dessin montre ses pays (les ronds) et leurs frontières communes (les traits) ; l’anneau est ce contour extérieur. Tapez des couleurs pour l’anneau et testez si l’intérieur se colorie.

RechercheRéductionχ de l’intérieurConfiguration

abcd

Les arêtes épaisses orange appartiennent au contrat historique. En cas d’obstruction, les sommets entourés en rouge forment le noyau minimal vérifié pour ce coloriage.

Couleurs du bord (lettres a à d)

Le test interactif porte sur le remplissage direct. Il ne simule pas les connexions de l’extérieur et ne remplace pas la vérification des échanges de Kempe.

Peut-on toujours débloquer ce coloriage ? Les échanges de Kempe

L’idée, pas à pas (à lire avant de regarder le dessin)

Le problème. On a colorié l’anneau de pays, par exemple ababab. Mais à l’intérieur, des pays se touchent et n’ont plus assez de couleurs disponibles : impossible de finir. On dit que ce coloriage est bloqué.
L’idée. On ne peut pas changer l’intérieur… mais on peut changer l’extérieur, la partie inconnue de la carte autour de l’anneau. Si on recolorie bien l’extérieur, les couleurs de l’anneau changent, et le nouveau coloriage de l’anneau se remplira peut-être.
L’échange de Kempe. Choisis deux couleurs, par exemple a (bleu) et c (vert). Pars d’un pays bleu et ajoute ses voisins verts, puis leurs voisins bleus, et ainsi de suite : tu obtiens une chaîne de pays qui alternent bleu / vert, comme un collier de perles. Échange alors le bleu et le vert sur toute la chaîne. La carte reste correctement coloriée : un voisin bleu ou vert d’un pays de la chaîne ferait déjà partie de la chaîne, donc tous les autres voisins sont orange ou violets, et rien ne change pour eux.
Ce que ça change sur l’anneau. On numérote les 6 « arêtes » de l’anneau : l’arête k est la frontière entre le pays k et le pays k+1. Une chaîne de l’extérieur qui relie l’arête X à l’arête Y recolorie seulement les pays de l’anneau situés entre les deux : les pays X+1 à Y.
Le hic. On ne connaît pas l’extérieur, donc on ne sait pas quelles chaînes existent. Mais un théorème (Robertson, Sanders, Seymour, Thomas) assure que les arêtes sont reliées deux par deux par des chaînes qui ne se croisent jamais. Il n’y a que peu de façons de les relier (5 pour six arêtes) : le dessin ci-dessous les montre toutes, avec le curseur.
Chaîne utile. Un trait vert est une chaîne utile : après l’échange, le coloriage de l’anneau est plus près d’un coloriage qui se remplit. Le rang compte le nombre d’échanges qu’il faut encore : rang 0 = le coloriage se remplit tout de suite, rang 1 = un échange suffit pour y arriver, etc. Une chaîne utile fait baisser le rang.
Ce qu’on veut montrer. Que, quelle que soit la façon de relier les arêtes, il y a au moins un trait vert. Alors, même sans connaître l’extérieur, on est sûr qu’un échange utile existe, et le coloriage bloqué n’est pas un vrai obstacle. Trois astuces (« règles ») évitent d’essayer toutes les façons ; l’ordinateur indique laquelle fonctionne pour chaque coloriage.

Pour les curieux : le vrai énoncé (frontières à trois types, arêtes actives, θ)

Écrivons les couleurs a, b, c, d comme 00, 01, 10, 11. La couleur d’une frontière entre deux pays est la somme (XOR) des couleurs des deux pays : a|b donne 01, a|c donne 10, a|d donne 11, b|c donne 11, b|d donne 10, c|d donne 01. Il y a donc trois « types de frontière » (01, 10, 11). Là où trois pays se touchent, les trois frontières sont de trois types différents. Fixons un type θ. Les frontières qui ne sont pas de type θ forment des boucles qui alternent les deux autres types : ce sont les chaînes de l’atlas. Échanger le long d’une boucle, c’est ajouter θ (XOR) à la couleur de tous les pays situés d’un côté de la boucle ; pour θ = 10, cela échange a↔c et b↔d. Aucun conflit n’apparaît : une frontière de la boucle n’est jamais de type θ, donc après l’échange elle change de type sans devenir « nulle » (deux pays de même couleur). Quand la boucle n’enferme que deux couleurs, par exemple b et d, c’est exactement une chaîne de Kempe classique et l’échange se réduit à b↔d.

Chaque arête de l’anneau reçoit aussi un type. Les arêtes de type θ ne servent pas de départ aux chaînes ; les autres sont les « positions actives » : elles vont par deux (début et fin d’une chaîne), d’où une façon de les relier sans croisement. L’atlas teste les trois choix de θ et garde celui qui marche.

Un extérieur concret, pour voir un échange de Kempe en vrai

Reprenons la configuration 0.7322 et son coloriage bloqué ababab. Autour de l’anneau, nous dessinons une vraie carte : une couche de six pays « extérieurs », puis un grand pays qui entoure tout. Toute la carte est correctement coloriée : aucun pays n’a un voisin de la même couleur. Il existe beaucoup d’extérieurs possibles ; en voici deux.

La règle de l’échange. On trace une boucle (en orange) autour d’un groupe de pays. Dans la boucle, on échange a ↔ c et b ↔ d en même temps ; dehors, rien ne change. C’est permis quand la boucle ne sépare jamais un a d’un c, ni un b d’un d : sinon, après l’échange, deux voisins auraient la même couleur.

ExtérieurChaîne à échanger

Avant l’échange

Après l’échange

Les numéros 1 à 6 en blanc sont les pays de l’anneau ; les ronds foncés numérotés sont les arêtes de l’anneau (l’arête k sépare les pays k et k+1). Le disque gris au centre représente les quatre pays intérieurs. Dans l’extérieur A, par exemple, les trois chaînes possibles relient les arêtes 1–2, 3–4 et 5–6 : on ne peut pas toutes les échanger sans réfléchir, car elles ne mènent pas toutes à un coloriage qui se remplit. C’est tout l’enjeu : l’extérieur réel est inconnu, il faut donc montrer qu’au moins une chaîne marche pour tous les extérieurs possibles.

Coloriage bloqué à débloquer

Façon de relier les arêtes (faites glisser le curseur pour toutes les voir)

Les ronds numérotés sont les arêtes de l’anneau. Un trait relie deux arêtes : c’est une chaîne de Kempe qui passerait par l’extérieur. Vert : chaîne utile, son échange rapproche d’un coloriage qui se remplit. Gris : chaîne qui n’aide pas. Le dessin montre toutes les façons possibles de relier les arêtes, sans inventer un extérieur particulier.

Trace de la réductibilité historique de la configuration sélectionnée

Ces nombres concernent les codes de couleurs d’arêtes du programme RSST. Une itération n’est pas un échange individuel de Kempe. Le dernier résidu est nul pour un cas D ; pour un cas C, le contrat est ensuite confirmé.

Admissibilité de la contraction (hypothèse 2)

Une contraction n'est valide que si aucune arête extérieure à la configuration n'a ses deux extrémités identifiées. Voir 4CT_admissibilite_contractions.md et 4CT_contractions_de_remplacement.md pour les preuves.

Noyau d'obstruction minimal

Sous-ensemble minimal de sommets intérieurs dont les listes de couleurs héritées du premier mot bloqué n'admettent aucune coloration propre. Voir 4CT_noyaux_obstruction.md pour les preuves.

Toutes les lignes du bilan

Configuration	Anneau	Intérieur	Type	Coloriages	Directes	χ	Contrat

Ce qui est démontré, et ce qui reste

Les chiffres ci-dessous portent sur le corpus entier. Le tableau suivant résume chaque étape de la preuve lisible, avec le document qui la détaille.

633 / 633calculs finis indépendants confirmés

249 + 384sans contraction / avec contraction

44,7 millionscoloriages testés indépendamment

1,52 milliardrelations de dépendance contrôlées

Portée exacte. Les trois règles ci-dessous couvrent le calcul fini des 633 configurations. Depuis, la preuve lisible a nettement avancé (section suivante) : chaque déduction a un argument vérifiable à la main, l’admissibilité des contractions est prouvée pour 383 des 384 configurations C, et les 127 configurations d’anneau ≤ 11 ont un dossier de preuve mot par mot. Restent la rédaction des configurations d’anneau 12 à 14, l’admissibilité d’une seule configuration (126.62942, sur citation) et l’inévitabilité, non réexécutée.

Dossier reproductible complet (.zip)Méthode corrigée (.md)Bilan des 633 configurations (.csv)

Où en est la preuve lisible

État au 26 septembre 2026. Les documents liés donnent les énoncés, les preuves et les contrôles de chaque étape.

Étape	Résultat	Document
Règles d’échange nommées	29 991 188 des 29 991 189 déductions : une chaîne (23 746 169), marques fixes (5 752 626), coupure d’intervalle (491 874), deux catégories (519). Le dernier état, 128.25876 / 12323212343232, reçoit un argument en 50 cas.	intervalles
Pourquoi un coloriage est bloqué	Les 633 noyaux d’obstruction et les 39 941 300 mots bloqués s’expliquent par la propagation des singletons et le lemme de la composante bicolore, avec au plus une disjonction sur un sommet (1 444 mots).	noyaux, mots bloqués
Chaque mot bloqué relié à sa règle	29 991 189 mots résolus par une règle d’échange, 9 950 111 dans le résidu couvert par la contraction.	mots bloqués
Arbres de cas	Chaque déduction a un arbre vérifié : au plus 53 cas et 5 questions, 11 cas ou moins pour 99 %. 60 321 formes ; 2 couvrent la moitié des déductions, 11 en couvrent 90 %.	arbres de cas, formes
Admissibilité des contractions	383 / 384 configurations C : 307 par un lemme combinatoire, 68 par un triangle séparateur, 8 par une contraction de remplacement. 126.62942 reste sur citation : aucune contraction protégée par des triangles n’y suffit (7 328 989 candidats).	admissibilité, remplacement
Dossiers de preuve mot par mot	127 / 633 configurations (toutes celles d’anneau ≤ 11, 682 204 mots) : remplissage, ou blocage et règle rédigée, avec les rangs. 0 erreur de revérification.	dossiers
Ce qui reste	506 configurations d’anneau 12 à 14 sans dossier (leurs règles d’intervalle ne sont rédigées que sur échantillon, jusqu’à 297 connexions) ; 126.62942 ; l’inévitabilité.	article

Pour aller plus loin : quand une chaîne ne suffit pas

Dans « Explorer », on a vu l’idée de base : un coloriage de l’anneau est bloqué, et on cherche un échange de Kempe qui le rapproche d’un coloriage qui se remplit, quel que soit l’extérieur. Pour un seul échange, trois astuces suffisent souvent (étoile, oreilles, séparation).

Il reste des coloriages bloqués pour lesquels aucune chaîne seule n’est sûre. Les sections qui suivent présentent, dans l’ordre, des outils de plus en plus fins : deux ou trois chaînes échangées ensemble, des marques choisies à l’avance, puis une coupure de l’anneau. Chaque outil rattrape une partie de ce que les précédents laissent passer. Les pourcentages comptent des coloriages bloqués, sur les 633 configurations à la fois. Les dessins interactifs montrent la configuration choisie dans « Explorer ».

Une seule chaîne : 79,18 % des coloriages bloqués

Parmi les 29 991 189 coloriages bloqués qui se règlent par échanges (les 9 950 111 autres sont traités par une autre méthode, la contraction), 23 746 169 se règlent avec une seule chaîne, grâce à l’une des trois astuces ci-dessous. Les 6 245 020 autres ne sont pas des échecs : ils sont repris par les outils suivants.

Astuce	En clair	Coloriages réglés
Étoile	Une arête de départ dont toutes les partenaires possibles donnent une chaîne utile : peu importe l’extérieur, elle a une partenaire, donc une chaîne utile existe.	19 593 637
Oreilles	Dans toute façon de relier les arêtes, deux arêtes voisines sont reliées entre elles, et ces « oreilles » sont toutes utiles.	1 426
Séparation	On montre, en découpant le cercle en morceaux, qu’il est impossible de relier les arêtes en n’utilisant que des chaînes inutiles.	4 151 106

Une chaîne est utile quand son échange mène à un coloriage de rang plus petit, c’est-à-dire plus proche d’un coloriage qui se remplit. Ici, une « chaîne » est une boucle de frontières (voir l’extérieur concret plus haut), échangée en un seul coup.

Deux ou trois chaînes : 98,95 % ; trois suffisent toujours

Si aucune chaîne seule n’est sûre, on en échange deux à la fois. Ce test règle 5 930 669 coloriages de plus, ce qui porte le total à 98,95 %. Les 314 351 restants ont besoin de trois chaînes dans notre ordre de preuve : on a vérifié qu’avec deux chaînes ça ne marche pas, et que trois suffisent.

Pourquoi jamais plus de trois ? Échanger un ensemble S de chaînes, ou bien toutes les autres chaînes, donne le même coloriage de l’anneau, aux noms de couleurs près (on a seulement renommé les couleurs partout). Avec au plus sept chaînes (un anneau a au plus 14 arêtes), on peut donc toujours prendre le plus petit des deux ensembles : il contient au plus trois chaînes. C’est une borne pour un seul pas ; on peut devoir enchaîner plusieurs pas, chacun faisant baisser le rang.

127 configurations n’ont jamais besoin de plus de deux chaînes ; les 506 autres ont au moins un coloriage qui en demande trois.

Voir deux ou trois chaînes échangées ensemble

24 exemples vérifiés : 12 où deux chaînes suffisent, 12 où il en faut trois. Choisissez une façon de relier les arêtes : les chaînes en orange sont échangées ensemble, et les pays de l’anneau prennent leurs nouvelles couleurs.

ExempleFaçon de relier les arêtesCouleurs des pays de l’anneau

Les marques : choisir à l’avance quelles chaînes échanger

Voici la difficulté : l’extérieur est inconnu, donc on ne sait pas quelles chaînes existent, et on ne peut pas décider à l’avance « j’échange la chaîne 1–4 ». Mais une chose est sûre : de chaque arête de l’anneau part une chaîne, quel que soit l’extérieur. On choisit donc à l’avance deux ou trois arêtes, les marques, et on s’intéresse aux chaînes qui partent des marques. Deux façons de s’en servir :

Échange imposé : on échange toutes les chaînes qui partent des marques.
Échange au choix : parmi ces chaînes, on choisit un groupe à échanger (au plus 3 groupes possibles avec deux chaînes, 7 avec trois). Selon l’extérieur, ce n’est pas toujours le même groupe, mais il y en a toujours un qui fait baisser le rang.

Cette règle règle 5 752 626 coloriages de plus. Avec les règles à une chaîne, 29 498 795 coloriages sur 29 991 189 (98,36 %) ont un schéma ; 492 394 restent hors de ces schémas.

Règle	Coloriages réglés (attribués par priorité)
Deux marques : on échange toutes leurs chaînes	300 661
Deux oreilles : échange imposé	0
Trois marques : on échange toutes leurs chaînes	35 787
Deux marques : on choisit parmi leurs chaînes	2 950 509
Trois marques : on choisit parmi leurs chaînes	2 465 669

Pourquoi c’est économique. Il y a jusqu’à 429 façons de relier les arêtes de l’anneau. Mais, vues depuis les marques, elles ne donnent que 33 situations différentes (deux marques) ou 105 (trois marques). L’ordinateur ne vérifie que celles-là.

Les marques à l’œuvre

Règle et exempleFaçon de relier les arêtes

La coupure de l’anneau : 99,9983 %

Dernier outil : on coupe l’anneau en deux par un intervalle d’arêtes consécutives (en orange sur le dessin) et le reste. Cette coupure est choisie à l’avance, sans connaître l’extérieur. Ensuite, chaque chaîne est d’un des trois types : intérieure (ses deux bouts sont dans l’intervalle), extérieure (ses deux bouts sont dehors) ou traversante (un bout dedans, un bout dehors).

Selon l’extérieur, on choisit alors jusqu’à trois chaînes du même type, et on les échange ensemble. Ce test règle 491 874 coloriages de plus. Le catalogue complet de règles couvre 29 990 669 coloriages sur 29 991 189 ; les 520 derniers restent justifiés par la méthode générale de l’ordinateur.

Ce qui est fixé, ce qui varie. La coupure est fixée à l’avance ; le type de chaînes et le choix des chaînes peuvent dépendre de l’extérieur. On teste toutes les façons de relier les arêtes : cela marche donc quel que soit l’extérieur. Que l’échange fasse bien baisser le rang est vérifié par calcul.

510 configurations ont tous leurs coloriages couverts par ce catalogue. Un résultat de plus : les chaînes traversantes seules n’ajoutent aucun cas par rapport à la règle à une chaîne, ce qui explique qu’elles ne servent pas à elles seules.

La coupure à l’œuvre

ExempleFaçon de relier les arêtes

Trois règles, un même moteur

Règle	Condition	Couverture calculée
A · Remplir	Une coloration intérieure respecte toutes les listes.	4 806 391 coloriages
B · Éliminer	Pour un choix de couleur, toute famille compatible contient un coloriage de rang inférieur.	29 991 189 coloriages supplémentaires
C · Contracter	Aucun coloriage fourni par la contraction ne rencontre le résidu bloqué.	2 200 962 coloriages ; aucune intersection

La règle B est vérifiée après le calcul en reprenant toutes les familles concernées et en contrôlant que leurs témoins ont un rang strictement inférieur. Il s’agit d’un ordre de preuve, pas d’une borne du nombre d’échanges de Kempe.

Les corrections de l’esquisse qui restent essentielles

Le K₄ n’est pas le noyau général. Les 119 intérieurs de nombre chromatique quatre du corpus ne contiennent aucun K₄. Une roue impaire suffit à l’illustrer.

Les triangles peuvent interagir. Dans 126.687602, deux triangles ont chacun des listes compatibles, mais forcent deux sommets adjacents à prendre la même couleur. Le test séparé des cliques ne suffit pas.

La planéité doit être contrôlée avant les recolorations. Le P6'' de l’esquisse retrouve bien 21 remplissages directs sur 31 coloriages, mais contracter son anneau donne un K₅ : ce graphe ne peut pas être utilisé comme configuration planaire.

Le résultat exhaustif et ses limites

Contrôle	Résultat	Fondement
Graphes et plongements	633 / 633	Nouveau vérificateur des rotations, faces et d’Euler
Remplissages directs	4 806 391 sur 44 747 691 coloriages	Nouveau solveur C de coloration des sommets
Réductibilité finie	249 D + 384 C	Seconde implémentation : familles, fermeture et quotients
Ordre des déductions	1 521 833 472 contrôles	Chaque famille concernée fournit un témoin de rang inférieur
Témoins consultables	633 remplissages + 633 noyaux	Recalcul Python, minimalité par suppression de sommets
Admissibilité des contractions	383 / 384 configurations C	Lemme combinatoire, triangle séparateur, contraction de remplacement ; 126.62942 sur citation
Preuves humaines de tous les cas	127 / 633 dossiers mot par mot	Anneaux ≤ 11 rédigés et revérifiés ; anneaux 12 à 14 : arbres de cas vérifiés, non rédigés
Inévitabilité	Non réexécutée	Résultat historique distinct

Les noyaux exposés portent sur un seul mot bloqué par configuration. Leur taille va de 2 à 11 ; 31 de ces exemples passent tous les tests de Hall sur les cliques et restent impossibles à remplir. Au-delà de ces exemples, les 39 941 300 mots bloqués du corpus sont tous expliqués par le lemme de la composante bicolore (voir « Où en est la preuve lisible »).

Les notes ci-dessous retracent les étapes dans l’ordre où elles ont été franchies ; leurs paragraphes « prochaine étape » sont historiques.

Lire la méthode corrigée, les lemmes et leurs preuves

Une coupure fixe et trois catégories de chaînes

Résultat exhaustif sur les 633 configurations

Les arguments par intervalles couvrent 491 874 des 492 394 déductions encore hors du catalogue des règles à une chaîne et à marques fixes. Le catalogue cumulé couvre donc 29 990 669 des 29 991 189 déductions, soit 99.998266 %. Il reste 520 états hors catalogue. Ces états conservent le certificat général et la borne de trois chaînes par étape.

Règles	Déductions
Une chaîne ou marques fixes : couverture antérieure	29 498 795
Chaînes traversantes uniquement : ajout	0
Chaînes d'une même catégorie par rapport à une coupure fixe : ajout	491 874
Hors catalogue après cette étape	520

510 configurations ont toutes leurs déductions couvertes par le catalogue cumulé. Cela ne transforme pas leurs certificats en preuves intégralement vérifiées à la main : les conditions de rang restent calculées.

Le pourcentage mesure les états éliminés après remplissage direct, cumulés sur les configurations, à permutation des couleurs près. Il ne mesure ni une proportion de pages de preuve, ni une proportion du théorème démontré. Le test précédent à deux chaînes et la mesure de couverture des marques fixes sont des indicateurs distincts.

La règle de la coupure fixe

Pour un coloriage du bord w, on choisit une couleur d'arête θ et un intervalle cyclique I de positions actives. Une position active porte l'une des deux couleurs autres que θ. Les positions θ ne sont pas des extrémités de chaînes et sont ignorées dans l'ordre cyclique utilisé ici.

Dans tout appariement extérieur, chaque chaîne appartient à une des trois catégories : traversant, s'il a une extrémité dans I et une hors de I ; intérieur, si ses deux extrémités sont dans I ; extérieur, si aucune n'est dans I.

La condition est la suivante : pour chaque appariement extérieur, il existe une catégorie et un sous-ensemble non vide d'au plus trois chaînes de cette catégorie dont l'inversion donne un coloriage de rang inférieur.

θ et I sont fixés avant de connaître l'appariement. La catégorie et les chaînes choisies peuvent ensuite dépendre de l'appariement. Les inversions d'une même étape appartiennent toutes à une même catégorie et au même appariement réel.

Pourquoi cette règle suffit

La connexion extérieure réelle est l'un des appariements compatibles. L'hypothèse lui fournit un sous-ensemble utile de chaînes effectivement présents. On les inverse ensemble et on rejoint un état déjà résolu, puisque son rang est inférieur. L'argument est valable quelle que soit cette connexion réelle.

La restriction à une seule catégorie est le contenu nouveau de la règle. Le moteur général peut mélanger les trois catégories ; la présente règle le lui interdit pour une même inversion. Elle permet au lecteur de raisonner par position relative à une coupure de l’anneau.

Cette formulation fournit un schéma commun, mais son hypothèse universelle reste vérifiée par énumération. Elle n'élimine pas, à elle seule, les 429 appariements possibles dans le plus grand cas. Contrairement à la réduction par marques fixes, aucun gain uniforme sur leur nombre n'est revendiqué ici.

Un lemme qui élimine la piste des traversants seuls

Une règle qui n'autorise que les chaînes traversantes ne peut ajouter aucun cas à la garantie générale à une chaîne. Ce constat est ici justifié mathématiquement, au-delà du résultat nul de l'expérience.

Si I contient un nombre pair de positions actives, son complément aussi. Il existe alors un appariement qui apparie séparément les positions de chaque côté, sans chaîne traversante. Aucun échange non vide de traversants ne peut être garanti.

Supposons maintenant les deux côtés impairs. Dans un appariement quelconque, il y a un nombre impair, donc non nul, de chaînes traversantes. Prenons celui dont l'extrémité dans I apparaît en premier dans l'ordre de I. L'absence de croisement impose que son autre extrémité soit la dernière extrémité traversante dans le complément.

Les positions précédant cette première extrémité dans I sont appariées entre elles : un arc qui les relierait au-delà de l'extrémité couperait la chaîne choisie. Elles sont donc en nombre pair. De même, les positions suivant la dernière extrémité traversante dans le complément sont en nombre pair. Puisque chaque côté a une taille impaire, les deux autres intervalles laissés par ces extrémités ont aussi une taille paire.

On peut donc conserver cette chaîne et apparier séparément chacun des quatre intervalles pairs, par paires consécutives. Cela produit un autre appariement où la chaîne choisie est le seul traversant.

Si une garantie par traversants seuls est valable pour tous les appariements, elle doit fonctionner dans ce dernier appariement. Son unique échange non vide est l'inversion de cette chaîne seule ; il est donc utile. L'utilité dépend de ses extrémités et du coloriage du bord, pas du reste de l'appariement. Il est ainsi utile dans l'appariement initial. Tout appariement contient donc une chaîne utile : la garantie à une chaîne était déjà satisfaite.

Le lemme vaut pour toute taille paire de l'ensemble actif, indépendamment du corpus. Un contrôle combinatoire complémentaire vérifie sa construction sur 4 081 cas à rotation près, jusqu'à 14 positions actives.

Comment le test exhaustif est construit

Les coupures cycliques sont générées à complément près, y compris les intervalles d'une seule position. Pour chaque coupure, on énumère les appariements non croisés et les sous-ensembles non vides d'au plus trois chaînes appartenant à une même catégorie. Chaque sous-ensemble est codé par ses extrémités. Des appariements offrant exactement la même liste d'échanges candidats donnent la même contrainte et sont regroupés.

Le programme cherche sur les trois couleurs θ et toutes les coupures ainsi générées. La première règle testée, traversants seuls, ne sert que de contrôle et n'ajoute aucun cas. La règle à catégorie unique est appliquée aux états laissés par les règles antérieures. Les comptes antérieurs sont conservés exactement.

Les 520 échecs signifient qu'aucune couleur et aucune coupure de ce catalogue ne garantissent une baisse de rang par un échange d'au plus trois chaînes d'une même catégorie. Ce n'est pas une impossibilité pour un autre ordre de preuve, une autre règle géométrique ou un parcours autorisant une hausse intermédiaire de rang.

Contrôles et exemples

Les calculs finis ont été reconstruits sur les 633 configurations. Tous les comptes précédents sont comparés, configuration par configuration : remplissage direct, résidu, contractions, dépendances, une chaîne et marques fixes. Les nouvelles catégories partitionnent exactement les 492 394 états ciblés.

Un vérificateur Python distinct reconstruit les cibles et contrôle 587 exemples sur 89 841 appariements, ainsi que 9 436 cibles inscrites. Il vérifie la continuité cyclique de l'intervalle, la catégorie commune des chaînes choisies, leur nombre au plus trois et la baisse de rang. Les rangs proviennent du certificat C contrôlé ; le vérificateur d'exemples ne les reconstruit pas indépendamment.

Dans l'atlas, l'intervalle orangé reste fixe pendant qu'on fait varier la connexion extérieure. Les chaînes choisies sont verts ; le texte indique s'ils sont traversantes, intérieures ou extérieures. Les cibles et les rangs sont affichés pour chaque connexion.

Exécuter python3 run_interval_rules.py pour reconstruire les résultats. Le bilan complet est interval_results.csv ; les exemples contrôlés sont dans interval_examples_verified.json. Le programme check_crossing_lemma.py contrôle séparément la construction du lemme.

Les 520 états restants sont explicitement extraits

Ils se répartissent sur 123 configurations. Leurs coloriages du bord, rangs et trois choix de couleur sont enregistrés. Le programme a extrait tous les échanges utiles d'au plus trois chaînes, codés par leurs extrémités ; certains ensembles d'extrémités ne sont utilisables que dans les appariements qui les réalisent effectivement comme union de chaînes.

Le vérificateur Python contrôle 397 939 cibles utiles et 71 173 échecs de coupures. Pour chaque couleur et chaque coupure, il fournit l'indice d'un appariement sans échange utile d'une même catégorie. Les indices, à partir de zéro, suivent l'ordre récursif documenté par la fonction matchings du vérificateur. Pour la couleur du certificat général, il vérifie au contraire que tout appariement dispose d'un échange utile d'au plus trois chaînes lorsque les mélanges de catégories sont permis.

Sur ces 520 états, sept disposent encore d'une garantie à deux chaînes ; les 513 autres exigent trois dans l'ordre de preuve fixé. Ces sept états illustrent que le nombre minimal de chaînes et l'appartenance au catalogue géométrique sont deux propriétés distinctes.

La complétude de la liste des échanges utiles repose sur leur extraction exhaustive par le programme C ; le contrôle Python recalcule les cibles présentes et vérifie les couvertures et les échecs à partir de cette liste. Les rangs restent ceux du certificat C. La recherche suivante peut travailler directement sur ces 520 objets plutôt que reconstruire tous les millions d'états.

Prochaine étape

Examiner les 520 états hors catalogue pour identifier les mélanges de catégories indispensables dans l'ordre fixé. Il faudra chercher une règle supplémentaire qui apporte une contrainte réelle, et éviter de simplement reformuler la garantie générale en autorisant tous les mélanges. Les conditions de rang, l'inévitabilité et l'admissibilité globale des contractions restent des obligations distinctes.

Les sections suivantes conservent les résultats et les limites des étapes antérieures.

Mise à jour (corrigée). Une première version de ce test autorisait des coupures d'une seule position, où la catégorie « intérieur » est vide par construction — un faux positif qui redonnait simplement le certificat général. Repris en imposant des coupures d'au moins deux positions, le test montre qu'une coupure fixe mélangeant deux catégories — exclusivement extérieur + traversant, jamais intérieur — couvre 519 des 520 états restants. Le catalogue combinatoire atteint 29 991 188 / 29 991 189 déductions (99,999997 %). Un état résiste (configuration 128.25876, coloriage 12323212343232) : il est démontré qu'aucune coupure ne permet d'éviter la catégorie intérieure pour son appariement le plus difficile — il reste couvert par le seul certificat général. Voir 4CT_633/experiments/README.md pour la preuve complète.

---

Des échanges aux règles : marquer deux ou trois extrémités

Résultat du test sur les 633 configurations

Les règles de cette étape couvrent 5 752 626 des 6 245 020 déductions laissées par les arguments à une chaîne. En conservant les 23 746 169 cas déjà classés à une chaîne, on obtient 29 498 795 déductions décrites par les schémas proposés, soit 98.3582 % des 29 991 189 déductions. Il reste 492 394 cas hors de ces schémas. Ils gardent leur certificat général et la borne locale de trois chaînes.

Règle supplémentaire retenue	Déductions
Deux marques, inversion de toutes leurs chaînes	300 661
Deux oreilles, inversion imposée	0
Trois marques, inversion de toutes leurs chaînes	35 787
Deux marques, choix parmi leurs chaînes	2 950 509
Trois marques, choix parmi leurs chaînes	2 465 669
Hors de ces nouvelles règles	492 394

Les catégories sont disjointes par priorité : deux marques imposées, deux oreilles, trois marques imposées, deux marques avec choix, trois marques avec choix. Le programme cherche sur les trois couleurs et retient la première catégorie applicable dans cette priorité. Les règles ne sont donc pas comparées par leur couverture totale prise séparément. En particulier, une catégorie à trois marques n'implique pas que le coloriage exige trois chaînes au sens du test précédent.

46 configurations ont toutes leurs déductions couvertes par les règles à une chaîne et celles de cette étape. Ce sont des couvertures de schémas dont les conditions sont calculées ; elles ne constituent pas des preuves intégralement vérifiées à la main.

Le pourcentage précédent de 98,95 % répondait à une autre question : combien de déductions disposent d'une garantie à deux chaînes, sans imposer de marques fixes ? Le pourcentage présent mesure la couverture de règles structurées, pouvant utiliser trois chaînes. Les deux indicateurs ne doivent pas être confondus.

L'idée : fixer les marques avant de connaître les connexions

On choisit une couleur d'arête θ et deux ou trois positions actives de l’anneau, les marques. Ces positions restent fixées pendant tout l'argument, indépendamment de la connexion extérieure réelle.

Dans une connexion donnée, chaque marque appartient à une seule chaîne. Deux marques peuvent appartenir à la même chaîne : on le compte une seule fois. Il y a donc au plus deux ou trois chaînes concernés. Tous les autres chaînes sont laissés de côté.

La règle imposée inverse toutes les chaînes qui touchent au moins une marque. La règle avec choix inverse un sous-ensemble non vide de ces chaînes. Avec deux chaînes distinctes, il y a trois choix ; avec trois, sept choix. Si les marques partagent des chaînes, ce nombre diminue.

Lemme des marques fixes

Supposons qu'il existe θ et un ensemble A d'au plus k marques tels que, pour chaque appariement partiel possible des marques avec leurs partenaires, on puisse choisir parmi les chaînes incidentes à A un sous-ensemble non vide conduisant à un coloriage de rang inférieur. Alors tout appariement extérieur complet permet un échange utile d'au plus k chaînes.

Preuve. Tout appariement extérieur complet induit un des appariements partiels testés : on ne garde que les chaînes qui touchent A. L'hypothèse fournit un sous-ensemble utile de ces chaînes. Ceux-ci appartiennent tous au même appariement réel et peuvent être inversés ensemble. Leur nombre est au plus k. La cible a un rang inférieur. Le reste de l'appariement n'intervient pas dans le calcul du coloriage cible. Cela établit la garantie cherchée.

L'ordre des choix est essentiel : θ et A dépendent du coloriage initial mais sont fixés avant l'appariement extérieur ; le choix des chaînes inversées peut dépendre de l'appariement partiel observé. Autoriser A à changer pour chaque connexion reviendrait au test général et perdrait le contenu de la règle.

Combien de connexions faut-il encore contrôler ?

Pour au plus 14 positions actives, il existe jusqu'à 429 appariements parfaits non croisés. En ne retenant que les connexions de deux marques fixes, le catalogue calculé contient au plus 33 appariements partiels distincts. Avec trois marques, il en contient au plus 105.

Ces nombres sont des maxima finis établis par génération exhaustive du catalogue pour 2, 4, 6, 8, 10, 12 et 14 positions. Les partenaires des marques sont les seules données conservées. Les prolongements différents d'une même connexion partielle sont regroupés, car ils produisent exactement les mêmes choix de modifications sur l’anneau.

Cette réduction donne une consigne géométrique commune. Elle ne transforme pas automatiquement 105 vérifications de rang en une preuve courte. Les marques, les couleurs et les cibles restent choisies par le programme. La suite du travail doit expliquer les inégalités de rang ou regrouper encore les connexions partielles.

La piste des deux oreilles

Un appariement parfait non croisé sur un cercle, comportant au moins deux arcs, contient au moins deux arcs disjoints entre positions cycliquement consécutives. Pour le voir, choisissons un arc. S'il sépare deux régions contenant chacune des positions, un arc d'intervalle minimal dans chaque région est une oreille. Si un côté est vide, l'arc choisi est déjà une oreille et un arc d'intervalle minimal du côté non vide fournit la seconde.

Il suffirait donc que toute paire de telles oreilles donne une cible de rang inférieur lorsqu'on les inverse ensemble. Le test n'apporte ici aucun cas supplémentaire après les deux marques imposées et avant les trois marques imposées. Cette absence de gain concerne cette règle précise et cette priorité ; elle n'exclut pas d'autres arguments utilisant les oreilles.

Vérifications réalisées

Les deux programmes reconstruisent les certificats finis sur les 633 configurations. Leurs comptes directs, résidus, coloriages de contractions, profils à une chaîne et nombres de contrôles de dépendance sont comparés aux résultats précédents. La partition des 6 245 020 états testés est vérifiée. Le second programme conserve exactement la classification des règles imposées du premier.

Un vérificateur Python distinct contrôle 2 471 exemples, 216 270 appariements complets et 275 893 cibles inscrites. Il recalcule les coloriages après inversion, vérifie les rangs inscrits, puis contrôle que les marques restent fixes et que la règle fournit un choix utile pour chaque appariement. Les rangs eux-mêmes proviennent du certificat C contrôlé, ils ne sont pas reconstruits par ce vérificateur d'exemples.

L'atlas expose les exemples disponibles pour la configuration sélectionnée. Les marques sont cerclées d'orange ; les chaînes effectivement inversées sont verts. Changer la connexion extérieure change éventuellement les chaînes choisies, jamais les marques.

Reproduire et poursuivre

Exécuter python3 run_anchor_rules.py dans le dossier reproductible après les étapes antérieures. Le bilan complet est dans adaptive_results.csv, le bilan des règles imposées dans anchor_results.csv, les exemples contrôlés dans anchor_examples_verified.json.

La prochaine étape cible les 492 394 états non couverts : déterminer si leurs témoins utiles peuvent se regrouper par séparation du cercle en intervalles. L'objectif est aussi de réduire les 33 ou 105 connexions partielles à des lemmes de familles. L'inévitabilité et l'admissibilité globale des contractions restent des obligations distinctes.

---

Un, deux ou trois chaînes : une borne locale sur les 633 configurations

Résultat complet, et portée exacte

Les 633 configurations ont toutes été traitées. Dans l'ordre de preuve certifié, 29 991 189 coloriages sont éliminées après les 4 806 391 remplissages directs. La classification suivante porte sur ces déductions, cumulées sur les configurations, à permutation des couleurs près.

Nombre maximal de chaînes nécessaire pour garantir une baisse de rang	Déductions	Justification
Un	23 746 169	Classification géométrique exhaustive précédente
Deux, mais pas un	5 930 669	Nouveau test exhaustif sur les trois choix de couleur
Trois, mais pas deux	314 351	Échec exhaustif à deux ; borne supérieure par complément et certificat général
Total	29 991 189	Tous les états éliminés du corpus

Un ou deux chaînes couvrent 29 676 838 déductions, soit 98,951855 %. 127 configurations n'ont aucune déduction exigeant trois chaînes dans cet ordre ; les 506 autres en ont au moins une. Tous restent certifiés par le moteur général. Il ne s'agit ni d'une preuve du théorème des quatre couleurs sans ordinateur, ni d'une borne de trois échanges au total.

Le lemme du complément

Fixons un coloriage du bord w, une couleur d'arête θ, et un appariement extérieur M. Les positions dont la couleur diffère de θ sont les extrémités des chaînes ; elles sont au nombre de 2m. Inverser une chaîne échange les deux autres couleurs sur ses deux extrémités.

Si inverser un ensemble S de chaînes donne w′, inverser les chaînes complémentaires M privé de S donne le même coloriage à une permutation globale des deux couleurs non θ près. En effet, inverser toutes les chaînes échange ces deux couleurs sur toutes leurs positions et laisse θ fixe. Notre codage identifie les permutations globales des couleurs. Les deux résultats ont donc le même identifiant et le même rang.

On peut toujours choisir le plus petit des deux ensembles S et son complément : il contient au plus la partie entière de m/2 chaînes. L’anneau a au plus 14 arêtes, donc m est au plus 7 et ce nombre est au plus 3. Plus généralement la borne locale est la partie entière de r/4, où r est la longueur de l’anneau.

Le certificat général fournit, pour chaque coloriage éliminé, une couleur θ telle que tout appariement compatible contient un choix S menant à un coloriage de rang strictement inférieur. Appliquer le lemme du complément à ce S prouve la borne de trois. La cible ne peut être le coloriage initial puisque son rang est inférieur ; le choix utile réduit n'est donc pas vide.

Cette borne est une conséquence de la symétrie des familles RSST et du certificat existant. Elle n'est pas présentée comme une découverte historique nouvelle. Elle ne supprime pas le calcul des rangs ni l'énumération des appariements. Elle rend toutefois uniforme la taille de l'échange à expliquer à chaque étape.

Ce que teste exactement le nouveau calcul

Pour chaque état non couvert à une chaîne, le programme essaie les trois couleurs θ. Pour chaque θ, il énumère tous les appariements parfaits non croisés des positions actives, au plus 429. Un appariement passe si l'inversion d'un de ses arcs, ou de deux de ses arcs ensemble, rejoint un état de rang strictement inférieur. La couleur passe seulement si tous ses appariements passent. Il suffit qu'une couleur passe.

Les deux arcs doivent appartenir au même appariement. Les prendre dans deux appariements possibles différents ne prouverait rien sur leur réalisation simultanée. Le code utilise la somme des modifications sur les quatre extrémités distinctes, puis retrouve le coloriage canonique cible.

L'ordre de preuve est fixé. Un échec à deux signifie : pour chaque θ, il existe un appariement sans échange utile d'un ou deux chaînes. Cela ne prouve pas qu'un autre ordre, ou un chemin autorisant une hausse provisoire de rang, échouerait. Il ne s'agit pas non plus de deux échanges sur des composantes bicolores de sommets : les chaînes sont définis dans le langage des couleurs d'arêtes.

Les contractions

Sur les 2 200 962 coloriages compatibles avec les contractions, 794 925 sont directes ; 899 670 relèvent d'une étape à une chaîne ; 473 019 nécessitent deux chaînes dans la classification ; 33 348 nécessitent trois. Aucune ne rencontre le résidu bloqué. Ces nombres décrivent les étapes de départ ; leurs dépendances se déroulent dans le même ordre de preuve certifié.

Contrôles et reproductibilité

Le nouveau calcul vérifie à nouveau les comptes directs, les résidus, les contractions et les 1 521 833 472 relations de dépendance du moteur indépendant. Les profils à une chaîne sont comparés exactement aux résultats précédents pour chacun des 633 configurations. Les deux nouvelles catégories partitionnent exactement les 6 245 020 cas restants.

Un vérificateur Python indépendant reconstruit les coloriages du bord après échange et réénumère les appariements de 24 exemples : 12 succès à deux et 12 échecs à deux. Il contrôle 1 752 appariements d'exemples, les cibles et les inégalités de rang inscrites dans le certificat. Dans les 12 échecs exposés, le θ choisi est celui du certificat général ; une cible à trois chaînes est vérifiée pour chaque appariement. Ce contrôle d'exemples complète le calcul C exhaustif ; il ne le remplace pas et ne reconstruit pas indépendamment tous les rangs.

Le fichier two_results.csv donne le bilan complet. Le script run_two.py recompile et exécute le calcul complet puis les exemples et leur vérification. La preuve générale de la borne trois est le lemme ci-dessus ; le calcul exhaustif nouveau mesure la couverture à deux. Les exemples graphiques permettent d'observer des échanges à deux et à trois sur une connexion extérieure choisie.

Prochaine réduction du travail humain

La borne locale trois est maintenant uniforme. Le prochain objectif utile est de remplacer les centaines d'appariements possibles par quelques schémas géométriques couvrants pour les échanges à deux ou trois, et de réduire les dépendances de rang à des arguments lisibles. L'inévitabilité et l'admissibilité globale des contractions demeurent des obligations séparées.

---

Compression géométrique des déductions de recoloration

Résultat exact

Nous avons repris tous les 29 991 189 coloriages non directement remplissables que le moteur indépendant élimine dans les 633 configurations. Pour chacune, nous avons testé si un seul échange de chaîne peut être garanti par la géométrie, tout en rejoignant un coloriage de rang inférieur dans le certificat déjà vérifié.

Le test réussit pour 23 746 169 coloriages, soit 79,18 % des déductions examinées. Le corpus entier a été parcouru. Les 6 245 020 autres coloriages conservent leur justification par le moteur général ; ce ne sont pas des échecs de la réductibilité.

La proportion porte sur les déductions de recoloration, pas sur les configurations. Des déductions simplifiées peuvent mener à des cibles qui utilisent encore la règle générale. Dans l’ordre de preuve utilisé, seules les configurations 0.7322 et 2.122 ont toutes leurs déductions couvertes par les règles à une chaîne ci-dessous.

1. Les objets que nous recolorions

Les quatre couleurs des sommets sont représentées par les deux bits 00, 01, 10, 11. La couleur d’une arête est la différence binaire, ou XOR, de celles de ses extrémités ; elle appartient aux trois vecteurs non nuls. Sur l’anneau, on normalise ces trois couleurs d’arêtes par ordre de première apparition.

Fixons une couleur d’arête θ. Retirons de la liste circulaire les positions de couleur θ. Il reste 2m positions actives, avec m ≤ 7 pour le corpus. Tout extérieur réel fournit un appariement sans croisement de ces positions, par les chaînes bicolores du lemme de consistance. Les signes sont déterminés par la coloration : deux extrémités d’une paire portent soit la même couleur, soit des couleurs différentes.

Pour un coloriage et un choix de θ fixés, il y a au plus Cₘ appariements, où Cₘ est le nombre de Catalan. Pour m=1,…,7, cela donne 1, 2, 5, 14, 42, 132, 429. Ce décompte concerne les appariements d’un coloriage fixée ; il ne faut pas le confondre avec les 1 485 004 familles signées de toute la bibliothèque à anneau de 14 sommets, ni avec les partitions de plages comptées précédemment en 1/3/12/55/…

Un arc est une paire possible dans cet appariement. Inverser les deux couleurs autres que θ sur la chaîne correspondante change les couleurs de ses deux extrémités sur l’anneau. L’inversion porte sur la chaîne entière de l’extérieur. Nous ne recolorions pas arbitrairement deux arêtes isolées.

Ces chaînes sont définis dans le langage des couleurs d’arêtes. « Un échange de chaîne » n’est pas ici une revendication d’un échange unique sur une composante bicolore des sommets.

2. Définir un arc utile

Le moteur précédent fournit un ordre de preuve : les remplissages directs ont rang zéro ; chaque coloriage éliminé a un rang positif et une justification ne faisant intervenir que des rangs inférieurs. Ce rang est un outil de certification, pas une quantité géométrique intrinsèque.

Pour un coloriage w et une couleur θ, nous appelons un arc utile lorsque l’inversion de ses deux couleurs d’extrémités produit un coloriage dont le rang est strictement inférieur à celui de w. Les deux positions de l’arc doivent avoir des parités opposées dans la liste active ; c’est exactement la condition pour pouvoir appartenir à un appariement sans croisement du cercle.

Le test à une chaîne est le suivant :

Existe-t-il un choix de θ tel que tout appariement compatible contienne au moins un arc utile ?

S’il réussit, quel que soit l’extérieur réel, son appariement contient un arc utile. On inverse la chaîne associée et on poursuit avec un coloriage de rang inférieur. La même récurrence que dans le certificat général justifie cette déduction.

Le programme teste les trois choix de θ. Il préfère les arguments les plus courts ci-dessous. Quand aucun choix ne réussit, cela signifie seulement que cette propriété de progression stricte échoue dans l’ordre de preuve fixé. Un autre ordre ou une stratégie conservant davantage d’informations pourrait réussir.

3. Premier lemme : un partenaire quelconque suffit

Hypothèse. Il existe une position active p telle que tous ses partenaires possibles soient utiles.

Conclusion. Tout appariement contient un arc utile.

Preuve. Dans l’appariement réel, p a un partenaire. Un arc d’appariement sépare deux intervalles comportant chacun un nombre pair de positions restantes : son partenaire est donc de parité opposée à p dans la liste active. Par hypothèse, tous ces partenaires donnent un arc utile. ∎

C’est la règle dite « étoile » dans l’atlas. Il suffit de contrôler au plus sept partenaires ; on n’a pas à parcourir jusqu’à 429 appariements.

Couverture mesurée : 19 593 637 coloriages.

4. Deuxième lemme : une paire consécutive existe toujours

Hypothèse. Tous les arcs joignant deux positions consécutives de la liste active circulaire sont utiles.

Conclusion. Tout appariement contient un arc utile.

Preuve. Tout appariement parfait sans croisement contient une paire de positions consécutives. On peut le voir en choisissant un arc ayant un nombre minimal de positions entre ses extrémités sur l’un des deux côtés. Si cet intervalle n’était pas vide, les positions qu’il contient devraient être appariées entre elles, ce qui donnerait un arc enfermant un intervalle plus petit. Contradiction. La paire consécutive ainsi obtenue est utile par hypothèse. ∎

« Consécutives » se rapporte aux positions actives, après retrait des positions de couleur θ. Elles ne sont pas forcément consécutives sur l’anneau initial.

Couverture mesurée supplémentaire : 1 426 coloriages. Le programme privilégie le lemme précédent lorsqu’il s’applique aussi ; cette colonne n’est donc pas le nombre total de coloriages satisfaisant l’hypothèse du deuxième lemme.

5. Troisième lemme : séparer récursivement le cercle

Quand les deux arguments précédents ne suffisent pas, demandons si un appariement peut éviter tous les arcs utiles. Appelons « non utile » un arc qui ne diminue pas strictement le rang.

Numérotons linéairement les positions actives de 0 à 2m−1 en coupant le cercle entre deux positions. Pour un intervalle [i,j), notons P(i,j) la possibilité de l’apparier sans croisement en n’utilisant que des arcs non utiles. L’intervalle vide est possible : P(i,i) est vrai.

Dans tout appariement d’un intervalle non vide, i est apparié à une position k de parité opposée. L’arc i–k laisse deux intervalles indépendants. On a donc exactement :

P(i,j) = OU, pour k=i+1,i+3,…,j−1, de [arc i–k non utile ET P(i+1,k) ET P(k+1,j)].

Conclusion. Si P(0,2m) est faux, tout appariement contient un arc utile.

Preuve. La récurrence décrit toutes les possibilités pour le partenaire de la première position. Un arc non utile et deux appariements non croisés de ses intervalles constituent un appariement évitant les arcs utiles ; inversement, tout appariement qui les évite se décompose ainsi. ∎

Cette vérification par intervalles utilise une table de taille quadratique et un nombre cubique d’opérations en 2m. Elle peut donc remplacer l’énumération explicite des 429 appariements du cas maximal. Pour chaque intervalle, il y a au plus sept partenaires à examiner dans notre corpus.

Couverture mesurée supplémentaire : 4 151 106 coloriages.

6. Tableau de couverture

Justification retenue	Nombre de coloriages
Partenaire quelconque d’une position : règle de l’étoile	19 593 637
Existence d’une paire consécutive utile	1 426
Séparation récursive excluant tout appariement non utile	4 151 106
Total justifié par une seule chaîne de rang décroissant	23 746 169
Non couvert par ce test dans l’ordre fixé	6 245 020
Total des coloriages éliminés après les remplissages directs	29 991 189

Le calcul général de réductibilité a été revérifié pendant cette analyse : mêmes nombres de remplissages et de résidus, mêmes 1 521 833 472 contrôles de dépendance, mêmes contrats compatibles et aucune intersection avec les résidus.

Les coloriages directement remplissables, au nombre cumulé de 4 806 391, ne figurent pas dans le tableau : elles n’ont besoin d’aucune recoloration.

7. Le sous-ensemble fourni par les contrats

Parmi les 2 200 962 coloriages que les 384 contractions peuvent fournir :

Situation	Nombre
Directement remplissables	794 925
Étoile utile	632 185
Paire consécutive utile	173
Séparation récursive	267 312
Test à une chaîne non concluant dans l’ordre fixé	506 367

Un coloriage de contrat couvert par un lemme peut avoir pour cible un coloriage auxiliaire qui utilise encore le certificat général. Ce tableau ne démontre donc pas, à lui seul, que les contractions concernées possèdent une preuve entièrement à une chaîne.

8. Contrôle distinct des exemples

Nous avons extrait, pour chaque configuration et chaque catégorie non vide, un exemple : 2 325 exemples au total, couvrant les 633 configurations. Un second programme Python vérifie les changements de couleurs et leurs cibles, puis énumère explicitement tous les appariements du cercle actif.

Pour les catégories réussies, il vérifie que chaque appariement possède un arc utile. Pour une catégorie non concluante, il exhibe un appariement qui évite tous les arcs utiles pour la couleur montrée. Le moteur C a testé les trois couleurs ; l’exemple affiché illustre l’une d’elles.

Ces exemples ne remplacent pas le calcul sur les 29 991 189 coloriages. Ils offrent une contre-vérification de la traduction des règles et des supports, et donnent au lecteur des instances inspectables dans l’atlas.

9. Lecture du visualiseur

Le coloriage indiqué dans la section de compression donne les couleurs des sommets de l’anneau. Le dessin de connexions porte sur ses positions d’arêtes actives : eᵢ relie les sommets i et i+1, avec retour au sommet 1.

Le curseur parcourt tous les appariements abstraits compatibles avec la disposition des positions. Un arc vert est utile : le tableau donne le coloriage cible et son rang inférieur. Un arc gris ne satisfait pas ce test de rang ; cela ne prouve pas qu’il serait inutile dans une autre stratégie. Dans un exemple non concluant, le visualiseur commence par un appariement sans arc vert.

Le dessin ne représente pas un extérieur particulier. Il permet d’inspecter les possibilités que tout argument de recoloration doit couvrir.

10. Ce que cette étape apporte et ce qui reste

Nous avons remplacé une grande partie des tests de familles par trois arguments géométriques démontrés, avec une mesure exhaustive de leur couverture sur tout le corpus. La règle de l’étoile suffit à elle seule pour près de vingt millions de déductions.

Ce n’est pas encore une preuve que l’on peut entièrement lire à la main : les couleurs utiles et les rangs de leurs cibles proviennent toujours du certificat calculé. Le prochain travail est de traiter les 6 245 020 cas restants, notamment par des arguments garantissant l’existence de deux chaînes utiles ensemble, puis de compresser les tests de rang eux-mêmes.

L’inévitabilité demeure distincte et n’a pas été réexécutée. Aucune borne universelle de huit échanges ni aucune nouveauté sur le théorème des quatre couleurs n’est revendiquée.

Reproduction et source mathématique

Le dossier contient geometric_compression.c, geometric_results.csv, les exemples, leur vérificateur Python et run_geometric.py. Ce dernier reconstruit le calcul fini et l’analyse géométrique sur les 633 configurations. La génération des chaînes et des appariements repose sur le lemme de consistance de RSST, §3 : https://thomas.math.gatech.edu/PAP/fc.pdf

Les trois arguments géométriques de cette note sont démontrés ci-dessus ; les décomptes proviennent de notre exécution du programme.

Prochaine étape de la preuve lisible

Le catalogue géométrique couvre désormais 29 991 188 déductions sur 29 991 189 (99,999997 %). Sur les 520 états qui échappaient au catalogue à une seule catégorie, 519 sont couverts par une coupure fixe mélangeant deux catégories (extérieur + traversant, jamais intérieur), un résultat vérifié deux fois indépendamment — voir 4CT_633/experiments/. Un état (128.25876, coloriage 12323212343232) résiste à toute coupure et nécessite prouvablement la catégorie intérieure ; il reste couvert par le seul certificat général. Cet état reçoit depuis un argument en 50 cas (arbre de cas), et toutes les étapes suivantes sont résumées plus haut, dans « Où en est la preuve lisible ». Restent la rédaction des configurations d’anneau 12 à 14, l’admissibilité de 126.62942 et l’inévitabilité.

Sources : RSST, programmes et données de réductibilité ; article complet sur le théorème des quatre couleurs. Les contrôles indépendants et l’audit ont été réalisés pour cette exploration.

Les 633 configurations,une à une et toutes ensemble