nicolas.cantu/algo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

collatz: add palier iteration tooling and C3 palier run reports

Browse Source 
**Motivations:**
- Support deterministic iteration beyond 2^13 with palier-scoped artefacts and reports.

**Root causes:**
- C3 palier runs needed distinct report naming; universal clause reports referenced a hard-coded C3 input.
- Palier iteration lacked a deterministic way to mass-generate local H6 run reports and keep `local_H6_index.md` consistent.

**Correctifs:**
- Add `c3_local_descent_palier` report profile (distinct filename per palier) and fix C3 report wording to use the actual palier.
- Make `universal_clauses` report profile derive its C3 input from `clauses_universelles.json`.

**Evolutions:**
- Add `collatz_generate_local_h6_run_reports.py` and extend `collatz_iterate_palier_protocol.py` to include C1 reports + palier-scoped universal clause outputs.
- Update documentation and proof pointers for palier2p14 artefacts/reports.

**Pages affectées:**
- applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
- applications/collatz/collatz_k_scripts/collatz_generate_local_h6_run_reports.py
- applications/collatz/collatz_k_scripts/collatz_iterate_palier_protocol.py
- docs/collatz_run_report_format.md
- docs/features/collatz_run_report_generator.md
- applications/collatz/démonstration collatz.md
- applications/collatz/conjoncture_collatz.md
This commit is contained in:
ncantu 2026-03-09 05:06:03 +01:00
parent 67eb6a5e68
commit 06fd3e920f
7 changed files with 278 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

165
applications/collatz/collatz_k_scripts/collatz_generate_local_h6_run_reports.py Normal file
View File

@ -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<m>/`
- 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_<date>_<scope>.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<m>/")
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()

73
applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
View File

@ -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<n) et agrégats (N*).")
lines.append("")
lines.append("## Code et reproductibilité")
@ -515,6 +517,24 @@ def write_universal_clauses_run_report(
output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
def _extract_universal_clauses_c3_input_path(*, clauses_json_path: Path, repo_root: Path) -> 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,

20
applications/collatz/collatz_k_scripts/collatz_iterate_palier_protocol.py
View File

@ -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<m>.{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)

10
applications/collatz/conjoncture_collatz.md
View File

@ -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<m>.{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`.

12
applications/collatz/démonstration collatz.md
View File

@ -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<m>.{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}\))

11
docs/collatz_run_report_format.md
View File

@ -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

7
docs/features/collatz_run_report_generator.md
View File

@ -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<m>.{json,md}`).
- Pour `c3_local_descent_palier`, le nom de fichier du rapport est déterministe : `docs/collatz_run_report_<date>_c3_local_descent_palier2p<m>.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