Collatz: formalize local completeness (E1) and extend run report generator

**Motivations:**
- Start C1 with a concrete state E1 and a citable local-completeness (H6) target
- Support run reports beyond D18→D21 (section 7 validation)

**Root causes:**
- C1/H6 lacked a first explicit state-level coverage target
- Run report automation was limited to the extend pipeline

**Correctifs:**
- Add an explicit H6(E1) lift coverage plan with certified D/F semantics

**Evolutions:**
- Extend the report generator with profiles (extend_finale, validation_section7)
- Document the new profile usage in docs/ and docs/features/

**Pages affectées:**
- applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md
- applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
- docs/collatz_run_report_format.md
- docs/features/collatz_run_report_generator.md

applications/collatz/collatz_k_scripts/collatz_generate_run_report.py

@@ -0,0 +1,431 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+"""
+collatz_generate_run_report.py
+
+Generate a Collatz run report in docs/:
+- compute sha256 for selected scripts + artefacts
+- extract counters/metrics from pipeline logs
+- write a markdown file using the standard format
+
+This script is intended to keep proof documents free of terminal transcripts.
+"""
+
+from __future__ import annotations
+
+import argparse
+import hashlib
+import re
+import subprocess
+from dataclasses import dataclass
+from datetime import datetime
+from pathlib import Path
+
+
+@dataclass(frozen=True)
+class Sha256Entry:
+    path: str
+    sha256: str
+
+
+def sha256_file(path: Path, chunk_size: int = 16 * 1024 * 1024) -> str:
+    h = hashlib.sha256()
+    with path.open("rb") as f:
+        while True:
+            chunk = f.read(chunk_size)
+            if not chunk:
+                break
+            h.update(chunk)
+    return h.hexdigest()
+
+
+def compute_sha256_entries(paths: list[Path]) -> list[Sha256Entry]:
+    entries: list[Sha256Entry] = []
+    for p in paths:
+        if not p.exists():
+            raise FileNotFoundError(str(p))
+        digest = sha256_file(p)
+        entries.append(Sha256Entry(path=str(p), sha256=digest))
+    return entries
+
+
+def read_text(path: Path) -> str:
+    if not path.exists():
+        raise FileNotFoundError(str(path))
+    return path.read_text(encoding="utf-8", errors="strict")
+
+
+def parse_last_extend_run_date(pipeline_extend_log: str) -> str:
+    """
+    Return YYYY-MM-DD for the last extend run that reached completion.
+    """
+    lines = pipeline_extend_log.splitlines()
+    complete_idx = -1
+    for i, line in enumerate(lines):
+        if "STEP done D21 - extend pipeline complete" in line:
+            complete_idx = i
+    if complete_idx < 0:
+        raise ValueError("No completed extend run found in pipeline_extend.log")
+    m = re.match(r"^\[(\d{4}-\d{2}-\d{2})\s", lines[complete_idx])
+    if not m:
+        raise ValueError("Cannot parse date from completion line")
+    return m.group(1)
+
+
+@dataclass(frozen=True)
+class ExtendMetrics:
+    f16_rows: int
+    f16_new_noyau_residues: int
+    d21_candidates: int
+    d21_final_noyau_residues: int
+
+
+@dataclass(frozen=True)
+class Section7Metrics:
+    nstar: int
+    max_modulus_power: int
+    max_modulus_coverage_pct: float
+
+
+def parse_extend_metrics_from_logs(pipeline_extend_log: str, paliers_finale_log: str) -> ExtendMetrics:
+    """
+    Extract metrics needed for the report.
+
+    - F16: parse from paliers_finale.log line "Wrote merged fusion CSV: ... (N rows)"
+      and "Stream update: ... new noyau N residues"
+    - D21: parse from pipeline_extend.log lines:
+      "cand/cover done len(cand)=X ..." and "noyau written (Y residues)"
+    """
+    f16_rows = None
+    f16_new_noyau = None
+    for line in paliers_finale_log.splitlines():
+        m_rows = re.search(r"Wrote merged fusion CSV: .* \((\d+) rows\)", line)
+        if m_rows:
+            f16_rows = int(m_rows.group(1))
+        m_noyau = re.search(r"Stream update: covered \d+, new noyau (\d+) residues", line)
+        if m_noyau:
+            f16_new_noyau = int(m_noyau.group(1))
+    if f16_rows is None:
+        raise ValueError("Cannot find F16 merged CSV row count in paliers_finale.log")
+    if f16_new_noyau is None:
+        raise ValueError("Cannot find F16 new noyau residue count in paliers_finale.log")
+
+    d21_candidates = None
+    d21_noyau = None
+    for line in pipeline_extend_log.splitlines():
+        m_cand = re.search(r"cand/cover done len\(cand\)=(\d+)\s", line)
+        if m_cand:
+            d21_candidates = int(m_cand.group(1))
+        m_noyau = re.search(r"noyau written \((\d+) residues\)", line)
+        if m_noyau:
+            d21_noyau = int(m_noyau.group(1))
+    if d21_candidates is None:
+        raise ValueError("Cannot find D21 candidate count in pipeline_extend.log")
+    if d21_noyau is None:
+        raise ValueError("Cannot find D21 noyau residue count in pipeline_extend.log")
+
+    return ExtendMetrics(
+        f16_rows=f16_rows,
+        f16_new_noyau_residues=f16_new_noyau,
+        d21_candidates=d21_candidates,
+        d21_final_noyau_residues=d21_noyau,
+    )
+
+
+def parse_section7_metrics(seuil_global_md: str, coverage_md: str) -> Section7Metrics:
+    m = re.search(r"N\*\s*=\s*(\d+)", seuil_global_md)
+    if not m:
+        raise ValueError("Cannot parse N* from seuil_global_Nstar.md")
+    nstar = int(m.group(1))
+
+    max_power = -1
+    max_cov = 0.0
+    current_power: int | None = None
+    for line in coverage_md.splitlines():
+        m_mod = re.match(r"^###\s+Modulus\s+2\^(\d+)\b", line.strip())
+        if m_mod:
+            current_power = int(m_mod.group(1))
+            continue
+        m_cov = re.match(r"^-+\s*Coverage:\s*([0-9.]+)%\s*$", line.strip())
+        if m_cov and current_power is not None:
+            cov = float(m_cov.group(1))
+            if current_power > max_power:
+                max_power = current_power
+                max_cov = cov
+            current_power = None
+
+    if max_power < 0:
+        raise ValueError("Cannot parse coverage summary from verification_couverture_complete.md")
+
+    return Section7Metrics(nstar=nstar, max_modulus_power=max_power, max_modulus_coverage_pct=max_cov)
+
+
+def parse_running_command_from_paliers_finale_log(paliers_finale_log: str) -> str:
+    """
+    Extract the last 'Running: ...' command from paliers_finale.log.
+    """
+    cmd = ""
+    for line in paliers_finale_log.splitlines():
+        if "Running:" in line:
+            idx = line.find("Running:")
+            cmd = line[idx + len("Running:") :].strip()
+    if not cmd:
+        raise ValueError("Cannot find a 'Running:' line in paliers_finale.log")
+    return cmd
+
+
+def git_head_hash(repo_root: Path) -> str:
+    try:
+        out = subprocess.check_output(
+            ["git", "-C", str(repo_root), "rev-parse", "HEAD"],
+            text=True,
+        )
+        return out.strip()
+    except (subprocess.CalledProcessError, FileNotFoundError):
+        return ""
+
+
+def format_sha256_list(entries: list[Sha256Entry]) -> list[str]:
+    lines: list[str] = []
+    for e in entries:
+        lines.append(f"- `{e.path}`")
+        lines.append(f"  - sha256: `{e.sha256}`")
+    return lines
+
+
+def write_extend_run_report(
+    *,
+    output_path: Path,
+    report_title: str,
+    command: str,
+    git_commit: str,
+    sha_entries: list[Sha256Entry],
+    metrics: ExtendMetrics,
+    out_dir: Path,
+) -> None:
+    lines: list[str] = []
+    lines.append("**Auteur** : Équipe 4NK")
+    lines.append("")
+    lines.append(f"# {report_title}")
+    lines.append("")
+    lines.append("## Contexte")
+    lines.append("")
+    lines.append("- **But du run** : exécuter la fin du pipeline d’extension (F16 puis D21) en reprenant depuis D20.")
+    lines.append("- **Assertion ciblée** : produire les artefacts F16 et D21 à partir d’un noyau existant au palier \\(2^{34}\\).")
+    lines.append("- **Statut logique** :")
+    lines.append(f"  - le run produit un noyau résiduel final au palier \\(2^{{36}}\\) ;")
+    lines.append(f"  - le run ne prouve pas \\(|R_{{36}}|=0\\) : `noyau_post_D21.json` est non vide.")
+    lines.append("")
+    lines.append("## Code et reproductibilité")
+    lines.append("")
+    if git_commit:
+        lines.append(f"- **Commit Git** : `{git_commit}`")
+    if command:
+        lines.append("- **Commande** :")
+        lines.append("")
+        lines.append("```bash")
+        lines.append(command)
+        lines.append("```")
+        lines.append("")
+    lines.append("## Empreintes sha256 (scripts, logs, artefacts)")
+    lines.append("")
+    lines.extend(format_sha256_list(sha_entries))
+    lines.append("")
+    lines.append("## Compteurs et métriques (extraits des logs)")
+    lines.append("")
+    lines.append("### Étape F16 (fusion, palier \\(2^{35}\\))")
+    lines.append("")
+    lines.append(f"- lignes CSV fusionnées : {metrics.f16_rows}")
+    lines.append(f"- noyau post-F16 (résidus) : {metrics.f16_new_noyau_residues}")
+    lines.append("")
+    lines.append("### Étape D21 (descente, palier \\(2^{36}\\))")
+    lines.append("")
+    lines.append(f"- candidats D21 : {metrics.d21_candidates}")
+    lines.append(f"- noyau post-D21 (résidus) : {metrics.d21_final_noyau_residues}")
+    lines.append("")
+    lines.append("## Chemins d’artefacts")
+    lines.append("")
+    lines.append(f"- OUT : `{out_dir}`")
+    lines.append(f"- noyaux : `{out_dir / 'noyaux'}`")
+    lines.append(f"- candidats : `{out_dir / 'candidats'}`")
+    lines.append(f"- certificats : `{out_dir / 'certificats'}`")
+    lines.append("")
+    output_path.parent.mkdir(parents=True, exist_ok=True)
+    output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
+
+
+def write_section7_run_report(
+    *,
+    output_path: Path,
+    report_title: str,
+    command: str,
+    git_commit: str,
+    sha_entries: list[Sha256Entry],
+    metrics: Section7Metrics,
+    out_dir: Path,
+) -> None:
+    lines: list[str] = []
+    lines.append("**Auteur** : Équipe 4NK")
+    lines.append("")
+    lines.append(f"# {report_title}")
+    lines.append("")
+    lines.append("## Contexte")
+    lines.append("")
+    lines.append("- **But du run** : exécuter la validation “section 7” (N*, certificat complet, vérification de couverture, et vérification sur [1,N*] si applicable).")
+    lines.append("- **Assertion ciblée** : produire N* et les artefacts de validation, et obtenir une mesure de couverture du certificat complet.")
+    lines.append("- **Statut logique** :")
+    lines.append("  - la sortie `verification_couverture_complete.md` est un diagnostic de couverture au niveau des classes de résidus ;")
+    lines.append("  - la preuve de terminaison sur \\(\\mathbb{N}\\) requiert en plus un lemme de clôture (cf. plan).")
+    lines.append("")
+    lines.append("## Code et reproductibilité")
+    lines.append("")
+    if git_commit:
+        lines.append(f"- **Commit Git** : `{git_commit}`")
+    if command:
+        lines.append("- **Commande** :")
+        lines.append("")
+        lines.append("```bash")
+        lines.append(command)
+        lines.append("```")
+        lines.append("")
+    lines.append("## Empreintes sha256 (scripts, artefacts)")
+    lines.append("")
+    lines.extend(format_sha256_list(sha_entries))
+    lines.append("")
+    lines.append("## Compteurs et métriques")
+    lines.append("")
+    lines.append(f"- N* : {metrics.nstar}")
+    lines.append(f"- Couverture (modulus max 2^{metrics.max_modulus_power}) : {metrics.max_modulus_coverage_pct:.2f}%")
+    lines.append("")
+    lines.append("## Chemins d’artefacts")
+    lines.append("")
+    lines.append(f"- OUT : `{out_dir}`")
+    lines.append(f"- certificats : `{out_dir / 'certificats'}`")
+    lines.append(f"- audits : `{out_dir / 'audits'}`")
+    lines.append("")
+    output_path.parent.mkdir(parents=True, exist_ok=True)
+    output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
+
+
+def pick_report_date_from_mtime(paths: list[Path]) -> str:
+    mtimes = [p.stat().st_mtime for p in paths if p.exists()]
+    if not mtimes:
+        raise ValueError("Cannot infer report date: no existing artefact paths")
+    ts = max(mtimes)
+    return datetime.fromtimestamp(ts).strftime("%Y-%m-%d")
+
+
+def main() -> None:
+    ap = argparse.ArgumentParser(description="Generate a Collatz run report (sha256 + log metrics)")
+    ap.add_argument("--repo-root", default=None, help="Repository root (defaults to current working directory)")
+    ap.add_argument("--out-dir", required=True, help="Path to applications/collatz/out directory")
+    ap.add_argument("--docs-dir", required=True, help="Path to docs/ directory")
+    ap.add_argument(
+        "--profile",
+        default="extend_finale",
+        choices=["extend_finale", "validation_section7"],
+        help="Report profile",
+    )
+    ap.add_argument("--pipeline-extend-log", default=None, help="Path to pipeline_extend.log (defaults to OUT/pipeline_extend.log)")
+    ap.add_argument("--paliers-finale-log", default=None, help="Path to paliers_finale.log (defaults to OUT/paliers_finale.log)")
+    ap.add_argument("--scope", default="extend_D18_D21_resume_from_D20", help="Scope identifier for output filename")
+    ap.add_argument(
+        "--command",
+        default="",
+        help="Command line to embed in report (profile-dependent default if empty)",
+    )
+    args = ap.parse_args()
+
+    repo_root = Path(args.repo_root).resolve() if args.repo_root else Path.cwd().resolve()
+    out_dir = Path(args.out_dir).resolve()
+    docs_dir = Path(args.docs_dir).resolve()
+
+    pipeline_log_path = Path(args.pipeline_extend_log).resolve() if args.pipeline_extend_log else out_dir / "pipeline_extend.log"
+    paliers_log_path = Path(args.paliers_finale_log).resolve() if args.paliers_finale_log else out_dir / "paliers_finale.log"
+
+    commit_hash = git_head_hash(repo_root)
+
+    if args.profile == "extend_finale":
+        pipeline_log = read_text(pipeline_log_path)
+        paliers_log = read_text(paliers_log_path)
+
+        date_str = parse_last_extend_run_date(pipeline_log)
+        metrics = parse_extend_metrics_from_logs(pipeline_log, paliers_log)
+        command = args.command.strip() if args.command.strip() else parse_running_command_from_paliers_finale_log(paliers_log)
+
+        sha_paths: list[Path] = [
+            repo_root / "applications" / "collatz" / "scripts" / "08-paliers-finale.sh",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_k_pipeline.py",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_fusion_pipeline.py",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_update_noyau.py",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_scission.py",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "audit_60_etats_B12_mod4096_horizon7.json",
+            pipeline_log_path,
+            paliers_log_path,
+            out_dir / "candidats" / "candidats_F16_palier2p35.csv",
+            out_dir / "certificats" / "certificat_F16_palier2p35.json",
+            out_dir / "noyaux" / "noyau_post_F16.json",
+            out_dir / "candidats" / "candidats_D21_palier2p36.csv",
+            out_dir / "noyaux" / "noyau_post_D21.json",
+        ]
+
+        sha_entries = compute_sha256_entries(sha_paths)
+        output_path = docs_dir / f"collatz_run_report_{date_str}_{args.scope}.md"
+        write_extend_run_report(
+            output_path=output_path,
+            report_title=f"Rapport d’exécution — {args.scope}",
+            command=command,
+            git_commit=commit_hash,
+            sha_entries=sha_entries,
+            metrics=metrics,
+            out_dir=out_dir,
+        )
+        print(f"Wrote: {output_path}")
+        return
+
+    if args.profile == "validation_section7":
+        command = args.command.strip() if args.command.strip() else "cd applications/collatz && ./scripts/09-validation-certificat.sh"
+
+        seuil_md_path = out_dir / "certificats" / "seuil_global_Nstar.md"
+        full_cert_path = out_dir / "certificats" / "certificat_complet_depth21.json"
+        coverage_md_path = out_dir / "audits" / "verification_couverture_complete.md"
+        nstar_csv_path = out_dir / "audits" / "verification_Nstar_range.csv"
+
+        seuil_md = read_text(seuil_md_path)
+        coverage_md = read_text(coverage_md_path)
+        metrics = parse_section7_metrics(seuil_md, coverage_md)
+        date_str = pick_report_date_from_mtime([seuil_md_path, full_cert_path, coverage_md_path])
+
+        sha_paths: list[Path] = [
+            repo_root / "applications" / "collatz" / "scripts" / "09-validation-certificat.sh",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_calculate_Nstar.py",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_generate_full_certificate.py",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_verify_coverage.py",
+            repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_verify_Nstar_range.py",
+            seuil_md_path,
+            full_cert_path,
+            coverage_md_path,
+        ]
+        if nstar_csv_path.exists():
+            sha_paths.append(nstar_csv_path)
+
+        sha_entries = compute_sha256_entries(sha_paths)
+        output_path = docs_dir / f"collatz_run_report_{date_str}_{args.scope}.md"
+        write_section7_run_report(
+            output_path=output_path,
+            report_title=f"Rapport d’exécution — {args.scope}",
+            command=command,
+            git_commit=commit_hash,
+            sha_entries=sha_entries,
+            metrics=metrics,
+            out_dir=out_dir,
+        )
+        print(f"Wrote: {output_path}")
+        return
+
+    raise ValueError(f"Unknown profile: {args.profile}")
+
+
+if __name__ == "__main__":
+    main()
+

applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md

@@ -134,6 +134,65 @@ Fixer un horizon \(h\) (ex. \(h=7\) sur \(B_{12}\)) et sa partition en états. P
 
 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é.
 
+Énoncé (version “pipeline + math”, à rendre exact).
+
+Soit \(h=7\) et \(B_{12}\subset(\mathbb{Z}/2^{12}\mathbb{Z})^\times\) la base projective, avec une partition en états \(\{E\}\) donnée par les mots de valuations \((a_0,\dots,a_{h-1})\) observés sur \(B_{12}\) (cf. `audit_60_etats_B12_mod4096_horizon7.md`). Pour un état \(E\), on note \(B_{12}(E)\subset B_{12}\) l’ensemble des résidus réalisant \(E\).
+
+On dit qu’une classe \(x\in(\mathbb{Z}/2^m\mathbb{Z})^\times\) est :
+
+- **certifiée D au palier \(m\)** s’il existe un fichier `out/certificats/certificat_Dk_palier2pm.json` (pour un certain \(k\)) tel que \(x\) appartienne à l’ensemble `covered` de ce certificat ;
+- **certifiée F au palier \(m\)** s’il existe un fichier `out/certificats/certificat_Ft_palier2pm.json` (pour un certain \(t\)) tel que \(x\) appartienne à l’ensemble `covered` de ce certificat.
+
+On définit alors, pour un état \(E\), \(\Delta m(E)\) comme le plus petit entier \(\Delta\ge 0\) tel que, pour tout \(r\in B_{12}(E)\), l’ensemble de ses relèvements impairs au palier \(m=12+\Delta\),
+\[
+\mathrm{Lift}_{12\to m}(r)=\{r+ j\cdot 2^{12}\;:\; j=0,\dots,2^{m-12}-1\},
+\]
+soit entièrement couvert par une union finie de certificats \(D/F\) aux paliers \(\le m\) (au sens ci-dessus).
+
+Le lemme C1 vise à montrer que \(\Delta m(E)\) est fini pour tout état \(E\), et à produire une borne explicite (idéalement une borne uniforme \(\Delta m_{\max}\)).
+
+Hypothèses exactes à expliciter dans la preuve de C1.
+
+- (H1) **Affinité de \(U^h\)** : pour tout impair \(n\), la forme affine \(U^{(h)}(n)=(3^h n + C_h)/2^{A_h}\) est valable, avec \(A_h=\sum_{i<h} v_2(3n_i+1)\).
+- (H2) **Donnée d’état** : les constantes \((A,C_h)\) associées à un état \(E\) sont celles du calcul sur \(B_{12}\) (cf. table `audit_60_etats_B12_mod4096_horizon7.md`), et l’analyse du pas \(h+1\) repose sur une congruence linéaire de type \(3^{h+1}n+D_{h+1}\equiv 0 \pmod{2^s}\).
+- (H3) **Relèvement 2-adique effectif (Hensel linéaire)** : pour une congruence linéaire \(an+b\equiv 0\pmod{2^s}\) avec \(a\) impair, il existe une solution unique modulo \(2^s\), et le relèvement de solutions contrôle les valuations du pas suivant.
+- (H4) **Sémantique “certifiée D” (correction)** : une classe \(x\) figurant dans `covered` de `certificat_Dk_palier2pm.json` satisfait effectivement, par construction de la clause D correspondante, une réduction bien fondée dans la dynamique (au sens arithmétique, pas seulement au sens “appartenance au fichier”).
+- (H5) **Sémantique “certifiée F” (correction)** : une classe \(x\) figurant dans `covered` de `certificat_Ft_palier2pm.json` est effectivement reliée par une fusion (au sens défini par `collatz_k_fusion.py`) à une classe déjà contrôlée, et cette relation est compatible avec la clôture par bon ordre.
+- (H6) **Complétude locale** : la famille finie de certificats invoquée pour l’état \(E\) couvre bien tous les relèvements impairs de \(B_{12}(E)\) au palier \(m\) (c’est le point à démontrer).
+
+Choix d’un premier état \(E\) et formalisation de (H6).
+
+On choisit comme premier cas \(E=E_1\), l’état 1 de la table (mot \(1\,1\,1\,1\,1\,1\,1\), somme \(A=7\), constantes \(C_7=2059\), \(D_8=6305\)).
+Références :
+
+- définition de \(E_1\) : `audit_60_etats_B12_mod4096_horizon7.md` (État 1)
+- analyse hensélienne au pas 8 : `extraction analytique_60états.md` (section “État 1”)
+
+On note \(B_{12}(E_1)\subset B_{12}\) les 16 résidus modulo \(2^{12}\) listés dans l’audit (État 1).
+
+Sous (H1)–(H3), la contrainte “forcer une clause D au pas 8” se traduit par la congruence linéaire :
+\[
+3^8 n + D_8 \equiv 0 \pmod{2^{A+s}},
+\]
+ici \(3^8=6561\), \(D_8=6305\), \(A=7\). En particulier, l’exigence \(a_7\ge 6\) (donc \(A_8\ge 13\)) impose :
+\[
+6561n + 6305 \equiv 0 \pmod{2^{13}}.
+\]
+Cette congruence admet une solution unique modulo \(2^{13}\) (car 6561 est impair). Dans les calculs existants, elle correspond à la classe \(n\equiv 255\pmod{8192}\), pour laquelle \(A_8=13\) et une clause de descente (D) est déclenchée à \(k=8\).
+
+Complétude locale (H6) — formulation explicite sur les relèvements de \(E_1\).
+
+On fixe un palier de relèvement \(m\ge 13\) et on partitionne explicitement les relèvements \(\mathrm{Lift}_{12\to m}(B_{12}(E_1))\) en deux sous-ensembles :
+
+- **branche D** : les relèvements satisfaisant la congruence de descente au pas 8 (par ex. modulo \(2^{13}\)) ; ce sous-ensemble est couvert par un certificat D correspondant au pas 8 (dans une version “localisée” de la pipeline, cf. ci-dessous).
+- **branche F** : le complémentaire ; l’objectif est de montrer qu’il est couvert par une union finie de certificats F (par exemple à un horizon t=9 ou t=10), ce qui est vérifiable par construction via les critères de `collatz_k_fusion.py` (delta_F>0, seuil Nf, préimage m < n0).
+
+Pour rendre cette complétude locale *citable* (et alignée avec la notion “certifié D/F”), l’artefact attendu est un CSV+certificat construit sur un domaine fini explicitement défini :
+
+- domaine \(L\) : la liste explicite des relèvements impairs de \(B_{12}(E_1)\) au palier \(m\) (pour un premier essai : \(m=13\), donc \(L\) a cardinal \(2^{m-12}\cdot 16 = 32\)) ;
+- certificats produits : `certificat_D8_palier2p13.json` et/ou `certificat_Ft_palier2p13.json` (selon les horizons retenus), obtenus par les scripts existants `collatz_k_pipeline.py` (pour D) et `collatz_fusion_pipeline.py` + `collatz_scission.py` (pour F) appliqués à \(L\) ;
+- assertion (H6) : l’union des ensembles `covered` de ces certificats recouvre exactement \(L\).
+
 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.

docs/collatz_run_report_format.md

@@ -16,6 +16,27 @@ Le rapport d’exécution doit être ajouté dans `docs/` (par exemple `docs/col
 
 ## 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 d’un `OUT` existant (sha256 + compteurs extraits des logs) :
+
+```bash
+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) :
+
+```bash
+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
+```
+
 ### Contexte
 
 - **But du run** : (énoncé court)

docs/features/collatz_run_report_generator.md

@@ -0,0 +1,35 @@
+**Auteur** : Équipe 4NK
+
+# Collatz — Génération automatisée des rapports d’exécution
+
+## Objectif
+
+Fournir un mécanisme standard et reproductible pour produire un rapport d’exécution séparé du texte de preuve, contenant :
+
+- la commande,
+- les artefacts d’entrée et de sortie,
+- les empreintes sha256,
+- des compteurs extraits des logs,
+
+afin d’éviter toute insertion de transcript terminal dans les documents mathématiques.
+
+## Impacts
+
+- Les rapports d’exécution sont centralisés dans `docs/` et référencés depuis les documents de preuve par un chemin stable.
+- Les empreintes sha256 permettent de citer précisément les artefacts utilisés.
+
+## Modifications
+
+- Ajout d’un format standard : `docs/collatz_run_report_format.md`.
+- Ajout d’un générateur : `applications/collatz/collatz_k_scripts/collatz_generate_run_report.py`.
+- Ajout d’un exemple réel de rapport : `docs/collatz_run_report_2026-03-04_extend_D18_D21_resume_from_D20.md`.
+
+## Modalités d’analyse
+
+- Vérifier que `applications/collatz/out/pipeline_extend.log` et `applications/collatz/out/paliers_finale.log` existent et contiennent un run complet.
+- Vérifier la présence des artefacts listés (noyaux/candidats/certificats) dans `applications/collatz/out/`.
+
+## Modalités de déploiement
+
+Aucun déploiement.
+