Collatz: formalize hybrid targets and standardize run reports
**Motivations:** - Make the hybrid path (C1→C2→C3) operational with explicit targets - Define R_m exactly as used by the pipeline for citable artefacts - Keep execution transcripts out of proof documents via stable run reports **Root causes:** - Hybrid continuation lacked a concrete invariant/lemma agenda and a precise R_m definition - No standardized run report format in docs/ **Correctifs:** - Document the pipeline-level definition of R_m (D/F update rules and artefact schema) - Add explicit prioritization and lemma targets for the hybrid trajectory **Evolutions:** - Add a standard run report template and a filled example with sha256 fingerprints **Pages affectées:** - applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md - docs/fixKnowledge/collatz_docs_status_and_transcript_cleanup.md - docs/collatz_run_report_format.md - docs/collatz_run_report_2026-03-04_extend_D18_D21_resume_from_D20.md
This commit is contained in:
ncantu
parent
949886bb22
commit
242ec6c03f
@ -2,7 +2,7 @@
|
||||
|
||||
## Introduction
|
||||
|
||||
Ce document formalise l’objectif unique restant pour transformer une trajectoire d’audit en preuve complète : obtenir un lemme global transformant le registre \(\mathcal{K}\) en couverture universelle de \(\mathbb{N}\), soit par extinction finie à un palier \(2^M\), soit par contraction uniforme.
|
||||
Ce document formalise les verrous restants pour transformer une trajectoire d’audit en preuve complète : obtenir un lemme de clôture transformant le registre \(\mathcal{K}\) en couverture universelle de \(\mathbb{N}\), soit par extinction finie à un palier \(2^M\), soit par contraction uniforme, soit par une trajectoire hybride (réduction par certificats puis élimination théorique du noyau restant).
|
||||
|
||||
## Cadre
|
||||
|
||||
@ -13,6 +13,38 @@ Ce document formalise l’objectif unique restant pour transformer une trajectoi
|
||||
q_m = \frac{|R_{m+1}|}{2|R_m|}.
|
||||
\]
|
||||
|
||||
### Définition opérationnelle de \(R_m\) (implémentation pipeline)
|
||||
|
||||
Cette section fixe la définition exacte de \(R_m\) utilisée par les scripts de pipeline (c’est cette définition qui doit être citée lorsqu’un artefact `out/noyaux/noyau_post_*.json` est invoqué).
|
||||
|
||||
Représentation.
|
||||
|
||||
- Un noyau résiduel au palier \(m\) est stocké dans un fichier JSON de la forme :
|
||||
\[
|
||||
\{\;\text{"noyau"}:\,[r_1,\dots,r_N],\;\text{"palier"}:m\;\},
|
||||
\]
|
||||
où chaque \(r_i\) est un entier impair représentant une classe modulo \(2^m\).
|
||||
Référence : écriture dans `collatz_k_pipeline.py` (`run_single_palier`, écriture de `output_noyau_path`).
|
||||
|
||||
Règle D (montée de palier + soustraction des classes couvertes).
|
||||
|
||||
- Entrée : un noyau précédent \(R_{m_0}\) stocké dans `input_noyau`.
|
||||
- Relèvement au palier \(m\) : l’ensemble relevé \(L\subset (\mathbb{Z}/2^m\mathbb{Z})^\times\) est construit par ajouts de \(2^{m_0}\) (en pratique via `prev_shift` et `lift_count` dans `run_single_palier`).
|
||||
- Candidats : \(C=\{n\in L\mid A_k(n)=\text{valeur}\}\).
|
||||
- Couverture par scission des sœurs : \(\mathrm{cover}=C\cup\{n\oplus 2^{m-1}\mid n\in C\}\) (XOR avec `curr_shift = 2^{m-1}`).
|
||||
- Sortie : le noyau résiduel est \(R_m = L\setminus \mathrm{cover}\), écrit dans `output_noyau_path`.
|
||||
|
||||
Référence : `collatz_k_pipeline.py` (`run_single_palier` et `_run_single_palier_stream`).
|
||||
|
||||
Règle F (soustraction au même palier via certificat de fusion).
|
||||
|
||||
- Un certificat de fusion est construit en deux étapes :
|
||||
1) `collatz_fusion_pipeline.py` produit un CSV de clauses de fusion (colonne `classe_mod_2^m` et `sœur`) ;
|
||||
2) `collatz_scission.py` extrait un JSON `certificat_*.json` contenant `covered` (incluant les sœurs).
|
||||
- La mise à jour du noyau est alors : \(R_m \leftarrow R_m \setminus \mathrm{covered}\), au même palier \(m\) (le champ `palier` est conservé depuis le noyau précédent).
|
||||
|
||||
Référence : `collatz_scission.py` (`run_scission`) et `collatz_update_noyau.py` (`run_update_noyau`).
|
||||
|
||||
## Objectif 1 : extinction à palier fini (certificat total)
|
||||
|
||||
Énoncé cible
|
||||
@ -56,6 +88,60 @@ Minimum publiable pour une étape de vérification :
|
||||
- un script déterministe `verify_extinction.py` + une commande de reproduction ;
|
||||
- si |R_M|>0 : un fichier exportant les résidus survivants.
|
||||
|
||||
Format recommandé (rapport d’exécution).
|
||||
Pour éviter toute insertion de transcript dans les textes de preuve, utiliser un rapport d’exécution séparé et stable dans `docs/`, qui regroupe : commande, paramètres, artefacts d’entrée/sortie, empreintes, et assertion exacte vérifiée. Voir `docs/collatz_run_report_format.md`.
|
||||
|
||||
## Objectif 3 : trajectoire hybride (certificats + invariants + lemme spécifique)
|
||||
|
||||
Principe.
|
||||
La trajectoire hybride vise à éviter une “extinction brute” par montée indéfinie des paliers, en remplaçant la fin du calcul par une preuve sur un noyau survivant caractérisé. Elle se décompose en :
|
||||
|
||||
- réduction par certificats : pousser la construction de \(\mathcal{K}\) pour diminuer \(R_m\) et isoler un noyau survivant “simple” (au sens structural) ;
|
||||
- extraction d’invariants : dériver, depuis les artefacts, des contraintes arithmétiques stables satisfaites par tout élément de \(R_m\) ;
|
||||
- lemme d’élimination : prouver qu’aucun élément satisfaisant ces contraintes ne peut porter une orbite Collatz non terminante.
|
||||
|
||||
### 3.1. Invariants “naturels” à extraire sur \(R_m\)
|
||||
|
||||
Les invariants ci-dessous sont choisis pour être :
|
||||
1) définissables à partir des objets déjà présents (mots de valuations, constantes affines, congruences),
|
||||
2) vérifiables sur artefacts,
|
||||
3) utilisables comme hypothèses explicites d’un lemme (réfutables par contre-exemple).
|
||||
|
||||
- Invariance projective (sous-noyau both).
|
||||
Référence : `applications/collatz/collatz_k_scripts/noyau_both_base_4096.md`.
|
||||
À partir d’un certain rang, l’ensemble des “parents both” se projette sur une base \(B_{12}\subset (\mathbb{Z}/2^{12}\mathbb{Z})^\times\) de cardinal 192, avec stabilité \(B_m \bmod 2^{12}=B_{12}\) (à formaliser précisément au niveau où l’on l’utilise).
|
||||
|
||||
- Décomposition en automates de valuations à horizon fixé.
|
||||
Référence : `applications/collatz/collatz_k_scripts/audit_60_etats_B12_mod4096_horizon7.md`.
|
||||
Pour \(B_{12}\), l’horizon 7 induit une partition finie en états (mots \((a_0,\dots,a_6)\) et sommes \(A=\sum a_i\)), avec constantes affines \(C_7\) et \(D_8\) pour analyser le pas 8 via \(3^8n+D_8\).
|
||||
|
||||
- Congruences henséliennes et “relèvements” contrôlés.
|
||||
Référence : `applications/collatz/collatz_k_scripts/extraction analytique_60états.md`.
|
||||
Les conditions \(v_2(3n_7+1)\ge s\) se traduisent par une congruence linéaire \(3^8n+D_8\equiv 0 \pmod{2^{A+s}}\), qui admet une solution unique modulo \(2^{A+s}\) (car \(3^8\) est inversible modulo \(2^{A+s}\)). Cela fournit un mécanisme de scission arithmétique explicite dans lequel “un relèvement” est distingué.
|
||||
|
||||
### 3.2. Cibles de lemmes (formes à rendre vraies)
|
||||
|
||||
Les lemmes ci-dessous sont formulés comme cibles ; ils ne sont pas supposés vrais a priori, et doivent être évalués/ajustés par confrontation aux artefacts.
|
||||
|
||||
Priorisation (choix demandé).
|
||||
|
||||
1) traiter C1, puis 2) C2, puis 3) C3.
|
||||
|
||||
Lemme C1 (élimination par états).
|
||||
Fixer un horizon \(h\) (ex. \(h=7\) sur \(B_{12}\)) et sa partition en états. Pour chaque état \(E\), il existe une profondeur de relèvement \(\Delta m(E)\) et une règle d’élimination explicite telle que tout relèvement suffisamment haut d’un résidu de \(E\) tombe soit :
|
||||
- sous une clause de descente (D) certifiée, soit
|
||||
- sous une clause de fusion (F) certifiée vers une classe déjà contrôlée.
|
||||
|
||||
Objectif : prouver l’existence d’un \(\Delta m_{\max}\) uniforme sur les états, ou au minimum de bornes explicites état par état, puis “rassembler” ces éliminations en un certificat théorique de clôture du sous-noyau analysé.
|
||||
|
||||
Lemme C2 (réduction de \(R_m\) vers un noyau projectif).
|
||||
Il existe un mécanisme (à préciser : scission par frères + règles de fermeture) montrant que tout élément de \(R_m\) possède, après un nombre borné d’étapes de relèvement et de normalisation, un représentant dans un noyau projectif de type \(B_{12}\) (ou dans une famille finie de noyaux projectifs).
|
||||
Objectif : réduire la preuve globale à une élimination de noyaux projectifs finis.
|
||||
|
||||
Lemme C3 (impossibilité d’orbite infinie sous contraintes).
|
||||
Sous un paquet explicite de contraintes arithmétiques \(P\) (congruences, bornes sur sommes de valuations sur des horizons, contraintes modulo \(3^k\), etc.) extraites comme invariants des survivants, aucune orbite de la dynamique accélérée \(U\) ne peut être infinie.
|
||||
Objectif : fournir une mesure de rang ou une contradiction directe stable sous \(U\) sur le sous-ensemble défini par \(P\).
|
||||
|
||||
## Conclusion
|
||||
|
||||
La trajectoire D18–D21 (F15/F16) augmente le matériau et affine la cartographie du noyau résiduel, mais la preuve complète exige encore l’un des deux verrous : extinction à palier fini (certificat total) ou contraction uniforme (lemme analytique).
|
||||
|
||||
@ -0,0 +1,80 @@
|
||||
**Auteur** : Équipe 4NK
|
||||
|
||||
# Rapport d’exécution — extension D18→D21 (reprise depuis D20)
|
||||
|
||||
## Contexte
|
||||
|
||||
- **But du run** : exécuter la fin du pipeline d’extension (F16 puis D21) en reprenant depuis D20.
|
||||
- **Assertion ciblée** : produire les artefacts `candidats_F16_palier2p35.csv`, `certificat_F16_palier2p35.json`, `noyau_post_F16.json`, puis `candidats_D21_palier2p36.csv` et `noyau_post_D21.json` à partir d’un noyau existant au palier \(2^{34}\).
|
||||
- **Statut logique** :
|
||||
- le run produit des artefacts de couverture partielle (candidats/certificats) et un noyau résiduel final au palier \(2^{36}\) ;
|
||||
- le run ne prouve pas \(|R_{36}|=0\) : `noyau_post_D21.json` est non vide.
|
||||
|
||||
## Code et reproductibilité
|
||||
|
||||
- **Commande (tel que journalisé)** :
|
||||
|
||||
```bash
|
||||
cd /home/ncantu/code/algo/applications/collatz && source .venv/bin/activate && RESUME_FROM=D20 ./scripts/08-paliers-finale.sh
|
||||
```
|
||||
|
||||
- **Script orchestrateur** :
|
||||
- `applications/collatz/scripts/08-paliers-finale.sh`
|
||||
- sha256: `b6c55ef3d00356f6040331f3f54c169eb2e6836c982e1ff23b9cd542bc576a6a`
|
||||
- **Scripts Python principaux** :
|
||||
- `applications/collatz/collatz_k_scripts/collatz_k_pipeline.py`
|
||||
- sha256: `d74cbba1b2d040a88f7249e7a021e0f70310bb9988408996bf8b4aa1ffbdb340`
|
||||
- `applications/collatz/collatz_k_scripts/collatz_fusion_pipeline.py`
|
||||
- sha256: `e8d58bbf0ae222d6a1c93cdd64348910f776c57ff1886f7dbb54d08440bac2d4`
|
||||
- `applications/collatz/collatz_k_scripts/collatz_update_noyau.py`
|
||||
- sha256: `0c1082c060f5561420d16707c69769bc6360c60760c2b17f1f4a7c547b712b40`
|
||||
- `applications/collatz/collatz_k_scripts/collatz_scission.py`
|
||||
- sha256: `9d402b5b1352348c599cade7f39396150add7fed6b4f4472ca4ffc853f9d90e9`
|
||||
|
||||
## Entrées (artefacts consommés)
|
||||
|
||||
- `applications/collatz/collatz_k_scripts/audit_60_etats_B12_mod4096_horizon7.json`
|
||||
- sha256: `902a237c8dd4686f505772e632b12a79db4c5df7de4743758ec79247fa5c8307`
|
||||
- `applications/collatz/out/noyaux/noyau_post_D20.json`
|
||||
- utilisé comme noyau d’entrée au palier \(2^{34}\) (présent avant la reprise)
|
||||
|
||||
## Sorties (artefacts produits)
|
||||
|
||||
### Logs
|
||||
|
||||
- `applications/collatz/out/pipeline_extend.log`
|
||||
- sha256: `dc6b793ff9ac72e263c918f99d12615b1d9c7c8c74f525fb6de85b3c741d7027`
|
||||
- `applications/collatz/out/paliers_finale.log`
|
||||
- sha256: `0fa4fe924d2f05a1dd432ef513e754220517a10579058c2acf633d514a1bca32`
|
||||
|
||||
### Étape F16 (fusion, palier \(2^{35}\))
|
||||
|
||||
- `applications/collatz/out/candidats/candidats_F16_palier2p35.csv`
|
||||
- sha256: `536b80fc119a940f97e8d5c5f845b6d4f09e2ca81555b9d2c2dd63bb0ad7f876`
|
||||
- `applications/collatz/out/certificats/certificat_F16_palier2p35.json`
|
||||
- sha256: `32adaaec63dfd270c5ea23cd0ae7ea4abeb93fbc76dad17f9224954e8907d68d`
|
||||
- `applications/collatz/out/noyaux/noyau_post_F16.json`
|
||||
- sha256: `cc0310a62ba7a1b63d6059e467fd525f602f79ce077151dec29d403895589f96`
|
||||
|
||||
### Étape D21 (descente, palier \(2^{36}\))
|
||||
|
||||
- `applications/collatz/out/candidats/candidats_D21_palier2p36.csv`
|
||||
- sha256: `9248c0e9fe46fa228820aa251cefff2e9247f83ee3e751fa4fddbe8f57480da6`
|
||||
- `applications/collatz/out/noyaux/noyau_post_D21.json`
|
||||
- sha256: `80ca6647424a605ca520e14e0ac7114e4029532149e34e85addafddb946b11f1`
|
||||
|
||||
## Compteurs et métriques (extrait du log)
|
||||
|
||||
D’après `applications/collatz/out/pipeline_extend.log` :
|
||||
|
||||
- F16 :
|
||||
- certificats : 259 766 clauses / 259 766 couvertes
|
||||
- noyau post-F16 : 155 782 672 résidus
|
||||
- D21 :
|
||||
- candidats : 33 068 362 (candidats) ; couverture de même cardinalité dans le log
|
||||
- noyau post-D21 : 590 062 326 résidus
|
||||
|
||||
## Vérification
|
||||
|
||||
- Résultat observé : le noyau résiduel final au palier \(2^{36}\) est **non vide** (`noyau_post_D21.json`).
|
||||
|
||||
63
docs/collatz_run_report_format.md
Normal file
63
docs/collatz_run_report_format.md
Normal file
@ -0,0 +1,63 @@
|
||||
**Auteur** : Équipe 4NK
|
||||
|
||||
# Format standard de rapport d’exécution (Collatz)
|
||||
|
||||
## Objectif
|
||||
|
||||
Standardiser la rédaction d’un rapport d’exécution séparé du texte de preuve, afin que :
|
||||
|
||||
- le texte de preuve ne contienne pas de transcript terminal ;
|
||||
- chaque résultat computationnel soit citable avec une assertion explicite et des artefacts vérifiables ;
|
||||
- la reproduction soit déterministe (commande, paramètres, empreintes).
|
||||
|
||||
## Emplacement stable
|
||||
|
||||
Le rapport d’exécution doit être ajouté dans `docs/` (par exemple `docs/collatz_run_report_<YYYY-MM-DD>_<scope>.md`) et référencé depuis les documents mathématiques par un chemin stable.
|
||||
|
||||
## Gabarit (à copier-coller)
|
||||
|
||||
### Contexte
|
||||
|
||||
- **But du run** : (énoncé court)
|
||||
- **Assertion ciblée** : (ex. “montrer \(|R_M|=0\) pour \(M=\dots\)” ou “produire `certificat_F16...`”)
|
||||
- **Statut logique** : (ce que le run prouve, et ce qu’il ne prouve pas)
|
||||
|
||||
### Code et reproductibilité
|
||||
|
||||
- **Commit Git** : (hash)
|
||||
- **Commande exacte** : (copier-coller)
|
||||
- **Paramètres** : (liste structurée)
|
||||
- **Environnement** :
|
||||
- OS
|
||||
- Python
|
||||
- dépendances (si pertinent)
|
||||
|
||||
### Entrées (artefacts consommés)
|
||||
|
||||
Liste exhaustive avec chemins et empreintes :
|
||||
|
||||
- `path/to/input_1` : (sha256)
|
||||
- `path/to/input_2` : (sha256)
|
||||
|
||||
### Sorties (artefacts produits)
|
||||
|
||||
Liste exhaustive avec chemins et empreintes :
|
||||
|
||||
- `path/to/output_1` : (sha256)
|
||||
- `path/to/output_2` : (sha256)
|
||||
|
||||
### Compteurs et métriques
|
||||
|
||||
- \(|R_m|\), \(|B_m|\), \(q_m\) (si calculés)
|
||||
- tailles fichiers (optionnel)
|
||||
- bornes / maxima observés (ex. `max_r`)
|
||||
|
||||
### Vérification
|
||||
|
||||
- **Script de vérification** : (chemin + commande)
|
||||
- **Résultat** : (succès/échec, et valeur vérifiée, par ex. \(|R_M|=0\) ou \(|R_M|>0\))
|
||||
|
||||
### Notes (optionnel)
|
||||
|
||||
Informations d’exploitation non mathématiques (temps, mémoire) si elles sont utiles, sans les mélanger au texte de preuve.
|
||||
|
||||
@ -33,6 +33,7 @@ This combination makes the documents non-citable as a proof document: conclusion
|
||||
## Analysis modalities
|
||||
|
||||
- When a run transcript is needed, store it in a dedicated file (or in `out/` artefacts) and reference it from the proof document via a stable path and reproducible script invocation.
|
||||
- Use the standard run report template in `docs/collatz_run_report_format.md`, and keep at least one concrete filled report in `docs/` for citation.
|
||||
- For status checks, prefer referencing:
|
||||
- `applications/collatz/collatz_k_scripts/diagnostic_run_D18_D21_et_statut_preuve.md`
|
||||
- `applications/collatz/collatz_k_scripts/errata_demonstration_collatz.md`
|
||||
@ -46,5 +47,8 @@ No deployment. This change is documentation-only.
|
||||
|
||||
- `applications/collatz/conjoncture_collatz.md`
|
||||
- `applications/collatz/démonstration collatz.md`
|
||||
- `applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md`
|
||||
- `docs/fixKnowledge/collatz_docs_status_and_transcript_cleanup.md`
|
||||
- `docs/collatz_run_report_format.md`
|
||||
- `docs/collatz_run_report_2026-03-04_extend_D18_D21_resume_from_D20.md`
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user