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 3705240..31f956f 100644 --- a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py +++ b/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py @@ -132,6 +132,18 @@ class C2ProjectiveMetrics: proj_both15_equals_b12: bool +@dataclass(frozen=True) +class C3LocalDescentMetrics: + palier: int + lifted_domain_size: int + d8_nodes: int + d8_exact_nodes: int + d8_brother_nodes: int + fusion_nodes: int + n_star: int + base_checked_up_to: int + + def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics: obj = read_json(Path(verification_json)) if not isinstance(obj, dict): @@ -172,6 +184,35 @@ def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics: ) +def parse_c3_local_descent_metrics(verification_json: str) -> C3LocalDescentMetrics: + obj = read_json(Path(verification_json)) + if not isinstance(obj, dict): + raise ValueError("Invalid C3 verification JSON: expected object") + + domain = obj.get("domain") + elim = obj.get("elimination") + base = obj.get("base_validation") + if not isinstance(domain, dict) or not isinstance(elim, dict) or not isinstance(base, dict): + raise ValueError("Invalid C3 verification JSON: missing domain/elimination/base_validation blocks") + + def req_int(d: dict, k: str) -> int: + v = d.get(k) + if not isinstance(v, int): + raise ValueError(f"Invalid C3 verification JSON: {k} must be int") + return v + + return C3LocalDescentMetrics( + palier=req_int(domain, "palier"), + lifted_domain_size=req_int(domain, "lifted_domain_size"), + d8_nodes=req_int(elim, "d8_nodes"), + d8_exact_nodes=req_int(elim, "d8_exact_nodes"), + d8_brother_nodes=req_int(elim, "d8_brother_nodes"), + fusion_nodes=req_int(elim, "fusion_nodes"), + n_star=req_int(elim, "N_star"), + base_checked_up_to=req_int(base, "checked_up_to"), + ) + + def write_c2_projective_run_report( *, output_path: Path, @@ -224,6 +265,58 @@ def write_c2_projective_run_report( output_path.write_text("\n".join(lines) + "\n", encoding="utf-8") +def write_c3_local_descent_run_report( + *, + output_path: Path, + report_title: str, + command: str, + git_commit: str, + sha_entries: list[Sha256Entry], + metrics: C3LocalDescentMetrics, + artefacts_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** : vérifier C3 (clôture locale sur Lift(B12) au palier 2^13) 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: candidates = sorted((artefacts_dir / "noyaux").glob("noyau_*_B12.json")) if len(candidates) != 1: @@ -805,6 +898,7 @@ def main() -> None: "local_H6", "local_H6_E1", "c2_projective", + "c3_local_descent", ], help="Report profile", ) @@ -826,6 +920,11 @@ def main() -> None: default="", help="For profile c2_projective: path to deterministic artefacts directory (e.g. docs/artefacts/collatz/c2_projective)", ) + ap.add_argument( + "--c3-artefacts-dir", + default="", + help="For profile c3_local_descent: path to deterministic artefacts directory (e.g. docs/artefacts/collatz/c3_local_descent)", + ) args = ap.parse_args() repo_root = Path(args.repo_root).resolve() if args.repo_root else Path.cwd().resolve() @@ -1078,6 +1177,47 @@ def main() -> None: print(f"Wrote: {output_path}") return + if args.profile == "c3_local_descent": + command = args.command.strip() + if not command: + command = ( + "python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py " + "--profile c3_local_descent --scope c3_local_descent " + "--out-dir applications/collatz/out --docs-dir docs " + "--c3-artefacts-dir docs/artefacts/collatz/c3_local_descent" + ) + + artefacts_dir = ( + Path(args.c3_artefacts_dir).resolve() + if args.c3_artefacts_dir.strip() + else (docs_dir / "artefacts" / "collatz" / "c3_local_descent") + ) + verification_json = artefacts_dir / "verification_c3_local_descent.json" + verification_md = artefacts_dir / "verification_c3_local_descent.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}_{args.scope}.md" + write_c3_local_descent_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, + artefacts_dir=artefacts_dir, + ) + print(f"Wrote: {output_path}") + return + raise ValueError(f"Unknown profile: {args.profile}") diff --git a/applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py b/applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py new file mode 100644 index 0000000..61aa784 --- /dev/null +++ b/applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py @@ -0,0 +1,421 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- +""" +collatz_verify_c3_local_descent.py + +Deterministic verification artefact for the C3 step, starting from the +instrumented C1 (local H6 cover) and C2 (projective reduction). + +Scope of this verifier: +- domain L := Lift_{12->13}(B12) (represented by the versioned local H6 artefacts) +- for each n in L, select a witnessed elimination: + - D8 branch: verify U^8(n) < n (direct check on the representative n) + - Fusion branch: verify the row witnesses a fusion to a strictly smaller preimage m < n, + and that U^t(n) == U(m) (shared suffix) using U_step computations. +- additionally, verify that every reached integer <= max_seen terminates to 1 + under the standard Collatz map (accelerated on odds), so the local descent + proof for representatives is closed unconditionally at this finite bound. + +Inputs: +- docs/artefacts/collatz/local_E*_palier2p13/** (generated by collatz_generate_local_h6_artefacts.py) + +Outputs: +- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json +- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md +""" + +from __future__ import annotations + +import argparse +import csv +import json +import re +from dataclasses import dataclass +from pathlib import Path + +from collatz_k_core import U_step, prefix_data, N0_D, fusion_choice_a, delta_F, Nf_F + + +def _read_json(path: Path) -> object: + return json.loads(path.read_text(encoding="utf-8", errors="strict")) + + +def _discover_state_dirs(root: Path) -> list[Path]: + dirs = sorted([p for p in root.glob("local_E*_palier2p13") if p.is_dir()]) + if not dirs: + raise ValueError(f"No local_E*_palier2p13 directories found under {root}") + return dirs + + +def _load_covered_from_cert(cert_path: Path) -> set[int]: + obj = _read_json(cert_path) + if not isinstance(obj, dict) or "covered" not in obj: + raise ValueError(f"Invalid certificate JSON (missing covered): {cert_path}") + cov = obj["covered"] + if not isinstance(cov, list) or not all(isinstance(x, int) for x in cov): + raise ValueError(f"Invalid certificate JSON covered list: {cert_path}") + return set(cov) + + +@dataclass(frozen=True) +class FusionWitness: + n: int + t: int + a: int + y: int + preimage_m: int + source_csv: str + + +def _parse_int_field(row: dict[str, str], key: str, source: Path) -> int: + if key not in row: + raise ValueError(f"Missing column {key} in {source}") + raw = row[key].strip() + if not raw: + raise ValueError(f"Empty column {key} in {source}") + try: + return int(raw) + except ValueError as e: + raise ValueError(f"Invalid int for {key} in {source}: {raw}") from e + + +def _load_fusion_witnesses(state_dir: Path) -> list[FusionWitness]: + candidats_dir = state_dir / "candidats" + paths = sorted(candidats_dir.glob("candidats_F9to*_E*_palier2p13.csv")) + if not paths: + return [] + + witnesses: list[FusionWitness] = [] + for p in paths: + if p.stat().st_size == 0: + continue + with p.open("r", encoding="utf-8") as f: + r = csv.DictReader(f) + for row in r: + n = _parse_int_field(row, "classe_mod_2^m", p) + t = _parse_int_field(row, "t", p) + a = _parse_int_field(row, "a", p) + y = _parse_int_field(row, "y", p) + m = _parse_int_field(row, "preimage_m", p) + witnesses.append( + FusionWitness(n=n, t=t, a=a, y=y, preimage_m=m, source_csv=str(p)) + ) + return witnesses + + +def _u_iter(n: int, k: int) -> int: + x = n + for _ in range(k): + x, _ = U_step(x) + return x + + +def _collatz_terminates(n: int) -> bool: + x = n + seen = 0 + while x != 1: + if x <= 0: + return False + if x % 2 == 0: + x //= 2 + else: + x, _ = U_step(x) + seen += 1 + if seen > 10_000_000: + return False + return True + + +def _pick_best_witness(witnesses: list[FusionWitness]) -> dict[int, FusionWitness]: + """ + For each n, choose a canonical witness: minimal t, then minimal preimage_m, + then lexical source_csv (for determinism). + """ + out: dict[int, FusionWitness] = {} + for w in witnesses: + prev = out.get(w.n) + if prev is None: + out[w.n] = w + continue + if (w.t, w.preimage_m, w.source_csv) < (prev.t, prev.preimage_m, prev.source_csv): + out[w.n] = w + return out + + +def _infer_state_id(state_dir: Path) -> int: + m = re.search(r"local_E(\d+)_palier2p13", state_dir.name) + if not m: + raise ValueError(f"Cannot infer state id from {state_dir}") + return int(m.group(1)) + + +def run( + *, + artefacts_root: Path, + output_dir: Path, +) -> None: + state_dirs = _discover_state_dirs(artefacts_root) + + # Domain L as union of per-state lifted noyaux + L: set[int] = set() + d8_covered: set[int] = set() + fusion_witnesses_all: list[FusionWitness] = [] + + for sd in state_dirs: + sid = _infer_state_id(sd) + lift_candidates = sorted((sd / "noyaux").glob(f"noyau_Lift_E{sid}_palier2p13.json")) + if len(lift_candidates) != 1: + raise ValueError(f"Expected exactly one lift noyau for {sd}, got {len(lift_candidates)}") + lift_obj = _read_json(lift_candidates[0]) + if not isinstance(lift_obj, dict) or "noyau" not in lift_obj: + raise ValueError(f"Invalid lift noyau JSON: {lift_candidates[0]}") + lift_list = lift_obj["noyau"] + if not isinstance(lift_list, list) or not all(isinstance(x, int) for x in lift_list): + raise ValueError(f"Invalid lift noyau list: {lift_candidates[0]}") + L |= set(lift_list) + + cert_d8 = sd / "certificats" / f"certificat_D8_E{sid}_palier2p13.json" + if cert_d8.exists(): + d8_covered |= _load_covered_from_cert(cert_d8) + + fusion_witnesses_all.extend(_load_fusion_witnesses(sd)) + + if not L: + raise ValueError("Empty domain L") + + fusion_by_n = _pick_best_witness(fusion_witnesses_all) + + d8_nodes = sorted([n for n in L if n in d8_covered]) + f_nodes = sorted([n for n in L if n not in d8_covered]) + + missing_f = [n for n in f_nodes if n not in fusion_by_n] + if missing_f: + raise ValueError(f"Missing fusion witness for {len(missing_f)} residues (e.g. {missing_f[:20]})") + + records: list[dict[str, object]] = [] + next_values: list[int] = [] + thresholds: list[int] = [] + d8_exact_nodes = 0 + d8_brother_nodes = 0 + d8_exact_base_cases = 0 + d8_exact_descent_witnesses = 0 + + shift = 1 << (13 - 1) + d8_exact_set: set[int] = set() + d8_brother_set: set[int] = set() + for n in d8_nodes: + pref = prefix_data(n, 8) + if pref.A == 13: + d8_exact_set.add(n) + else: + d8_brother_set.add(n) + + for n in sorted(L): + if n in d8_covered: + pref = prefix_data(n, 8) + if n in d8_exact_set: + d8_exact_nodes += 1 + N0 = N0_D(pref.C, pref.A, 8) + thresholds.append(N0) + + if n >= N0: + y = pref.y + if y >= n: + raise ValueError(f"D8 descent check failed for n={n}: U^8(n)={y} not < n (N0={N0})") + next_values.append(y) + d8_exact_descent_witnesses += 1 + records.append( + { + "n": n, + "kind": "D_exact", + "k": 8, + "A_k": pref.A, + "C_k": pref.C, + "N0": N0, + "next": y, + "base_case": False, + } + ) + else: + d8_exact_base_cases += 1 + records.append( + { + "n": n, + "kind": "D_exact", + "k": 8, + "A_k": pref.A, + "C_k": pref.C, + "N0": N0, + "next": None, + "base_case": True, + } + ) + else: + d8_brother_nodes += 1 + mate = n ^ shift + if mate not in d8_exact_set: + raise ValueError( + f"D8 brother check failed for n={n}: expected mate={mate} to be an exact D8 candidate (A8=13)" + ) + records.append( + { + "n": n, + "kind": "D_brother", + "k": 8, + "A_k": pref.A, + "C_k": pref.C, + "mate_exact": mate, + } + ) + else: + w = fusion_by_n[n] + pref = prefix_data(n, w.t) + y = pref.y + if y != w.y: + raise ValueError(f"Fusion witness y mismatch for n={n}: computed U^{w.t}(n)={y}, row y={w.y}") + m = w.preimage_m + if m >= n: + raise ValueError(f"Fusion witness preimage not smaller for n={n}: m={m} >= n") + y2, _ = U_step(m) + if y2 != y: + raise ValueError(f"Fusion witness invalid: U(m) != U^t(n) for n={n}: U({m})={y2}, U^{w.t}({n})={y}") + a = fusion_choice_a(y) + if a is None: + raise ValueError(f"Fusion witness invalid: y mod 3 == 0 for n={n}, y={y}") + if a != w.a: + raise ValueError(f"Fusion witness a mismatch for n={n}: computed a={a}, row a={w.a}") + dF = delta_F(pref.A, w.t, a) + if dF <= 0: + raise ValueError(f"Fusion witness invalid: DeltaF<=0 for n={n}: DeltaF={dF}") + Nf = Nf_F(pref.C, pref.A, w.t, a) + thresholds.append(Nf) + if n < Nf: + raise ValueError(f"Fusion witness invalid: n < Nf for n={n}: Nf={Nf}") + records.append( + { + "n": n, + "kind": "F", + "t": w.t, + "a": a, + "y": y, + "preimage_m": m, + "A_t": pref.A, + "C_t": pref.C, + "DeltaF": dF, + "Nf": Nf, + "source_csv": w.source_csv, + "next": m, + } + ) + next_values.append(m) + + max_n = max(L) + max_next = max(next_values) if next_values else 0 + max_seen = max(max_n, max_next) + N_star = max(thresholds) if thresholds else 0 + base_check_up_to = max(max_seen, N_star) + + # Base validation at finite bound + non_terminating: list[int] = [] + for x in range(1, base_check_up_to + 1): + if not _collatz_terminates(x): + non_terminating.append(x) + break + if non_terminating: + raise ValueError(f"Base validation failed at n={non_terminating[0]}") + + summary = { + "inputs": { + "artefacts_root": str(artefacts_root), + "states": len(state_dirs), + }, + "domain": { + "palier": 13, + "lifted_domain_size": len(L), + "min_n": min(L), + "max_n": max_n, + }, + "elimination": { + "d8_nodes": len(d8_nodes), + "d8_exact_nodes": d8_exact_nodes, + "d8_exact_descent_witnesses": d8_exact_descent_witnesses, + "d8_exact_base_cases": d8_exact_base_cases, + "d8_brother_nodes": d8_brother_nodes, + "fusion_nodes": len(f_nodes), + "max_next": max_next, + "N_star": N_star, + }, + "base_validation": { + "checked_up_to": base_check_up_to, + "ok": True, + }, + "records": records, + } + + output_dir.mkdir(parents=True, exist_ok=True) + out_json = output_dir / "verification_c3_local_descent.json" + out_md = output_dir / "verification_c3_local_descent.md" + out_json.write_text(json.dumps(summary, indent=2, ensure_ascii=False) + "\n", encoding="utf-8") + + lines: list[str] = [] + lines.append("**Auteur** : Équipe 4NK") + lines.append("") + lines.append("# Vérification déterministe — C3 (clôture locale par descente/fusion)") + lines.append("") + lines.append("## Entrées") + lines.append("") + lines.append(f"- ARTEFACTS ROOT : `{artefacts_root}`") + lines.append("") + lines.append("## Domaine") + lines.append("") + lines.append(f"- palier : 2^13") + lines.append(f"- |L| (Lift(B12) à 2^13) : {len(L)}") + lines.append(f"- min(L) : {min(L)}, max(L) : {max_n}") + lines.append("") + lines.append("## Élimination (témoins)") + lines.append("") + lines.append( + f"- D8 : {len(d8_nodes)} (exact A8=13 : {d8_exact_nodes}, " + f"descente vérifiée pour n>=N0 : {d8_exact_descent_witnesses}, " + f"cas de base n None: + ap = argparse.ArgumentParser(description="Deterministic C3 verification from local H6 artefacts (palier 2^13)") + ap.add_argument( + "--local-h6-root", + default="docs/artefacts/collatz", + help="Root directory containing local_E*_palier2p13 directories", + ) + ap.add_argument( + "--output-dir", + default="docs/artefacts/collatz/c3_local_descent", + help="Output directory for deterministic artefacts (JSON + MD)", + ) + args = ap.parse_args() + run( + artefacts_root=Path(args.local_h6_root), + output_dir=Path(args.output_dir), + ) + + +if __name__ == "__main__": + main() + 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 e87a13b..68be969 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 @@ -261,6 +261,23 @@ Lemme C3 (impossibilité d’orbite infinie sous contraintes). Sous un paquet explicite de contraintes arithmétiques \(P\) (congruences, bornes sur sommes de valuations sur des horizons, contraintes modulo \(3^k\), etc.) extraites comme invariants des survivants, aucune orbite de la dynamique accélérée \(U\) ne peut être infinie. Objectif : fournir une mesure de rang ou une contradiction directe stable sous \(U\) sur le sous-ensemble défini par \(P\). +### Instance instrumentée (palier \(2^{13}\), domaine Lift(\(B_{12}\))) + +On pose \(L=\mathrm{Lift}_{12\to 13}(B_{12})\subset(\mathbb{Z}/2^{13}\mathbb{Z})^\times\). +Une instance vérifiable de C3 consiste à exhiber, pour chaque \(n\in L\), un témoin d’élimination de type : + +- **fusion** : un entier impair \(m0\)) et fournit un seuil \(N_0\) ; pour \(n\ge N_0\), on a \(U^{(k)}(n)=N0 : 27, cas de base n