# Dossiers de preuve complets, mot par mot

Un fichier par configuration de bord ≤ 11 : ici pour les 7 configurations de
bord ≤ 8, et dans [bords_9_11/](bords_9_11/README.md) pour les 120
configurations de bord 9 à 11 (680 712 mots, fichiers compressés en gzip).
Chaque mot de bord (coloration du
bord à permutation des couleurs près) y reçoit sa justification complète :

- **rang 0** : un remplissage explicite de l'intérieur ;
- **mot bloqué** : pourquoi il ne se remplit pas directement (sommets
  forcés, lemme de la composante bicolore, au besoin une disjonction), puis
  comment il est résolu — couleur d'arête θ, règle à un ruban (étoile,
  oreilles, séparation récursive) avec chaque ruban utile, ou règle à
  marques fixes rédigée en conditions « si ces rubans existent, les
  échanger », avec le mot obtenu et son rang, strictement inférieur ;
- **mot du résidu** (configuration à contraction) : pourquoi il est bloqué,
  et le fait que la contraction ne le produit jamais.

| Configuration | Type | Mots | Remplis | Bloqués | dont résidu | dont marques fixes (rédigées) |
| --- | --- | ---: | ---: | ---: | ---: | ---: |
| [0.7322](0.7322.md) | D | 31 | 16 | 15 | 0 | 0 |
| [2.122](2.122.md) | D | 91 | 39 | 52 | 0 | 0 |
| [3.442802](3.442802.md) | D | 274 | 111 | 163 | 0 | 2 |
| [2.126](2.126.md) | C | 274 | 81 | 193 | 154 | 4 |
| [0.453962](0.453962.md) | D | 274 | 100 | 174 | 0 | 3 |
| [0.79077722](0.79077722.md) | D | 274 | 104 | 170 | 0 | 7 |
| [122.122](122.122.md) | D | 274 | 95 | 179 | 0 | 3 |

**Les sept dossiers sont entièrement rédigés** : chaque mot est justifié à la
main, sans aucun renvoi au calcul, à une seule exception près —
l'existence des rubans dans l'extérieur réel, qui est le lemme de
consistance de RSST, cité. `0.7322` et `2.122` n'utilisent que des règles à
un ruban ; dans les cinq autres, 2 à 7 mots par configuration utilisent une
règle à marques fixes, rédigée en 4 à 7 conditions. Pour `2.126`, il faut y
ajouter l'admissibilité de sa contraction, prouvée dans
`4CT_admissibilite_contractions.md`.

**Lire une règle à marques fixes.** θ et deux ou trois arêtes, les marques,
sont fixées avant de connaître l'extérieur. Chaque condition porte sur des
rubans qui touchent les marques, par exemple « si 1–2 et 5–8 : échanger ».
La liste finale donne toutes les façons dont les marques peuvent être
reliées à leurs partenaires dans un appariement sans croisement ; chacune
contient l'une des conditions, qu'il suffit donc de vérifier. Échanger
plusieurs rubans ensemble applique la permutation de θ aux sommets de bord
couverts un nombre impair de fois par les intervalles X+1..Y des rubans
échangés.

Tout est revérifié par `experiments/build_proof_dossiers.py`, indépendamment
du programme C qui fournit les rangs :
- chaque remplissage est vérifié arête par arête, et l'absence de
  remplissage de chaque mot bloqué par recherche exhaustive ;
- chaque dérivation de non-remplissage est recalculée ;
- chaque mot cible est recalculé à partir du mot par la règle « échanger le
  ruban qui relie les arêtes X et Y revient à appliquer une permutation fixe
  aux sommets de bord X+1 à Y » ;
- chaque ruban déclaré utile mène à un rang strictement inférieur, et la
  condition de chaque règle (centre de l'étoile, oreilles, séparation) est
  revérifiée ;
- chaque règle à marques fixes est retrouvée par `experiments/fixed_marks.py`
  sans rien emprunter au programme C que la table des rangs (même nature de
  règle que le programme C dans les 19 cas) ; on vérifie que chaque connexion
  possible des marques contient une condition, et que chaque condition est
  indispensable ;
- la règle générale d'élimination (règle B) est revérifiée pour chacun des
  792 mots bloqués de rang positif, en énumérant tous les appariements ;
- pour `2.126`, les 18 mots produits par la contraction sont recalculés par
  coloration du graphe contracté, et aucun n'est dans le résidu.

Le fichier [128.25876_12323212343232.md](128.25876_12323212343232.md)
donne à part l'argument en 50 cas du seul mot qui n'avait aucune règle
lisible (voir `4CT_arbres_de_cas.md`).

[catalogue_des_formes.md](catalogue_des_formes.md) décrit les 30 formes
d'arbres de cas les plus fréquentes du corpus (95 % des déductions), avec
des exemples complets. [familles_de_formes.md](familles_de_formes.md) les
regroupe en familles plus larges (squelettes, profils, gabarits, types).

Pour régénérer : `python3 experiments/run_exchange_link.py` (environ 6 min
CPU, il rejoue toute la chaîne des règles d'échange), puis
`python3 experiments/build_proof_dossiers.py` (environ 10 min sur 4 cœurs ;
`petits` ou `9-11` en argument pour ne refaire qu'une partie).

**Bords 9 à 11.** Mêmes vérifications, et deux ajouts. Les 303 mots relevant
d'une règle d'intervalle y sont rédigés comme une règle à quatre marques
fixes (`experiments/interval_readable.py`), lue exactement comme les autres.
Pour `128.136`, la contraction utilisée est la contraction de remplacement
de `4CT_contractions_de_remplacement.md`, et le résidu est revérifié
contre elle. Bilan : 53 352 règles à marques fixes et 303 règles
d'intervalle rédigées, aucun mot sans règle lisible, 0 erreur
(`experiments/proof_dossiers_check.json`).