# Les 39 941 300 mots de bord bloqués, expliqués un par un ## Ce qui est traité ici Pour chaque patch, on énumère les colorations canoniques du bord (à permutation des 4 couleurs près) : 44 747 691 mots au total sur les 633 patchs. Chaque mot impose aux sommets intérieurs des listes de couleurs autorisées (les couleurs non prises par leurs voisins de bord). Un mot est **directement remplissable** si ces listes admettent une coloration propre de l'intérieur : c'est le cas de 4 806 391 mots. Les **39 941 300 autres** sont **bloqués**. Jusqu'ici, qu'un mot soit bloqué n'était établi que par une recherche exhaustive (`check_direct.c`, backtracking). `4CT_noyaux_obstruction.md` explique à la main un seul mot bloqué par patch (le premier dans l'ordre du générateur). Ce document traite **tous** les mots bloqués. ## Les outils Exactement ceux du document sur les noyaux, appliqués cette fois à l'intérieur entier du patch plutôt qu'à un noyau extrait : - **R1 (singleton).** Si L(v) = {c}, retirer c des listes des voisins de v. - **R2 (composante bicolore).** Pour une paire {a,b}, une composante connexe C des sommets dont la liste est incluse dans {a,b} est soit non bipartie (contradiction), soit 2-coloriée de façon unique à l'échange près ; un sommet hors de C adjacent à ses deux classes perd a et b. - **Disjonction sur un sommet.** Si, pour chaque couleur c de la liste d'un sommet v, fixer L(v) = {c} mène à une contradiction par R1 et R2, alors aucune coloration n'existe. On range chaque mot bloqué au premier niveau qui suffit : | Niveau | Argument | | --- | --- | | 0 | une liste est vide dès le départ (conflit direct avec le bord) | | 1 | R1 seule | | 2 | R1 et R2 | | 3 | une disjonction sur un sommet, chaque branche fermée par R1 et R2 | | 4 | deux disjonctions imbriquées | | — | non expliqué à ces niveaux | ## Résultat `experiments/run_bicolor_all_words.py` (programme C `experiments/bicolor_all_words.c`, 32 s de CPU) : ``` mots de bord 44 747 691 directement remplissables 4 806 391 (décompte identique à check_direct.c) bloqués 39 941 300 niveau 0 (liste vide) 0 niveau 1 (R1 seule) 39 531 381 98,97 % niveau 2 (R1 + R2) 408 475 1,02 % niveau 3 (une disjonction) 1 444 0,0036 % niveau 4 (deux disjonctions) 0 non expliqués 0 ``` **Tous les mots bloqués ont une explication locale.** 39 939 856 (99,996 %) n'ont besoin d'aucune disjonction ; R2 intervient au plus 6 fois par mot. Les 1 444 autres demandent une seule disjonction sur un sommet ; pour 1 405 d'entre eux, il existe même une disjonction dont chaque branche se ferme par R1 seule. Par patch, niveau le plus élevé nécessaire : R1 seule pour 1 patch (`2.122`), R1 + R2 pour 389, une disjonction pour 243. Aucun patch ne demande davantage. Le niveau 0 est vide : le bord seul ne vide jamais directement une liste intérieure. Tout blocage passe par au moins une interaction entre sommets intérieurs. ## Un exemple de disjonction `3.442802`, mot `12324323` (bord de 8 sommets). Listes intérieures : 9 : {2,3} ; 10 : {3,4} ; 11 : {1,3} ; 12 : {1,2} ; 13 : {2,4} ; 14 : {1,4} ; 15 : {1,4}. Arêtes intérieures utiles : 9 est adjacent à 10, 11, 12 et 13 ; 14 à 10 et 11 ; 15 à 12 et 13. - Si 9 = 2 : 12 reçoit 1, 13 reçoit 4 ; 15, adjacent aux deux, n'a plus de couleur. - Si 9 = 3 : 10 reçoit 4, 11 reçoit 1 ; 14, adjacent aux deux, n'a plus de couleur. Deux « ailes » symétriques autour de 9 : chaque couleur de 9 en bloque une. Aucune des deux ailes ne se bloque seule, ce qui explique pourquoi R1 et R2, sans disjonction, n'aboutissent pas. Dans les 42 mots de niveau 3 des patchs de bord ≤ 11, examinés un par un, entre 6 et 9 sommets différents peuvent servir de pivot : la disjonction n'a rien d'un choix délicat. ## Contrôles - **Décompte de référence.** Pour chaque patch, le nombre de mots remplissables retrouvé coïncide avec `expected_direct` (donc avec `check_direct.c` et le programme historique). Cela valide l'entrée, l'énumération et le solveur exact. - **Aucune fausse contradiction.** Sur chacun des 4 806 391 mots remplissables, les deux moteurs sont lancés : ni l'un ni l'autre ne conclut jamais à une contradiction. C'est le contrôle de correction essentiel, sur un volume de cas coloriables très supérieur au contrôle négatif fait sur les noyaux (2 018 instances). - **Deux moteurs indépendants dans le programme C** (masques de bits et parcours en largeur ; listes explicites et parcours en profondeur récursif, ordres inversés) : même verdict sur les 44 747 691 mots. - **Contre-vérification en Python** (`experiments/verify_bicolor_all_words.py`) : pour les 127 patchs de bord ≤ 11, réénumération complète des 682 204 mots, recherche exacte réécrite, classement par le moteur Python déjà validé sur les noyaux et une disjonction réécrite. Les décomptes par niveau (0, 1, 2, 3, ≥ 4) coïncident exactement avec le programme C, patch par patch. ## Portée exacte Ce qui est établi : **pour chaque mot de bord de chacun des 633 patchs, l'impossibilité d'un remplissage direct a une preuve locale courte** — propagation de singletons, lemme de la composante bicolore, et au plus une disjonction sur un sommet. Les 39 941 300 faits « ce mot ne se remplit pas », jusqu'ici établis par recherche exhaustive, deviennent chacun une dérivation de quelques lignes, reproductible à la main. Ce qui ne l'est pas, à ce stade : la réductibilité elle-même. Un mot bloqué doit ensuite être ramené, par échanges de Kempe à l'extérieur (§4 du corpus complet) ou par une contraction (§5), à un mot remplissable. C'est l'objet de la section suivante. ## Des mots bloqués aux règles d'échange ### La liaison, mot par mot `experiments/run_exchange_link.py` rejoue toute la chaîne des règles d'échange (`interval_rules.c`, dans une copie instrumentée générée à l'exécution et dont la logique n'est pas modifiée) et attache à chaque mot bloqué ses deux moitiés : son niveau de non-remplissage, et la règle qui le résout — ou son appartenance au résidu couvert par la contraction. ``` mots bloqués 39 941 300 résolus par échange (règle B) 29 991 189 un ruban : étoile 19 593 637 un ruban : oreilles 1 426 un ruban : séparation récursive 4 151 106 marques fixes : deux marques 300 661 marques fixes : trois marques 35 787 rubans au choix : deux marques 2 950 509 rubans au choix : trois marques 2 465 669 intervalle homogène 491 874 catégorie mixte (extérieur + traversant) 519 certificat général seul 1 résidu, couvert par la contraction (règle C) 9 950 111 ``` **Chaque mot bloqué a ses deux moitiés** : une dérivation locale de son non-remplissage, et une règle d'échange nommée (ou la contraction). Un seul mot sur 39 941 300 n'avait pas de règle d'échange lisible (il en a désormais une, en arbre de cas : `4CT_arbres_de_cas.md`) : `128.25876`, mot `12323212343232`, déjà identifié comme seul état hors du catalogue combinatoire (`4CT_intervalles.md`). Son non-remplissage, lui, s'explique par la seule propagation des singletons. Contrôles, tous passés : - la sortie habituelle du programme instrumenté est identique, colonne par colonne, à `interval_results.csv` (la colonne `interval_remaining` de ce fichier ayant été diminuée après coup de `mixed_category_interval`, on compare à leur somme) ; - par configuration, les niveaux de non-remplissage coïncident avec `bicolor_all_words.csv`, produit par un programme distinct ; - les 520 mots hors catalogue d'intervalle sont exactement ceux de `experiments/two_category_results.json`. ### Ce que la table croisée montre Part des mots dont le blocage demande le lemme de la composante bicolore (le reste : propagation des singletons seule, à l'exception de 1 444 mots qui demandent une disjonction) : | Règle d'échange | Mots | Avec composante bicolore | | --- | ---: | ---: | | résidu (contraction) | 9 950 111 | 0,31 % | | étoile | 19 593 637 | 0,74 % | | séparation récursive | 4 151 106 | 2,02 % | | deux marques fixes | 300 661 | 1,66 % | | rubans au choix, deux marques | 2 950 509 | 2,10 % | | rubans au choix, trois marques | 2 465 669 | 2,56 % | | intervalle homogène | 491 874 | 3,48 % | | oreilles | 1 426 | 11,7 % | | hors catalogue d'intervalle | 520 | 12,9 % | Les deux difficultés vont ensemble, modestement : plus la règle d'échange nécessaire est élaborée, plus le blocage demande souvent autre chose que la propagation. C'est une corrélation observée, pas un mécanisme démontré. ### Des preuves complètes, lisibles mot par mot Pour les sept configurations de bord ≤ 8, le dossier `dossiers/` donne, pour chaque mot de bord, sa justification complète : un remplissage explicite, ou bien la dérivation de son blocage puis la règle d'échange qui le résout, avec chaque ruban utile, le mot obtenu et son rang. La lecture en termes de sommets rend chaque échange vérifiable à la main. Les arêtes du bord sont colorées par la différence (XOR) des couleurs de leurs extrémités. Échanger les deux couleurs autres que θ le long du ruban qui relie les arêtes de bord X et Y change la différence sur ces deux arêtes de θ ; les sommets de bord X+1 à Y subissent donc tous la même permutation fixe (1↔2 et 3↔4 si θ = 1 ; 1↔3 et 2↔4 si θ = 2 ; 1↔4 et 2↔3 si θ = 3). Exemple, `0.7322`, mot `123212` (rang 4) : - **Blocage** : les sommets intérieurs 7, 9 et 10, deux à deux adjacents, n'ont que les couleurs 3 et 4 — un triangle à deux couleurs. - **Résolution** : θ = 2. Les six arêtes de bord ont une couleur ≠ θ, et l'extérieur réel les relie deux à deux par des rubans sans croisement. L'arête 1 ne peut être reliée qu'aux arêtes 2, 4 ou 6 (parité), et les trois rubans correspondants mènent à `123414` (rang 0), `121213` (rang 2) et `121232` (rang 0) : quel que soit l'extérieur, un échange fait descendre le rang. `0.7322` (31 mots) et `2.122` (91 mots) sont **entièrement** justifiés ainsi, sans aucun renvoi au calcul, sauf le lemme de consistance de RSST qui garantit l'existence des rubans. Ce sont des preuves de réductibilité complètes, que l'on peut vérifier à la main ligne par ligne. Dans les cinq autres, 2 à 7 mots par configuration relèvent d'une règle à marques fixes ; elle est désormais rédigée en entier dans le dossier (4 à 7 conditions « si ces rubans existent, les échanger », voir `4CT_marques_fixes.md`), si bien que **les sept dossiers sont entièrement lisibles**. Pour `2.126`, les 154 mots du résidu sont listés avec leur raison de blocage, et les 18 mots que produit la contraction sont recalculés : aucun n'est dans le résidu. `experiments/build_proof_dossiers.py` revérifie chaque ligne indépendamment du programme C : remplissages, absence de remplissage, dérivations, mots cibles recalculés par la permutation ci-dessus, décroissance des rangs, condition de chaque règle, mots de la contraction. 0 erreur sur les sept dossiers.