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)