c29bbaec4b
**Motivations:**
- Make C2 verification robust when completion documents provide counts instead of full residual lists
- Prepare the verifier to support additional completion transitions with the same artefact structure
**Root causes:**
- m=15→m=16 completion doc may omit residual list and only state |R_16^comp| = 2*|both| = 2202
**Correctifs:**
- Parse and validate declared |R_{m+1}^comp| size when present
- Add generic transition discovery output in verification JSON
**Evolutions:**
- Regenerate versioned C2 verification artefacts and run report
**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
- docs/collatz_run_report_2026-03-09_c2_projective.md
346 lines
13 KiB
Python
346 lines
13 KiB
Python
#!/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 _discover_both_parent_blocks(md: str) -> dict[int, list[int]]:
|
|
"""
|
|
Discover "Parents « both » au palier 2^m" blocks in a completion markdown file.
|
|
Returns m -> residues list.
|
|
"""
|
|
out: dict[int, list[int]] = {}
|
|
for m in re.findall(r"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^(\d+)\b", md, flags=re.M):
|
|
mm = int(m)
|
|
out[mm] = _parse_list_under_heading(
|
|
md, rf"^###\s+Parents\s+«\s+both\s+»\s+au\s+palier\s+2\^{mm}\b"
|
|
)
|
|
return out
|
|
|
|
|
|
def _discover_listed_residual_after_completion(md: str, child_palier: int) -> list[int] | None:
|
|
"""
|
|
Optional: "Résidu restant au palier 2^(m+1) après complétion « one » (...)".
|
|
"""
|
|
pattern = rf"^###\s+Résidu\s+restant\s+au\s+palier\s+2\^{child_palier}\s+après\s+complétion\s+«\s+one\s+»"
|
|
try:
|
|
return _parse_list_under_heading(md, pattern)
|
|
except ValueError:
|
|
return None
|
|
|
|
|
|
def _discover_declared_residual_size(md: str, child_palier: int) -> int | None:
|
|
"""
|
|
Optional: parse a declared residual size like "|R_16^comp| = 2202".
|
|
"""
|
|
matches = re.findall(rf"\|R_{child_palier}\^comp\|\s*=\s*([^\n]+)", md)
|
|
if not matches:
|
|
return None
|
|
# Extract the last integer on the matched RHS (e.g. "2*|both| = 2202" -> 2202).
|
|
rhs = matches[-1]
|
|
ints = re.findall(r"\b(\d+)\b", rhs)
|
|
return int(ints[-1]) if ints else None
|
|
|
|
|
|
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")
|
|
|
|
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)):
|
|
both_blocks = _discover_both_parent_blocks(md)
|
|
for m_parent, both in sorted(both_blocks.items()):
|
|
child_palier = m_parent + 1
|
|
children = _lift_children(both, m_parent)
|
|
listed = _discover_listed_residual_after_completion(md, child_palier)
|
|
declared = _discover_declared_residual_size(md, child_palier)
|
|
transitions.append(
|
|
{
|
|
"source": src_name,
|
|
"palier_parent": m_parent,
|
|
"palier_child": child_palier,
|
|
"both_parent_count": len(both),
|
|
"computed_children_count": len(children),
|
|
"listed_residual_count": len(listed) if listed is not None else declared,
|
|
"children_equals_listed_residual": (set(children) == set(listed)) if listed is not None else None,
|
|
"projection_mod_4096_equals_b12": (_project_mod_4096(both) == 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)},
|
|
"transitions": transitions,
|
|
"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|)")
|
|
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}")
|
|
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()
|
|
|