algo/v0/démonstration collatz.md

Introduction

La formalisation peut être reprise proprement en séparant ce qui relève déjà d’un cadre mathématique standard (définitions, lemmes de correction des clauses, descente bien fondée) de ce qui reste à établir pour obtenir une preuve complète (un lemme de couverture totale à un palier fini, ou un lemme de contraction uniforme du noyau « both »). Cette séparation est indispensable, car la conjecture de Collatz est toujours considérée comme ouverte dans la littérature de synthèse récente, malgré de nombreuses revendications de preuve. (Wikipédia)

Ce qui suit reprend la démonstration comme un texte formel, en précisant les objets, les énoncés, les hypothèses exactes et les points encore à verrouiller.

Contexte de référence et niveau de certitude

La communauté dispose de résultats très solides de type « presque tous » (densité naturelle/logarithmique), mais qui ne concluent pas l’énoncé universel (\forall n). C’est un point de consensus dans les exposés de référence (Lagarias, Tao). (arXiv) La démarche présente est d’un autre type : elle vise une preuve universelle via un certificat fini (registre (K)) et des lemmes de couverture congruentielle.

Définitions de base

Soit (C:\mathbb{N}{\ge 1}\to\mathbb{N}{\ge 1}) la fonction de Collatz : [ C(n)= \begin{cases} 3n+1 & \text{si }n\text{ est impair},
n/2 & \text{si }n\text{ est pair}. \end{cases} ]

On utilise la dynamique accélérée « impairs (\to) impairs » : [ a(n)=v_2(3n+1)\ge 1,\qquad U(n)=\frac{3n+1}{2^{a(n)}}\in 2\mathbb{N}+1. ] La conjecture de Collatz est équivalente à : [ \forall n\in\mathbb{N}_{\ge 1},\ \exists k,\ C^{(k)}(n)=1, ] et, sur les impairs, à : [ \forall n\in 2\mathbb{N}+1,\ \exists k,\ U^{(k)}(n)=1. ]

Forme affine le long d’un mot de valuations

Soit (n_0=n) impair et (n_{i+1}=U(n_i)). Poser (a_i=v_2(3n_i+1)) et [ A_0=0,\quad A_{i+1}=A_i+a_i,\quad A=A_k=\sum_{i=0}^{k-1} a_i. ]

Définir (C_k) par récurrence : [ C_0=0,\qquad C_{i+1}=3C_i+2^{A_i}. ]

Lemme (forme affine exacte) Pour tout (k\ge 0), [ U^{(k)}(n)=\frac{3^k n + C_k}{2^{A}}. ]

Preuve Induction standard : la récurrence sur (C_{i+1}) est exactement celle obtenue en développant (3n_i+1) puis en divisant par (2^{a_i}).

Ce lemme est la base unique de toutes les clauses (D) et (F).

Clauses de descente (D) : condition structurelle et seuil

À partir de la forme affine : [ U^{(k)}(n)<n \iff \frac{3^k n + C_k}{2^A}<n \iff C_k < (2^A-3^k)n. ]

Paramètres

• (\Delta_D = 2^A-3^k)

Si (\Delta_D>0), un seuil suffisant est : [ N_0=\left\lfloor\frac{C_k}{\Delta_D}\right\rfloor+1, ] et l’on a : [ \forall n\ge N_0,\ U^{(k)}(n)<n. ]

Calculs structurants déjà utilisés Longueur (k=8) :

• (3^8=6561)
• (2^{13}=8192)
• (\Delta_D=2^{13}-3^8=8192-6561=1631)

Donc un bloc exact de longueur 8 avec (A_8\ge 13) est contractif.

Longueur (k=10) :

• (3^{10}=59049)
• (2^{16}=65536)
• (\Delta_D=2^{16}-3^{10}=65536-59049=6487)

Donc un bloc exact longueur 10 avec (A_{10}\ge 16) est contractif.

Clauses de descente minorées (D⋆) : fermeture sans exactitude de valuation

Si une condition congruentielle assure seulement une minoration (A(n)\ge \underline A), on a : [ U^{(k)}(n)=\frac{3^k n + C_k}{2^{A(n)}} \le \frac{3^k n + C_k}{2^{\underline A}}. ] Donc une condition suffisante est : [ \frac{3^k n + C_k}{2^{\underline A}}<n \iff C_k < (2^{\underline A}-3^k)n. ] Avec (\underline\Delta_D=2^{\underline A}-3^k>0), [ N_0=\left\lfloor\frac{C_k}{\underline\Delta_D}\right\rfloor+1. ]

Cette clause est le mécanisme formel qui permet de fermer tôt les relèvements « plus profonds » (valuation plus grande) sans attendre la stabilité exacte (2^{A+1}).

Clauses de fusion (F1) : réduction inductive stricte

Soit (y=U^{(t)}(n)). Si (y\equiv 2\pmod 3), alors [ m=\frac{2y-1}{3}\in\mathbb{N} \quad\text{et}\quad U(m)=y, ] car (3m+1=2y) et (v_2(2y)=1) puisque (y) est impair.

La condition clé est (m<n). En écrivant [ y=\frac{3^t n + C_t}{2^A}, ] on obtient : [ m<n \iff (3\cdot 2^A-2\cdot 3^t),n > 2C_t-2^A. ]

Paramètres

• (\Delta_F=3\cdot 2^A-2\cdot 3^t)

Cette condition est plus permissive que la descente directe pour (t=6) et (t=7) (seuils déjà exploités dans la construction).

Lemme de scission des sœurs

Ce lemme est l’ingrédient qui rend la « complétion par frères » mathématiquement automatique.

Lemme (scission) Soient (m\ge 0), (\alpha) impair, (\beta\in\mathbb{Z}). Poser (N(n)=\alpha n+\beta). Si (v_2(N(n))=m), alors [ v_2(N(n+2^m))\ge m+1. ]

Preuve Écrire (N(n)=2^m u) avec (u) impair. Alors [ N(n+2^m)=N(n)+\alpha 2^m = 2^m(u+\alpha), ] et (u+\alpha) est pair (impair + impair), donc (v_2(u+\alpha)\ge 1).

Corollaire (complétion « one ») Si une clause exacte stabilisée au bit nouveau ferme une sœur via (v_2(N)=m), l’autre sœur vérifie automatiquement (v_2(N)\ge m+1), donc une clause (D⋆) au même horizon est disponible dès que (2^{m+1}>3^k).

Cette propriété a été exploitée et auditée sur les transitions (m=14\to 15) et (m=15\to 16). Documents d’audit :

• complétion (m=14\to 15) : sandbox:/mnt/data/complétion_minorée_m14_vers_m15.md
• complétion (m=15\to 16) : sandbox:/mnt/data/complétion_minorée_m15_vers_m16.md

Réduction du problème au noyau « both »

Après complétion à chaque palier, le résidu restant au niveau suivant est exactement la double descendance des parents « both ». Cette réduction est formelle : elle ne dépend pas d’une observation numérique, seulement de la définition des cas « one/both » et du lemme de scission.

À partir des paliers déjà audités, un fait structurel supplémentaire a été établi :

Proposition (base projective) Le noyau « both » admet une base projective stable modulo (4096) à partir de (m=12). Autrement dit, tous les noyaux « both » aux paliers supérieurs sont des relèvements d’un ensemble fini (B_{12}) de 192 résidus modulo 4096. Audit : sandbox:/mnt/data/noyau_both_base_4096.md

Cela transforme la fin de preuve en un objectif fini : fermer tous les relèvements de (B_{12}) à un palier fini.

Décomposition finie du noyau projectif : 60 états

Sur (B_{12}) (192 résidus modulo 4096), l’audit a produit :

• 60 états distincts à l’horizon 7, définis par les mots de valuations ((a_0,\dots,a_6)),
• la distribution exacte de (A_7) sur (B_{12}),
• pour chaque état : (C_7), (D_8=3C_7+2^{A_7}) et les listes exhaustives des résidus de l’état.

Audit :

• Markdown : sandbox:/mnt/data/audit_60_etats_B12_mod4096_horizon7.md
• JSON : sandbox:/mnt/data/audit_60_etats_B12_mod4096_horizon7.json

Point méthodologique Cette réduction en 60 états transforme le noyau « both » en un automate fini (au moins jusqu’à l’horizon 7). La preuve globale devient « état par état ».

Premier traitement des états : analyse au pas 8

Sur (B_{12}), l’analyse au pas 8 a isolé 31 résidus atteignant (A_8\ge 13), répartis sur 31 états distincts. Ces 31 cas sont des points d’entrée immédiats pour des clauses (D) de longueur 8, puis complétion par scission sur les sœurs.

Audit :

• sandbox:/mnt/data/analyse_pas8_B12.md

Cela laisse 29 états qui n’atteignent jamais (A_8\ge 13) sur (B_{12}). Ces états doivent être traités par horizon 9 ou 10 (nouvelle forme linéaire du numérateur) et/ou par fusions.

Attaque du noyau à l’horizon 10 : candidats D10 stabilisés à (2^{17})

Sur le noyau persistant au palier (2^{16}) après complétion, un sous-ensemble atteint (A_{10}=16). Comme :

• (3^{10}=59049)
• (2^{16}=65536)
• (\Delta_D=6487)

un bloc exact longueur 10 avec (A_{10}=16) est contractif, et sa stabilité requiert (2^{17}). Un audit complet a extrait 175 classes candidates (modulo (2^{17})) avec seuil maximal (N_0=23).

Audit :

• sandbox:/mnt/data/candidats_D10_palier2p17.md

Rôle dans la preuve Ces 175 clauses sont conçues pour convertir une partie du noyau « both » en « one » au palier (2^{17}), puis à éliminer l’autre sœur par la scission (D⋆), au même horizon.

Ce qu’il reste à verrouiller pour une preuve complète

À ce stade, tout ce qui précède constitue un socle formel correct, mais la preuve complète exige encore un lemme global de fermeture. Il peut prendre deux formes, toutes deux standard.

Version certificat fini Montrer qu’il existe un palier (M) et un registre fini (K) (clauses D, D⋆, F1 et complétions par scission) tel que : [ \text{toutes les classes impaires modulo }2^M\text{ sont couvertes au-delà d’un seuil }N^. ] La conclusion « Collatz » suit alors par descente bien fondée et vérification finie sous (N^).

Version contraction uniforme du noyau both Montrer qu’il existe une profondeur bornée (L) et une constante (\theta>0) telles que, pour tout parent « both », parmi ses (2^L) descendants, au moins (\theta 2^L) tombent dans la toile (D ou F), ce qui force l’extinction en profondeur finie.

Dans les deux cas, le point technique décisif est l’extinction du noyau « both », donc l’étude des relèvements des 60 états, puis des 29 états restants après pas 8, puis l’impact cumulatif des nouvelles clauses D10 au palier (2^{17}).

Conclusion

La formalisation est maintenant structurée comme une preuve : définitions, lemmes de correction (forme affine, descente, fusion), lemmes d’abstraction (descente minorée), et un lemme fondamental 2-adique (scission des sœurs) qui rend la complétion « one » automatique. À partir de là, tout se réduit à un problème fini sur un noyau projectif (B_{12}) (192 classes modulo 4096), décomposé en 60 états, puis filtré à l’horizon 8 et attaqué à l’horizon 10 par des clauses stabilisées à (2^{17}).

La suite de la formalisation consiste à écrire, état par état, l’énoncé « extinction » manquant, et à prouver qu’avec les familles déjà construites (D8, F6/F7, D10) et la complétion automatique par scission, aucun relèvement des 29 états non contractifs à l’horizon 8 ne peut persister indéfiniment. Ce lemme est la charnière unique entre “programme de preuve audité” et “preuve complète”.