Auto-discover C2 completion docs and add multi-transition table
**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
This commit is contained in:
parent
071da20b19
commit
ace28bbecf
@ -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:
|
def parse_c3_local_descent_metrics(verification_json: str) -> C3LocalDescentMetrics:
|
||||||
obj = read_json(Path(verification_json))
|
obj = read_json(Path(verification_json))
|
||||||
if not isinstance(obj, dict):
|
if not isinstance(obj, dict):
|
||||||
@ -1153,13 +1166,13 @@ def main() -> None:
|
|||||||
verification_json = artefacts_dir / "verification_c2_projective.json"
|
verification_json = artefacts_dir / "verification_c2_projective.json"
|
||||||
verification_md = artefacts_dir / "verification_c2_projective.md"
|
verification_md = artefacts_dir / "verification_c2_projective.md"
|
||||||
metrics = parse_c2_projective_metrics(str(verification_json))
|
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])
|
date_str = pick_report_date_from_mtime([verification_json, verification_md])
|
||||||
sha_paths: list[Path] = [
|
sha_paths: list[Path] = [
|
||||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_verify_c2_projective.py",
|
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" / "noyau_both_base_4096.md",
|
||||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "complétion_minorée_m14_vers_m15.md",
|
*[repo_root / p for p in completion_docs],
|
||||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "complétion_minorée_m15_vers_m16.md",
|
|
||||||
verification_json,
|
verification_json,
|
||||||
verification_md,
|
verification_md,
|
||||||
]
|
]
|
||||||
|
|||||||
@ -11,8 +11,7 @@ From completion-by-brothers audit documents, verify that:
|
|||||||
|
|
||||||
Inputs (Markdown):
|
Inputs (Markdown):
|
||||||
- noyau_both_base_4096.md (contains B12 list)
|
- 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)
|
- completion documents (e.g. complétion_minorée_m14_vers_m15.md, complétion_minorée_m15_vers_m16.md)
|
||||||
- complétion_minorée_m15_vers_m16.md (contains both-parent list at 2^15)
|
|
||||||
|
|
||||||
Outputs:
|
Outputs:
|
||||||
- a short JSON summary (machine-checkable)
|
- 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(
|
def verify_c2(
|
||||||
*,
|
*,
|
||||||
noyau_both_base_4096_md: Path,
|
noyau_both_base_4096_md: Path,
|
||||||
completion_m14_to_m15_md: Path,
|
completion_docs: list[Path],
|
||||||
completion_m15_to_m16_md: Path,
|
|
||||||
repo_root: Path,
|
repo_root: Path,
|
||||||
output_json: Path,
|
output_json: Path,
|
||||||
output_md: Path,
|
output_md: Path,
|
||||||
) -> None:
|
) -> None:
|
||||||
b12_md = _read_text(noyau_both_base_4096_md)
|
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")
|
b12 = _parse_list_under_heading(b12_md, r"^##\s+Base projective B_12\b")
|
||||||
_assert_all_odd(b12, "B12")
|
_assert_all_odd(b12, "B12")
|
||||||
if len(b12) != 192:
|
if len(b12) != 192:
|
||||||
raise ValueError(f"B12: expected 192 residues, got {len(b12)}")
|
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]] = []
|
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)
|
both_blocks = _discover_both_parent_blocks(md)
|
||||||
for m_parent, both in sorted(both_blocks.items()):
|
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
|
child_palier = m_parent + 1
|
||||||
children = _lift_children(both, m_parent)
|
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)
|
listed = _discover_listed_residual_after_completion(md, child_palier)
|
||||||
declared = _discover_declared_residual_size(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(
|
transitions.append(
|
||||||
{
|
{
|
||||||
"source": src_name,
|
"source": src,
|
||||||
"palier_parent": m_parent,
|
"palier_parent": m_parent,
|
||||||
"palier_child": child_palier,
|
"palier_child": child_palier,
|
||||||
"both_parent_count": len(both),
|
"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 = {
|
summary = {
|
||||||
"inputs": {
|
"inputs": {
|
||||||
"noyau_both_base_4096_md": _display_path(noyau_both_base_4096_md, repo_root),
|
"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_docs": [_display_path(p, repo_root) for p in completion_docs],
|
||||||
"completion_m15_to_m16_md": _display_path(completion_m15_to_m16_md, repo_root),
|
|
||||||
},
|
},
|
||||||
"B12": {"count": len(b12), "min": min(b12), "max": max(b12)},
|
"B12": {"count": len(b12), "min": min(b12), "max": max(b12)},
|
||||||
"transitions": transitions,
|
"transitions": transitions,
|
||||||
@ -248,9 +238,11 @@ def verify_c2(
|
|||||||
"m15_to_m16": c1516.__dict__,
|
"m15_to_m16": c1516.__dict__,
|
||||||
},
|
},
|
||||||
"ok": {
|
"ok": {
|
||||||
"m14_to_m15_children_equals_listed_residual": bool(c1415.children_equals_listed_residual),
|
"all_transitions_project_to_B12": all(bool(t["projection_mod_4096_equals_b12"]) for t in transitions),
|
||||||
"m14_projection_equals_b12": bool(c1415.projection_mod_4096_equals_b12),
|
"all_listed_residuals_match_children": all(
|
||||||
"m15_projection_equals_b12": bool(c1516.projection_mod_4096_equals_b12),
|
(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("## Entrées")
|
||||||
lines.append("")
|
lines.append("")
|
||||||
lines.append(f"- `noyau_both_base_4096.md` : `{_display_path(noyau_both_base_4096_md, repo_root)}`")
|
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)}`")
|
for p in completion_docs:
|
||||||
lines.append(f"- `complétion_minorée_m15_vers_m16.md` : `{_display_path(completion_m15_to_m16_md, repo_root)}`")
|
lines.append(f"- completion : `{_display_path(p, repo_root)}`")
|
||||||
lines.append("")
|
lines.append("")
|
||||||
lines.append("## Base projective B12")
|
lines.append("## Base projective B12")
|
||||||
lines.append("")
|
lines.append("")
|
||||||
lines.append(f"- |B12| = {len(b12)} (attendu 192)")
|
lines.append(f"- |B12| = {len(b12)} (attendu 192)")
|
||||||
lines.append(f"- min(B12) = {min(b12)}, max(B12) = {max(b12)}")
|
lines.append(f"- min(B12) = {min(b12)}, max(B12) = {max(b12)}")
|
||||||
lines.append("")
|
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("")
|
||||||
lines.append(f"- |both parents (m=14)| = {c1415.both_parent_count}")
|
header = [
|
||||||
lines.append(f"- |computed children (m=15)| = {c1415.computed_children_count} (attendu 2*|both|)")
|
"source",
|
||||||
lines.append(f"- |listed residual (m=15)| = {c1415.listed_residual_count}")
|
"m",
|
||||||
lines.append(f"- computed children == listed residual : {c1415.children_equals_listed_residual}")
|
"m+1",
|
||||||
lines.append(f"- projection both(m=14) mod 4096 == B12 : {c1415.projection_mod_4096_equals_b12}")
|
"|both(m)|",
|
||||||
lines.append("")
|
"|children(m+1)|",
|
||||||
lines.append("## Transition m=15 → m=16 (projection des both)")
|
"|listed residual|",
|
||||||
lines.append("")
|
"children==listed",
|
||||||
lines.append(f"- |both parents (m=15)| = {c1516.both_parent_count}")
|
"both mod 4096 == B12",
|
||||||
lines.append(f"- |computed children (m=16)| = {c1516.computed_children_count} (attendu 2*|both|)")
|
]
|
||||||
if c1516.listed_residual_count is not None:
|
lines.append("| " + " | ".join(header) + " |")
|
||||||
lines.append(f"- |listed residual (m=16)| : {c1516.listed_residual_count}")
|
lines.append("| " + " | ".join(["---"] * len(header)) + " |")
|
||||||
lines.append(f"- projection both(m=15) mod 4096 == B12 : {c1516.projection_mod_4096_equals_b12}")
|
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("")
|
||||||
lines.append("## Sorties")
|
lines.append("## Sorties")
|
||||||
lines.append("")
|
lines.append("")
|
||||||
@ -306,21 +314,22 @@ def main() -> None:
|
|||||||
default="",
|
default="",
|
||||||
help="Repository root used to display relative paths in outputs (defaults to current working directory)",
|
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(
|
ap.add_argument(
|
||||||
"--noyau-both-base-4096-md",
|
"--noyau-both-base-4096-md",
|
||||||
default=str(Path(__file__).parent / "noyau_both_base_4096.md"),
|
default=str(Path(__file__).parent / "noyau_both_base_4096.md"),
|
||||||
help="Path to 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(
|
ap.add_argument(
|
||||||
"--output-dir",
|
"--output-dir",
|
||||||
default="docs/artefacts/collatz/c2_projective",
|
default="docs/artefacts/collatz/c2_projective",
|
||||||
@ -329,11 +338,19 @@ def main() -> None:
|
|||||||
args = ap.parse_args()
|
args = ap.parse_args()
|
||||||
|
|
||||||
repo_root = Path(args.repo_root).resolve() if args.repo_root.strip() else Path.cwd().resolve()
|
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)
|
out_dir = Path(args.output_dir)
|
||||||
verify_c2(
|
verify_c2(
|
||||||
noyau_both_base_4096_md=Path(args.noyau_both_base_4096_md),
|
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_docs=completion_docs,
|
||||||
completion_m15_to_m16_md=Path(args.completion_m15_to_m16_md),
|
|
||||||
repo_root=repo_root,
|
repo_root=repo_root,
|
||||||
output_json=out_dir / "verification_c2_projective.json",
|
output_json=out_dir / "verification_c2_projective.json",
|
||||||
output_md=out_dir / "verification_c2_projective.md",
|
output_md=out_dir / "verification_c2_projective.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<n\) pour les témoins de fusion, la cohérence des seuils \(N_0\) (descente exacte) et \(N_F\) (fusion) lorsqu’ils sont calculables, et agrège une borne \(N^\star\) sur cette instance.
|
Cet artefact vérifie l’égalité \(U(m)=U^{(t)}(n)\), la stricte inégalité \(m<n\) pour les témoins de fusion, la cohérence des seuils \(N_0\) (descente exacte) et \(N_F\) (fusion) lorsqu’ils sont calculables, et agrège une borne \(N^\star\) sur cette instance.
|
||||||
|
|
||||||
|
### Statut et forme générale (au-delà de \(2^{13}\))
|
||||||
|
|
||||||
|
Décision explicite.
|
||||||
|
À ce stade, C3 est **instrumenté comme une instance locale** au palier \(2^{13}\) sur \(L=\mathrm{Lift}_{12\to 13}(B_{12})\).
|
||||||
|
La preuve “globale” ne suit pas encore d’une simple citation de cette instance : le verrou redevient une **uniformisation / itération** du schéma \(C1+C2\to C3\) au-delà du palier \(2^{13}\).
|
||||||
|
|
||||||
|
Cible formelle (C3 général).
|
||||||
|
Une forme générale exploitable de C3 doit expliciter un mécanisme uniformisable, par exemple :
|
||||||
|
|
||||||
|
- (C3.gen) pour tout \(m\ge 13\) et tout \(n\in \mathrm{Lift}_{12\to m}(B_{12})\), il existe un témoin D/F (au sens de (H4)–(H5)) produisant un entier impair \(n'\) strictement plus petit que \(n\), et une borne \(N^\star\) telle que ce mécanisme soit valide pour tous \(n\ge N^\star\) dans les classes concernées ;
|
||||||
|
- et la réduction obtenue par itération amène nécessairement sous \(N^\star\) (clôture par validation de base finie).
|
||||||
|
|
||||||
|
Verrou technique précis.
|
||||||
|
Passer de l’instance locale au cas général exige de relier les témoins observés à des **clauses** valides au sens global :
|
||||||
|
|
||||||
|
- D exact : contrôler l’extension “pour tout \(n\) dans une classe modulo \(2^m\), pour tout \(n\ge N_0\)” via les formules affines (seuil \(N_0\)) ;
|
||||||
|
- fusion : contrôler l’extension “pour tout \(n\) dans une classe modulo \(2^m\), pour tout \(n\ge N_F\)” et la propriété de réduction \(m<n\) sans la prouver seulement sur un représentant.
|
||||||
|
|
||||||
|
En l’absence de ce passage, l’instance locale reste un artefact d’audit (citable), et le verrou global est formulé comme “uniformiser / itérer” (C1+C2→C3) sur des paliers arbitraires.
|
||||||
|
|
||||||
## Conclusion
|
## Conclusion
|
||||||
|
|
||||||
La trajectoire D18–D21 (F15/F16) augmente le matériau et affine la cartographie du noyau résiduel, mais la preuve complète exige encore l’un des deux verrous : extinction à palier fini (certificat total) ou contraction uniforme (lemme analytique).
|
La trajectoire D18–D21 (F15/F16) augmente le matériau et affine la cartographie du noyau résiduel, mais la preuve complète exige encore l’un des deux verrous : extinction à palier fini (certificat total) ou contraction uniforme (lemme analytique).
|
||||||
|
|||||||
@ -1,8 +1,10 @@
|
|||||||
{
|
{
|
||||||
"inputs": {
|
"inputs": {
|
||||||
"noyau_both_base_4096_md": "applications/collatz/collatz_k_scripts/noyau_both_base_4096.md",
|
"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_docs": [
|
||||||
"completion_m15_to_m16_md": "applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md"
|
"applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md",
|
||||||
|
"applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md"
|
||||||
|
]
|
||||||
},
|
},
|
||||||
"B12": {
|
"B12": {
|
||||||
"count": 192,
|
"count": 192,
|
||||||
@ -11,7 +13,7 @@
|
|||||||
},
|
},
|
||||||
"transitions": [
|
"transitions": [
|
||||||
{
|
{
|
||||||
"source": "completion_m14_to_m15",
|
"source": "applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md",
|
||||||
"palier_parent": 14,
|
"palier_parent": 14,
|
||||||
"palier_child": 15,
|
"palier_child": 15,
|
||||||
"both_parent_count": 593,
|
"both_parent_count": 593,
|
||||||
@ -21,7 +23,7 @@
|
|||||||
"projection_mod_4096_equals_b12": true
|
"projection_mod_4096_equals_b12": true
|
||||||
},
|
},
|
||||||
{
|
{
|
||||||
"source": "completion_m15_to_m16",
|
"source": "applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md",
|
||||||
"palier_parent": 15,
|
"palier_parent": 15,
|
||||||
"palier_child": 16,
|
"palier_child": 16,
|
||||||
"both_parent_count": 1101,
|
"both_parent_count": 1101,
|
||||||
@ -52,8 +54,7 @@
|
|||||||
}
|
}
|
||||||
},
|
},
|
||||||
"ok": {
|
"ok": {
|
||||||
"m14_to_m15_children_equals_listed_residual": true,
|
"all_transitions_project_to_B12": true,
|
||||||
"m14_projection_equals_b12": true,
|
"all_listed_residuals_match_children": true
|
||||||
"m15_projection_equals_b12": true
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@ -5,28 +5,20 @@
|
|||||||
## Entrées
|
## Entrées
|
||||||
|
|
||||||
- `noyau_both_base_4096.md` : `applications/collatz/collatz_k_scripts/noyau_both_base_4096.md`
|
- `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`
|
- completion : `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`
|
- completion : `applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md`
|
||||||
|
|
||||||
## Base projective B12
|
## Base projective B12
|
||||||
|
|
||||||
- |B12| = 192 (attendu 192)
|
- |B12| = 192 (attendu 192)
|
||||||
- min(B12) = 27, max(B12) = 4095
|
- min(B12) = 27, max(B12) = 4095
|
||||||
|
|
||||||
## Transition m=14 → m=15 (complétion par frères ⇒ résidu = enfants des both)
|
## Transitions détectées (table multi-transitions)
|
||||||
|
|
||||||
- |both parents (m=14)| = 593
|
| source | m | m+1 | |both(m)| | |children(m+1)| | |listed residual| | children==listed | both mod 4096 == B12 |
|
||||||
- |computed children (m=15)| = 1186 (attendu 2*|both|)
|
| --- | --- | --- | --- | --- | --- | --- | --- |
|
||||||
- |listed residual (m=15)| = 1186
|
| applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md | 14 | 15 | 593 | 1186 | 1186 | True | True |
|
||||||
- computed children == listed residual : True
|
| applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md | 15 | 16 | 1101 | 2202 | 2202 | | 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|)
|
|
||||||
- |listed residual (m=16)| : 2202
|
|
||||||
- projection both(m=15) mod 4096 == B12 : True
|
|
||||||
|
|
||||||
## Sorties
|
## Sorties
|
||||||
|
|
||||||
|
|||||||
@ -9,7 +9,7 @@
|
|||||||
|
|
||||||
## Code et reproductibilité
|
## Code et reproductibilité
|
||||||
|
|
||||||
- **Commit Git** : `e3e68fe39c8ad466e5741e87d20311ca93b2456e`
|
- **Commit Git** : `071da20b190207aebcbbbaad8e57b9e21b8282c6`
|
||||||
- **Commande** :
|
- **Commande** :
|
||||||
|
|
||||||
```bash
|
```bash
|
||||||
@ -19,7 +19,7 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py --
|
|||||||
## Empreintes sha256 (scripts, artefacts)
|
## Empreintes sha256 (scripts, artefacts)
|
||||||
|
|
||||||
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py`
|
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py`
|
||||||
- sha256: `bad3ddd4288af4a8b7bcc4fa30c1f5350db16f352b6eaf29918e8c1e1428a5b0`
|
- sha256: `40fc1ae3e560f4baa5ae47ee63412a8634a7314899ff21eb117bf64023d61e5d`
|
||||||
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/noyau_both_base_4096.md`
|
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/noyau_both_base_4096.md`
|
||||||
- sha256: `d0abffeca9ce2356d13b31ee4325b68fd85cf061670a8524b8e60fd15aba881b`
|
- sha256: `d0abffeca9ce2356d13b31ee4325b68fd85cf061670a8524b8e60fd15aba881b`
|
||||||
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md`
|
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/complétion_minorée_m14_vers_m15.md`
|
||||||
@ -27,9 +27,9 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py --
|
|||||||
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md`
|
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/complétion_minorée_m15_vers_m16.md`
|
||||||
- sha256: `956f8fd19570b7614705384995b52b6bf81399ca8dc36c3ea33bcbad3e4aff50`
|
- sha256: `956f8fd19570b7614705384995b52b6bf81399ca8dc36c3ea33bcbad3e4aff50`
|
||||||
- `/home/ncantu/code/algo/docs/artefacts/collatz/c2_projective/verification_c2_projective.json`
|
- `/home/ncantu/code/algo/docs/artefacts/collatz/c2_projective/verification_c2_projective.json`
|
||||||
- sha256: `259901a9e4e307dae238672cc3e2e1e016800f034cdd98efe929e69bc1e4068a`
|
- sha256: `3f5ee61f259c90138d7c9fd3e8a2331947a2e25988bea349f246ad90fb1e43ec`
|
||||||
- `/home/ncantu/code/algo/docs/artefacts/collatz/c2_projective/verification_c2_projective.md`
|
- `/home/ncantu/code/algo/docs/artefacts/collatz/c2_projective/verification_c2_projective.md`
|
||||||
- sha256: `dc5562fea53f62e88acc08bcd29c89c53e9ad6e5fc4d41351642e7942cc49bdc`
|
- sha256: `f4f5e00365ec6cc2253f2ef80ca51414d4ad79dc51bc0a408ff1bb352eba39f5`
|
||||||
|
|
||||||
## Compteurs et métriques
|
## Compteurs et métriques
|
||||||
|
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user