From ace28bbecf9c9c768ed124ffe1dcd36aada5425a Mon Sep 17 00:00:00 2001 From: ncantu Date: Mon, 9 Mar 2026 01:52:04 +0100 Subject: [PATCH] Auto-discover C2 completion docs and add multi-transition table MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit **Motivations:** - Keep C2 verification up to date when new completion documents (m>16) are added - Make C3 status explicit: local instance vs general uniformization lock **Root causes:** - C2 verifier was hardwired to two completion files and could not generalize to future transitions - C3 general form required an explicit decision and statement of the remaining lock **Correctifs:** - Auto-discover completion docs and validate declared residual sizes and optional lists per transition - Restore backward-compatible checks block for downstream tooling **Evolutions:** - Add a deterministic multi-transition table to c2_projective artefacts - Hash the discovered completion docs list in the c2_projective run report profile - Record the explicit C3 “local vs general” decision and C3.gen target in the proof plan **Pages affectées:** - applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py - docs/artefacts/collatz/c2_projective/verification_c2_projective.json - docs/artefacts/collatz/c2_projective/verification_c2_projective.md - applications/collatz/collatz_k_scripts/collatz_generate_run_report.py - docs/collatz_run_report_2026-03-09_c2_projective.md - applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md --- .../collatz_generate_run_report.py | 17 +- .../collatz_verify_c2_projective.py | 195 ++++++++++-------- ...lemmes_manquants_et_programme_de_preuve.md | 20 ++ .../verification_c2_projective.json | 15 +- .../verification_c2_projective.md | 22 +- ...atz_run_report_2026-03-09_c2_projective.md | 8 +- 6 files changed, 160 insertions(+), 117 deletions(-) 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 31f956f..3a88032 100644 --- a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py +++ b/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py @@ -184,6 +184,19 @@ def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics: ) +def _extract_c2_completion_docs_from_verification(verification_json_path: Path) -> list[Path]: + obj = read_json(verification_json_path) + if not isinstance(obj, dict): + return [] + inputs = obj.get("inputs") + if not isinstance(inputs, dict): + return [] + docs = inputs.get("completion_docs") + if not isinstance(docs, list) or not all(isinstance(x, str) for x in docs): + return [] + return [Path(x) for x in docs] + + def parse_c3_local_descent_metrics(verification_json: str) -> C3LocalDescentMetrics: obj = read_json(Path(verification_json)) if not isinstance(obj, dict): @@ -1153,13 +1166,13 @@ def main() -> None: verification_json = artefacts_dir / "verification_c2_projective.json" verification_md = artefacts_dir / "verification_c2_projective.md" metrics = parse_c2_projective_metrics(str(verification_json)) + completion_docs = _extract_c2_completion_docs_from_verification(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", + *[repo_root / p for p in completion_docs], verification_json, verification_md, ] diff --git a/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py b/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py index a5d2014..ae73dd4 100644 --- a/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py +++ b/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py @@ -11,8 +11,7 @@ From completion-by-brothers audit documents, verify that: 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) +- completion documents (e.g. complétion_minorée_m14_vers_m15.md, complétion_minorée_m15_vers_m16.md) Outputs: - a short JSON summary (machine-checkable) @@ -151,80 +150,46 @@ def _discover_declared_residual_size(md: str, child_palier: int) -> int | None: def verify_c2( *, noyau_both_base_4096_md: Path, - completion_m14_to_m15_md: Path, - completion_m15_to_m16_md: Path, + completion_docs: list[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") - - listed_r16 = _discover_listed_residual_after_completion(c1516_md, 16) - declared_r16_size = _discover_declared_residual_size(c1516_md, 16) - if listed_r16 is not None: - _assert_all_odd(listed_r16, "Listed residual at m=16") - if set(listed_r16) != set(children16): - raise ValueError("Listed residual at m=16 does not match computed children of both(m=15)") - if declared_r16_size is not None and declared_r16_size != len(children16): - raise ValueError(f"Declared |R_16^comp|={declared_r16_size} does not match computed {len(children16)}") - - # This completion file may omit the full residual after completion. - c1516 = C2CheckResult( - palier_parent=15, - palier_child=16, - both_parent_count=len(both15), - computed_children_count=len(children16), - listed_residual_count=len(listed_r16) if listed_r16 is not None else declared_r16_size, - children_equals_listed_residual=(set(children16) == set(listed_r16)) if listed_r16 is not None else None, - projection_mod_4096_equals_b12=(_project_mod_4096(both15) == set(b12)), - ) - transitions: list[dict[str, object]] = [] - for src_name, md in (("completion_m14_to_m15", c1415_md), ("completion_m15_to_m16", c1516_md)): + for doc_path in completion_docs: + md = _read_text(doc_path) + src = _display_path(doc_path, repo_root) both_blocks = _discover_both_parent_blocks(md) for m_parent, both in sorted(both_blocks.items()): + _assert_all_odd(both, f"Parents both (m={m_parent}) in {src}") child_palier = m_parent + 1 children = _lift_children(both, m_parent) + _assert_all_odd(children, f"Computed children (m={child_palier}) in {src}") + listed = _discover_listed_residual_after_completion(md, child_palier) declared = _discover_declared_residual_size(md, child_palier) + if listed is not None: + _assert_all_odd(listed, f"Listed residual (m={child_palier}) in {src}") + if set(children) != set(listed): + raise ValueError( + f"Residual list mismatch for m={m_parent}→{child_palier} in {src}: " + "listed residual does not match computed children of both" + ) + if declared is not None and declared != len(children): + raise ValueError( + f"Declared |R_{child_palier}^comp|={declared} does not match computed {len(children)} for {src}" + ) + transitions.append( { - "source": src_name, + "source": src, "palier_parent": m_parent, "palier_child": child_palier, "both_parent_count": len(both), @@ -235,11 +200,36 @@ def verify_c2( } ) + # Stable ordering for deterministic JSON/MD + transitions = sorted( + transitions, + key=lambda d: (str(d["source"]), int(d["palier_parent"]), int(d["palier_child"])), + ) + + def _pick_check(parent_m: int) -> C2CheckResult: + matches = [t for t in transitions if int(t["palier_parent"]) == parent_m and int(t["palier_child"]) == parent_m + 1] + if not matches: + raise ValueError(f"Missing expected transition m={parent_m}→{parent_m+1} in discovered completion docs") + # deterministic: pick first by our transition ordering + t = matches[0] + return C2CheckResult( + palier_parent=int(t["palier_parent"]), + palier_child=int(t["palier_child"]), + both_parent_count=int(t["both_parent_count"]), + computed_children_count=int(t["computed_children_count"]), + listed_residual_count=(int(t["listed_residual_count"]) if t["listed_residual_count"] is not None else None), + children_equals_listed_residual=(bool(t["children_equals_listed_residual"]) if t["children_equals_listed_residual"] is not None else None), + projection_mod_4096_equals_b12=bool(t["projection_mod_4096_equals_b12"]), + ) + + # Backward-compatible checks block for report generator / downstream tooling. + c1415 = _pick_check(14) + c1516 = _pick_check(15) + 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), + "completion_docs": [_display_path(p, repo_root) for p in completion_docs], }, "B12": {"count": len(b12), "min": min(b12), "max": max(b12)}, "transitions": transitions, @@ -248,9 +238,11 @@ def verify_c2( "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), + "all_transitions_project_to_B12": all(bool(t["projection_mod_4096_equals_b12"]) for t in transitions), + "all_listed_residuals_match_children": all( + (t["children_equals_listed_residual"] is None) or bool(t["children_equals_listed_residual"]) + for t in transitions + ), }, } @@ -265,29 +257,45 @@ def verify_c2( 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)}`") + for p in completion_docs: + lines.append(f"- completion : `{_display_path(p, 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("## Transitions détectées (table multi-transitions)") 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|)") - if c1516.listed_residual_count is not None: - lines.append(f"- |listed residual (m=16)| : {c1516.listed_residual_count}") - lines.append(f"- projection both(m=15) mod 4096 == B12 : {c1516.projection_mod_4096_equals_b12}") + header = [ + "source", + "m", + "m+1", + "|both(m)|", + "|children(m+1)|", + "|listed residual|", + "children==listed", + "both mod 4096 == B12", + ] + lines.append("| " + " | ".join(header) + " |") + lines.append("| " + " | ".join(["---"] * len(header)) + " |") + for t in transitions: + lines.append( + "| " + + " | ".join( + [ + str(t["source"]), + str(t["palier_parent"]), + str(t["palier_child"]), + str(t["both_parent_count"]), + str(t["computed_children_count"]), + str(t["listed_residual_count"]) if t["listed_residual_count"] is not None else "", + str(t["children_equals_listed_residual"]) if t["children_equals_listed_residual"] is not None else "", + str(t["projection_mod_4096_equals_b12"]), + ] + ) + + " |" + ) lines.append("") lines.append("## Sorties") lines.append("") @@ -306,21 +314,22 @@ def main() -> None: default="", help="Repository root used to display relative paths in outputs (defaults to current working directory)", ) + ap.add_argument( + "--completion-dir", + default="", + help="Directory to auto-discover completion markdown files (default: collatz_k_scripts directory)", + ) + ap.add_argument( + "--completion-md", + action="append", + default=[], + help="Completion markdown file (repeatable). If provided, disables auto-discovery.", + ) 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", @@ -329,11 +338,19 @@ def main() -> None: args = ap.parse_args() repo_root = Path(args.repo_root).resolve() if args.repo_root.strip() else Path.cwd().resolve() + completion_docs: list[Path] + if args.completion_md: + completion_docs = [Path(p).resolve() for p in args.completion_md] + else: + completion_dir = Path(args.completion_dir).resolve() if args.completion_dir.strip() else Path(__file__).parent.resolve() + completion_docs = sorted(completion_dir.glob("complétion*_m*_vers_m*.md")) + if not completion_docs: + raise ValueError(f"No completion docs found under {completion_dir}") + 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), + completion_docs=completion_docs, repo_root=repo_root, output_json=out_dir / "verification_c2_projective.json", output_md=out_dir / "verification_c2_projective.md", 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 68be969..962a77a 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 @@ -278,6 +278,26 @@ Artefact déterministe (script + sorties courtes) : Cet artefact vérifie l’égalité \(U(m)=U^{(t)}(n)\), la stricte inégalité \(m