Add local H6 palier audit to run reports

**Motivations:**
- Prevent citing local H6 reports with inconsistent paliers
- Make expected vs certified palier explicit in generated reports

**Root causes:**
- Certificates can be produced from CSVs where the palier is not encoded in the class column name
- Reports did not surface palier expectations vs certificate metadata

**Correctifs:**
- Add an explicit audit section comparing artefact expected palier to certificate palier

**Evolutions:**
- Document the palier audit in report format and generator docs
- Record observed uniform bounds (Δm(E), max fusion horizon) in the proof plan as audit facts

**Pages affectées:**
- 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/plan_lemmes_manquants_et_programme_de_preuve.md

applications/collatz/collatz_k_scripts/collatz_generate_run_report.py

@@ -116,6 +116,7 @@ class LocalH6Metrics:
     lifted_domain_size: int
     union_covered: int
     certificate_coverages: list[tuple[str, int]]
+    certificate_paliers: list[tuple[str, int]]
 
 
 def _discover_base_noyau_path(artefacts_dir: Path) -> Path:
@@ -156,6 +157,7 @@ def compute_local_h6_metrics(
     palier: int | None = None
     covered_union: set[int] = set()
     certificate_coverages: list[tuple[str, int]] = []
+    certificate_paliers: list[tuple[str, int]] = []
     for cert_path in certificate_paths:
         cert_obj = read_json(cert_path)
         if not isinstance(cert_obj, dict):
@@ -173,6 +175,7 @@ def compute_local_h6_metrics(
         s = set(cov)
         covered_union |= s
         certificate_coverages.append((str(cert_path), len(s)))
+        certificate_paliers.append((str(cert_path), cert_palier))
 
     if palier is None:
         raise ValueError("Cannot infer target palier from certificates")
@@ -203,9 +206,25 @@ def compute_local_h6_metrics(
         lifted_domain_size=len(lifted_domain),
         union_covered=len(covered_union),
         certificate_coverages=certificate_coverages,
+        certificate_paliers=certificate_paliers,
     )
 
 
+def _discover_expected_palier_for_local_h6(artefacts_dir: Path) -> int | None:
+    metadata_path = artefacts_dir / "metadata.json"
+    if metadata_path.exists():
+        obj = read_json(metadata_path)
+        if isinstance(obj, dict):
+            target = obj.get("target_palier")
+            if isinstance(target, int) and target > 0:
+                return target
+
+    m = re.search(r"palier2p(\d+)", str(artefacts_dir))
+    if m:
+        return int(m.group(1))
+    return None
+
+
 def parse_extend_metrics_from_logs(pipeline_extend_log: str, paliers_finale_log: str) -> ExtendMetrics:
     """
     Extract metrics needed for the report.
@@ -608,7 +627,7 @@ def write_local_h6_e1_run_report(
     lines.append("## Contexte")
     lines.append("")
     lines.append("- **But** : vérifier H6(E1) (complétude locale) par couverture explicite des relèvements au palier cible.")
-    lines.append("- **Assertion vérifiée** : l’union des ensembles `covered` (certificats D8 et F9–F40) est égale au domaine relevé.")
+    lines.append("- **Assertion vérifiée** : l’union des ensembles `covered` (certificats locaux D/F) est égale au domaine relevé.")
     lines.append("- **Statut logique** : ce rapport vérifie une égalité d’ensembles sur des artefacts versionnés ; il ne prouve pas la correction sémantique des clauses D/F.")
     lines.append("")
     lines.append("## Code et reproductibilité")
@@ -634,6 +653,21 @@ def write_local_h6_e1_run_report(
         lines.append(f"- |covered({Path(path_str).name})| : {c}")
     lines.append(f"- |covered(∪ certificats)| : {metrics.union_covered}")
     lines.append("")
+    lines.append("## Audit — palier attendu vs palier certifié")
+    lines.append("")
+    expected_palier = _discover_expected_palier_for_local_h6(artefacts_dir)
+    if expected_palier is None:
+        lines.append("- palier attendu : (indéterminé : aucun `metadata.json` et nom de répertoire sans `palier2p<m>`)")
+    else:
+        lines.append(f"- palier attendu : {expected_palier}")
+    lines.append(f"- palier certifié (d’après certificats) : {metrics.target_palier}")
+    for path_str, p in metrics.certificate_paliers:
+        lines.append(f"- palier({Path(path_str).name}) : {p}")
+    if expected_palier is not None and expected_palier != metrics.target_palier:
+        raise ValueError(
+            f"Local H6 report palier mismatch: expected {expected_palier} (artefacts), certified {metrics.target_palier} (certificates)"
+        )
+    lines.append("")
     lines.append("## Chemins d’artefacts (versionnés)")
     lines.append("")
     lines.append(f"- ARTEFACTS : `{artefacts_dir}`")

applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md

@@ -205,6 +205,15 @@ Un index versionné agrège \(\Delta m(E)\) et les horizons minimaux observés p
 
 - `docs/artefacts/collatz/local_H6_index.md`
 
+Constats (à partir de l’index, palier cible \(2^{13}\)).
+Les artefacts versionnés montrent, pour les 60 états \(E\) de \(B_{12}\) :
+
+- \(\Delta m(E)=1\) (donc relèvement \(12\to 13\)) ;
+- l’horizon maximal observé pour la complétude par fusion est \(t_{\max}=51\) (états \(E9\) et \(E25\)) ;
+- certains états sont complets par D8 seul (pas de clause de fusion observée sur le complément après D8 : \(E56\), \(E57\), \(E58\)).
+
+Ces constats sont des assertions d’audit (égalité d’ensembles sur artefacts) et ne remplacent pas la preuve des hypothèses (H4)–(H5).
+
 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

@@ -78,6 +78,14 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
   --docs-dir docs
 ```
 
+Audit palier (local_H6).
+Lors de la génération d’un rapport `local_H6`/`local_H6_E1`, un audit automatique compare :
+
+- le **palier attendu** (d’après `metadata.json` dans le répertoire d’artefacts, sinon d’aprè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ë d’artefacts).
+
 ### Contexte
 
 - **But du run** : (énoncé court)

docs/features/collatz_run_report_generator.md

@@ -24,6 +24,7 @@ afin d’éviter toute insertion de transcript terminal dans les documents math
 - 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`.
  - Profils supportés : `extend_finale`, `validation_section7`, `pipeline_d16_d17`, `fusion_palier2p25`, `local_H6_E1`, `local_H6`.
+ - Pour `local_H6`/`local_H6_E1`, un audit automatique compare le **palier attendu** (artefacts) au **palier certifié** (certificats) et échoue en cas de désaccord.
 
 ## Modalités d’analyse