nicolas.cantu/algo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
algo/docs/features/collatz_c2_projective_verification.md
ncantu e3e68fe39c Formalize C2 and add deterministic projective verification artefacts 
**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
2026-03-09 01:25:16 +01:00

1.9 KiB
Raw Blame History

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 :
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) :
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.