**Motivations:** - Extend refinement tooling with hensel chain leaves, targeted refinement leaves and brother-derived minorated clauses. - Document grammar extensions and targeted leaves/diagnostics workflows. **Root causes:** - N/A (evolutions) **Correctifs:** - N/A **Evolutions:** - Add collatz_build_hensel_chain_leaves.py, collatz_verify_hensel_chain_leaves.py. - Add collatz_build_targeted_refinement_leaves.py, collatz_verify_targeted_refinement_leaves.py, collatz_diagnose_targeted_leaves_failure.py. - Add collatz_build_refinement_bundle_over_Sm_multilevel.py. - Add collatz_derive_brother_minorated_clauses_from_terminal_over_Sm.py, collatz_verify_brother_derived_minorated_clauses_over_Sm.py. - Add refinement_K artefacts (bundle, hensel_chain_leaves, targeted_leaves) and minorated_clauses_over_Sm_derived_from_brothers. - Update README, conjoncture, and feature docs. **Pages affectées:** - applications/collatz/collatz_k_scripts/README.md - applications/collatz/conjoncture_collatz.md - applications/collatz/collatz_k_scripts/*.py (new) - docs/features/*.md - docs/artefacts/collatz/**
154 lines
6.1 KiB
Markdown
154 lines
6.1 KiB
Markdown
**Auteur** : Équipe 4NK
|
||
|
||
# Minorated descent clauses (D_minor) over S_M
|
||
|
||
## Objectif
|
||
|
||
Ajouter une grammaire de feuilles terminales de type **descente minorée** (notée \(D_{\underline{}}\) dans `applications/collatz/conjoncture_collatz.md`) pour fermer, à palier fixé \(2^M\), des classes qui échouent à produire une clause exacte directement décidable (typiquement parce que la dernière valuation n’est pas figée).
|
||
|
||
Cette grammaire vise en particulier les branches dominantes du résidu non couvert (p.ex. classes congruentes aux “sommets” \(2^t-1\)) où une simple **borne inférieure** sur une valuation suffit à conclure à la descente.
|
||
|
||
## Impacts
|
||
|
||
- Extension du jeu de feuilles utilisables par `collatz_build_refinement_certificate_over_Sm_multilevel.py` via des clauses `D_minor` exprimées à un palier \(2^M\).
|
||
- Réduction observée de `open_roots` sur `S_15` lors de l’ajout des feuilles `D_minor` (horizon \(k=8\), \(\underline A=13\)).
|
||
|
||
## Modifications
|
||
|
||
### Scripts
|
||
|
||
- `applications/collatz/collatz_k_scripts/collatz_generate_minorated_descent_clauses_over_Sm.py`
|
||
- Génère les clauses `D_minor` sur \(S_M\) (tous résidus impairs modulo \(2^M\)).
|
||
- Paramètres: `--palier M`, `--k`, `--underlineA`.
|
||
|
||
- `applications/collatz/collatz_k_scripts/collatz_verify_minorated_descent_clauses_over_Sm.py`
|
||
- Vérifie déterministiquement les clauses produites (stabilité du préfixe, cohérence de \(C_k\), congruence \(\bmod 2^{\underline A}\), seuil \(N_0\)).
|
||
|
||
- `applications/collatz/collatz_k_scripts/collatz_derive_brother_minorated_clauses_from_terminal_over_Sm.py`
|
||
- Dérive des clauses `D_minor` pour des frères à partir de clauses `D_exact` sur \(S_m\) (complétion par frères, via le même numérateur affine).
|
||
- Sort un JSON de feuilles additionnel, consommable par la fermeture multi-niveaux.
|
||
|
||
### Artefacts
|
||
|
||
Par défaut, sortie sous:
|
||
|
||
- `docs/artefacts/collatz/minorated_clauses_over_Sm/palier2p<M>/clauses_D_minor_over_Sm_mod2p<M>.json`
|
||
- `docs/artefacts/collatz/minorated_clauses_over_Sm/palier2p<M>/clauses_D_minor_over_Sm_mod2p<M>.md`
|
||
- `docs/artefacts/collatz/minorated_clauses_over_Sm/palier2p<M>/verification_D_minor_over_Sm_mod2p<M>.{json,md}`
|
||
|
||
Clauses dérivées “par frères” :
|
||
|
||
- `docs/artefacts/collatz/minorated_clauses_over_Sm_derived_from_brothers/palier2p<M>/clauses_D_minor_derived_from_brothers_over_Sm_mod2p<M>.json`
|
||
|
||
## Modalités d’analyse
|
||
|
||
### Génération (exemple M=15, k=8, underlineA=13)
|
||
|
||
```bash
|
||
cd /home/ncantu/code/algo
|
||
python3 applications/collatz/collatz_k_scripts/collatz_generate_minorated_descent_clauses_over_Sm.py \
|
||
--repo-root /home/ncantu/code/algo \
|
||
--palier 15 \
|
||
--k 8 \
|
||
--underlineA 13
|
||
```
|
||
|
||
### Génération (familles, M=15..18)
|
||
|
||
Exemple de génération “familles” par horizons \(k\) avec \(\underline A\) minimal contractif \((2^{\underline A}>3^k)\) :
|
||
|
||
```bash
|
||
cd /home/ncantu/code/algo
|
||
for palier in 15 16 17 18; do
|
||
for k in 6 7 8 9 10 11; do
|
||
u=$(K="$k" python3 - <<'PY'
|
||
import os
|
||
k=int(os.environ["K"])
|
||
a=3**k
|
||
u=0
|
||
while (1<<u) <= a:
|
||
u += 1
|
||
print(u)
|
||
PY
|
||
)
|
||
if [ "$u" -le "$palier" ]; then
|
||
python3 applications/collatz/collatz_k_scripts/collatz_generate_minorated_descent_clauses_over_Sm.py \
|
||
--repo-root /home/ncantu/code/algo \
|
||
--palier "$palier" \
|
||
--k "$k" \
|
||
--underlineA "$u"
|
||
python3 applications/collatz/collatz_k_scripts/collatz_verify_minorated_descent_clauses_over_Sm.py \
|
||
--clauses-json "docs/artefacts/collatz/minorated_clauses_over_Sm/palier2p${palier}/clauses_D_minor_over_Sm_mod2p${palier}_k${k}_u${u}.json"
|
||
fi
|
||
done
|
||
done
|
||
```
|
||
|
||
### Vérification
|
||
|
||
```bash
|
||
cd /home/ncantu/code/algo
|
||
python3 applications/collatz/collatz_k_scripts/collatz_verify_minorated_descent_clauses_over_Sm.py \
|
||
--clauses-json docs/artefacts/collatz/minorated_clauses_over_Sm/palier2p15/clauses_D_minor_over_Sm_mod2p15_k8_u13.json
|
||
```
|
||
|
||
### Intégration dans la fermeture par raffinement multi-niveaux
|
||
|
||
Ajouter le JSON de clauses `D_minor` comme source de feuilles supplémentaire:
|
||
|
||
```bash
|
||
cd /home/ncantu/code/algo
|
||
python3 applications/collatz/collatz_k_scripts/collatz_build_refinement_certificate_over_Sm_multilevel.py \
|
||
--repo-root /home/ncantu/code/algo \
|
||
--root-palier 15 \
|
||
--max-palier 18 \
|
||
--leaf-json docs/artefacts/collatz/terminal_clauses_over_Sm/palier2p15/clauses_terminal_over_Sm_mod2p15.json \
|
||
--leaf-json docs/artefacts/collatz/minorated_clauses_over_Sm/palier2p15/clauses_D_minor_over_Sm_mod2p15_k8_u13.json \
|
||
--leaf-json docs/artefacts/collatz/terminal_clauses_over_Sm/palier2p16/clauses_terminal_over_Sm_mod2p16.json \
|
||
--leaf-json docs/artefacts/collatz/terminal_clauses_over_Sm/palier2p17/clauses_terminal_over_Sm_mod2p17.json \
|
||
--leaf-json docs/artefacts/collatz/terminal_clauses_over_Sm/palier2p18/clauses_terminal_over_Sm_mod2p18.json
|
||
```
|
||
|
||
## Tableau comparatif automatisé (par ajout incrémental de familles)
|
||
|
||
Le script `collatz_compare_dminor_families_incremental.py` produit une table versionnable par “run” :
|
||
- \(\Delta open\_roots\)
|
||
- \(\Delta q_m\) (au palier racine, et les valeurs \(q_m\) restent disponibles dans chaque certificat)
|
||
- \(\Delta parents\_one\_child\)
|
||
- quantiles `lb_any` (p99/max) sur les racines encore ouvertes après chaque ajout
|
||
|
||
```bash
|
||
cd /home/ncantu/code/algo
|
||
python3 applications/collatz/collatz_k_scripts/collatz_compare_dminor_families_incremental.py \
|
||
--repo-root /home/ncantu/code/algo \
|
||
--root-palier 15 \
|
||
--max-palier 18 \
|
||
--k-max 256 \
|
||
--t-max 256 \
|
||
--search-max-required-m 256 \
|
||
--target-extremes-top-n 200
|
||
```
|
||
|
||
### Suivi d’une liste fixe (tracked roots file)
|
||
|
||
Pour comparer des runs sur exactement le même sous-ensemble d’extrêmes (liste stable), fournir un fichier texte :
|
||
- une racine par ligne (entier impair strictement positif)
|
||
- commentaires `# ...` autorisés
|
||
|
||
```bash
|
||
cd /home/ncantu/code/algo
|
||
python3 applications/collatz/collatz_k_scripts/collatz_compare_dminor_families_incremental.py \
|
||
--repo-root /home/ncantu/code/algo \
|
||
--root-palier 15 \
|
||
--max-palier 18 \
|
||
--k-max 256 \
|
||
--t-max 256 \
|
||
--search-max-required-m 256 \
|
||
--tracked-roots-file /path/to/tracked_roots.txt
|
||
```
|
||
|
||
## Déploiement
|
||
|
||
Aucun déploiement.
|
||
|