From e12c544e7bf8d7a6f9518cdd4959d0da07bccc07 Mon Sep 17 00:00:00 2001 From: ncantu Date: Mon, 9 Mar 2026 01:18:40 +0100 Subject: [PATCH] Add local H6 palier audit to run reports MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit **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 --- .../collatz_generate_run_report.py | 36 ++++++++++++++++++- ...lemmes_manquants_et_programme_de_preuve.md | 9 +++++ docs/collatz_run_report_format.md | 8 +++++ docs/features/collatz_run_report_generator.md | 1 + 4 files changed, 53 insertions(+), 1 deletion(-) diff --git a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py b/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py index 7d0ef43..a8c747c 100644 --- a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py +++ b/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`)") + 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}`") diff --git a/applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md b/applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md index 47b8752..81319fa 100644 --- a/applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md +++ b/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. diff --git a/docs/collatz_run_report_format.md b/docs/collatz_run_report_format.md index 51ba048..2f4a03d 100644 --- a/docs/collatz_run_report_format.md +++ b/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`), +- 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) diff --git a/docs/features/collatz_run_report_generator.md b/docs/features/collatz_run_report_generator.md index 36bb237..4e14d03 100644 --- a/docs/features/collatz_run_report_generator.md +++ b/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