Collatz: certify H6(E1) and add run report profiles
**Motivations:** - Certify local completeness H6(E1) via explicit covered-union on lifts - Support additional run-report scopes (D16/D17 pipeline, fusion 2^25) **Root causes:** - H6(E1) needed a concrete certified artefact set to be citable - Report generator profiles were too limited for other paliers outputs **Correctifs:** - Produce local certificates for E1 lifts and verify covered union equals L **Evolutions:** - Add generator profiles: pipeline_d16_d17, fusion_palier2p25 - Document usage in docs/ and docs/features/ **Pages affectées:** - applications/collatz/out/local_E1_palier2p13/noyaux/noyau_E1_B12.json - applications/collatz/out/local_E1_palier2p13/noyaux/noyau_post_D8_E1_palier2p13.json - applications/collatz/out/local_E1_palier2p13/noyaux/noyau_missing_after_D8_F9to12.json - applications/collatz/out/local_E1_palier2p13/candidats/candidats_D8_E1_palier2p13.csv - applications/collatz/out/local_E1_palier2p13/candidats/candidats_F9to12_E1_palier2p13.csv - applications/collatz/out/local_E1_palier2p13/candidats/candidats_F13to20_E1_palier2p13.csv - applications/collatz/out/local_E1_palier2p13/candidats/candidats_F9to40_E1_palier2p13.csv - applications/collatz/out/local_E1_palier2p13/certificats/certificat_D8_E1_palier2p13.json - applications/collatz/out/local_E1_palier2p13/certificats/certificat_F9to12_E1_palier2p13.json - applications/collatz/out/local_E1_palier2p13/certificats/certificat_F13to20_E1_palier2p13.json - applications/collatz/out/local_E1_palier2p13/certificats/certificat_F9to40_E1_palier2p13.json - applications/collatz/out/local_E1_palier2p13/audits/verification_H6_E1_palier2p13.md - applications/collatz/collatz_k_scripts/collatz_generate_run_report.py - docs/collatz_run_report_format.md - docs/features/collatz_run_report_generator.md
This commit is contained in:
ncantu
parent
f8f71e7cbe
commit
9d702cd1d3
@ -87,6 +87,21 @@ class Section7Metrics:
|
||||
max_modulus_coverage_pct: float
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class D16D17Metrics:
|
||||
d16_candidates: int
|
||||
d16_cover: int
|
||||
d16_maxA_after: int
|
||||
d17_pairs: int
|
||||
noyau_post_d17_size: int
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class Fusion25Metrics:
|
||||
t_to_valid_clauses: dict[int, int]
|
||||
t_to_domain_size: dict[int, int]
|
||||
|
||||
|
||||
def parse_extend_metrics_from_logs(pipeline_extend_log: str, paliers_finale_log: str) -> ExtendMetrics:
|
||||
"""
|
||||
Extract metrics needed for the report.
|
||||
@ -160,6 +175,73 @@ def parse_section7_metrics(seuil_global_md: str, coverage_md: str) -> Section7Me
|
||||
return Section7Metrics(nstar=nstar, max_modulus_power=max_power, max_modulus_coverage_pct=max_cov)
|
||||
|
||||
|
||||
def _parse_int_after_colon(line: str) -> int | None:
|
||||
m = re.search(r":\s*([0-9][0-9_]*)\b", line)
|
||||
if not m:
|
||||
return None
|
||||
return int(m.group(1).replace("_", ""))
|
||||
|
||||
|
||||
def parse_d16_d17_metrics(d16_impact_md: str, d17_impact_md: str, noyau_post_d17_json: str) -> D16D17Metrics:
|
||||
d16_candidates = None
|
||||
d16_cover = None
|
||||
d16_maxA_after = None
|
||||
for line in d16_impact_md.splitlines():
|
||||
if "candidats D16" in line:
|
||||
d16_candidates = _parse_int_after_colon(line)
|
||||
if "couverture (avec sœurs)" in line:
|
||||
d16_cover = _parse_int_after_colon(line)
|
||||
if "invariant max A16 après" in line:
|
||||
d16_maxA_after = _parse_int_after_colon(line)
|
||||
if d16_candidates is None or d16_cover is None or d16_maxA_after is None:
|
||||
raise ValueError("Cannot parse D16 metrics from impact md")
|
||||
|
||||
d17_pairs = None
|
||||
for line in d17_impact_md.splitlines():
|
||||
if "paires candidates D17" in line:
|
||||
d17_pairs = _parse_int_after_colon(line)
|
||||
if d17_pairs is None:
|
||||
raise ValueError("Cannot parse D17 metrics from impact md")
|
||||
|
||||
data = read_text(Path(noyau_post_d17_json))
|
||||
j = re.search(r'"noyau"\s*:\s*\[', data)
|
||||
if not j:
|
||||
raise ValueError("Cannot locate noyau list in noyau_post_D17.json")
|
||||
# The file is JSON with {"noyau":[...], "palier": 28}. To avoid loading huge data,
|
||||
# count commas in the noyau array region with a bounded approach (file is ~30MB).
|
||||
# We do a lightweight parse by counting numbers.
|
||||
import json as _json
|
||||
|
||||
obj = _json.loads(data)
|
||||
noyau_post_d17_size = len(obj.get("noyau", []))
|
||||
|
||||
return D16D17Metrics(
|
||||
d16_candidates=d16_candidates,
|
||||
d16_cover=d16_cover,
|
||||
d16_maxA_after=d16_maxA_after,
|
||||
d17_pairs=d17_pairs,
|
||||
noyau_post_d17_size=noyau_post_d17_size,
|
||||
)
|
||||
|
||||
|
||||
def parse_fusion25_metrics(md_text_by_t: dict[int, str]) -> Fusion25Metrics:
|
||||
t_to_valid: dict[int, int] = {}
|
||||
t_to_domain: dict[int, int] = {}
|
||||
for t, text in md_text_by_t.items():
|
||||
domain = None
|
||||
valid = None
|
||||
for line in text.splitlines():
|
||||
if "Taille du domaine analysé" in line:
|
||||
domain = _parse_int_after_colon(line)
|
||||
if "Clauses valides" in line:
|
||||
valid = _parse_int_after_colon(line)
|
||||
if domain is None or valid is None:
|
||||
raise ValueError(f"Cannot parse fusion metrics from md for t={t}")
|
||||
t_to_domain[t] = domain
|
||||
t_to_valid[t] = valid
|
||||
return Fusion25Metrics(t_to_valid_clauses=t_to_valid, t_to_domain_size=t_to_domain)
|
||||
|
||||
|
||||
def parse_running_command_from_paliers_finale_log(paliers_finale_log: str) -> str:
|
||||
"""
|
||||
Extract the last 'Running: ...' command from paliers_finale.log.
|
||||
@ -307,6 +389,104 @@ def write_section7_run_report(
|
||||
output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
|
||||
|
||||
|
||||
def write_d16_d17_run_report(
|
||||
*,
|
||||
output_path: Path,
|
||||
report_title: str,
|
||||
command: str,
|
||||
git_commit: str,
|
||||
sha_entries: list[Sha256Entry],
|
||||
metrics: D16D17Metrics,
|
||||
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 le pipeline D16/D17 après fusion (sections “pipeline directe”).")
|
||||
lines.append("- **Assertion ciblée** : produire les CSV D16/D17 et le noyau résiduel `noyau_post_D17.json`.")
|
||||
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"- candidats D16 : {metrics.d16_candidates}")
|
||||
lines.append(f"- couverture D16 (avec sœurs) : {metrics.d16_cover}")
|
||||
lines.append(f"- max A16 après : {metrics.d16_maxA_after}")
|
||||
lines.append(f"- paires candidates D17 : {metrics.d17_pairs}")
|
||||
lines.append(f"- noyau post-D17 (résidus) : {metrics.noyau_post_d17_size}")
|
||||
lines.append("")
|
||||
lines.append("## Chemins d’artefacts")
|
||||
lines.append("")
|
||||
lines.append(f"- OUT : `{out_dir}`")
|
||||
lines.append("")
|
||||
output_path.parent.mkdir(parents=True, exist_ok=True)
|
||||
output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
|
||||
|
||||
|
||||
def write_fusion25_run_report(
|
||||
*,
|
||||
output_path: Path,
|
||||
report_title: str,
|
||||
command: str,
|
||||
git_commit: str,
|
||||
sha_entries: list[Sha256Entry],
|
||||
metrics: Fusion25Metrics,
|
||||
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** : produire des clauses de fusion F(t) au palier \\(2^{25}\\) (t=11,12,14).")
|
||||
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("")
|
||||
for t in sorted(metrics.t_to_valid_clauses.keys()):
|
||||
lines.append(f"- t={t} : domaine={metrics.t_to_domain_size[t]}, clauses_valides={metrics.t_to_valid_clauses[t]}")
|
||||
lines.append("")
|
||||
lines.append("## Chemins d’artefacts")
|
||||
lines.append("")
|
||||
lines.append(f"- OUT : `{out_dir}`")
|
||||
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:
|
||||
@ -323,7 +503,7 @@ def main() -> None:
|
||||
ap.add_argument(
|
||||
"--profile",
|
||||
default="extend_finale",
|
||||
choices=["extend_finale", "validation_section7"],
|
||||
choices=["extend_finale", "validation_section7", "pipeline_d16_d17", "fusion_palier2p25"],
|
||||
help="Report profile",
|
||||
)
|
||||
ap.add_argument("--pipeline-extend-log", default=None, help="Path to pipeline_extend.log (defaults to OUT/pipeline_extend.log)")
|
||||
@ -423,6 +603,79 @@ def main() -> None:
|
||||
print(f"Wrote: {output_path}")
|
||||
return
|
||||
|
||||
if args.profile == "pipeline_d16_d17":
|
||||
command = args.command.strip() if args.command.strip() else "cd applications/collatz && ./scripts/02-run-pipeline.sh"
|
||||
d16_impact_path = out_dir / "candidats_D16_apres_fusion_palier2p27_et_impact.md"
|
||||
d17_impact_path = out_dir / "candidats_D17_apres_fusion_palier2p28_et_impact.md"
|
||||
noyau_post_d17_path = out_dir / "noyaux" / "noyau_post_D17.json"
|
||||
metrics = parse_d16_d17_metrics(
|
||||
read_text(d16_impact_path),
|
||||
read_text(d17_impact_path),
|
||||
str(noyau_post_d17_path),
|
||||
)
|
||||
date_str = pick_report_date_from_mtime([d16_impact_path, d17_impact_path, noyau_post_d17_path])
|
||||
sha_paths: list[Path] = [
|
||||
repo_root / "applications" / "collatz" / "scripts" / "02-run-pipeline.sh",
|
||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "reproduce_all_audits.py",
|
||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_k_pipeline.py",
|
||||
d16_impact_path,
|
||||
d17_impact_path,
|
||||
out_dir / "candidats_D16_apres_fusion_palier2p27.csv",
|
||||
out_dir / "candidats_D17_apres_fusion_palier2p28.csv",
|
||||
noyau_post_d17_path,
|
||||
]
|
||||
sha_entries = compute_sha256_entries(sha_paths)
|
||||
output_path = docs_dir / f"collatz_run_report_{date_str}_{args.scope}.md"
|
||||
write_d16_d17_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 == "fusion_palier2p25":
|
||||
command = args.command.strip() if args.command.strip() else "cd applications/collatz && ./scripts/02-run-pipeline.sh"
|
||||
md_by_t = {
|
||||
11: read_text(out_dir / "fusion_t11_palier2p25.md"),
|
||||
12: read_text(out_dir / "fusion_t12_palier2p25.md"),
|
||||
14: read_text(out_dir / "fusion_t14_palier2p25.md"),
|
||||
}
|
||||
metrics = parse_fusion25_metrics(md_by_t)
|
||||
paths_for_date = [
|
||||
out_dir / "fusion_t11_palier2p25.md",
|
||||
out_dir / "fusion_t12_palier2p25.md",
|
||||
out_dir / "fusion_t14_palier2p25.md",
|
||||
]
|
||||
date_str = pick_report_date_from_mtime(paths_for_date)
|
||||
sha_paths: list[Path] = [
|
||||
repo_root / "applications" / "collatz" / "scripts" / "02-run-pipeline.sh",
|
||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_k_pipeline.py",
|
||||
out_dir / "fusion_t11_palier2p25.md",
|
||||
out_dir / "fusion_t11_palier2p25.csv",
|
||||
out_dir / "fusion_t12_palier2p25.md",
|
||||
out_dir / "fusion_t12_palier2p25.csv",
|
||||
out_dir / "fusion_t14_palier2p25.md",
|
||||
out_dir / "fusion_t14_palier2p25.csv",
|
||||
]
|
||||
sha_entries = compute_sha256_entries(sha_paths)
|
||||
output_path = docs_dir / f"collatz_run_report_{date_str}_{args.scope}.md"
|
||||
write_fusion25_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}")
|
||||
|
||||
|
||||
|
||||
@ -37,6 +37,26 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
|
||||
--docs-dir docs
|
||||
```
|
||||
|
||||
Pour le pipeline D16/D17 après fusion :
|
||||
|
||||
```bash
|
||||
python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
|
||||
--profile pipeline_d16_d17 \
|
||||
--scope pipeline_d16_d17 \
|
||||
--out-dir applications/collatz/out \
|
||||
--docs-dir docs
|
||||
```
|
||||
|
||||
Pour les fusions au palier \(2^{25}\) (t=11,12,14) :
|
||||
|
||||
```bash
|
||||
python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
|
||||
--profile fusion_palier2p25 \
|
||||
--scope fusion_palier2p25 \
|
||||
--out-dir applications/collatz/out \
|
||||
--docs-dir docs
|
||||
```
|
||||
|
||||
### Contexte
|
||||
|
||||
- **But du run** : (énoncé court)
|
||||
|
||||
@ -23,6 +23,7 @@ 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`.
|
||||
|
||||
## Modalités d’analyse
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user