Appliquer la rédaction scientifique sur le manuscrit Collatz
**Motivations:** - Aligner la rédaction de `v0/conjoncture_collatz.md` avec la règle `IA_agents/redaction scientifique.md` - Supprimer les formulations méta qui ne relèvent pas du contenu mathématique de la preuve **Root causes:** - Présence de formulations déictiques (`ci-dessous`) et de transitions conversationnelles - Présence de formulations orientées processus plutôt que démonstration **Correctifs:** - Remplacer les formulations déictiques et méta par des formulations neutres et factuelles - Reformuler les transitions pour enchaîner par le contenu mathématique **Evolutions:** - Aucune **Pages affectées:** - v0/conjoncture_collatz.md
This commit is contained in:
parent
77d79645de
commit
8ff41e856d
@ -2315,7 +2315,7 @@ Un certificat fini, explicite, auditable, qui matérialise la contrainte stabili
|
||||
|
||||
Une procédure de vérification exacte (arithmétique rationnelle, congruences, bornes explicites), éventuellement formalisée, de manière à rendre l’argument indépendant de l’heuristique.
|
||||
|
||||
Si la discussion doit continuer dans le registre « go », l’étape suivante consiste à choisir l’une des deux familles de certificats ci-dessus et à écrire, noir sur blanc, le format exact du certificat publié (champs, contraintes, preuves locales), puis à dériver l’ensemble des obligations de preuve qui restent à fermer.
|
||||
Dans le registre « go », l’étape suivante consiste à choisir l’une des deux familles de certificats ci-dessus et à écrire le format exact du certificat publié (champs, contraintes, preuves locales), puis à dériver l’ensemble des obligations de preuve qui restent à fermer.
|
||||
|
||||
[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"
|
||||
@ -2495,7 +2495,7 @@ Cette approche clôt le débat en fournissant le **"Pourquoi"**. Elle transforme
|
||||
|
||||
Dans cette approche, « go » signifie passer du cadre conceptuel (futurs accessibles, contraintes, stabilisation) à un objet de preuve publiable au sens classique : un certificat fini (K) et un théorème-cadre du type « si (K) satisfait telles propriétés vérifiables, alors la conjecture de Collatz est vraie ». La suite explicite ce qui est nécessaire et suffisant pour que l’argument devienne une démonstration standard, en choisissant une voie principale (certificats par mots de parité et descente) et en indiquant précisément les obligations de preuve, les calculs à fournir, et les points où la difficulté connue se concentre.
|
||||
|
||||
Les références externes ci-dessous confirment que la conjecture est traitée comme ouverte dans les synthèses récentes et que les reformulations 2-adiques, « parity vectors » et techniques de sufficiency/recursive sufficiency constituent des cadres existants, utiles mais non conclusifs à ce jour. ([arXiv][1])
|
||||
Les références externes suivantes confirment que la conjecture est traitée comme ouverte dans les synthèses récentes et que les reformulations 2-adiques, « parity vectors » et techniques de sufficiency/recursive sufficiency constituent des cadres existants, utiles mais non conclusifs à ce jour. ([arXiv][1])
|
||||
|
||||
## Objet mathématique à publier
|
||||
|
||||
@ -3429,7 +3429,7 @@ Ces classes ne sont pas “intraitables” ; elles demandent un raffinement supp
|
||||
|
||||
## Algorithme de génération de (K) (spécification complète)
|
||||
|
||||
L’algorithme ci-dessous est la traduction directe “contraintes → stabilisation”.
|
||||
L’algorithme suivant est la traduction directe “contraintes → stabilisation”.
|
||||
|
||||
Initialisation
|
||||
|
||||
@ -4448,7 +4448,7 @@ La v2.3 va dans la bonne direction : elle produit une clause D réellement audit
|
||||
|
||||
## Introduction à la reprise de la démonstration et au format des clauses
|
||||
|
||||
La démonstration à reprendre peut être structurée comme une preuve conditionnelle standard : si un registre fini (K) de clauses arithmétiques universelles (descente, valuation, fusion) couvre tous les entiers impairs au-delà d’un seuil global, alors la conjecture de Collatz suit par descente bien fondée. Le travail déjà produit (v2.3) est précisément un générateur de clauses de descente universelles (D) à partir d’une trajectoire de la dynamique (U) (impairs (\to) impairs). La reprise ci-dessous formalise les lemmes nécessaires, puis réécrit la clause obtenue pour (n_0=27) dans un format mathématiquement correct et minimal (module réduit), avant de situer exactement ce qu’il reste à démontrer pour conclure.
|
||||
La démonstration à reprendre peut être structurée comme une preuve conditionnelle standard : si un registre fini (K) de clauses arithmétiques universelles (descente, valuation, fusion) couvre tous les entiers impairs au-delà d’un seuil global, alors la conjecture de Collatz suit par descente bien fondée. Le travail déjà produit (v2.3) est précisément un générateur de clauses de descente universelles (D) à partir d’une trajectoire de la dynamique (U) (impairs (\to) impairs). La reprise de cette section formalise les lemmes nécessaires, puis réécrit la clause obtenue pour (n_0=27) dans un format mathématiquement correct et minimal (module réduit), avant de situer exactement ce qu’il reste à démontrer pour conclure.
|
||||
|
||||
## Cadre et définitions
|
||||
|
||||
@ -4820,7 +4820,7 @@ Ce niveau modulo (64) sert surtout à organiser l’arbre. La fermeture effectiv
|
||||
|
||||
L’objectif immédiat est de produire des clauses (D) à petit horizon (k\le 5) et module (2^m) avec (m\le 11) (donc (\le 2048)), car ce sont les clauses qui augmentent réellement la couverture sans explosion.
|
||||
|
||||
Les quatre démonstrations ci-dessous ferment chacune une sous-branche “dure” par une clause universelle entièrement calculée.
|
||||
Les quatre démonstrations suivantes ferment chacune une sous-branche “dure” par une clause universelle entièrement calculée.
|
||||
|
||||
### Classe (n\equiv 7\pmod{256}) fermée en (k=4)
|
||||
|
||||
@ -5042,7 +5042,7 @@ Cette clause ferme une sous-branche de (15\pmod{32}) (car (175\equiv 15\pmod{32}
|
||||
|
||||
## Affinement exhaustif modulo (512) des huit branches modulo (64)
|
||||
|
||||
Pour continuer la démonstration de manière structurée, le registre (K) peut être organisé en huit “branches modulo (64)”, chacune se décomposant exhaustivement en huit résidus modulo (512). La liste ci-dessous donne, pour chaque résidu modulo (512), le premier horizon de descente trouvé sur le représentant, avec les paramètres ((k,A_k,m=A_k+1,N_0)). Cette liste constitue un état de travail directement exploitable par l’algorithme de stabilisation de (K).
|
||||
Pour continuer la démonstration de manière structurée, le registre (K) peut être organisé en huit “branches modulo (64)”, chacune se décomposant exhaustivement en huit résidus modulo (512). La liste suivante donne, pour chaque résidu modulo (512), le premier horizon de descente trouvé sur le représentant, avec les paramètres ((k,A_k,m=A_k+1,N_0)). Cette liste constitue un état de travail directement exploitable par l’algorithme de stabilisation de (K).
|
||||
|
||||
Branche (7\pmod{64}) : (7,71,135,199,263,327,391,455\pmod{512})
|
||||
|
||||
@ -5144,7 +5144,7 @@ Cette section formalise un schéma de preuve algorithmique par partitionnement d
|
||||
|
||||
## Introduction à l'affinement (2)-adique et au résidu au niveau 2^10
|
||||
|
||||
La suite de la démonstration consiste à passer d’un registre (K) composé de clauses grossières (modules faibles, horizons courts) à un registre plus fin obtenu par affinement (2)-adique contrôlé, tout en gardant la propriété essentielle : chaque clause est une implication universelle arithmétique, auditée par ((k,A_k,C_k,\Delta_k,N_0)), et ne repose ni sur une mesure ni sur une hypothèse ergodique. La démonstration ci-dessous reprend exactement ce fil : état au niveau (2^9), liste exhaustive du résidu restant, puis affinement au niveau (2^{10}) avec ajout de nouvelles clauses certifiées et liste exhaustive du nouveau résidu.
|
||||
La suite de la démonstration consiste à passer d’un registre (K) composé de clauses grossières (modules faibles, horizons courts) à un registre plus fin obtenu par affinement (2)-adique contrôlé, tout en gardant la propriété essentielle : chaque clause est une implication universelle arithmétique, auditée par ((k,A_k,C_k,\Delta_k,N_0)), et ne repose ni sur une mesure ni sur une hypothèse ergodique. La démonstration de cette section reprend exactement ce fil : état au niveau (2^9), liste exhaustive du résidu restant, puis affinement au niveau (2^{10}) avec ajout de nouvelles clauses certifiées et liste exhaustive du nouveau résidu.
|
||||
|
||||
## État du registre au niveau 512
|
||||
|
||||
@ -5195,7 +5195,7 @@ Ces quatre clauses ferment exactement (192) résidus impairs sur (256) modulo (5
|
||||
|
||||
### Clauses de descente certifiées supplémentaires à module ≤ 512
|
||||
|
||||
Les clauses ci-dessous sont de type « certifié (D) » : elles s’appuient sur la forme affine exacte
|
||||
Les clauses suivantes sont de type « certifié (D) » : elles s’appuient sur la forme affine exacte
|
||||
[
|
||||
U^{(k)}(n)=\frac{3^k n + C_k}{2^{A_k}}
|
||||
]
|
||||
@ -5397,7 +5397,7 @@ La suite de la démonstration suit exactement la même logique : affiner les ré
|
||||
|
||||
La démonstration peut maintenant être poursuivie à un niveau où l’affinement (2)-adique devient un objet de preuve à part entière : fixer une résolution (2^m), puis fermer (par clauses universelles) toutes les classes impaires modulo (2^m) qui admettent un bloc contractif dont la somme de valuations (A_k) reste (\le m-1). Ce palier permet de transformer l’intuition « beaucoup de classes descendent vite » en une assertion certifiée et localisée, et isole explicitement les classes qui exigent soit une résolution plus fine ((m) plus grand), soit un mécanisme supplémentaire de compression (fusion, contraintes mixtes).
|
||||
|
||||
La suite ci-dessous fixe d’abord le palier (m=11) (modulo (2^{11}=2048)), établit des clauses (D) typiques (avec calculs complets), puis donne la liste exhaustive du résidu non fermé à ce palier. Ensuite, le palier (m=12) (modulo (4096)) est engagé sur les premiers cas où (A_k=11), ce qui produit immédiatement un nouvel ensemble de clauses certifiées.
|
||||
La suite suivante fixe d’abord le palier (m=11) (modulo (2^{11}=2048)), établit des clauses (D) typiques (avec calculs complets), puis donne la liste exhaustive du résidu non fermé à ce palier. Ensuite, le palier (m=12) (modulo (4096)) est engagé sur les premiers cas où (A_k=11), ce qui produit immédiatement un nouvel ensemble de clauses certifiées.
|
||||
|
||||
## Palier (2^{11}=2048)
|
||||
|
||||
@ -5945,7 +5945,7 @@ Les clauses de fusion (F) exploitent la non-injectivité de $U$ pour relier des
|
||||
|
||||
La démonstration peut maintenant être prolongée sur un point qui manquait aux étapes précédentes : la construction de clauses universelles de fusion (F) réellement arithmétiques, c’est-à-dire formulées comme des égalités d’itérés impliquant une réduction stricte (m<n). C’est le bon niveau “formel et standard”, car il s’agit d’ajouter au registre (K) des règles transmissibles (collisions de futurs) qui compressent les branches où les clauses (D) deviennent trop fines.
|
||||
|
||||
La suite ci-dessous fixe d’abord un lemme de fusion minimal (préimage courte (a=1)), puis un schéma général “préfixe de valuations fixé (\Rightarrow) fusion universelle”, puis donne quatre clauses (F) explicites, entièrement démontrées (calculs complets). Enfin, l’état du registre au palier (2^{11}=2048) est mis à jour : la liste exhaustive des résidus encore non couverts par les règles (D) et (F) retenues est donnée.
|
||||
La suite suivante fixe d’abord un lemme de fusion minimal (préimage courte (a=1)), puis un schéma général “préfixe de valuations fixé (\Rightarrow) fusion universelle”, puis donne quatre clauses (F) explicites, entièrement démontrées (calculs complets). Enfin, l’état du registre au palier (2^{11}=2048) est mis à jour : la liste exhaustive des résidus encore non couverts par les règles (D) et (F) retenues est donnée.
|
||||
|
||||
## Lemme de fusion élémentaire par préimage (a=1)
|
||||
|
||||
@ -6948,7 +6948,7 @@ La trajectoire est bien orientée vers le passage “arithmétique (\to) analyse
|
||||
|
||||
La prochaine étape, pour aller réellement “dans ce sens” et non rester dans l’expérimental, est de choisir et de démontrer un lemme analytique de contraction uniforme de (R_m) (ou une fonction de Lyapunov déterministe équivalente). Le lemme (U(n)\equiv (-1)^{a(n)}\pmod 3) est une brique centrale pour y parvenir, car il relie de manière déterministe valuations et admissibilité des fusions, ce qui correspond au type de pont arithmétique requis pour une preuve publiable.
|
||||
|
||||
Si la continuation est engagée immédiatement, la suite naturelle est d’énoncer formellement une “propriété locale de fermeture d’un enfant sur deux” (ou d’une fraction fixe) dans chacune des quatre branches (\equiv 7,15,27,31\pmod{32}), puis de démontrer ce lemme par analyse congruentielle (transport des contraintes sous (U)) en utilisant le pont modulo 3 ci-dessus.
|
||||
La suite naturelle est d’énoncer formellement une “propriété locale de fermeture d’un enfant sur deux” (ou d’une fraction fixe) dans chacune des quatre branches (\equiv 7,15,27,31\pmod{32}), puis de démontrer ce lemme par analyse congruentielle (transport des contraintes sous (U)) en utilisant le pont modulo 3 ci-dessus.
|
||||
Le lemme modulo 3, $U(n)\equiv (-1)^{a(n)} \pmod 3$, relie la parité des valuations $a(n)$ à l’admissibilité des fusions (F). L’objectif restant est d’établir que, pour chaque branche de $R_m$, une profondeur finie ouvre une fenêtre de fusion ou de descente.
|
||||
|
||||
## Introduction au seuil vérification / analyse et aux bornes uniformes
|
||||
@ -8029,7 +8029,7 @@ La couverture explicitée au module 512 réduit l’analyse à un problème fini
|
||||
|
||||
Cette section consiste à transformer ce qui était encore une exploration (des feuilles fines) en une analyse structurée : construire, sur la branche (,n\equiv 31\pmod{32},), un **arbre déterministe de valuations** fondé sur des congruences linéaires, qui produit des **lemmes de descente uniformes** sur des sous-classes de petit module. C’est exactement le passage arithmétique (\to) analyse : la dynamique est traduite en contraintes (2)-adiques explicites, et la fermeture devient une conséquence de bornes et de congruences, non d’un calcul au cas par cas.
|
||||
|
||||
La suite ci-dessous établit d’abord un préfixe universel (quatre valuations égales à 1), puis calcule la valuation suivante sous forme d’un problème de divisibilité de la quantité linéaire (243n+211). Cette analyse donne une partition fine des sous-classes (par modules (64,128,256,512,\dots)) et permet de produire trois nouveaux lemmes de descente uniformes (et de réinterpréter ceux déjà obtenus) sous une forme systématique. Enfin, la couverture exhaustive au module (2048) pour la branche (31\pmod{32}) est mise à jour, avec liste explicite du résidu restant.
|
||||
La suite suivante établit d’abord un préfixe universel (quatre valuations égales à 1), puis calcule la valuation suivante sous forme d’un problème de divisibilité de la quantité linéaire (243n+211). Cette analyse donne une partition fine des sous-classes (par modules (64,128,256,512,\dots)) et permet de produire trois nouveaux lemmes de descente uniformes (et de réinterpréter ceux déjà obtenus) sous une forme systématique. Enfin, la couverture exhaustive au module (2048) pour la branche (31\pmod{32}) est mise à jour, avec liste explicite du résidu restant.
|
||||
|
||||
## Préfixe universel sur la branche (31 \pmod{32})
|
||||
|
||||
@ -8469,7 +8469,7 @@ Au palier (2048), sur la branche (31\pmod{32}), la fermeture uniforme obtenue pr
|
||||
[
|
||||
\frac{16}{64}=0.2500000000000000.
|
||||
]
|
||||
Au palier (8192), la branche contient (256) résidus. L’objectif est d’augmenter la fraction fermée par des lemmes uniformes en profondeur (k\le 8). Le résultat effectif (démontrable par les lemmes ci-dessous et leurs analogues) est :
|
||||
Au palier (8192), la branche contient (256) résidus. L’objectif est d’augmenter la fraction fermée par des lemmes uniformes en profondeur (k\le 8). Le résultat effectif (démontrable par les lemmes suivants et leurs analogues) est :
|
||||
[
|
||||
\frac{102}{256}=0.3984375000000000.
|
||||
]
|
||||
@ -8643,7 +8643,7 @@ Au palier $2^{13}=8192$, la branche $31\pmod{32}$ est décomposée en sous-ensem
|
||||
|
||||
La démarche “ainsi” peut désormais s’appuyer sur une étape d’analyse pleinement structurante : au lieu d’ajouter des feuilles profondes sans principe, il est possible d’énoncer un schéma canonique sur la branche (n\equiv 31\pmod{32}) qui engendre, par congruences linéaires, des familles de clauses (D) **uniformes** à profondeur bornée. L’étape qui suit consiste à franchir un nouveau palier (2)-adique, (m=14) (modulo (16384)), car c’est le premier palier où des blocs contractifs de somme (A=13) deviennent stables, et donc où des clauses universelles à horizon (k=8) peuvent être produites systématiquement.
|
||||
|
||||
Le propos ci-dessous poursuit exactement cette direction : construction explicite d’une nouvelle famille de clauses (D) au palier (16384), preuve détaillée d’un exemple, puis bilan quantitatif sur la branche (31\pmod{32}) au palier (8192) (ce qui est déjà fermé) et au palier (16384) (ce qui devient nouvellement fermable).
|
||||
Le propos de cette section poursuit exactement cette direction : construction explicite d’une nouvelle famille de clauses (D) au palier (16384), preuve détaillée d’un exemple, puis bilan quantitatif sur la branche (31\pmod{32}) au palier (8192) (ce qui est déjà fermé) et au palier (16384) (ce qui devient nouvellement fermable).
|
||||
|
||||
## Consolidation analytique au palier (8192) sur la branche (31\pmod{32})
|
||||
|
||||
@ -10497,7 +10497,7 @@ Au palier $4096$, la liste de neuf classes minimales de fusion ($A=11$) est obte
|
||||
|
||||
La “toile” de règles devient un objet mathématique à part entière dès qu’elle est formulée comme un ensemble fini de clauses universelles (D, F, et D minorées) agissant sur des classes congruentielles, avec un mécanisme de réduction strict (descente ou fusion vers un entier plus petit). À partir de ce moment, la recherche ne consiste plus à explorer des trajectoires, mais à prouver une propriété de **couverture totale** et de **réduction bien fondée**.
|
||||
|
||||
Le texte ci-dessous fixe explicitement le théorème cible, puis détaille les lemmes analytiques qui transforment les observations “congruences linéaires” en preuve générale, et enfin donne le plan opératoire pour obtenir un certificat fini (K) concluant Collatz.
|
||||
Le texte de cette section fixe explicitement le théorème cible, puis détaille les lemmes analytiques qui transforment les observations “congruences linéaires” en preuve générale, et enfin donne le plan opératoire pour obtenir un certificat fini (K) concluant Collatz.
|
||||
|
||||
## Théorème cible
|
||||
|
||||
@ -10666,7 +10666,7 @@ Le registre $(K)$ est formulé comme un ensemble fini de clauses universelles su
|
||||
Une preuve complète, dans la logique analytique déjà mise en place, consiste à établir un énoncé de couverture universelle : pour tout impair assez grand, au moins une règle du registre (K) s’applique et produit une réduction stricte (descente) ou une réduction inductive stricte (fusion vers un entier plus petit). À partir de là, la terminaison suit par descente bien fondée.
|
||||
|
||||
Avant d’entrer dans la partie formelle, un point de rigueur sur le contexte : dans les sources de référence grand public et dans les synthèses académiques de référence, la conjecture de Collatz reste présentée comme non résolue à ce jour, malgré de nombreuses prépublications revendiquant une preuve. ([Wikipédia][1])
|
||||
Le travail ci-dessous se place donc explicitement dans une démarche de preuve : poser les lemmes standard, exhiber des familles de clauses (D) et (F) démontrées, puis isoler l’ultime lemme de couverture à établir pour clôturer.
|
||||
Le travail de cette section se place explicitement dans une démarche de preuve : poser les lemmes standard, exhiber des familles de clauses (D) et (F) démontrées, puis isoler l’ultime lemme de couverture à établir pour clôturer.
|
||||
|
||||
## Cadre formel de preuve
|
||||
|
||||
@ -11153,7 +11153,7 @@ La fermeture par clauses minorées traite des classes non stabilisées au bit pr
|
||||
|
||||
La preuve avance par une étape formelle, auditable et finie : au palier (2^{15}=32768), la difficulté est de transformer la structure parent → enfants du résidu (R_{14}\to R_{15}) en un lemme de complétion systématique par clauses **minorées**. Toute situation « un seul enfant survit » doit être fermée sans attendre un palier supérieur, en utilisant le fait que l’enfant survivant a une valuation finale **plus grande** (donc une somme (A) plus grande), ce qui rend la descente minorée immédiate.
|
||||
|
||||
La suite ci-dessous établit cela au palier (m=15) : toutes les branches « one » (un seul enfant survivant) se ferment par des clauses minorées explicites. Le résidu restant devient alors exactement la pleine expansion binaire des parents « both » (deux enfants survivants). Cela réduit le problème à une sous-famille structurellement plus dure et mieux caractérisée.
|
||||
La suite suivante établit cela au palier (m=15) : toutes les branches « one » (un seul enfant survivant) se ferment par des clauses minorées explicites. Le résidu restant devient alors exactement la pleine expansion binaire des parents « both » (deux enfants survivants). Cela réduit le problème à une sous-famille structurellement plus dure et mieux caractérisée.
|
||||
|
||||
Le fichier d’audit exhaustif est fourni à la fin.
|
||||
|
||||
@ -12447,7 +12447,7 @@ La formalisation peut maintenant entrer dans la partie où la « méthode par re
|
||||
- les théorèmes de correction locaux (déjà disponibles),
|
||||
- puis l’unique énoncé global manquant : la **couverture totale** (ou extinction du noyau « both » à un palier fini).
|
||||
|
||||
Le texte ci-dessous continue la démonstration en précisant ces éléments, en gardant une forme standard (définitions, lemmes, théorèmes, dépendances).
|
||||
Le texte de cette section continue la démonstration en précisant ces éléments, en gardant une forme standard (définitions, lemmes, théorèmes, dépendances).
|
||||
|
||||
## Espace d’état étendu et statut du registre (K)
|
||||
|
||||
@ -13038,7 +13038,7 @@ Au palier \(2^{21}\), le paquet minimal \(D_{12}\) fournit 2225 clauses exactes
|
||||
|
||||
La formalisation peut se poursuivre en gardant exactement la même discipline : à chaque palier où un seuil contractif devient stabilisable, construire un paquet fini de clauses (D) minimales, fermer systématiquement les sœurs par scission, puis auditer la réduction effective sur l’ensemble résiduel et sur la distribution d’états.
|
||||
|
||||
Après (D_{10}) complet ((2^{17})), (D_{11}) ((2^{19})) et (D_{12}) minimal ((2^{21})), le seuil suivant est l’horizon 13, avec (A_{13}=21) stabilisé au palier (2^{22}). Un audit exhaustif du paquet (D_{13}) est produit ci-dessous.
|
||||
Après (D_{10}) complet ((2^{17})), (D_{11}) ((2^{19})) et (D_{12}) minimal ((2^{21})), le seuil suivant est l’horizon 13, avec (A_{13}=21) stabilisé au palier (2^{22}). Un audit exhaustif du paquet (D_{13}) est produit dans la section suivante.
|
||||
|
||||
[Télécharger l’audit « candidats D13 au palier 2^22 et impact »](sandbox:/mnt/data/candidats_D13_palier2p22_et_impact.md)
|
||||
|
||||
@ -13757,7 +13757,7 @@ La continuation consiste à intégrer ces paquets dans le registre (K), puis à
|
||||
|
||||
La section intègre la couche « fusion » au registre (K) au palier (2^{25}), puis recalcule les paquets (D_{16}) et (D_{17}) sur le noyau réduit, avec les mêmes objets auditables : liste exhaustive des clauses, statistiques de couverture, invariants de type (\max A_k) après élimination, et impact par états (projection (B_{12}), 60 états). L’évolution est formulée sur l’espace étendu où le registre de contraintes constitue une composante d’état.
|
||||
|
||||
Les fichiers d’audit correspondants sont produits ci-dessous.
|
||||
Les fichiers d’audit correspondants sont produits dans la section suivante.
|
||||
|
||||
## Intégration de la fusion au palier (2^{25})
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user