ace28bbecf
**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
363 lines
13 KiB
Python
363 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)
|
|
- 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)
|
|
- 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_docs: list[Path],
|
|
repo_root: Path,
|
|
output_json: Path,
|
|
output_md: Path,
|
|
) -> None:
|
|
b12_md = _read_text(noyau_both_base_4096_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)}")
|
|
|
|
transitions: list[dict[str, object]] = []
|
|
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,
|
|
"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)),
|
|
}
|
|
)
|
|
|
|
# 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_docs": [_display_path(p, repo_root) for p in completion_docs],
|
|
},
|
|
"B12": {"count": len(b12), "min": min(b12), "max": max(b12)},
|
|
"transitions": transitions,
|
|
"checks": {
|
|
"m14_to_m15": c1415.__dict__,
|
|
"m15_to_m16": c1516.__dict__,
|
|
},
|
|
"ok": {
|
|
"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
|
|
),
|
|
},
|
|
}
|
|
|
|
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)}`")
|
|
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("## Transitions détectées (table multi-transitions)")
|
|
lines.append("")
|
|
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("")
|
|
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(
|
|
"--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(
|
|
"--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()
|
|
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_docs=completion_docs,
|
|
repo_root=repo_root,
|
|
output_json=out_dir / "verification_c2_projective.json",
|
|
output_md=out_dir / "verification_c2_projective.md",
|
|
)
|
|
|
|
|
|
if __name__ == "__main__":
|
|
main()
|
|
|