# Audit palier 2^17 : réduction des états par 175 clauses D10 ## Introduction Ce document mesure, sur le noyau issu des parents « both » au palier 2^15, l’impact des 175 clauses D10 (longueur 10, somme A10=16) stabilisées au palier 2^17, complétées par la fermeture de la sœur via descente minorée. L’objectif est de quantifier la réduction effective des états survivants parmi les 60 états de la base projective B12 (module 4096, horizon 7). ## Ensembles considérés - Parents both au palier 2^15 : |B_15| = 1101 (mod 32768) - Noyau au palier 2^16 après complétion : |R_16^comp| = 2202 (mod 65536) - Noyau au palier 2^17 avant ajout D10 : |R_17^comp,0| = 4404 (mod 131072) Les 175 clauses D10 couvrent 175 classes modulo 2^17, chacune avec sa sœur (décalage 2^16). Ainsi, l’ajout « D10 exact + fermeture minorée de la sœur » supprime 350 résidus au palier 2^17 dans ce noyau. ## Résultats globaux - Résidus retirés par D10 + scission : 350 - Résidu restant : 4054 - États présents avant : 60 - États présents après : 60 - États éliminés (effectif→0) : 0 ## Table de réduction par état (60 états) | état_id | mot_7 | effectif_avant | effectif_après_D10 | retrait | taux_retrait | |----------:|:--------------|-----------------:|---------------------:|----------:|---------------:| | 30 | 1 1 1 1 2 2 2 | 36 | 30 | 6 | 0.166667 | | 33 | 1 1 1 2 1 1 3 | 36 | 30 | 6 | 0.166667 | | 36 | 1 1 1 2 2 2 1 | 36 | 30 | 6 | 0.166667 | | 38 | 1 1 2 1 1 2 2 | 36 | 30 | 6 | 0.166667 | | 41 | 1 1 2 2 1 1 2 | 36 | 30 | 6 | 0.166667 | | 43 | 1 2 1 1 1 1 3 | 36 | 30 | 6 | 0.166667 | | 46 | 1 2 1 1 2 2 1 | 36 | 30 | 6 | 0.166667 | | 47 | 1 2 1 2 1 1 2 | 36 | 30 | 6 | 0.166667 | | 49 | 1 1 1 1 1 2 4 | 12 | 10 | 2 | 0.166667 | | 50 | 1 1 1 1 1 4 2 | 12 | 10 | 2 | 0.166667 | | 51 | 1 1 1 1 2 1 4 | 12 | 10 | 2 | 0.166667 | | 52 | 1 1 1 1 3 2 2 | 12 | 10 | 2 | 0.166667 | | 53 | 1 1 1 2 1 1 4 | 12 | 10 | 2 | 0.166667 | | 54 | 1 1 1 2 2 2 2 | 12 | 10 | 2 | 0.166667 | | 55 | 1 1 2 1 1 1 4 | 12 | 10 | 2 | 0.166667 | | 56 | 1 1 2 1 2 2 2 | 12 | 10 | 2 | 0.166667 | | 57 | 1 1 2 2 1 2 2 | 12 | 10 | 2 | 0.166667 | | 60 | 1 2 1 2 1 2 2 | 12 | 10 | 2 | 0.166667 | | 11 | 1 1 1 1 2 1 2 | 96 | 84 | 12 | 0.125 | | 27 | 1 1 1 1 1 3 2 | 36 | 32 | 4 | 0.111111 | | 28 | 1 1 1 1 1 4 1 | 36 | 32 | 4 | 0.111111 | | 29 | 1 1 1 1 2 1 3 | 36 | 32 | 4 | 0.111111 | | 31 | 1 1 1 1 3 1 2 | 36 | 32 | 4 | 0.111111 | | 32 | 1 1 1 1 3 2 1 | 36 | 32 | 4 | 0.111111 | | 34 | 1 1 1 2 1 2 2 | 36 | 32 | 4 | 0.111111 | | 37 | 1 1 2 1 1 1 3 | 36 | 32 | 4 | 0.111111 | | 40 | 1 1 2 1 2 2 1 | 36 | 32 | 4 | 0.111111 | | 42 | 1 1 2 2 1 2 1 | 36 | 32 | 4 | 0.111111 | | 45 | 1 2 1 1 2 1 2 | 36 | 32 | 4 | 0.111111 | | 9 | 1 1 1 1 1 2 2 | 96 | 86 | 10 | 0.104167 | | 10 | 1 1 1 1 1 3 1 | 96 | 86 | 10 | 0.104167 | | 12 | 1 1 1 1 2 2 1 | 96 | 86 | 10 | 0.104167 | | 16 | 1 1 1 2 2 1 1 | 96 | 86 | 10 | 0.104167 | | 23 | 1 2 1 1 2 1 1 | 96 | 86 | 10 | 0.104167 | | 14 | 1 1 1 2 1 1 2 | 96 | 88 | 8 | 0.0833333 | | 17 | 1 1 2 1 1 1 2 | 96 | 88 | 8 | 0.0833333 | | 19 | 1 1 2 1 2 1 1 | 96 | 88 | 8 | 0.0833333 | | 20 | 1 1 2 2 1 1 1 | 96 | 88 | 8 | 0.0833333 | | 22 | 1 2 1 1 1 2 1 | 96 | 88 | 8 | 0.0833333 | | 3 | 1 1 1 1 1 2 1 | 216 | 200 | 16 | 0.0740741 | | 4 | 1 1 1 1 2 1 1 | 216 | 202 | 14 | 0.0648148 | | 6 | 1 1 2 1 1 1 1 | 216 | 202 | 14 | 0.0648148 | | 8 | 1 1 1 1 1 1 3 | 96 | 90 | 6 | 0.0625 | | 13 | 1 1 1 1 3 1 1 | 96 | 90 | 6 | 0.0625 | | 15 | 1 1 1 2 1 2 1 | 96 | 90 | 6 | 0.0625 | | 18 | 1 1 2 1 1 2 1 | 96 | 90 | 6 | 0.0625 | | 21 | 1 2 1 1 1 1 2 | 96 | 90 | 6 | 0.0625 | | 24 | 1 2 1 2 1 1 1 | 96 | 90 | 6 | 0.0625 | | 2 | 1 1 1 1 1 1 2 | 216 | 204 | 12 | 0.0555556 | | 5 | 1 1 1 2 1 1 1 | 216 | 204 | 12 | 0.0555556 | | 7 | 1 2 1 1 1 1 1 | 216 | 204 | 12 | 0.0555556 | | 25 | 1 1 1 1 1 1 4 | 36 | 34 | 2 | 0.0555556 | | 26 | 1 1 1 1 1 2 3 | 36 | 34 | 2 | 0.0555556 | | 35 | 1 1 1 2 2 1 2 | 36 | 34 | 2 | 0.0555556 | | 39 | 1 1 2 1 2 1 2 | 36 | 34 | 2 | 0.0555556 | | 44 | 1 2 1 1 1 2 2 | 36 | 34 | 2 | 0.0555556 | | 48 | 1 2 1 2 1 2 1 | 36 | 34 | 2 | 0.0555556 | | 1 | 1 1 1 1 1 1 1 | 468 | 456 | 12 | 0.025641 | | 58 | 1 2 1 1 1 1 4 | 12 | 12 | 0 | 0 | | 59 | 1 2 1 1 2 2 2 | 12 | 12 | 0 | 0 | ## États éliminés | état_id | mot_7 | effectif_avant | |-----------|---------|------------------| ## États survivants (triés par effectif après D10) | état_id | mot_7 | effectif_après_D10 | |----------:|:--------------|---------------------:| | 1 | 1 1 1 1 1 1 1 | 456 | | 2 | 1 1 1 1 1 1 2 | 204 | | 7 | 1 2 1 1 1 1 1 | 204 | | 5 | 1 1 1 2 1 1 1 | 204 | | 4 | 1 1 1 1 2 1 1 | 202 | | 6 | 1 1 2 1 1 1 1 | 202 | | 3 | 1 1 1 1 1 2 1 | 200 | | 24 | 1 2 1 2 1 1 1 | 90 | | 21 | 1 2 1 1 1 1 2 | 90 | | 18 | 1 1 2 1 1 2 1 | 90 | | 15 | 1 1 1 2 1 2 1 | 90 | | 13 | 1 1 1 1 3 1 1 | 90 | | 8 | 1 1 1 1 1 1 3 | 90 | | 17 | 1 1 2 1 1 1 2 | 88 | | 14 | 1 1 1 2 1 1 2 | 88 | | 19 | 1 1 2 1 2 1 1 | 88 | | 20 | 1 1 2 2 1 1 1 | 88 | | 22 | 1 2 1 1 1 2 1 | 88 | | 23 | 1 2 1 1 2 1 1 | 86 | | 9 | 1 1 1 1 1 2 2 | 86 | | 16 | 1 1 1 2 2 1 1 | 86 | | 12 | 1 1 1 1 2 2 1 | 86 | | 10 | 1 1 1 1 1 3 1 | 86 | | 11 | 1 1 1 1 2 1 2 | 84 | | 48 | 1 2 1 2 1 2 1 | 34 | | 44 | 1 2 1 1 1 2 2 | 34 | | 39 | 1 1 2 1 2 1 2 | 34 | | 35 | 1 1 1 2 2 1 2 | 34 | | 26 | 1 1 1 1 1 2 3 | 34 | | 25 | 1 1 1 1 1 1 4 | 34 | | 32 | 1 1 1 1 3 2 1 | 32 | | 27 | 1 1 1 1 1 3 2 | 32 | | 34 | 1 1 1 2 1 2 2 | 32 | | 29 | 1 1 1 1 2 1 3 | 32 | | 31 | 1 1 1 1 3 1 2 | 32 | | 45 | 1 2 1 1 2 1 2 | 32 | | 42 | 1 1 2 2 1 2 1 | 32 | | 40 | 1 1 2 1 2 2 1 | 32 | | 37 | 1 1 2 1 1 1 3 | 32 | | 28 | 1 1 1 1 1 4 1 | 32 | | 30 | 1 1 1 1 2 2 2 | 30 | | 33 | 1 1 1 2 1 1 3 | 30 | | 47 | 1 2 1 2 1 1 2 | 30 | | 36 | 1 1 1 2 2 2 1 | 30 | | 38 | 1 1 2 1 1 2 2 | 30 | | 41 | 1 1 2 2 1 1 2 | 30 | | 43 | 1 2 1 1 1 1 3 | 30 | | 46 | 1 2 1 1 2 2 1 | 30 | | 58 | 1 2 1 1 1 1 4 | 12 | | 59 | 1 2 1 1 2 2 2 | 12 | | 60 | 1 2 1 2 1 2 2 | 10 | | 49 | 1 1 1 1 1 2 4 | 10 | | 51 | 1 1 1 1 2 1 4 | 10 | | 52 | 1 1 1 1 3 2 2 | 10 | | 53 | 1 1 1 2 1 1 4 | 10 | | 54 | 1 1 1 2 2 2 2 | 10 | | 55 | 1 1 2 1 1 1 4 | 10 | | 56 | 1 1 2 1 2 2 2 | 10 | | 57 | 1 1 2 2 1 2 2 | 10 | | 50 | 1 1 1 1 1 4 2 | 10 | ## Conclusion Le palier 2^17 fournit une première itération explicite du « lemme d’extinction » : l’ajout d’un paquet fini de clauses contractives stabilisées (ici D10) retire un sous-ensemble mesurable du noyau issu des parents both, et modifie la distribution d’états survivants. La suite consiste à compléter cette réduction par (i) les blocs contractifs longueur 8 stabilisés à 2^14 (transposés aux relèvements), et (ii) des fusions additionnelles t=6,7 ciblant les états survivants dominants.