algo/docs/artefacts/collatz/conjoncture_rationalisation/audit_conjoncture.md

**Auteur** : Équipe 4NK

# Audit déterministe — `conjoncture_collatz.md`

## Entrée

- fichier : `/home/ncantu/code/algo/applications/collatz/conjoncture_collatz.md`

## Statistiques

- lignes : 16975
- headings total : 996
- groupes de headings dupliqués (tous niveaux) : 344

## Bornes détectées (rationalisation)

- occurrences `# Conjecture de Collatz:` : [1]
- canonical_end_line (premier bloc H1) : 16975
- début bloc importé : None
- fin bloc importé : None
- première section `## Branche ...` : 287

## Doublons — top groupes

| level | count | title_norm | occurrences (first 10) |
| --- | --- | --- | --- |
| 2 | 4 | `audit exhaustif` | L4432:Audit exhaustif, L4751:Audit exhaustif, L14005:Audit exhaustif, L14324:Audit exhaustif |
| 2 | 4 | `conclusion de l'analyse du palier 16384` | L2001:Conclusion de l'analyse du palier 16384, L2237:Conclusion de l'analyse du palier 16384, L11574:Conclusion de l'analyse du palier 16384, L11810:Conclusion de l'analyse du palier 16384 |
| 2 | 4 | `etape analytique suivante` | L462:Étape analytique suivante, L1589:Étape analytique suivante, L10035:Étape analytique suivante, L11162:Étape analytique suivante |
| 2 | 4 | `impact par etat` | L6427:Impact par état, L6633:Impact par état, L16000:Impact par état, L16206:Impact par état |
| 2 | 4 | `introduction de l'analyse du palier 16384` | L1814:Introduction de l'analyse du palier 16384, L2012:Introduction de l'analyse du palier 16384, L11387:Introduction de l'analyse du palier 16384, L11585:Introduction de l'analyse du palier 16384 |
| 2 | 4 | `prolongement immediat au palier (2^{14})` | L2206:Prolongement immédiat au palier (2^{14}), L2445:Prolongement immédiat au palier (2^{14}), L11779:Prolongement immédiat au palier (2^{14}), L12018:Prolongement immédiat au palier (2^{14}) |
| 3 | 4 | `enonce` | L5729:Énoncé, L7234:Énoncé, L7272:Énoncé, L15302:Énoncé |
| 1 | 2 | `\frac{2202}{2690}` | L4838:\frac{2202}{2690}, L14411:\frac{2202}{2690} |
| 2 | 2 | `ajout d’une fusion (f) deja demontree : (799\bmod 1024)` | L1524:Ajout d’une fusion (F) déjà démontrée : (799\bmod 1024), L11097:Ajout d’une fusion (F) déjà démontrée : (799\bmod 1024) |
| 2 | 2 | `application canonique au sommet (255) et a sa chaine henselienne` | L2333:Application canonique au sommet (255) et à sa chaîne henselienne, L11906:Application canonique au sommet (255) et à sa chaîne henselienne |
| 2 | 2 | `attaque du noyau a l’horizon 10 : candidats d10 stabilises a (2^{17})` | L5572:Attaque du noyau à l’horizon 10 : candidats D10 stabilisés à (2^{17}), L15145:Attaque du noyau à l’horizon 10 : candidats D10 stabilisés à (2^{17}) |
| 2 | 2 | `audit fourni` | L4896:Audit fourni, L14469:Audit fourni |
| 2 | 2 | `audits fournis (exhaustifs)` | L6893:Audits fournis (exhaustifs), L16466:Audits fournis (exhaustifs) |
| 2 | 2 | `autre raffinement : extinction sans borne uniforme stricte` | L2536:Autre raffinement : extinction sans borne uniforme stricte, L12109:Autre raffinement : extinction sans borne uniforme stricte |
| 2 | 2 | `bilan quantitatif sur la branche (31\pmod{32}) au palier (16384)` | L1971:Bilan quantitatif sur la branche (31\pmod{32}) au palier (16384), L11544:Bilan quantitatif sur la branche (31\pmod{32}) au palier (16384) |
| 2 | 2 | `bloc contractif au palier (2^{14})` | L2019:Bloc contractif au palier (2^{14}), L11592:Bloc contractif au palier (2^{14}) |
| 2 | 2 | `branche (15 \bmod 32) : fermeture uniforme d’une sous-classe de petit module` | L287:Branche (15 \bmod 32) : fermeture uniforme d’une sous-classe de petit module, L9860:Branche (15 \bmod 32) : fermeture uniforme d’une sous-classe de petit module |
| 2 | 2 | `branche (15 \pmod{32})` | L634:Branche (15 \pmod{32}), L10207:Branche (15 \pmod{32}) |
| 2 | 2 | `branche (27 \bmod 32) : fermeture uniforme deja disponible a petit module` | L341:Branche (27 \bmod 32) : fermeture uniforme déjà disponible à petit module, L9914:Branche (27 \bmod 32) : fermeture uniforme déjà disponible à petit module |
| 2 | 2 | `branche (27 \pmod{32})` | L768:Branche (27 \pmod{32}), L10341:Branche (27 \pmod{32}) |
| 2 | 2 | `branche (31 \bmod 32) : fermeture uniforme a module 512 (descente en profondeur 5)` | L396:Branche (31 \bmod 32) : fermeture uniforme à module 512 (descente en profondeur 5), L9969:Branche (31 \bmod 32) : fermeture uniforme à module 512 (descente en profondeur 5) |
| 2 | 2 | `branche (31 \pmod{32})` | L948:Branche (31 \pmod{32}), L10521:Branche (31 \pmod{32}) |
| 2 | 2 | `branche (7 \pmod{32})` | L501:Branche (7 \pmod{32}), L10074:Branche (7 \pmod{32}) |
| 2 | 2 | `cadre formel de preuve` | L3843:Cadre formel de preuve, L13416:Cadre formel de preuve |
| 2 | 2 | `cas difficile dans ce sous-cas : (t) impair, donc (a_5=1)` | L3184:Cas difficile dans ce sous-cas : (t) impair, donc (a_5=1), L12757:Cas difficile dans ce sous-cas : (t) impair, donc (a_5=1) |
| 2 | 2 | `ce que cela apporte a la preuve globale` | L4426:Ce que cela apporte à la preuve globale, L13999:Ce que cela apporte à la preuve globale |
| 2 | 2 | `ce que cette derivation apporte a la recherche` | L3325:Ce que cette dérivation apporte à la recherche, L12898:Ce que cette dérivation apporte à la recherche |
| 2 | 2 | `ce que doit exprimer le lemme` | L5215:Ce que doit exprimer le lemme, L14788:Ce que doit exprimer le lemme |
| 2 | 2 | `ce que fournit l’audit` | L6331:Ce que fournit l’audit, L15904:Ce que fournit l’audit |
| 2 | 2 | `ce qui reste a faire immediatement (et qui est pret a etre produit)` | L5012:Ce qui reste à faire immédiatement (et qui est prêt à être produit), L14585:Ce qui reste à faire immédiatement (et qui est prêt à être produit) |

## TOC canonique (bloc initial)

- L5 `Introduction de l'objet mathématique`
- L15 `Prérequis de lecture`
- L24 `Cadre de référence et notations`
  - L26 `Définition 1 (Application de Syracuse accélérée sur les impairs)`
  - L35 `Définition 2 (Conjecture de Collatz, forme impairs \(\to\) impairs)`
  - L41 `Définition 3 (Classe congruentielle et palier)`
  - L50 `Définition 4 (Clause de registre)`
- L63 `Statut des énoncés`
- L70 `Trajectoire hybride instrumentée (C1→C2→C3) et artefacts déterministes`
- L100 `Énoncés démontrés`
  - L102 `Lemme 1 (Forme affine le long d'un préfixe de valuations)`
  - L128 `Lemme 2 (Clause de descente directe \(D\))`
  - L154 `Lemme 3 (Clause de fusion \(F\), version \(a=1\))`
- L178 `Théorème-cadre conditionnel`
  - L180 `Théorème 1 (Certificat fini \((K)\Rightarrow\) terminaison globale)`
- L197 `État quantifié actuel (indexé par les choix)`
  - L201 `Proposition 1 (Couverture partielle à profondeur 16)`
- L220 `Protocoles de sensibilité`
  - L222 `Définition 5 (Sensibilités étudiées)`
  - L230 `Protocole R1 (Variation de palier)`
  - L234 `Protocole R2 (Variation de grammaire)`
  - L247 `Protocole R3 (Auditabilité du registre)`
- L257 `Limites explicites du cadre`
- L263 `Conclusion de l'état de preuve`
- L267 `Références`
- L276 `Annexes (contenu déplacé)`
- L287 `Branche (15 \bmod 32) : fermeture uniforme d’une sous-classe de petit module`
  - L289 `Proposition 15-A`
- L337 `Conclusion de la section précédente (CSP-001)`
- L341 `Branche (27 \bmod 32) : fermeture uniforme déjà disponible à petit module`
  - L345 `Proposition 27-A`
- L392 `Conclusion de la section précédente (CSP-002)`
- L396 `Branche (31 \bmod 32) : fermeture uniforme à module 512 (descente en profondeur 5)`
  - L398 `Proposition 31-A`
- L447 `Conclusion de la section précédente (CSP-003)`
- L451 `Lecture analytique commune des quatre propositions`
- L462 `Étape analytique suivante`
- L475 `Conclusion de la section sur les clauses grossières et la continuation analytique`
- L481 `Introduction à la densification des lemmes et à la couverture exhaustive`
- L487 `Rappels`
- L501 `Branche (7 \pmod{32})`
  - L503 `Proposition 7-B`
- L549 `Conclusion de la section précédente (CSP-004)`
  - L555 `Proposition 7-C`
- L601 `Conclusion de la section précédente (CSP-005)`
  - L607 `Couverture exhaustive au module 512 pour la branche (7 \pmod{32})`
- L634 `Branche (15 \pmod{32})`
  - L636 `Proposition 15-B`
- L682 `Conclusion de la section précédente (CSP-006)`
  - L688 `Proposition 15-C`
- L734 `Conclusion de la section précédente (CSP-007)`
  - L740 `Couverture exhaustive au module 512 pour la branche (15 \pmod{32})`
- L768 `Branche (27 \pmod{32})`
  - L770 `Proposition 27-B`
- L810 `Conclusion de la section précédente (CSP-008)`
  - L816 `Proposition 27-C`
- L862 `Conclusion de la section précédente (CSP-009)`
  - L868 `Proposition 27-D`
- L914 `Conclusion de la section précédente (CSP-010)`
  - L920 `Couverture exhaustive au module 512 pour la branche (27 \pmod{32})`
- L948 `Branche (31 \pmod{32})`
  - L952 `Proposition 31-B (descente)`
- L998 `Conclusion de la section précédente (CSP-011)`
  - L1004 `Proposition 31-C (fusion, préimage courte (a=1))`
- L1043 `Conclusion de la section précédente (CSP-012)`
  - L1050 `Proposition 31-D (descente à module 2048)`
- L1096 `Conclusion de la section précédente (CSP-013)`
  - L1102 `Proposition 31-E (descente à module 2048)`
- L1146 `Conclusion de la section précédente (CSP-014)`
  - L1152 `Couverture exhaustive au module 1024 pour la branche (31 \pmod{32})`
- L1180 `Lecture analytique de l’étape atteinte`
- L1192 `Conclusion de la section sur la couverture exhaustive aux modules 512 et 1024`
- L1200 `Introduction à l'analyse structurée de la branche 31 modulo 32`
- L1206 `Préfixe universel sur la branche (31 \pmod{32})`
  - L1208 `Lemme 31-0 (préfixe (1^4))`
- L1251 `Étape analytique : la valuation (a_4) est gouvernée par (v_2(243n+211))`
  - L1262 `Lemme 31-1 (divisibilité minimale)`
- L1283 `Conclusion de la section précédente (CSP-015)`
  - L1287 `Résolution systématique des congruences`
- L1322 `Premier lemme de descente uniforme à grande portée : (n\equiv 95 \pmod{256})`
  - L1324 `Proposition 31-A (descente en 5 pas sur (95\bmod 256))`
- L1357 `Conclusion de la section précédente (CSP-016)`
- L1368 `Deuxième lemme : descente en 6 pas via la congruence (575\bmod 1024)`
  - L1372 `Proposition 31-B (descente en 6 pas sur (575\bmod 1024))`
- L1408 `Conclusion de la section précédente (CSP-017)`
- L1417 `Troisième lemme : descente en 6 pas via la congruence (735\bmod 1024)`
  - L1421 `Proposition 31-C (descente en 6 pas sur (735\bmod 1024))`
- L1463 `Conclusion de la section précédente (CSP-018)`
- L1472 `Quatrième lemme : descente en 6 pas via la congruence (1311\bmod 2048)`
  - L1476 `Proposition 31-D (descente en 6 pas sur (1311\bmod 2048))`
- L1518 `Conclusion de la section précédente (CSP-019)`
- L1524 `Ajout d’une fusion (F) déjà démontrée : (799\bmod 1024)`
  - L1528 `Proposition 31-E (fusion en 6 pas sur (799\bmod 1024))`
- L1550 `Couverture exhaustive au module (2048) pour la branche (31 \pmod{32})`
  - L1552 `Liste exhaustive des 64 résidus (modulo 2048)`
  - L1564 `Résidus couverts par les propositions 31-A à 31-E`
  - L1577 `Complément non couvert (exhaustif)`
- L1589 `Étape analytique suivante`
- L1600 `Conclusion de la section sur la couverture de la branche 31 au module 2048`
- L1608 `Introduction à l'analyse de la branche 31`
- L1806 `Conclusion de la section précédente (CSP-020)`
- L1814 `Introduction de l'analyse du palier 16384`
- L1820 `Consolidation analytique au palier (8192) sur la branche (31\pmod{32})`
- L1865 `Nouvelle clause analytique significative : (n\equiv 1759 \pmod{2048}\Rightarrow U^{(6)}(n)<n)`
  - L1869 `Proposition`
- L1921 `Conclusion de l'étape (CE-001)`
- L1925 `Passage analytique au palier (16384) : nouvelles clauses contractives à horizon (k=8)`
  - L1933 `Exemple détaillé : clause (n\equiv 255\pmod{16384})`
  - L1965 `Ensemble des nouvelles classes au palier (16384)`
- L1971 `Bilan quantitatif sur la branche (31\pmod{32}) au palier (16384)`
- L2001 `Conclusion de l'analyse du palier 16384`
- L2012 `Introduction de l'analyse du palier 16384`
- L2019 `Bloc contractif au palier (2^{14})`
- L2036 `Sommet (255) au palier (2^{14}) : clause (D) explicite`
  - L2043 `Préfixe long (a_i=1)`
  - L2053 `Numérateur linéaire contrôlant la valuation suivante`
  - L2068 `Cas (n\equiv 255\pmod{16384}) : (a_7=6), donc (A=13)`
- L2108 `Dédoublement au palier (2^{14}) : (255) et (8447)`
- L2128 `Clause de descente par minoration : fermer (8447) dès (2^{14})`
- L2163 `Indicateur pertinent vers une “masse critique” : coefficient de survie (q_m)`

(TOC tronquée : 991 entrées)

## Table de renvois (headings `##` dupliqués)

Chaque ligne pointe vers une occurrence canonique (première) et liste les duplicats.

| title_norm | canonical | duplicates (lines) |
| --- | --- | --- |
| `ajout d’une fusion (f) deja demontree : (799\bmod 1024)` | L1524:Ajout d’une fusion (F) déjà démontrée : (799\bmod 1024) | L11097 |
| `application canonique au sommet (255) et a sa chaine henselienne` | L2333:Application canonique au sommet (255) et à sa chaîne henselienne | L11906 |
| `attaque du noyau a l’horizon 10 : candidats d10 stabilises a (2^{17})` | L5572:Attaque du noyau à l’horizon 10 : candidats D10 stabilisés à (2^{17}) | L15145 |
| `audit exhaustif` | L4432:Audit exhaustif | L4751, L14005, L14324 |
| `audit fourni` | L4896:Audit fourni | L14469 |
| `audits fournis (exhaustifs)` | L6893:Audits fournis (exhaustifs) | L16466 |
| `autre raffinement : extinction sans borne uniforme stricte` | L2536:Autre raffinement : extinction sans borne uniforme stricte | L12109 |
| `bilan quantitatif sur la branche (31\pmod{32}) au palier (16384)` | L1971:Bilan quantitatif sur la branche (31\pmod{32}) au palier (16384) | L11544 |
| `bloc contractif au palier (2^{14})` | L2019:Bloc contractif au palier (2^{14}) | L11592 |
| `branche (15 \bmod 32) : fermeture uniforme d’une sous-classe de petit module` | L287:Branche (15 \bmod 32) : fermeture uniforme d’une sous-classe de petit module | L9860 |
| `branche (15 \pmod{32})` | L634:Branche (15 \pmod{32}) | L10207 |
| `branche (27 \bmod 32) : fermeture uniforme deja disponible a petit module` | L341:Branche (27 \bmod 32) : fermeture uniforme déjà disponible à petit module | L9914 |
| `branche (27 \pmod{32})` | L768:Branche (27 \pmod{32}) | L10341 |
| `branche (31 \bmod 32) : fermeture uniforme a module 512 (descente en profondeur 5)` | L396:Branche (31 \bmod 32) : fermeture uniforme à module 512 (descente en profondeur 5) | L9969 |
| `branche (31 \pmod{32})` | L948:Branche (31 \pmod{32}) | L10521 |
| `branche (7 \pmod{32})` | L501:Branche (7 \pmod{32}) | L10074 |
| `cadre formel de preuve` | L3843:Cadre formel de preuve | L13416 |
| `cas difficile dans ce sous-cas : (t) impair, donc (a_5=1)` | L3184:Cas difficile dans ce sous-cas : (t) impair, donc (a_5=1) | L12757 |
| `ce que cela apporte a la preuve globale` | L4426:Ce que cela apporte à la preuve globale | L13999 |
| `ce que cette derivation apporte a la recherche` | L3325:Ce que cette dérivation apporte à la recherche | L12898 |
| `ce que doit exprimer le lemme` | L5215:Ce que doit exprimer le lemme | L14788 |
| `ce que fournit l’audit` | L6331:Ce que fournit l’audit | L15904 |
| `ce qui reste a faire immediatement (et qui est pret a etre produit)` | L5012:Ce qui reste à faire immédiatement (et qui est prêt à être produit) | L14585 |
| `ce qui reste a faire pour la suite immediate (deja prepare conceptuellement)` | L6912:Ce qui reste à faire pour la suite immédiate (déjà préparé conceptuellement) | L16485 |
| `ce qu’il reste a verrouiller pour une preuve complete` | L5589:Ce qu’il reste à verrouiller pour une preuve complète | L15162 |
| `chaine de domaines analyses` | L6137:Chaîne de domaines analysés | L15710 |
| `clause de descente par minoration : fermer (8447) des (2^{14})` | L2128:Clause de descente par minoration : fermer (8447) dès (2^{14}) | L11701 |
| `clause de fusion contractante correspondante` | L3297:Clause de fusion contractante correspondante | L12870 |
| `clauses de descente (d) : condition structurelle et seuil` | L5420:Clauses de descente (D) : condition structurelle et seuil | L14993 |
| `clauses de descente minorees` | L2287:Clauses de descente minorées | L11860 |
| `clauses de descente minorees (d⋆) : fermeture sans exactitude de valuation` | L5461:Clauses de descente minorées (D⋆) : fermeture sans exactitude de valuation | L15034 |
| `clauses de fusion (f1) : reduction inductive stricte` | L5480:Clauses de fusion (F1) : réduction inductive stricte | L15053 |
| `clauses et correction locale` | L5646:Clauses et correction locale | L15219 |
| `comment cela se reinjecte dans le « lemme d’extinction » (forme standard)` | L6170:Comment cela se réinjecte dans le « lemme d’extinction » (forme standard) | L15743 |
| `comment les clauses (f) s’integrent dans la table de transition d’etats` | L6793:Comment les clauses (F) s’intègrent dans la table de transition d’états | L16366 |
| `comment transformer cela en un lemme d’extinction au palier 2^17` | L5892:Comment transformer cela en un lemme d’extinction au palier 2^17 | L15465 |
| `comparaison des seuils d et f sur les longueurs utiles` | L2626:Comparaison des seuils D et F sur les longueurs utiles | L12199 |
| `conclusion de l'analyse au pas 8 sur la base projective b12` | L5091:Conclusion de l'analyse au pas 8 sur la base projective B12 | L14664 |
| `conclusion de l'analyse du palier 16384` | L2001:Conclusion de l'analyse du palier 16384 | L2237, L11574, L11810 |
| `conclusion de l'audit de reduction au palier \(2^{17}\)` | L5957:Conclusion de l'audit de réduction au palier \(2^{17}\) | L15530 |
| `conclusion de l'espace d'etat etendu` | L5803:Conclusion de l'espace d'état étendu | L15376 |
| `conclusion de l'etape sur les clauses d10` | L5198:Conclusion de l'étape sur les clauses D10 | L14771 |
| `conclusion de l'etat de preuve` | L263:Conclusion de l'état de preuve | L16962 |
| `conclusion de la formalisation structuree` | L5605:Conclusion de la formalisation structurée | L15178 |
| `conclusion de la section sur la base projective du noyau both` | L4907:Conclusion de la section sur la base projective du noyau both | L14480 |
| `conclusion de la section sur la completion au palier 16384` | L4314:Conclusion de la section sur la complétion au palier 16384 | L13887 |
| `conclusion de la section sur la completion au palier 32768` | L4443:Conclusion de la section sur la complétion au palier 32768 | L14016 |
| `conclusion de la section sur la couverture de la branche 31 au module 2048` | L1600:Conclusion de la section sur la couverture de la branche 31 au module 2048 | L11173 |
| `conclusion de la section sur la couverture exhaustive aux modules 512 et 1024` | L1192:Conclusion de la section sur la couverture exhaustive aux modules 512 et 1024 | L10765 |
| `conclusion de la section sur la couverture universelle` | L4088:Conclusion de la section sur la couverture universelle | L13661 |
| `conclusion de la section sur la transition m15 vers m16` | L4763:Conclusion de la section sur la transition m15 vers m16 | L14336 |
| `conclusion de la section sur le lemme de frere` | L4623:Conclusion de la section sur le lemme de frère | L14196 |
| `conclusion de la section sur les clauses grossieres et la continuation analytique` | L475:Conclusion de la section sur les clauses grossières et la continuation analytique | L10048 |
| `conclusion de la section sur les etats projectifs a l’horizon 7` | L5043:Conclusion de la section sur les états projectifs à l’horizon 7 | L14616 |
| `conclusion de la strategie hybride \(d/f\)` | L6841:Conclusion de la stratégie hybride \(D/F\) | L16414 |
| `conclusion de la table de transition au palier \(2^{17}\)` | L5919:Conclusion de la table de transition au palier \(2^{17}\) | L15492 |
| `conclusion de l’integration fusion pour \(d_{16}\) et \(d_{17}\)` | L6995:Conclusion de l’intégration fusion pour \(D_{16}\) et \(D_{17}\) | L16568 |
| `conclusion des clauses de fusion au palier \(2^{25}\)` | L6922:Conclusion des clauses de fusion au palier \(2^{25}\) | L16495 |
| `conclusion du lemme de scission des sœurs` | L5356:Conclusion du lemme de scission des sœurs | L14929 |
| `conclusion du paquet \(d_{11}\) au palier \(2^{19}\)` | L6075:Conclusion du paquet \(D_{11}\) au palier \(2^{19}\) | L15648 |
| `conclusion du paquet \(d_{12}\) au palier \(2^{21}\)` | L6201:Conclusion du paquet \(D_{12}\) au palier \(2^{21}\) | L15774 |
| `conclusion du paquet \(d_{13}\) au palier \(2^{22}\)` | L6269:Conclusion du paquet \(D_{13}\) au palier \(2^{22}\) | L15842 |
| `conclusion du paquet \(d_{14}\) au palier \(2^{24}\)` | L6358:Conclusion du paquet \(D_{14}\) au palier \(2^{24}\) | L15931 |
| `conclusion du paquet \(d_{15}\) au palier \(2^{25}\)` | L6438:Conclusion du paquet \(D_{15}\) au palier \(2^{25}\) | L16011 |
| `conclusion du paquet \(d_{16}\) au palier \(2^{27}\)` | L6541:Conclusion du paquet \(D_{16}\) au palier \(2^{27}\) | L16114 |
| `conclusion du paquet \(d_{17}\) au palier \(2^{28}\)` | L6644:Conclusion du paquet \(D_{17}\) au palier \(2^{28}\) | L16217 |
| `conclusion du paquet complet \(d_{10}\)` | L6011:Conclusion du paquet complet \(D_{10}\) | L15584 |
| `conclusion du paquet de scripts` | L7015:Conclusion du paquet de scripts | L16588 |
| `conclusion sur l'analyse de la dissymetrie des seuils` | L3823:Conclusion sur l'analyse de la dissymétrie des seuils | L13396 |
| `conclusion sur l'analyse des sous-branches dominantes` | L3072:Conclusion sur l'analyse des sous-branches dominantes | L12645 |
| `conclusion sur la classification congruentielle` | L3346:Conclusion sur la classification congruentielle | L12919 |
| `conclusion sur la fusion contractante` | L2714:Conclusion sur la fusion contractante | L12287 |
| `conclusion sur le seuil de survie et l'extinction` | L2546:Conclusion sur le seuil de survie et l'extinction | L12119 |
| `conclusion sur le theoreme cible et le certificat fini` | L3656:Conclusion sur le théorème cible et le certificat fini | L13229 |
| `conclusion sur les clauses de descente par minoration` | L2462:Conclusion sur les clauses de descente par minoration | L12035 |
| `condition (y\equiv 2\pmod 3) sans heuristique` | L2666:Condition (y\equiv 2\pmod 3) sans heuristique | L12239 |
| `conditions de validite et limites a expliciter dans une preuve finale` | L5334:Conditions de validité et limites à expliciter dans une preuve finale | L14907 |
| `consequence pour la suite de preuve` | L5999:Conséquence pour la suite de preuve | L15572 |
| `consolidation analytique au palier (8192) sur la branche (31\pmod{32})` | L1820:Consolidation analytique au palier (8192) sur la branche (31\pmod{32}) | L11393 |
| `contexte de reference et niveau de certitude` | L5368:Contexte de référence et niveau de certitude | L14941 |
| `continuer : strategie de fermeture systematique par “freres”` | L4262:Continuer : stratégie de fermeture systématique par “frères” | L13835 |
| `couverture exhaustive au module (2048) pour la branche (31 \pmod{32})` | L1550:Couverture exhaustive au module (2048) pour la branche (31 \pmod{32}) | L11123 |
| `decision methodologique` | L6662:Décision méthodologique | L16235 |
| `decomposition finie du noyau projectif : 60 etats` | L5546:Décomposition finie du noyau projectif : 60 états | L15119 |
| `dedoublement au palier (2^{14}) : (255) et (8447)` | L2108:Dédoublement au palier (2^{14}) : (255) et (8447) | L11681 |
| `definitions de base` | L5373:Définitions de base | L14946 |
| `deuxieme lemme : descente en 6 pas via la congruence (575\bmod 1024)` | L1368:Deuxième lemme : descente en 6 pas via la congruence (575\bmod 1024) | L10941 |
| `donnee utile immediate au palier 2^17 : impact des 175 clauses d10` | L5875:Donnée utile immédiate au palier 2^17 : impact des 175 clauses D10 | L15448 |
| `enonce formel du lemme de completion par freres au palier (2^{15})` | L4334:Énoncé formel du lemme de complétion par frères au palier (2^{15}) | L13907 |
| `enonce standard du lemme de scission des sœurs` | L5228:Énoncé standard du lemme de scission des sœurs | L14801 |
| `ensemble complet des fusions minimales (t=7, a=11) sur la branche (31 \pmod{32})` | L2801:Ensemble complet des fusions minimales (t=7, A=11) sur la branche (31 \pmod{32}) | L12374 |
| `ensemble complet des neuf fusions minimales (t=7,a=11) modulo (4096)` | L3546:Ensemble complet des neuf fusions minimales (t=7,A=11) modulo (4096) | L13119 |
| `espace d’etat etendu et statut du registre (k)` | L5624:Espace d’état étendu et statut du registre (K) | L15197 |
| `etape 1 : constat structurel sur le noyau « both » apres completion au palier (2^{16})` | L5113:Étape 1 : constat structurel sur le noyau « both » après complétion au palier (2^{16}) | L14686 |
| `etape 1 : decomposition exacte des parents au palier (2^{15})` | L4643:Étape 1 : décomposition exacte des parents au palier (2^{15}) | L14216 |
| `etape 2 : completion systematique des cas « one » au palier (2^{16})` | L4673:Étape 2 : complétion systématique des cas « one » au palier (2^{16}) | L14246 |
| `etape 2 : extraction du sous-ensemble stabilisable au palier (2^{17})` | L5134:Étape 2 : extraction du sous-ensemble stabilisable au palier (2^{17}) | L14707 |
| `etape 3 : amelioration quantitative du coefficient de survie` | L4695:Étape 3 : amélioration quantitative du coefficient de survie | L14268 |
| `etape 3 : audit exhaustif des 175 clauses candidates (d10)` | L5172:Étape 3 : audit exhaustif des 175 clauses candidates (D10) | L14745 |
| `etape 4 : ce que cela implique pour la preuve` | L5185:Étape 4 : ce que cela implique pour la preuve | L14758 |
| `etape 4 : structure du noyau « both » au palier (2^{15})` | L4715:Étape 4 : structure du noyau « both » au palier (2^{15}) | L14288 |
| `etape 6 : la valuation (a_5) est gouvernee par une forme lineaire en (t)` | L3153:Étape 6 : la valuation (a_5) est gouvernée par une forme linéaire en (t) | L12726 |
| `etape 7 : la valuation (a_6) est gouvernee par (v_2(2187t+2185))` | L3209:Étape 7 : la valuation (a_6) est gouvernée par (v_2(2187t+2185)) | L12782 |
| `etape a : un fait structurel a utiliser comme lemme` | L4777:Étape A : un fait structurel à utiliser comme lemme | L14350 |
| `etape analytique : la valuation (a_4) est gouvernee par (v_2(243n+211))` | L1251:Étape analytique : la valuation (a_4) est gouvernée par (v_2(243n+211)) | L10824 |
| `etape analytique suivante` | L462:Étape analytique suivante | L1589, L10035, L11162 |
| `etape b : quantification exacte des noyaux « both » deja observes` | L4797:Étape B : quantification exacte des noyaux « both » déjà observés | L14370 |
| `etape c : relevements et “epaisseur” du noyau` | L4843:Étape C : relèvements et “épaisseur” du noyau | L14416 |
| `etape d : ce que cette reduction change pour la preuve` | L4869:Étape D : ce que cette réduction change pour la preuve | L14442 |
| `etape e : la phase technique immediate` | L4881:Étape E : la phase technique immédiate | L14454 |
| `etape suivante de demonstration (formulation mathematique)` | L5026:Étape suivante de démonstration (formulation mathématique) | L14599 |
| `etape suivante immediate` | L4617:Étape suivante immédiate | L14190 |
| `etape suivante logique` | L6348:Étape suivante logique | L15921 |
| `etat formel au palier (2^{14}=16384)` | L4109:État formel au palier (2^{14}=16384) | L13682 |
| `etat quantifie du residu dur et raison de focalisation sur (31 \pmod{32})` | L2254:État quantifié du résidu dur et raison de focalisation sur (31 \pmod{32}) | L11827 |
| `fermeture immediate des 4 classes “hors branches”` | L4152:Fermeture immédiate des 4 classes “hors branches” | L13725 |
| `fin de preuve par certificat fini au palier (2^m)` | L3763:Fin de preuve par certificat fini au palier (2^M) | L13336 |
| `forcer (a_6\ge 5) par congruence lineaire sur (t)` | L3227:Forcer (a_6\ge 5) par congruence linéaire sur (t) | L12800 |
| `formalisation du lemme d’extinction par table de transition` | L5820:Formalisation du lemme d’extinction par table de transition | L15393 |
| `forme affine le long d’un mot de valuations` | L5397:Forme affine le long d’un mot de valuations | L14970 |
| `formulation standard d’une clause de fusion generalisee` | L6721:Formulation standard d’une clause de fusion généralisée | L16294 |
| `fusion contractante a longueur 6 : le cas minimal (a=9) sur (31\pmod{32})` | L2991:Fusion contractante à longueur 6 : le cas minimal (A=9) sur (31\pmod{32}) | L12564 |
| `fusion contractante a longueur 7 : seuil structurel et forme generale` | L2728:Fusion contractante à longueur 7 : seuil structurel et forme générale | L12301 |
| `fusion contractante et seuils non arbitraires` | L2560:Fusion contractante et seuils non arbitraires | L12133 |
| `generalisation non arbitraire : profondeur (l)` | L2508:Généralisation non arbitraire : profondeur (L) | L12081 |
| `impact analytique attendu sur le coefficient de survie` | L2428:Impact analytique attendu sur le coefficient de survie | L12001 |
| `impact par etat` | L6427:Impact par état | L6633, L16000, L16206 |
| `impact par etat (table de transition d’etats etendus)` | L6530:Impact par état (table de transition d’états étendus) | L16103 |
| `impact sur les 60 etats` | L6161:Impact sur les 60 états | L15734 |
| `indicateur pertinent vers une “masse critique” : coefficient de survie (q_m)` | L2163:Indicateur pertinent vers une “masse critique” : coefficient de survie (q_m) | L11736 |
| `integration au registre au palier 4096 sur la branche (31\pmod{32})` | L3580:Intégration au registre au palier 4096 sur la branche (31\pmod{32}) | L13153 |
| `integration de la fusion au palier (2^{25})` | L6934:Intégration de la fusion au palier (2^{25}) | L16507 |
| `introduction a l'analyse de la branche 31` | L1608:Introduction à l'analyse de la branche 31 | L11181 |
| `introduction a l'analyse de la dissymetrie des seuils` | L3668:Introduction à l'analyse de la dissymétrie des seuils | L13241 |
| `introduction a l'analyse des sous-branches dominantes` | L2722:Introduction à l'analyse des sous-branches dominantes | L12295 |
| `introduction a l'analyse structuree de la branche 31 modulo 32` | L1200:Introduction à l'analyse structurée de la branche 31 modulo 32 | L10773 |
| `introduction a la classification congruentielle` | L3096:Introduction à la classification congruentielle | L12669 |
| `introduction a la densification des lemmes et a la couverture exhaustive` | L481:Introduction à la densification des lemmes et à la couverture exhaustive | L10054 |
| `introduction a la justification du seuil de survie 0.5` | L2470:Introduction à la justification du seuil de survie 0.5 | L12043 |
| `introduction au theoreme cible et au certificat fini` | L3363:Introduction au théorème cible et au certificat fini | L12936 |
| `introduction aux clauses de descente par minoration` | L2248:Introduction aux clauses de descente par minoration | L11821 |
| `introduction aux criteres de fusion contractante` | L2554:Introduction aux critères de fusion contractante | L12127 |
| `introduction de l'analyse au pas 8 sur la base projective b12` | L5051:Introduction de l'analyse au pas 8 sur la base projective B12 | L14624 |
| `introduction de l'analyse du palier 16384` | L1814:Introduction de l'analyse du palier 16384 | L2012, L11387, L11585 |
| `introduction de l'audit de reduction au palier \(2^{17}\)` | L5925:Introduction de l'audit de réduction au palier \(2^{17}\) | L15498 |
| `introduction de l'espace d'etat etendu` | L5614:Introduction de l'espace d'état étendu | L15187 |
| `introduction de l'horizon 10 au palier \(2^{17}\)` | L5095:Introduction de l'horizon 10 au palier \(2^{17}\) | L14668 |
| `introduction de la formalisation structuree` | L5362:Introduction de la formalisation structurée | L14935 |
| `introduction de la section sur la base projective du noyau both` | L4769:Introduction de la section sur la base projective du noyau both | L14342 |
| `introduction de la section sur la completion au palier 16384` | L4100:Introduction de la section sur la complétion au palier 16384 | L13673 |
| `introduction de la section sur la completion au palier 32768` | L4324:Introduction de la section sur la complétion au palier 32768 | L13897 |
| `introduction de la section sur la couverture universelle` | L3836:Introduction de la section sur la couverture universelle | L13409 |
| `introduction de la section sur la transition m15 vers m16` | L4633:Introduction de la section sur la transition m15 vers m16 | L14206 |
| `introduction de la section sur le lemme de frere` | L4451:Introduction de la section sur le lemme de frère | L14024 |
| `introduction de la section sur les etats projectifs a l’horizon 7` | L4915:Introduction de la section sur les états projectifs à l’horizon 7 | L14488 |
| `introduction de la strategie hybride \(d/f\) apres \(d_{17}\)` | L6656:Introduction de la stratégie hybride \(D/F\) après \(D_{17}\) | L16229 |
| `introduction de la table de transition au palier \(2^{17}\)` | L5809:Introduction de la table de transition au palier \(2^{17}\) | L15382 |
| `introduction de l’integration fusion pour \(d_{16}\) et \(d_{17}\)` | L6928:Introduction de l’intégration fusion pour \(D_{16}\) et \(D_{17}\) | L16501 |
| `introduction des clauses de fusion au palier \(2^{25}\)` | L6849:Introduction des clauses de fusion au palier \(2^{25}\) | L16422 |
| `introduction du lemme de scission des sœurs` | L5206:Introduction du lemme de scission des sœurs | L14779 |
| `introduction du paquet \(d_{11}\) au palier \(2^{19}\)` | L6015:Introduction du paquet \(D_{11}\) au palier \(2^{19}\) | L15588 |
| `introduction du paquet \(d_{12}\) au palier \(2^{21}\)` | L6086:Introduction du paquet \(D_{12}\) au palier \(2^{21}\) | L15659 |
| `introduction du paquet \(d_{13}\) au palier \(2^{22}\)` | L6209:Introduction du paquet \(D_{13}\) au palier \(2^{22}\) | L15782 |
| `introduction du paquet \(d_{14}\) au palier \(2^{24}\)` | L6277:Introduction du paquet \(D_{14}\) au palier \(2^{24}\) | L15850 |
| `introduction du paquet \(d_{15}\) au palier \(2^{25}\)` | L6364:Introduction du paquet \(D_{15}\) au palier \(2^{25}\) | L15937 |
| `introduction du paquet \(d_{16}\) au palier \(2^{27}\)` | L6455:Introduction du paquet \(D_{16}\) au palier \(2^{27}\) | L16028 |
| `introduction du paquet \(d_{17}\) au palier \(2^{28}\)` | L6554:Introduction du paquet \(D_{17}\) au palier \(2^{28}\) | L16127 |
| `introduction du paquet complet \(d_{10}\) au palier \(2^{17}\)` | L5969:Introduction du paquet complet \(D_{10}\) au palier \(2^{17}\) | L15542 |
| `introduction du paquet de scripts` | L6999:Introduction du paquet de scripts | L16572 |
| `justification arithmetique de l’echec de f6/f7 sur ce noyau` | L6875:Justification arithmétique de l’échec de F6/F7 sur ce noyau | L16448 |
| `le cœur restant : extinction du noyau « both » a un palier fini` | L5747:Le cœur restant : extinction du noyau « both » à un palier fini | L15320 |
| `le role central des fusions (f) dans la couverture` | L3747:Le rôle central des fusions (F) dans la couverture | L13320 |
| `lecture analytique commune des quatre propositions` | L451:Lecture analytique commune des quatre propositions | L10024 |
| `lecture analytique de l’etape atteinte` | L1180:Lecture analytique de l’étape atteinte | L10753 |
| `lemme 1 : forme affine de (u^{(k)}) le long d’un mot de valuations` | L3857:Lemme 1 : forme affine de (U^{(k)}) le long d’un mot de valuations | L13430 |
| `lemme 2 : clause de descente (d) et seuil explicite` | L3887:Lemme 2 : clause de descente (D) et seuil explicite | L13460 |
| `lemme 3 : clause de fusion contractante (f1) a preimage courte (a=1)` | L3912:Lemme 3 : clause de fusion contractante (F1) à préimage courte (a=1) | L13485 |
| `lemme de frere pour les clauses exactes` | L4462:Lemme de frère pour les clauses exactes | L14035 |
| `lemme de reduction a une couverture finie` | L4140:Lemme de réduction à une couverture finie | L13713 |
| `lemme de scission des sœurs` | L5507:Lemme de scission des sœurs | L15080 |
| `lemme de scission des sœurs et completion automatique` | L5709:Lemme de scission des sœurs et complétion automatique | L15282 |
| `lemme final a etablir pour conclure` | L4597:Lemme final à établir pour conclure | L14170 |
| `lien exact avec les clauses (d) et les clauses minorees` | L5269:Lien exact avec les clauses (D) et les clauses minorées | L14842 |
| `limites a expliciter dans la preuve finale` | L6835:Limites à expliciter dans la preuve finale | L16408 |
| `normalisation du certificat et “format publiable”` | L5770:Normalisation du certificat et “format publiable” | L15343 |
| `nouvelle clause analytique significative : (n\equiv 1759 \pmod{2048}\rightarrow u^{(6)}(n)<n)` | L1865:Nouvelle clause analytique significative : (n\equiv 1759 \pmod{2048}\Rightarrow U^{(6)}(n)<n) | L11438 |
| `ou en est exactement la preuve globale apres ces deux blocs` | L4056:Où en est exactement la preuve globale après ces deux blocs | L13629 |
| `palier (2^{21}) : seuil contractif a l’horizon 12` | L6099:Palier (2^{21}) : seuil contractif à l’horizon 12 | L15672 |
| `palier (2^{22}) : seuil contractif a l’horizon 13` | L6217:Palier (2^{22}) : seuil contractif à l’horizon 13 | L15790 |
| `palier (2^{24}) : seuil contractif a l’horizon 14` | L6286:Palier (2^{24}) : seuil contractif à l’horizon 14 | L15859 |
| `palier (2^{25}) : seuil contractif a l’horizon 15` | L6378:Palier (2^{25}) : seuil contractif à l’horizon 15 | L15951 |
| `palier (2^{27}) : seuil contractif a l’horizon 16` | L6470:Palier (2^{27}) : seuil contractif à l’horizon 16 | L16043 |
| `palier (2^{28}) : seuil contractif a l’horizon 17` | L6569:Palier (2^{28}) : seuil contractif à l’horizon 17 | L16142 |
| `palier 8192 : apparition des descentes (t=7,a=12) stables` | L3613:Palier 8192 : apparition des descentes (t=7,A=12) stables | L13186 |
| `paquet (d_{11}) : extraction finie des classes (a_{11}=18) et fermeture par scission` | L6043:Paquet (D_{11}) : extraction finie des classes (A_{11}=18) et fermeture par scission | L15616 |
| `paquet (d_{12}) minimal : taille et fermeture par scission` | L6148:Paquet (D_{12}) minimal : taille et fermeture par scission | L15721 |
| `paquet (d_{13}) minimal : taille et fermeture des sœurs` | L6236:Paquet (D_{13}) minimal : taille et fermeture des sœurs | L15809 |
| `paquet (d_{16}) apres fusion (palier (2^{27}))` | L6947:Paquet (D_{16}) après fusion (palier (2^{27})) | L16520 |
| `paquet (d_{17}) apres fusion et apres (d_{16}) (palier (2^{28}))` | L6967:Paquet (D_{17}) après fusion et après (D_{16}) (palier (2^{28})) | L16540 |
| `passage analytique au palier (16384) : nouvelles clauses contractives a horizon (k=8)` | L1925:Passage analytique au palier (16384) : nouvelles clauses contractives à horizon (k=8) | L11498 |

(table tronquée : 254 lignes)