diff --git a/applications/collatz/collatz_k_scripts/collatz_generate_local_h6_run_reports.py b/applications/collatz/collatz_k_scripts/collatz_generate_local_h6_run_reports.py new file mode 100644 index 0000000..b1485d9 --- /dev/null +++ b/applications/collatz/collatz_k_scripts/collatz_generate_local_h6_run_reports.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- +""" +collatz_generate_local_h6_run_reports.py + +Generate deterministic run reports (sha256 + counters) for all local H6(E) state +directories at a given palier 2^m. + +This script: +- iterates `docs/artefacts/collatz/local_E*_palier2p/` +- calls `collatz_generate_run_report.py --profile local_H6` for each state +- updates `docs/artefacts/collatz/local_H6_index.md` by filling the `report` column + when a report is found (by globbing the generated filename). +""" + +from __future__ import annotations + +import argparse +import re +import subprocess +from pathlib import Path + + +def _discover_state_dirs(local_h6_root: Path, palier: int) -> list[Path]: + return sorted([p for p in local_h6_root.glob(f"local_E*_palier2p{palier}") if p.is_dir()]) + + +def _infer_state_id(state_dir: Path, palier: int) -> int: + m = re.search(rf"local_E(\d+)_palier2p{palier}$", state_dir.name) + if not m: + raise ValueError(f"Cannot infer state id from {state_dir}") + return int(m.group(1)) + + +def _run_report_for_state( + *, + repo_root: Path, + out_dir: Path, + docs_dir: Path, + artefacts_dir: Path, + state_id: int, + palier: int, +) -> None: + scope = f"local_H6_E{state_id}_palier2p{palier}" + cmd = [ + "python3", + str(repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_generate_run_report.py"), + "--profile", + "local_H6", + "--scope", + scope, + "--local-h6-artefacts-dir", + str(artefacts_dir), + "--out-dir", + str(out_dir), + "--docs-dir", + str(docs_dir), + ] + subprocess.run(cmd, cwd=str(repo_root), check=True) + + +def _find_report_path(docs_dir: Path, state_id: int, palier: int) -> Path | None: + # Match the generator naming: docs/collatz_run_report__.md + scope = f"local_H6_E{state_id}_palier2p{palier}" + matches = sorted(docs_dir.glob(f"collatz_run_report_*_{scope}.md"), key=lambda p: p.stat().st_mtime) + return matches[-1] if matches else None + + +def _update_index( + *, + index_path: Path, + docs_dir: Path, + palier: int, +) -> None: + if not index_path.exists(): + raise FileNotFoundError(str(index_path)) + lines = index_path.read_text(encoding="utf-8", errors="strict").splitlines() + out: list[str] = [] + for line in lines: + if not line.startswith("|"): + out.append(line) + continue + parts = [p.strip() for p in line.strip().split("|")] + # Table rows have leading/trailing empty due to separators. + if len(parts) < 5: + out.append(line) + continue + # Header separator row + if parts[1] == "---": + out.append(line) + continue + # Try parse state_id from first column + try: + state_id = int(parts[1]) + except ValueError: + out.append(line) + continue + # palier column is after |B12(E)|, i.e. parts[4] in current table layout + palier_cell = parts[4] + if palier_cell != f"2^{palier}": + out.append(line) + continue + report_path = _find_report_path(docs_dir, state_id, palier) + if report_path is None: + out.append(line) + continue + rel = report_path.resolve().relative_to(docs_dir.resolve().parent.resolve()) + # last column is 'report' in the current layout + parts[-2] = f"`{rel}`" + rebuilt = "| " + " | ".join(parts[1:-1]) + " |" + out.append(rebuilt) + index_path.write_text("\n".join(out) + "\n", encoding="utf-8") + + +def run( + *, + repo_root: Path, + out_dir: Path, + docs_dir: Path, + local_h6_root: Path, + palier: int, + index_path: Path, +) -> None: + state_dirs = _discover_state_dirs(local_h6_root, palier) + if len(state_dirs) != 60: + raise ValueError(f"Expected 60 state dirs at palier2p{palier}, got {len(state_dirs)}") + + for sd in state_dirs: + sid = _infer_state_id(sd, palier) + _run_report_for_state( + repo_root=repo_root, + out_dir=out_dir, + docs_dir=docs_dir, + artefacts_dir=sd, + state_id=sid, + palier=palier, + ) + + _update_index(index_path=index_path, docs_dir=docs_dir, palier=palier) + + +def main() -> None: + ap = argparse.ArgumentParser(description="Generate local H6 run reports for all states at palier 2^m") + ap.add_argument("--repo-root", default="", help="Repo root (defaults to cwd)") + ap.add_argument("--out-dir", default="applications/collatz/out", help="OUT directory (required by run report generator)") + ap.add_argument("--docs-dir", default="docs", help="docs/ directory") + ap.add_argument("--local-h6-root", default="docs/artefacts/collatz", help="Root containing local_E*_palier2p/") + ap.add_argument("--palier", type=int, required=True, help="Target palier m") + ap.add_argument("--index-path", default="docs/artefacts/collatz/local_H6_index.md", help="Aggregated index to update") + args = ap.parse_args() + + repo_root = Path(args.repo_root).resolve() if args.repo_root.strip() else Path.cwd().resolve() + run( + repo_root=repo_root, + out_dir=Path(args.out_dir).resolve(), + docs_dir=Path(args.docs_dir).resolve(), + local_h6_root=Path(args.local_h6_root).resolve(), + palier=int(args.palier), + index_path=Path(args.index_path).resolve(), + ) + + +if __name__ == "__main__": + main() + 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 3b73c6b..5ded0b6 100644 --- a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py +++ b/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py @@ -426,7 +426,9 @@ def write_c3_local_descent_run_report( lines.append("") lines.append("## Contexte") lines.append("") - lines.append("- **But du run** : vérifier C3 (clôture locale sur Lift(B12) au palier 2^13) via témoins D8/Fusion.") + lines.append( + f"- **But du run** : vérifier C3 (clôture locale sur Lift(B12) au palier 2^{metrics.palier}) via témoins D8/Fusion." + ) lines.append("- **Assertion vérifiée** : cohérence arithmétique des témoins (U(m)=U^t(n), m Path: + obj = read_json(clauses_json_path) + if not isinstance(obj, dict): + raise ValueError("Invalid universal clauses JSON: expected object") + inputs = obj.get("inputs") + if not isinstance(inputs, dict): + raise ValueError("Invalid universal clauses JSON: missing inputs") + p = inputs.get("verification_c3_local_descent_json") + if not isinstance(p, str) or not p.strip(): + raise ValueError("Invalid universal clauses JSON: missing inputs.verification_c3_local_descent_json") + path = Path(p) + if not path.is_absolute(): + path = repo_root / path + if not path.exists(): + raise FileNotFoundError(str(path)) + return path + + def _discover_base_noyau_path(artefacts_dir: Path) -> Path: candidates = sorted((artefacts_dir / "noyaux").glob("noyau_*_B12.json")) if len(candidates) != 1: @@ -1097,6 +1117,7 @@ def main() -> None: "local_H6_E1", "c2_projective", "c3_local_descent", + "c3_local_descent_palier", "universal_clauses", ], help="Report profile", @@ -1434,6 +1455,53 @@ def main() -> None: print(f"Wrote: {output_path}") return + if args.profile == "c3_local_descent_palier": + m = int(args.c3_palier) + command = args.command.strip() + if not command: + command = ( + "python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py " + "--profile c3_local_descent_palier " + "--out-dir applications/collatz/out --docs-dir docs " + "--c3-artefacts-dir docs/artefacts/collatz/c3_local_descent " + f"--c3-palier {m}" + ) + + artefacts_dir = ( + Path(args.c3_artefacts_dir).resolve() + if args.c3_artefacts_dir.strip() + else (docs_dir / "artefacts" / "collatz" / "c3_local_descent") + ) + if m == 13: + verification_json = artefacts_dir / "verification_c3_local_descent.json" + verification_md = artefacts_dir / "verification_c3_local_descent.md" + else: + verification_json = artefacts_dir / f"verification_c3_local_descent_palier2p{m}.json" + verification_md = artefacts_dir / f"verification_c3_local_descent_palier2p{m}.md" + metrics = parse_c3_local_descent_metrics(str(verification_json)) + date_str = pick_report_date_from_mtime([verification_json, verification_md]) + + sha_paths: list[Path] = [ + repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_verify_c3_local_descent.py", + repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_k_core.py", + repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_k_fusion.py", + verification_json, + verification_md, + ] + sha_entries = compute_sha256_entries(sha_paths) + output_path = docs_dir / f"collatz_run_report_{date_str}_c3_local_descent_palier2p{m}.md" + write_c3_local_descent_run_report( + output_path=output_path, + report_title=f"Rapport d’exécution — c3_local_descent_palier2p{m}", + command=command, + git_commit=commit_hash, + sha_entries=sha_entries, + metrics=metrics, + artefacts_dir=artefacts_dir, + ) + print(f"Wrote: {output_path}") + return + if args.profile == "universal_clauses": command = ( args.command.strip() @@ -1457,11 +1525,12 @@ def main() -> None: ) date_str = pick_report_date_from_mtime([clauses_json, clauses_md, verification_json, verification_md]) + c3_input_json = _extract_universal_clauses_c3_input_path(clauses_json_path=clauses_json, repo_root=repo_root) sha_paths: list[Path] = [ repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_generate_run_report.py", repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_extract_universal_clauses.py", repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_verify_universal_clauses.py", - repo_root / "docs" / "artefacts" / "collatz" / "c3_local_descent" / "verification_c3_local_descent.json", + c3_input_json, clauses_json, clauses_md, verification_json, diff --git a/applications/collatz/collatz_k_scripts/collatz_iterate_palier_protocol.py b/applications/collatz/collatz_k_scripts/collatz_iterate_palier_protocol.py index 349da6c..6eb626a 100644 --- a/applications/collatz/collatz_k_scripts/collatz_iterate_palier_protocol.py +++ b/applications/collatz/collatz_k_scripts/collatz_iterate_palier_protocol.py @@ -122,22 +122,34 @@ def run( f"--palier-start {tgt} --palier-max {tgt} " "--t-min 9 --t-max 120 --write-index --index-path docs/artefacts/collatz/local_H6_index.md" ), + "C1_local_H6_run_reports": ( + "python3 applications/collatz/collatz_k_scripts/collatz_generate_local_h6_run_reports.py " + "--out-dir applications/collatz/out --docs-dir docs --local-h6-root docs/artefacts/collatz " + f"--palier {tgt} --index-path docs/artefacts/collatz/local_H6_index.md" + ), "C3_verify_local_descent": ( "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 " f"--palier {tgt}" ), + "C3_run_report_palier": ( + "python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py " + "--profile c3_local_descent_palier " + "--c3-artefacts-dir docs/artefacts/collatz/c3_local_descent " + f"--c3-palier {tgt} " + "--out-dir applications/collatz/out --docs-dir docs" + ), "Universal_clauses_extract": ( "python3 applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py " f"--verification-json docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent_palier2p{tgt}.json " - "--output-dir docs/artefacts/collatz/universal_clauses" + f"--output-dir docs/artefacts/collatz/universal_clauses/palier2p{tgt}" ), "Universal_clauses_verify": ( "python3 applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py " f"--verification-json docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent_palier2p{tgt}.json " - "--clauses-json docs/artefacts/collatz/universal_clauses/clauses_universelles.json " - "--output-dir docs/artefacts/collatz/universal_clauses" + f"--clauses-json docs/artefacts/collatz/universal_clauses/palier2p{tgt}/clauses_universelles.json " + f"--output-dir docs/artefacts/collatz/universal_clauses/palier2p{tgt}" ), "C2_verify_projective": ( "python3 applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py " @@ -195,7 +207,7 @@ def run( md.append("## Notes") md.append("") md.append("- Pour `C3_verify_local_descent` : si `palier != 13`, les sorties attendues sont suffixées `..._palier2p.{json,md}`.") - md.append("- La génération de run reports (sha256 + compteurs) pour des paliers `m != 13` peut nécessiter l’extension du profil `c3_local_descent` du générateur de rapports.") + md.append("- Les rapports C3 par palier sont générés via le profil `c3_local_descent_palier` (nom de fichier déterministe).") _write_md(out_md, md) diff --git a/applications/collatz/conjoncture_collatz.md b/applications/collatz/conjoncture_collatz.md index 2d05bed..ceba030 100644 --- a/applications/collatz/conjoncture_collatz.md +++ b/applications/collatz/conjoncture_collatz.md @@ -73,7 +73,7 @@ Cette trajectoire isole une chaîne de vérifications citable (sans transcript) - C1 (complétude locale H6(E) sur les états de \(B_{12}\)) : - index : `docs/artefacts/collatz/local_H6_index.md` - - rapports : `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p13.md` + - rapports : `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p13.md`, `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p14.md` - C2 (réduction projective par complétion “one” et stabilité \(B_m\bmod 2^{12}=B_{12}\)) : - script : `applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py` @@ -86,13 +86,13 @@ Cette trajectoire isole une chaîne de vérifications citable (sans transcript) - C3 (instance locale au palier \(2^{13}\) sur \(L=\mathrm{Lift}_{12\to 13}(B_{12})\)) : - script : `applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py` - - sorties : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}` - - rapport : `docs/collatz_run_report_2026-03-09_c3_local_descent.md` + - sorties : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}` et `..._palier2p.{json,md}` + - rapports : `docs/collatz_run_report_2026-03-09_c3_local_descent.md`, `docs/collatz_run_report_2026-03-09_c3_local_descent_palier2p14.md` - Extraction de clauses universelles candidates (Option A : Lift(\(B_{12}\))) : - scripts : `applications/collatz/collatz_k_scripts/{collatz_extract_universal_clauses.py,collatz_verify_universal_clauses.py}` - - sorties : `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}` - - rapport : `docs/collatz_run_report_2026-03-09_universal_clauses.md` + - sorties : `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}` et `docs/artefacts/collatz/universal_clauses/palier2p14/*` + - rapports : `docs/collatz_run_report_2026-03-09_universal_clauses.md`, `docs/collatz_run_report_2026-03-09_universal_clauses_palier2p14.md` Le verrou restant est la transformation des témoins observés en clauses universelles valides “pour tout \(n\) dans une classe modulo \(2^m\), pour tout \(n\ge N\)”, et l’itération du schéma \(C1+C2\to C3\) à paliers arbitraires. La formalisation minimale visée est donnée dans : - `applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md`. diff --git a/applications/collatz/démonstration collatz.md b/applications/collatz/démonstration collatz.md index 6fdc093..4b2e2a5 100644 --- a/applications/collatz/démonstration collatz.md +++ b/applications/collatz/démonstration collatz.md @@ -128,8 +128,8 @@ Pour chaque état \(E\) (mot de valuations sur \(B_{12}\) à horizon fixé), ét Artefacts (H6 locale). - index agrégé : `docs/artefacts/collatz/local_H6_index.md` -- répertoires par état : `docs/artefacts/collatz/local_E*_palier2p13/` -- rapports d’exécution : `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p13.md` +- répertoires par état : `docs/artefacts/collatz/local_E*_palier2p13/`, `docs/artefacts/collatz/local_E*_palier2p14/` +- rapports d’exécution : `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p13.md`, `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p14.md` 6.3. C3 (instance locale : clôture sur Lift(\(B_{12}\)) au palier \(2^{13}\)) @@ -138,8 +138,8 @@ Sur le domaine \(L=\mathrm{Lift}_{12\to 13}(B_{12})\), exhiber pour chaque class Artefact déterministe (C3 local). - script : `applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py` -- sorties versionnées : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}` -- rapport d’exécution : `docs/collatz_run_report_2026-03-09_c3_local_descent.md` +- sorties versionnées : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}` et `..._palier2p.{json,md}` +- rapports d’exécution : `docs/collatz_run_report_2026-03-09_c3_local_descent.md`, `docs/collatz_run_report_2026-03-09_c3_local_descent_palier2p14.md` 6.4. Verrou formel restant (au-delà de \(2^{13}\)) @@ -155,8 +155,8 @@ La formalisation minimale de ces clauses universelles (formes D/F, seuils \(N_0/ Artefacts déterministes : - extraction : `applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py` - vérification : `applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py` -- sorties versionnées : `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}` -- rapport d’exécution : `docs/collatz_run_report_2026-03-09_universal_clauses.md` +- sorties versionnées : `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}` et `docs/artefacts/collatz/universal_clauses/palier2p14/*` +- rapports d’exécution : `docs/collatz_run_report_2026-03-09_universal_clauses.md`, `docs/collatz_run_report_2026-03-09_universal_clauses_palier2p14.md` 6.6. Protocole déterministe d’itération de palier (au-delà de \(2^{13}\)) diff --git a/docs/collatz_run_report_format.md b/docs/collatz_run_report_format.md index 5a75eb5..081e5f2 100644 --- a/docs/collatz_run_report_format.md +++ b/docs/collatz_run_report_format.md @@ -117,6 +117,17 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \ --docs-dir docs ``` +Pour un rapport **distinct par palier** (sans surcharger `--scope`) : + +```bash +python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \ + --profile c3_local_descent_palier \ + --c3-artefacts-dir docs/artefacts/collatz/c3_local_descent \ + --c3-palier 14 \ + --out-dir applications/collatz/out \ + --docs-dir docs +``` + Pour l’extraction/vérification de clauses universelles candidates (Option A : Lift(\(B_{12}\))), à partir de l’artefact C3 (artefacts déterministes versionnés) : ```bash diff --git a/docs/features/collatz_run_report_generator.md b/docs/features/collatz_run_report_generator.md index bd56410..03c6218 100644 --- a/docs/features/collatz_run_report_generator.md +++ b/docs/features/collatz_run_report_generator.md @@ -23,11 +23,12 @@ afin d’éviter toute insertion de transcript terminal dans les documents math - 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`. - - Profils supportés : `extend_finale`, `validation_section7`, `pipeline_d16_d17`, `fusion_palier2p25`, `local_H6_E1`, `local_H6`, `c2_projective`, `c3_local_descent`, `universal_clauses`. + - Profils supportés : `extend_finale`, `validation_section7`, `pipeline_d16_d17`, `fusion_palier2p25`, `local_H6_E1`, `local_H6`, `c2_projective`, `c3_local_descent`, `c3_local_descent_palier`, `universal_clauses`. - 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. - Pour `c2_projective`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/c2_projective/verification_c2_projective.{json,md}`. - - Pour `c3_local_descent`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}`. - - Pour `universal_clauses`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}` et l’entrée `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`. + - Pour `c3_local_descent`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}` (et, si `--c3-palier != 13`, les variantes suffixées `..._palier2p.{json,md}`). + - Pour `c3_local_descent_palier`, le nom de fichier du rapport est déterministe : `docs/collatz_run_report__c3_local_descent_palier2p.md`. + - Pour `universal_clauses`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/universal_clauses/...` et l’entrée C3 est déduite de `clauses_universelles.json` (champ `inputs.verification_c3_local_descent_json`). ## Modalités d’analyse