algo/docs/collatz_run_report_format.md
ncantu 071da20b19 Add deterministic C3 local descent verification and run report profile
**Motivations:**
- Instrument the C3 “final lock” as a citeable deterministic artefact
- Provide a reproducible check over Lift(B12) at palier 2^13 using D8/Fusion witnesses

**Root causes:**
- C3 lacked a machine-checkable artefact aligned with the run-report standard

**Correctifs:**
- Add a deterministic verifier that checks fusion witnesses (m<n and U(m)=U^t(n)) and aggregates N* where computable

**Evolutions:**
- Version C3 verification artefacts under docs/artefacts
- Add run report profile c3_local_descent (sha256 + metrics)
- Document the new profile and reference the artefacts in the proof plan

**Pages affectées:**
- applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py
- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json
- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md
- applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
- docs/collatz_run_report_2026-03-09_c3_local_descent.md
- docs/collatz_run_report_format.md
- docs/features/collatz_run_report_generator.md
- docs/features/collatz_c3_local_descent_verification.md
- applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md
2026-03-09 01:44:01 +01:00

5.3 KiB
Raw Blame History

Auteur : Équipe 4NK

Format standard de rapport dexécution (Collatz)

Objectif

Standardiser la rédaction dun rapport dexé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 dexé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)

Génération automatisée

Le script applications/collatz/collatz_k_scripts/collatz_generate_run_report.py génère un rapport à partir des logs et des artefacts dun OUT existant (sha256 + compteurs extraits des logs) :

python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
  --profile extend_finale \
  --out-dir applications/collatz/out \
  --docs-dir docs

Pour la validation “section 7” (N*, certificat complet, coverage) :

python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
  --profile validation_section7 \
  --scope validation_section7 \
  --out-dir applications/collatz/out \
  --docs-dir docs

Pour le pipeline D16/D17 après fusion :

python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
  --profile pipeline_d16_d17 \
  --scope pipeline_d16_d17 \
  --out-dir applications/collatz/out \
  --docs-dir docs

Pour les fusions au palier 2^{25} (t=11,12,14) :

python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
  --profile fusion_palier2p25 \
  --scope fusion_palier2p25 \
  --out-dir applications/collatz/out \
  --docs-dir docs

Pour la complétude locale H6(E1) au palier 2^{13} (rapport basé sur des artefacts versionnés dans docs/artefacts/) :

python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
  --profile local_H6_E1 \
  --scope local_H6_E1 \
  --out-dir applications/collatz/out \
  --docs-dir docs

Pour une complétude locale H6 généralisée (artefacts versionnés, répertoire paramétrable) :

python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
  --profile local_H6 \
  --scope local_H6_E42 \
  --local-h6-artefacts-dir docs/artefacts/collatz/local_E42_palier2p13 \
  --out-dir applications/collatz/out \
  --docs-dir docs

Audit palier (local_H6). Lors de la génération dun rapport local_H6/local_H6_E1, un audit automatique compare :

  • le palier attendu (daprès metadata.json dans le répertoire dartefacts, sinon daprès le nom palier2p<m>),
  • au palier certifié (champ palier des certificat_*.json).

En cas de désaccord, la génération échoue (afin déviter une citation ambiguë dartefacts).

Pour la vérification C2 (complétion par frères ⇒ both ⇒ projection B_{12}, artefacts déterministes versionnés) :

python3 applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py \
  --repo-root /home/ncantu/code/algo \
  --output-dir docs/artefacts/collatz/c2_projective

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

Pour la vérification C3 (clôture locale au palier 2^{13} sur Lift(B_{12}) via témoins D8/Fusion, artefacts déterministes versionnés) :

python3 applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py \
  --local-h6-root docs/artefacts/collatz \
  --output-dir docs/artefacts/collatz/c3_local_descent

python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
  --profile c3_local_descent \
  --scope c3_local_descent \
  --c3-artefacts-dir docs/artefacts/collatz/c3_local_descent \
  --out-dir applications/collatz/out \
  --docs-dir docs

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 quil 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 dexploitation non mathématiques (temps, mémoire) si elles sont utiles, sans les mélanger au texte de preuve.