e3e68fe39c
**Motivations:** - Make Lemma C2 assertions citeable without terminal transcripts - Provide a deterministic check for “both-children residual” and projective projection to B12 **Root causes:** - C2 relied on narrative links between completion docs and B12 invariance without a machine-checkable artefact **Correctifs:** - Add a deterministic verifier that checks set equalities and projections from the existing completion MD sources **Evolutions:** - Version C2 verification artefacts in docs/artefacts - Add a run report profile (sha256 + metrics) for C2 projective verification - Update the proof plan with explicit C2 statements and references **Pages affectées:** - applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py - docs/artefacts/collatz/c2_projective/verification_c2_projective.json - docs/artefacts/collatz/c2_projective/verification_c2_projective.md - applications/collatz/collatz_k_scripts/collatz_generate_run_report.py - docs/collatz_run_report_2026-03-09_c2_projective.md - docs/collatz_run_report_format.md - docs/features/collatz_run_report_generator.md - docs/features/collatz_c2_projective_verification.md - applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md
53 lines
1.9 KiB
Markdown
53 lines
1.9 KiB
Markdown
**Auteur** : Équipe 4NK
|
||
|
||
# Collatz — Vérification déterministe de C2 (réduction projective)
|
||
|
||
## Objectif
|
||
|
||
Rendre citable (sans transcript terminal) une vérification déterministe des assertions utilisées dans le lemme C2 :
|
||
|
||
- **complétion par frères** : après fermeture des cas “one”, le résidu au palier suivant est exactement l’ensemble des **enfants** des parents “both” ;
|
||
- **projection projective** : l’ensemble des parents “both” à certains paliers se projette modulo \(2^{12}\) sur une base fixe \(B_{12}\subset(\mathbb{Z}/2^{12}\mathbb{Z})^\times\).
|
||
|
||
## Impacts
|
||
|
||
- Ajout d’un artefact versionné dans `docs/artefacts/` et d’un rapport d’exécution dans `docs/`, alignés sur le format standard des rapports.
|
||
|
||
## Modifications
|
||
|
||
- Script déterministe :
|
||
- `applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py`
|
||
- Artefacts versionnés (sortie du script) :
|
||
- `docs/artefacts/collatz/c2_projective/verification_c2_projective.json`
|
||
- `docs/artefacts/collatz/c2_projective/verification_c2_projective.md`
|
||
- Rapport d’exécution (sha256 + métriques) :
|
||
- `docs/collatz_run_report_2026-03-09_c2_projective.md`
|
||
- Extension du générateur de rapports :
|
||
- `applications/collatz/collatz_k_scripts/collatz_generate_run_report.py` (profil `c2_projective`)
|
||
|
||
## Modalités d’analyse
|
||
|
||
- Générer/mettre à jour les artefacts déterministes :
|
||
|
||
```bash
|
||
python3 applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py \
|
||
--repo-root /home/ncantu/code/algo \
|
||
--output-dir docs/artefacts/collatz/c2_projective
|
||
```
|
||
|
||
- Produire le rapport d’exécution (empreintes sha256 + métriques) :
|
||
|
||
```bash
|
||
python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
|
||
--profile c2_projective \
|
||
--scope c2_projective \
|
||
--c2-artefacts-dir docs/artefacts/collatz/c2_projective \
|
||
--out-dir applications/collatz/out \
|
||
--docs-dir docs
|
||
```
|
||
|
||
## Modalités de déploiement
|
||
|
||
Aucun déploiement.
|
||
|