algo/v0/démonstration collatz.md
Nicolas Cantu 1455d5dc1c Appliquer la rédaction scientifique et intégrer les mises à jour des manuscrits
**Motivations:**
- Enregistrer l’état courant des manuscrits de démonstration.
- Appliquer le guide de rédaction scientifique sur les sections modifiées de `v0/conjoncture_collatz.md`.

**Root causes:**
- Les ajouts récents de `v0/conjoncture_collatz.md` contenaient des formulations éditoriales et des titres non conformes au guide.
- Les références bibliographiques modifiées nécessitaient une stabilisation dans la version courante.

**Correctifs:**
- Neutralisation des formulations non scientifiques dans la zone ajoutée de `v0/conjoncture_collatz.md`.
- Normalisation des titres d’introduction et de conclusion dans les sections concernées.
- Conservation des éléments démonstratifs (lemmes, seuils, hypothèses, objectifs de fermeture) sans suppression d’informations utiles.

**Evolutions:**
- Intégration de la formalisation structurée sur le noyau projectif, les clauses D/F et le lemme de scission des sœurs.
- Mise à jour du manuscrit `v0/démonstration collatz.md` pour cohérence avec le fil de preuve courant.

**Pages affectées:**
- v0/conjoncture_collatz.md
- v0/démonstration collatz.md
2026-02-25 23:25:24 +01:00

252 lines
10 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

## Introduction
La formalisation peut être reprise proprement en séparant ce qui relève déjà dun 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][1])
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). Cest un point de consensus dans les exposés de référence (Lagarias, Tao). ([arXiv][2])
La démarche présente est dun 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 dun 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 lon 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 lingré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), lautre 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 daudit :
* 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 dune 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 dun 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), laudit a produit :
* 60 états distincts à lhorizon 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à lhorizon 7). La preuve globale devient « état par état ».
## Premier traitement des états : analyse au pas 8
Sur (B_{12}), lanalyse 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 dentré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 natteignent 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 à lhorizon 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 lautre sœur par la scission (D⋆), au même horizon.
## Ce quil 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 quil 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à dun 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 quil 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 lextinction en profondeur finie.
Dans les deux cas, le point technique décisif est lextinction du noyau « both », donc létude des relèvements des 60 états, puis des 29 états restants après pas 8, puis limpact 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 dabstraction (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é à lhorizon 8 et attaqué à lhorizon 10 par des clauses stabilisées à (2^{17}).
La suite de la formalisation consiste à écrire, état par état, lénoncé « extinction » manquant, et à prouver quavec les familles déjà construites (D8, F6/F7, D10) et la complétion automatique par scission, aucun relèvement des 29 états non contractifs à lhorizon 8 ne peut persister indéfiniment. Ce lemme est la charnière unique entre “programme de preuve audité” et “preuve complète”.
[1]: https://en.wikipedia.org/wiki/Collatz_conjecture"Collatz conjecture"
[2]: https://arxiv.org/abs/1909.03562"Almost all orbits of the Collatz map attain almost bounded values"