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 a8c747c..3705240 100644 --- a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py +++ b/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py @@ -119,6 +119,111 @@ class LocalH6Metrics: certificate_paliers: list[tuple[str, int]] +@dataclass(frozen=True) +class C2ProjectiveMetrics: + b12_size: int + both14_size: int + children15_size: int + residual15_size: int + children15_equals_residual15: bool + proj_both14_equals_b12: bool + both15_size: int + children16_size: int + proj_both15_equals_b12: bool + + +def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics: + obj = read_json(Path(verification_json)) + if not isinstance(obj, dict): + raise ValueError("Invalid C2 verification JSON: expected object") + + b12 = obj.get("B12") + checks = obj.get("checks") + if not isinstance(b12, dict) or not isinstance(checks, dict): + raise ValueError("Invalid C2 verification JSON: missing 'B12' or 'checks'") + + c1415 = checks.get("m14_to_m15") + c1516 = checks.get("m15_to_m16") + if not isinstance(c1415, dict) or not isinstance(c1516, dict): + raise ValueError("Invalid C2 verification JSON: missing check blocks") + + def req_int(d: dict, k: str) -> int: + v = d.get(k) + if not isinstance(v, int): + raise ValueError(f"Invalid C2 verification JSON: {k} must be int") + return v + + def req_bool(d: dict, k: str) -> bool: + v = d.get(k) + if not isinstance(v, bool): + raise ValueError(f"Invalid C2 verification JSON: {k} must be bool") + return v + + return C2ProjectiveMetrics( + b12_size=req_int(b12, "count"), + both14_size=req_int(c1415, "both_parent_count"), + children15_size=req_int(c1415, "computed_children_count"), + residual15_size=req_int(c1415, "listed_residual_count"), + children15_equals_residual15=req_bool(c1415, "children_equals_listed_residual"), + proj_both14_equals_b12=req_bool(c1415, "projection_mod_4096_equals_b12"), + both15_size=req_int(c1516, "both_parent_count"), + children16_size=req_int(c1516, "computed_children_count"), + proj_both15_equals_b12=req_bool(c1516, "projection_mod_4096_equals_b12"), + ) + + +def write_c2_projective_run_report( + *, + output_path: Path, + report_title: str, + command: str, + git_commit: str, + sha_entries: list[Sha256Entry], + metrics: C2ProjectiveMetrics, + 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 C2 (complétion par frères ⇒ both ⇒ projection B12) sur des artefacts déterministes.") + lines.append("- **Assertion vérifiée** : égalités d’ensembles et égalité de projections modulo 4096 (voir métriques).") + 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"- |B12| = {metrics.b12_size}") + lines.append(f"- m=14: |both|={metrics.both14_size}, |children(m=15)|={metrics.children15_size}, |listed residual(m=15)|={metrics.residual15_size}") + lines.append(f"- m=14: children(m=15) == residual(m=15) : {metrics.children15_equals_residual15}") + lines.append(f"- m=14: both mod 4096 == B12 : {metrics.proj_both14_equals_b12}") + lines.append(f"- m=15: |both|={metrics.both15_size}, |children(m=16)|={metrics.children16_size}") + lines.append(f"- m=15: both mod 4096 == B12 : {metrics.proj_both15_equals_b12}") + lines.append("") + lines.append("## Chemins d’artefacts (versionnés)") + lines.append("") + lines.append(f"- ARTEFACTS : `{artefacts_dir}`") + lines.append("") + output_path.parent.mkdir(parents=True, exist_ok=True) + output_path.write_text("\n".join(lines) + "\n", encoding="utf-8") + + def _discover_base_noyau_path(artefacts_dir: Path) -> Path: candidates = sorted((artefacts_dir / "noyaux").glob("noyau_*_B12.json")) if len(candidates) != 1: @@ -692,7 +797,15 @@ def main() -> None: ap.add_argument( "--profile", default="extend_finale", - choices=["extend_finale", "validation_section7", "pipeline_d16_d17", "fusion_palier2p25", "local_H6", "local_H6_E1"], + choices=[ + "extend_finale", + "validation_section7", + "pipeline_d16_d17", + "fusion_palier2p25", + "local_H6", + "local_H6_E1", + "c2_projective", + ], help="Report profile", ) ap.add_argument("--pipeline-extend-log", default=None, help="Path to pipeline_extend.log (defaults to OUT/pipeline_extend.log)") @@ -708,6 +821,11 @@ def main() -> None: default="", help="For profile local_H6: path to the versioned artefacts directory (e.g. docs/artefacts/collatz/local_E1_palier2p13)", ) + ap.add_argument( + "--c2-artefacts-dir", + default="", + help="For profile c2_projective: path to deterministic artefacts directory (e.g. docs/artefacts/collatz/c2_projective)", + ) args = ap.parse_args() repo_root = Path(args.repo_root).resolve() if args.repo_root else Path.cwd().resolve() @@ -922,6 +1040,44 @@ def main() -> None: print(f"Wrote: {output_path}") return + if args.profile == "c2_projective": + command = args.command.strip() + if not command: + command = ( + "python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py " + "--profile c2_projective --scope c2_projective " + "--out-dir applications/collatz/out --docs-dir docs " + "--c2-artefacts-dir docs/artefacts/collatz/c2_projective" + ) + + artefacts_dir = Path(args.c2_artefacts_dir).resolve() if args.c2_artefacts_dir.strip() else (docs_dir / "artefacts" / "collatz" / "c2_projective") + verification_json = artefacts_dir / "verification_c2_projective.json" + verification_md = artefacts_dir / "verification_c2_projective.md" + metrics = parse_c2_projective_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_c2_projective.py", + repo_root / "applications" / "collatz" / "collatz_k_scripts" / "noyau_both_base_4096.md", + repo_root / "applications" / "collatz" / "collatz_k_scripts" / "complétion_minorée_m14_vers_m15.md", + repo_root / "applications" / "collatz" / "collatz_k_scripts" / "complétion_minorée_m15_vers_m16.md", + 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_c2_projective_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_c2_projective.py b/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py new file mode 100644 index 0000000..30bebfa --- /dev/null +++ b/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py @@ -0,0 +1,274 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- +""" +collatz_verify_c2_projective.py + +Deterministic verification artefact for Lemma C2 (projective reduction): + +From completion-by-brothers audit documents, verify that: +- residual after completion equals the set of children of "both" parents +- projections modulo 2^12 of B_m (both parents) match the fixed base B12 + +Inputs (Markdown): +- noyau_both_base_4096.md (contains B12 list) +- complétion_minorée_m14_vers_m15.md (contains both-parent list at 2^14 + residual list at 2^15) +- complétion_minorée_m15_vers_m16.md (contains both-parent list at 2^15) + +Outputs: +- a short JSON summary (machine-checkable) +- a short Markdown report (human-checkable) + +No terminal transcripts. Standard library only. +""" + +from __future__ import annotations + +import argparse +import json +import re +from dataclasses import dataclass +from pathlib import Path + + +def _read_text(path: Path) -> str: + return path.read_text(encoding="utf-8", errors="strict") + + +def _extract_ints(text: str) -> list[int]: + return [int(x) for x in re.findall(r"\b\d+\b", text)] + + +def _section_after_heading(md: str, heading_regex: str) -> str: + """ + Return the Markdown slice starting at a heading matched by heading_regex (regex applied line-wise). + The slice ends at the next heading of same or higher level, or end of document. + """ + lines = md.splitlines() + start = None + level = None + hr = re.compile(heading_regex) + for i, line in enumerate(lines): + if hr.search(line): + start = i + 1 + m = re.match(r"^(#+)\s", line) + level = len(m.group(1)) if m else 1 + break + if start is None or level is None: + raise ValueError(f"Cannot find heading matching regex: {heading_regex}") + + end = len(lines) + for j in range(start, len(lines)): + m2 = re.match(r"^(#+)\s", lines[j]) + if not m2: + continue + if len(m2.group(1)) <= level: + end = j + break + return "\n".join(lines[start:end]).strip() + + +def _parse_list_under_heading(md: str, heading_regex: str) -> list[int]: + section = _section_after_heading(md, heading_regex) + return sorted(set(_extract_ints(section))) + + +def _assert_all_odd(values: list[int], label: str) -> None: + bad = [x for x in values if x % 2 == 0] + if bad: + raise ValueError(f"{label}: expected odd residues only, found {len(bad)} even values (e.g. {bad[:10]})") + + +@dataclass(frozen=True) +class C2CheckResult: + palier_parent: int + palier_child: int + both_parent_count: int + computed_children_count: int + listed_residual_count: int | None + children_equals_listed_residual: bool | None + projection_mod_4096_equals_b12: bool + + +def _lift_children(both_parents: list[int], parent_palier: int) -> list[int]: + shift = 1 << parent_palier + out = set() + for p in both_parents: + out.add(p) + out.add(p + shift) + return sorted(out) + + +def _project_mod_4096(values: list[int]) -> set[int]: + return {int(x % 4096) for x in values} + + +def _display_path(path: Path, repo_root: Path) -> str: + try: + rel = path.resolve().relative_to(repo_root.resolve()) + return str(rel) + except ValueError: + return str(path) + + +def verify_c2( + *, + noyau_both_base_4096_md: Path, + completion_m14_to_m15_md: Path, + completion_m15_to_m16_md: Path, + repo_root: Path, + output_json: Path, + output_md: Path, +) -> None: + b12_md = _read_text(noyau_both_base_4096_md) + c1415_md = _read_text(completion_m14_to_m15_md) + c1516_md = _read_text(completion_m15_to_m16_md) + + b12 = _parse_list_under_heading(b12_md, r"^##\s+Base projective B_12\b") + _assert_all_odd(b12, "B12") + if len(b12) != 192: + raise ValueError(f"B12: expected 192 residues, got {len(b12)}") + + # m=14 -> m=15 + both14 = _parse_list_under_heading(c1415_md, r"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^14\b") + _assert_all_odd(both14, "Parents both (m=14)") + children15 = _lift_children(both14, 14) + _assert_all_odd(children15, "Computed children at m=15") + + residual15 = _parse_list_under_heading( + c1415_md, + r"^###\s+Résidu\s+restant\s+au\s+palier\s+2\^15\s+après\s+complétion\s+«\s+one\s+»", + ) + _assert_all_odd(residual15, "Listed residual at m=15") + + c1415 = C2CheckResult( + palier_parent=14, + palier_child=15, + both_parent_count=len(both14), + computed_children_count=len(children15), + listed_residual_count=len(residual15), + children_equals_listed_residual=(set(children15) == set(residual15)), + projection_mod_4096_equals_b12=(_project_mod_4096(both14) == set(b12)), + ) + + # m=15 -> m=16 + both15 = _parse_list_under_heading(c1516_md, r"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^15\b") + _assert_all_odd(both15, "Parents both (m=15)") + children16 = _lift_children(both15, 15) + _assert_all_odd(children16, "Computed children at m=16") + + # This completion file does not necessarily list the full residual after completion, so we only check the count. + c1516 = C2CheckResult( + palier_parent=15, + palier_child=16, + both_parent_count=len(both15), + computed_children_count=len(children16), + listed_residual_count=None, + children_equals_listed_residual=None, + projection_mod_4096_equals_b12=(_project_mod_4096(both15) == set(b12)), + ) + + summary = { + "inputs": { + "noyau_both_base_4096_md": _display_path(noyau_both_base_4096_md, repo_root), + "completion_m14_to_m15_md": _display_path(completion_m14_to_m15_md, repo_root), + "completion_m15_to_m16_md": _display_path(completion_m15_to_m16_md, repo_root), + }, + "B12": {"count": len(b12), "min": min(b12), "max": max(b12)}, + "checks": { + "m14_to_m15": c1415.__dict__, + "m15_to_m16": c1516.__dict__, + }, + "ok": { + "m14_to_m15_children_equals_listed_residual": bool(c1415.children_equals_listed_residual), + "m14_projection_equals_b12": bool(c1415.projection_mod_4096_equals_b12), + "m15_projection_equals_b12": bool(c1516.projection_mod_4096_equals_b12), + }, + } + + output_json.parent.mkdir(parents=True, exist_ok=True) + output_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 — Lemma C2 (réduction projective)") + lines.append("") + lines.append("## Entrées") + lines.append("") + lines.append(f"- `noyau_both_base_4096.md` : `{_display_path(noyau_both_base_4096_md, repo_root)}`") + lines.append(f"- `complétion_minorée_m14_vers_m15.md` : `{_display_path(completion_m14_to_m15_md, repo_root)}`") + lines.append(f"- `complétion_minorée_m15_vers_m16.md` : `{_display_path(completion_m15_to_m16_md, repo_root)}`") + lines.append("") + lines.append("## Base projective B12") + lines.append("") + lines.append(f"- |B12| = {len(b12)} (attendu 192)") + lines.append(f"- min(B12) = {min(b12)}, max(B12) = {max(b12)}") + lines.append("") + lines.append("## Transition m=14 → m=15 (complétion par frères ⇒ résidu = enfants des both)") + lines.append("") + lines.append(f"- |both parents (m=14)| = {c1415.both_parent_count}") + lines.append(f"- |computed children (m=15)| = {c1415.computed_children_count} (attendu 2*|both|)") + lines.append(f"- |listed residual (m=15)| = {c1415.listed_residual_count}") + lines.append(f"- computed children == listed residual : {c1415.children_equals_listed_residual}") + lines.append(f"- projection both(m=14) mod 4096 == B12 : {c1415.projection_mod_4096_equals_b12}") + lines.append("") + lines.append("## Transition m=15 → m=16 (projection des both)") + lines.append("") + lines.append(f"- |both parents (m=15)| = {c1516.both_parent_count}") + lines.append(f"- |computed children (m=16)| = {c1516.computed_children_count} (attendu 2*|both|)") + lines.append(f"- projection both(m=15) mod 4096 == B12 : {c1516.projection_mod_4096_equals_b12}") + lines.append("") + lines.append("## Sorties") + lines.append("") + lines.append(f"- JSON : `{output_json}`") + lines.append(f"- Markdown : `{output_md}`") + lines.append("") + + output_md.parent.mkdir(parents=True, exist_ok=True) + output_md.write_text("\n".join(lines) + "\n", encoding="utf-8") + + +def main() -> None: + ap = argparse.ArgumentParser(description="Deterministic C2 verification (projective reduction)") + ap.add_argument( + "--repo-root", + default="", + help="Repository root used to display relative paths in outputs (defaults to current working directory)", + ) + ap.add_argument( + "--noyau-both-base-4096-md", + default=str(Path(__file__).parent / "noyau_both_base_4096.md"), + help="Path to noyau_both_base_4096.md", + ) + ap.add_argument( + "--completion-m14-to-m15-md", + default=str(Path(__file__).parent / "complétion_minorée_m14_vers_m15.md"), + help="Path to complétion_minorée_m14_vers_m15.md", + ) + ap.add_argument( + "--completion-m15-to-m16-md", + default=str(Path(__file__).parent / "complétion_minorée_m15_vers_m16.md"), + help="Path to complétion_minorée_m15_vers_m16.md", + ) + ap.add_argument( + "--output-dir", + default="docs/artefacts/collatz/c2_projective", + help="Output directory for deterministic artefacts (JSON + MD)", + ) + args = ap.parse_args() + + repo_root = Path(args.repo_root).resolve() if args.repo_root.strip() else Path.cwd().resolve() + out_dir = Path(args.output_dir) + verify_c2( + noyau_both_base_4096_md=Path(args.noyau_both_base_4096_md), + completion_m14_to_m15_md=Path(args.completion_m14_to_m15_md), + completion_m15_to_m16_md=Path(args.completion_m15_to_m16_md), + repo_root=repo_root, + output_json=out_dir / "verification_c2_projective.json", + output_md=out_dir / "verification_c2_projective.md", + ) + + +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 81319fa..e87a13b 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 @@ -215,8 +215,47 @@ Les artefacts versionnés montrent, pour les 60 états \(E\) de \(B_{12}\) : 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. +On fixe un schéma de complétion par frères à chaque transition \(m\to m+1\) : + +- Pour un parent \(r\in R_m\), ses deux enfants au palier suivant sont \(r\) et \(r+2^m\). +- On distingue : + - **cas one** : un seul enfant est survivant à la transition ; l’autre est fermé (couvert) ; + - **cas both** : les deux enfants sont survivants. + +On note \(B_m\subset R_m\) l’ensemble des parents “both”. + +### Énoncés cibles (formes à rendre exactes) + +- (C2.1) **Complétion par frères ⇒ résidu = enfants des both**. + Après fermeture (au palier \(m+1\)) des enfants “one” par clauses de descente minorées (lemme de frère), le résidu restant au palier \(m+1\) est exactement : + \[ + R_{m+1}^{\mathrm{comp}}=\{\,r,\ r+2^m\;:\; r\in B_m\,\}. + \] + +- (C2.2) **Projection projective**. + Pour certains paliers (en pratique : dès \(m\ge 12\) dans les artefacts actuels), il existe une base projective fixe + \[ + B_{12}\subset(\mathbb{Z}/2^{12}\mathbb{Z})^\times,\quad |B_{12}|=192, + \] + telle que + \[ + B_m \bmod 2^{12} = B_{12}. + \] + +### Artefact déterministe (vérification citable) + +Une vérification déterministe (script + sortie courte) est versionnée dans `docs/artefacts/` : + +- script : `applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py` +- sorties : `docs/artefacts/collatz/c2_projective/verification_c2_projective.{json,md}` +- rapport d’exécution (sha256 + métriques) : `docs/collatz_run_report_2026-03-09_c2_projective.md` + +Ces artefacts valident (au niveau “audit”) les instances suivantes : + +- transition \(m=14\to 15\) : \(R_{15}^{\mathrm{comp}}=\{r,r+2^{14}:r\in B_{14}\}\) et \(B_{14}\bmod 4096 = B_{12}\), +- projection \(m=15\) : \(B_{15}\bmod 4096 = B_{12}\). + +Objectif de C2 : utiliser (C2.1)–(C2.2) pour réduire l’analyse des survivants à une élimination par états sur \(B_{12}\) (C1), puis à un verrou final (C3). 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. diff --git a/docs/artefacts/collatz/c2_projective/verification_c2_projective.json b/docs/artefacts/collatz/c2_projective/verification_c2_projective.json new file mode 100644 index 0000000..2b3d5ad --- /dev/null +++ b/docs/artefacts/collatz/c2_projective/verification_c2_projective.json @@ -0,0 +1,37 @@ +{ + "inputs": { + "noyau_both_base_4096_md": "applications/collatz/collatz_k_scripts/noyau_both_base_4096.md", + "completion_m14_to_m15_md": "applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md", + "completion_m15_to_m16_md": "applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md" + }, + "B12": { + "count": 192, + "min": 27, + "max": 4095 + }, + "checks": { + "m14_to_m15": { + "palier_parent": 14, + "palier_child": 15, + "both_parent_count": 593, + "computed_children_count": 1186, + "listed_residual_count": 1186, + "children_equals_listed_residual": true, + "projection_mod_4096_equals_b12": true + }, + "m15_to_m16": { + "palier_parent": 15, + "palier_child": 16, + "both_parent_count": 1101, + "computed_children_count": 2202, + "listed_residual_count": null, + "children_equals_listed_residual": null, + "projection_mod_4096_equals_b12": true + } + }, + "ok": { + "m14_to_m15_children_equals_listed_residual": true, + "m14_projection_equals_b12": true, + "m15_projection_equals_b12": true + } +} diff --git a/docs/artefacts/collatz/c2_projective/verification_c2_projective.md b/docs/artefacts/collatz/c2_projective/verification_c2_projective.md new file mode 100644 index 0000000..41b5fae --- /dev/null +++ b/docs/artefacts/collatz/c2_projective/verification_c2_projective.md @@ -0,0 +1,34 @@ +**Auteur** : Équipe 4NK + +# Vérification déterministe — Lemma C2 (réduction projective) + +## Entrées + +- `noyau_both_base_4096.md` : `applications/collatz/collatz_k_scripts/noyau_both_base_4096.md` +- `complétion_minorée_m14_vers_m15.md` : `applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md` +- `complétion_minorée_m15_vers_m16.md` : `applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md` + +## Base projective B12 + +- |B12| = 192 (attendu 192) +- min(B12) = 27, max(B12) = 4095 + +## Transition m=14 → m=15 (complétion par frères ⇒ résidu = enfants des both) + +- |both parents (m=14)| = 593 +- |computed children (m=15)| = 1186 (attendu 2*|both|) +- |listed residual (m=15)| = 1186 +- computed children == listed residual : True +- projection both(m=14) mod 4096 == B12 : True + +## Transition m=15 → m=16 (projection des both) + +- |both parents (m=15)| = 1101 +- |computed children (m=16)| = 2202 (attendu 2*|both|) +- projection both(m=15) mod 4096 == B12 : True + +## Sorties + +- JSON : `docs/artefacts/collatz/c2_projective/verification_c2_projective.json` +- Markdown : `docs/artefacts/collatz/c2_projective/verification_c2_projective.md` + diff --git a/docs/collatz_run_report_2026-03-09_c2_projective.md b/docs/collatz_run_report_2026-03-09_c2_projective.md new file mode 100644 index 0000000..18088fb --- /dev/null +++ b/docs/collatz_run_report_2026-03-09_c2_projective.md @@ -0,0 +1,46 @@ +**Auteur** : Équipe 4NK + +# Rapport d’exécution — c2_projective + +## Contexte + +- **But du run** : vérifier C2 (complétion par frères ⇒ both ⇒ projection B12) sur des artefacts déterministes. +- **Assertion vérifiée** : égalités d’ensembles et égalité de projections modulo 4096 (voir métriques). + +## Code et reproductibilité + +- **Commit Git** : `e12c544e7bf8d7a6f9518cdd4959d0da07bccc07` +- **Commande** : + +```bash +python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py --profile c2_projective --scope c2_projective --out-dir applications/collatz/out --docs-dir docs --c2-artefacts-dir docs/artefacts/collatz/c2_projective +``` + +## Empreintes sha256 (scripts, artefacts) + +- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py` + - sha256: `4f515d649c44c4ffe55349b07c72e9e766f591f7596e1bcdf0f9447e6b94950d` +- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/noyau_both_base_4096.md` + - sha256: `d0abffeca9ce2356d13b31ee4325b68fd85cf061670a8524b8e60fd15aba881b` +- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md` + - sha256: `acc8667be8e93a33fadf45bacd5cd788ec05089d844616cf1762330ac0d41d67` +- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md` + - sha256: `956f8fd19570b7614705384995b52b6bf81399ca8dc36c3ea33bcbad3e4aff50` +- `/home/ncantu/code/algo/docs/artefacts/collatz/c2_projective/verification_c2_projective.json` + - sha256: `b1b9ab9d5d4f9d4ee60e7efd43b853ac29d3d51a19c2d71bdac45c4340d01bf0` +- `/home/ncantu/code/algo/docs/artefacts/collatz/c2_projective/verification_c2_projective.md` + - sha256: `8bd84cb2149d297487e0e0ff03ebe96ff27b07a5ab677407cb4b9a17a339c2ba` + +## Compteurs et métriques + +- |B12| = 192 +- m=14: |both|=593, |children(m=15)|=1186, |listed residual(m=15)|=1186 +- m=14: children(m=15) == residual(m=15) : True +- m=14: both mod 4096 == B12 : True +- m=15: |both|=1101, |children(m=16)|=2202 +- m=15: both mod 4096 == B12 : True + +## Chemins d’artefacts (versionnés) + +- ARTEFACTS : `/home/ncantu/code/algo/docs/artefacts/collatz/c2_projective` + diff --git a/docs/collatz_run_report_format.md b/docs/collatz_run_report_format.md index 2f4a03d..08821a5 100644 --- a/docs/collatz_run_report_format.md +++ b/docs/collatz_run_report_format.md @@ -86,6 +86,21 @@ Lors de la génération d’un rapport `local_H6`/`local_H6_E1`, un audit automa En cas de désaccord, la génération échoue (afin d’éviter une citation ambiguë d’artefacts). +Pour la vérification C2 (complétion par frères ⇒ both ⇒ projection \(B_{12}\), artefacts déterministes versionnés) : + +```bash +python3 applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py \ + --repo-root /home/ncantu/code/algo \ + --output-dir docs/artefacts/collatz/c2_projective + +python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \ + --profile c2_projective \ + --scope c2_projective \ + --c2-artefacts-dir docs/artefacts/collatz/c2_projective \ + --out-dir applications/collatz/out \ + --docs-dir docs +``` + ### Contexte - **But du run** : (énoncé court) diff --git a/docs/features/collatz_c2_projective_verification.md b/docs/features/collatz_c2_projective_verification.md new file mode 100644 index 0000000..ef83a50 --- /dev/null +++ b/docs/features/collatz_c2_projective_verification.md @@ -0,0 +1,52 @@ +**Auteur** : Équipe 4NK + +# Collatz — Vérification déterministe de C2 (réduction projective) + +## Objectif + +Rendre citable (sans transcript terminal) une vérification déterministe des assertions utilisées dans le lemme C2 : + +- **complétion par frères** : après fermeture des cas “one”, le résidu au palier suivant est exactement l’ensemble des **enfants** des parents “both” ; +- **projection projective** : l’ensemble des parents “both” à certains paliers se projette modulo \(2^{12}\) sur une base fixe \(B_{12}\subset(\mathbb{Z}/2^{12}\mathbb{Z})^\times\). + +## Impacts + +- Ajout d’un artefact versionné dans `docs/artefacts/` et d’un rapport d’exécution dans `docs/`, alignés sur le format standard des rapports. + +## Modifications + +- Script déterministe : + - `applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py` +- Artefacts versionnés (sortie du script) : + - `docs/artefacts/collatz/c2_projective/verification_c2_projective.json` + - `docs/artefacts/collatz/c2_projective/verification_c2_projective.md` +- Rapport d’exécution (sha256 + métriques) : + - `docs/collatz_run_report_2026-03-09_c2_projective.md` +- Extension du générateur de rapports : + - `applications/collatz/collatz_k_scripts/collatz_generate_run_report.py` (profil `c2_projective`) + +## Modalités d’analyse + +- Générer/mettre à jour les artefacts déterministes : + +```bash +python3 applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py \ + --repo-root /home/ncantu/code/algo \ + --output-dir docs/artefacts/collatz/c2_projective +``` + +- Produire le rapport d’exécution (empreintes sha256 + métriques) : + +```bash +python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \ + --profile c2_projective \ + --scope c2_projective \ + --c2-artefacts-dir docs/artefacts/collatz/c2_projective \ + --out-dir applications/collatz/out \ + --docs-dir docs +``` + +## Modalités de déploiement + +Aucun déploiement. + diff --git a/docs/features/collatz_run_report_generator.md b/docs/features/collatz_run_report_generator.md index 4e14d03..50c48ba 100644 --- a/docs/features/collatz_run_report_generator.md +++ b/docs/features/collatz_run_report_generator.md @@ -23,8 +23,9 @@ 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`. + - Profils supportés : `extend_finale`, `validation_section7`, `pipeline_d16_d17`, `fusion_palier2p25`, `local_H6_E1`, `local_H6`, `c2_projective`. - 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}`. ## Modalités d’analyse