# Les 633 noyaux d'obstruction, classés structurellement ## Contexte `4CT_corpus_complet.md` §7 (« Des noyaux d'obstruction réels, sans hypothèse de clique ») décrit, pour chaque patch, un noyau minimal par inclusion de sommets intérieurs : impossible à colorier avec les listes héritées du premier mot bloqué du générateur, mais coloriable dès qu'on retire n'importe lequel de ses sommets. Le texte propose une classification par forme — « conflit d'arête après propagation, triangle à deux couleurs, cycle impair à deux couleurs, deux triangles couplés, puis structures plus grandes » — mais ne la vérifie nulle part systématiquement sur les 633 patchs. C'est fait ici. ## Méthode `experiments/kernel_classification.py` construit, pour chaque patch, le sous-graphe induit par `minimal_obstruction` (à partir de `adj`), et classe sa forme : - **arête** : 2 sommets adjacents ; - **triangle** : 3 sommets formant un K3 ; - **cycle impair** : n ≥ 5 impair, sous-graphe = un cycle unique de longueur n (tous les sommets de degré 2, une seule composante) ; - **triangles couplés** : 6 sommets qui se scindent en deux triangles (éventuellement reliés par des arêtes supplémentaires) ; - **autre** : toute structure plus irrégulière. Vérifié par une ré-implémentation indépendante (0 écart sur les 633 patchs), et sémantiquement (pas seulement structurellement) pour les deux catégories les plus fréquentes : - les 17 **arêtes** ont bien deux listes réduites à un **même singleton** (le conflit direct après propagation) ; - les 569 **triangles** violent bien le test de Hall sur leur propre clique (union des trois listes de taille < 3) — c'est le cas trivial, pas les 31 cas « qui passent Hall » évoqués au §1.1 du corpus complet. ## Résultat ``` total : 633 arête : 17 (2 sommets) triangle : 569 (3 sommets) cycle impair : 19 (5 sommets : 17 ; 7 sommets : 2) triangles couplés : 6 (6 sommets) autre : 22 (5 : 13 ; 7 : 2 ; 8 : 3 ; 9 : 2 ; 10 : 1 ; 11 : 1) ``` **611 des 633 noyaux (96,5 %) se rangent dans l'une des quatre formes nommées par le manuscrit.** Les 22 restants (tailles 5 à 11) ont une structure plus irrégulière — ni cycle simple ni deux triangles nets, mais des graphes plus denses (par exemple `2.504366` : 5 sommets, 7 arêtes, degrés [2,2,3,3,4] — un triangle avec deux sommets supplémentaires accrochés). ## Les 31 cas qui passent le test de Hall `clique_hall_pass_for_bad` distingue les 31 patchs dont le noyau satisfait le test de Hall sur **toutes** ses cliques internes tout en restant impossible à colorier — le phénomène illustré au §1.1 du corpus complet avec l'exemple du chemin x–y–z. Ce ne sont jamais des arêtes ni des triangles simples (ces deux formes violent Hall directement, par construction) : ``` cycle impair : 8 / 19 triangles couplés : 3 / 6 autre : 20 / 22 ``` Les triangles couplés qui passent Hall confirment exactement l'exemple `126.687602` du §1.2 : chaque triangle, pris isolément, satisfait Hall (union de ses listes = 3 couleurs), mais l'arête qui relie les deux triangles force deux sommets adjacents à la même couleur — un phénomène invisible à un test qui ne regarde que les cliques une par une. Les 20 « autre » qui passent Hall sont les cas les plus substantiels du corpus : leur structure irrégulière est précisément ce qui leur permet d'échapper à un test local tout en restant bloqués globalement. ## Le lemme du triangle : un argument générique pour les 569 cas **Énoncé.** Soit {a, b, c} un noyau d'obstruction de forme « triangle » (les trois sommets mutuellement adjacents dans l'intérieur du patch), de listes de couleurs disponibles L(a), L(b), L(c) ⊆ {1,2,3,4}. Si |L(a) ∪ L(b) ∪ L(c)| ≤ 2, alors {a, b, c} n'admet aucune coloration propre — quelles que soient par ailleurs les listes individuelles. **Preuve.** a, b, c sont mutuellement adjacents : une coloration propre doit leur attribuer trois couleurs deux à deux distinctes, chacune puisée dans sa propre liste. Ces trois couleurs distinctes appartiennent nécessairement à L(a) ∪ L(b) ∪ L(c). Si cet ensemble a au plus 2 éléments, il ne peut pas contenir 3 valeurs deux à deux distinctes — contradiction directe (principe des tiroirs : 3 objets dans au plus 2 cases). ∎ C'est un cas particulier élémentaire du théorème de Hall pour les systèmes de représentants distincts (aucune chaîne de Kempe requise, contrairement au cas du quadrilatère séparateur de `4CT_admissibilite_contractions.md` — ici il n'y a pas deux côtés à réconcilier, seulement trois listes et un principe de comptage) : il suffit de vérifier la condition de Hall sur le sous-ensemble maximal {a,b,c} lui-même, pas sur tous ses sous-ensembles, puisque c'est déjà le plus contraignant. **Vérification sur les 569 cas** (ré-implémentation indépendante, 0 écart) : la condition |L(a)∪L(b)∪L(c)| ≤ 2 est satisfaite par construction dans **les 569 cas, sans exception** — et plus précisément toujours avec égalité stricte (union de taille exactement 2, jamais 0 ni 1) : ``` taille de l'union des 3 listes : 2 dans les 569 cas taille de chaque liste individuelle : 1 (133 fois) ou 2 (1574 fois) les 3 listes sont identiques dans 436 cas sur 569 ; distinctes (mais toujours de réunion 2) dans les 133 autres ``` **Ce lemme couvre donc, d'un seul argument tenant en quelques lignes et indépendant du calcul, 569 des 633 patchs (90 %)** — la première fois que ce nombre repose sur un énoncé général plutôt que sur 569 vérifications informatiques séparées. ## Le lemme de l'arête : le même argument, pour 17 cas de plus **Énoncé.** Soit {a, b} un noyau d'obstruction de forme « arête » (a et b adjacents dans l'intérieur du patch), de listes L(a), L(b) ⊆ {1,2,3,4}. Si |L(a) ∪ L(b)| ≤ 1, alors {a, b} n'admet aucune coloration propre. **Preuve.** a et b sont adjacents : une coloration propre leur attribue deux couleurs distinctes, chacune puisée dans sa propre liste, donc appartenant à L(a) ∪ L(b). Si cet ensemble a au plus 1 élément, il ne peut contenir 2 valeurs distinctes — même principe des tiroirs que pour le triangle, avec 2 objets et au plus 1 case. ∎ **Vérification sur les 17 cas** (ré-implémentation indépendante, 0 écart) : |L(a) ∪ L(b)| = 1 exactement dans les 17 cas, sans exception — les deux listes sont systématiquement des singletons identiques (le « conflit d'arête après propagation » du corpus complet §7 est précisément ce cas : les deux sommets ont été forcés, par les couleurs déjà posées ailleurs, à la même unique couleur restante). **Avec les deux lemmes, 586 des 633 patchs (92,6 %) reposent désormais sur un argument générique de quelques lignes plutôt que sur un calcul au cas par cas.** ## Le lemme du cycle impair : parité, pas Hall Contrairement au triangle et à l'arête, un cycle impair ne viole pas Hall sur sa propre clique — un cycle n'est pas une clique, la condition de Hall (réunion des listes trop petite) n'est donc pas la bonne prise. Le mécanisme est différent : c'est le même argument de parité que le lemme des traversants seuls déjà démontré dans `4CT_intervalles.md`, pas un argument de comptage. **Énoncé.** Soit v1–v2–…–vn–v1 un noyau d'obstruction de forme « cycle impair » (n ≥ 5 impair), de listes L(v1),…,L(vn). S'il existe deux couleurs {a, b} telles que L(vi) ⊆ {a, b} pour **tout** i, alors le cycle n'admet aucune coloration propre. **Preuve.** Chaque vi doit recevoir une couleur de {a, b} (sa liste y est incluse). Une coloration propre du cycle serait donc une 2-coloration propre du graphe cycle Cn utilisant uniquement {a, b}. Fixons la couleur de v1, disons a. À chaque arête vi–vi+1, l'adjacence force vi+1 à prendre l'unique autre couleur disponible : les couleurs alternent donc strictement a, b, a, b, … le long du cycle, et vi porte la couleur a si i est impair, b si i est pair. Le sommet vn porte donc la couleur b si n est pair, a si n est impair. Or n est impair par hypothèse : vn porte la couleur a, la même que v1 — mais vn et v1 sont adjacents (c'est un cycle), donc doivent porter des couleurs différentes. Contradiction. ∎ **Vérification sur les 19 cas** (ré-implémentation indépendante, 0 écart) : les 19 noyaux « cycle impair » ont tous une réunion de listes de taille ≤ 2, systématiquement égale à {3,4}, avec chaque liste individuelle incluse dans {3,4} (soit {3,4} soit {4} seul). La condition du lemme est donc satisfaite dans les 19 cas, sans exception. **Avec les trois lemmes, 605 des 633 patchs (95,6 %) reposent désormais sur un argument générique de quelques lignes plutôt que sur un calcul au cas par cas.** ## Le lemme des triangles couplés : deux pivots forcés à la même couleur C'est exactement le mécanisme déjà décrit à la main pour `126.687602` au §1.2 du corpus complet (« deux triangles ont chacun des listes compatibles, mais forcent deux sommets adjacents à prendre la même couleur »), généralisé et vérifié sur les 6 cas. **Structure commune.** Chaque triangle {pivot, jambe₁, jambe₂} a un sommet **pivot** de liste à 3 couleurs et deux sommets **jambes** adjacents entre eux, tous deux de liste incluse dans une même paire {a, b}. Les deux triangles sont reliés par une arête unique, entre leurs deux pivots. **Énoncé.** Si, dans chaque triangle, les deux jambes ont des listes incluses dans la **même** paire {a, b} (commune aux deux triangles), et si chaque pivot a une liste incluse dans {a, b, c} pour une **même** troisième couleur c, alors le noyau n'admet aucune coloration propre. **Preuve.** Dans un triangle, les deux jambes sont adjacentes : leurs couleurs doivent différer, et comme leurs listes sont toutes deux incluses dans {a, b} (2 couleurs), elles épuisent nécessairement {a, b} à elles deux — l'une reçoit a, l'autre b, dans un ordre ou l'autre. Le pivot, adjacent aux deux jambes, doit donc éviter à la fois a et b : la seule couleur qui lui reste dans sa liste {a, b, c} est c. Ce raisonnement, identique pour les deux triangles (même paire {a,b}, même couleur c), force les **deux pivots** à la couleur c. Mais les deux pivots sont adjacents (l'arête qui relie les deux triangles) — deux sommets adjacents de même couleur, contradiction. ∎ **Vérification sur les 6 cas** (ré-implémentation indépendante, 0 écart) : chaque noyau se scinde bien en deux triangles reliés par une unique arête pivot-pivot, avec une paire {a,b} et une couleur c communes aux deux côtés : ``` 126.687602 pivots 13-18 {a,b}={3,4} c=2 126.454572 pivots 15-18 {a,b}={3,4} c=2 7322.687602 pivots 13-19 {a,b}={3,4} c=2 8402.363 pivots 16-17 {a,b}={3,4} c=2 440402.363 pivots 18-19 {a,b}={3,4} c=1 504123.136 pivots 18-19 {a,b}={3,4} c=2 ``` **Avec les quatre lemmes, 611 des 633 patchs (96,5 %) — soit tous les noyaux classés dans l'une des quatre formes nommées — reposent désormais sur un argument générique plutôt que sur un calcul au cas par cas.** Ne restent que les 22 noyaux « autre », de structure trop irrégulière pour la classification par forme elle-même. ## Propagation forcée + lemme du triangle : 11 des 22 « autre » de plus Les 22 noyaux « autre » n'ont pas de forme unique, donc pas de lemme structurel unique. Mais une méthode en deux étapes, combinant un principe général et le lemme du triangle déjà démontré, en résout la moitié. **Principe de propagation forcée (arc-consistency).** Tant qu'un sommet v a une liste réduite à un singleton {c}, c est la seule couleur possible pour v dans toute coloration propre ; par adjacence, c doit donc être retirée de la liste de chacun de ses voisins. Répéter jusqu'à stabilisation. C'est valide pour n'importe quel graphe (pas seulement une clique ou un cycle) : c'est une conséquence directe de la définition d'une coloration propre, pas une hypothèse supplémentaire. Deux issues possibles : - un sommet se retrouve avec une liste **vide** : aucune coloration propre n'existe (rien ne peut lui être attribué) ; - sinon, les listes obtenues sont des restrictions **valides** — toute coloration propre du noyau original doit les respecter — auxquelles on peut appliquer un lemme déjà démontré (ici, le lemme du triangle : si un triangle du noyau a, après propagation, une réunion de listes ≤ 2, il est toujours bloqué). **Vérification** (`experiments/kernel_autre_propagation.py`, ré-implémentation indépendante, 0 écart) sur les 22 noyaux « autre » : ``` propagation seule (liste vide) : 6 cas propagation puis lemme du triangle : 5 cas de plus total résolu par cette méthode : 11 / 22 ``` **Avec cette méthode combinée, 622 des 633 patchs (98,3 %) reposent désormais sur un argument générique et vérifié — la propagation forcée étant elle-même un principe général, pas une astuce ad hoc par patch.** ### Les 11 cas qui résistaient à cette étape *(Résolus depuis : voir la section « Le lemme de la composante bicolore » plus bas. Le texte ci-dessous est conservé tel qu'écrit à cette étape.)* ``` 184.460806 2.745566 184.1310466 126.489786 126.458826 126.745566 122.174333962 126.78485226 7563.368 7562.1307280 11046.1307280 ``` Plusieurs (`2.745566`, `126.489786`, `126.458826`, `126.745566`, `7563.368`) partagent une structure en « éventail » : un sommet central adjacent à un chemin de 4 sommets, formant 3 triangles consécutifs qui partagent ce centre. Le mécanisme d'obstruction y est réel mais plus subtil que la propagation simple : il faut suivre, pour chaque couleur possible du centre, si le chemin restant peut encore être colorié — un raisonnement par disjonction de cas sur le centre, pas un critère fermé comme le triangle ou la parité. Je ne l'ai pas mené à bien ici. Les autres (`122.174333962`, `126.78485226`, `7562.1307280`, `11046.1307280`, `184.460806`, `184.1310466`) sont plus grands et plus denses (jusqu'à 11 sommets, 21 arêtes, 11 triangles internes) : leur obstruction reste, pour l'instant, uniquement établie par le calcul d'origine. ## Le lemme de la composante bicolore : les 11 derniers, et les 633 d'un coup ### L'éventail n'est pas un cas nouveau Regardons `2.745566` avec ses listes. Centre 17, liste {3,4} ; chemin 16–13–18–19 autour de lui ; listes 16 : {3,4}, 13 : {2,3,4}, 18 : {2,3,4}, 19 : {3,4}. Les cinq éventails ont exactement ce profil : le centre et les deux extrémités du chemin dans {3,4}, les deux sommets intérieurs du chemin dans {2,3,4}. Il n'y a pas besoin de disjonction de cas sur le centre. Le triangle {17, 16, 13} a deux jambes (17 et 16) adjacentes dont les listes sont dans {3,4} : elles épuisent {3,4}, donc 13 reçoit 2. Le triangle {17, 19, 18}, pour la même raison, force 18 à 2. Or 13 et 18 sont adjacents : contradiction. **C'est exactement le lemme des triangles couplés**, à ceci près que les deux triangles partagent une jambe (le centre) au lieu d'être disjoints — et la preuve écrite plus haut n'utilise jamais que les triangles sont disjoints. La classification par forme avait masqué ce mécanisme en rangeant ces noyaux dans « autre » parce qu'ils n'ont que 5 sommets au lieu de 6. ### Le lemme général La même idée, poussée un cran plus loin, couvre tout. **Énoncé.** Soit {a,b} une paire de couleurs et C une composante connexe du sous-graphe induit par les sommets dont la liste est incluse dans {a,b}. 1. Si C contient un cycle impair, le noyau n'admet aucune coloration. 2. Sinon, C est bipartie, de classes C₀ et C₁. Tout sommet z hors de C, adjacent à au moins un sommet de C₀ **et** à au moins un sommet de C₁, ne peut recevoir ni a ni b : on peut retirer a et b de sa liste. **Preuve.** Chaque sommet de C reçoit a ou b, et deux sommets adjacents de C reçoivent des couleurs différentes. Le long de n'importe quel chemin dans C, les couleurs alternent donc strictement entre a et b. Un cycle impair est impossible (c'est le lemme du cycle impair). Si C est bipartie et connexe, l'alternance fixe tout dès qu'on connaît la couleur d'un seul sommet : C₀ reçoit tout entière une couleur, C₁ tout entière l'autre. Un sommet z qui voit à la fois C₀ et C₁ a donc un voisin de couleur a et un voisin de couleur b. ∎ Avec la règle du singleton déjà utilisée (si L(v) = {c}, retirer c des listes des voisins de v), on applique ces deux règles jusqu'à stabilisation ; on conclut dès qu'une liste devient vide ou qu'un cycle impair apparaît au point 1. Les quatre lemmes structurels ci-dessus sont des cas particuliers : triangle à deux couleurs = cycle impair de longueur 3 dans une composante ; arête bloquée = règle du singleton ; cycle impair = point 1 ; triangles couplés = point 2 appliqué à une composante réduite à une arête (les deux jambes), deux fois. ### Les 11 derniers cas `experiments/kernel_bicolor_component.py` : ``` 184.460806 singleton (20=4 → 17=2 → 12 perd 2), puis cycle impair 12–13–18–19–15 dans {3,4} 2.745566 composante {16,17,19} ⊂ {3,4} → 13 = 2 et 18 = 2, adjacents 126.489786 composante {18,19,20} ⊂ {3,4} → 13 = 2 et 17 = 2, adjacents 126.458826 composante {18,19,22} ⊂ {3,4} → 15 = 2 et 20 = 2, adjacents 126.745566 composante {19,20,22} ⊂ {3,4} → 15 = 2 et 21 = 2, adjacents 7563.368 composante {13,15,18} ⊂ {3,4} → 16 = 2 et 17 = 2, adjacents 184.1310466 composantes {14,16,19,20} et {21,22} ⊂ {3,4} → 13 = 2 et 17 = 2 122.174333962 composante de 8 sommets ⊂ {3,4} → 16 = 2, puis 15 et 22 perdent 3, 4, 2 → 22 = 1 → liste de 15 vide 126.78485226 composantes {18,19,23} et {24,25} ⊂ {3,4} → 20 = 1, puis singletons → liste de 15 vide 7562.1307280 singletons depuis 19 = 4, puis composante {13,18} ⊂ {2,3} → 17 = 4, puis 7 singletons → liste de 16 vide 11046.1307280 même mécanisme que 7562.1307280 (même noyau central) ``` Au plus trois applications du point 2 par noyau ; tout le reste est de la propagation de singletons. Les six « grandes structures denses » ne l'étaient qu'en apparence : chacune contient une ou deux grandes composantes dans {3,4} qui, une fois vues comme telles, forcent tout. ### Contrôles - **Deux moteurs indépendants** (ensembles / masques de bits, ordres de parcours opposés, détection du bipartisme écrite deux fois) : même verdict sur les 633 noyaux, 0 écart. - **Chaque déduction est vérifiée localement par force brute** : pour chaque application du point 2, on énumère toutes les colorations du seul sous-graphe C ∪ {z} avec les listes du moment et on vérifie que z ne reçoit jamais a ni b ; pour chaque cycle impair, on vérifie que C n'a aucune coloration. Aucune déduction ne s'appuie donc sur autre chose que son voisinage immédiat. - **Contrôle négatif** : un moteur qui « trouve » des contradictions partout serait inutile. Chaque noyau privé d'un de ses sommets est coloriable par minimalité ; sur ces 2 018 instances coloriables (les 633 noyaux, un sommet retiré à la fois), les deux moteurs ne concluent **jamais** à une contradiction. ## Portée et ce qui reste **Les 633 noyaux d'obstruction reposent désormais tous sur un argument générique de quelques lignes** — la règle du singleton et le lemme de la composante bicolore, les deux seuls ingrédients nécessaires, appliqués localement et au plus trois fois pour le second. Aucun des 633 n'est plus « établi uniquement par le calcul d'origine ». Ce qui est établi, exactement : pour chaque patch, le premier mot de bord non directement remplissable (dans l'ordre du générateur) a une obstruction explicable à la main. Ce n'est pas une preuve de réductibilité du patch — celle-ci demande de traiter *tous* les mots de bord, par remplissage direct ou par échanges de Kempe (§4 du corpus complet). C'est une explication lisible de **pourquoi** le remplissage direct échoue, sur un témoin par patch. **Mise à jour :** l'extension à tous les mots de bord bloqués (39 941 300, et non plus un par patch) est faite dans `4CT_mots_bloques.md` : tous sont expliqués par les mêmes règles, avec au plus une disjonction sur un sommet pour 1 444 d'entre eux. `atlas_data.json` porte, par patch, les champs `kernel_classification` et `kernel_proof_status` (ce dernier vaut désormais `proven_by_bicolor_component` pour les 11 derniers cas). Le détail complet (répartition croisée forme × taille × test de Hall) est dans `experiments/kernel_classification_summary.json`, les traces des 11 derniers dans `experiments/kernel_bicolor_component_summary.json`.