collatz: extract and verify universal clause candidates (Option A)
**Motivations:** - Produce a deterministic bridge from C3 local witnesses to universal-clause candidates (D/F) usable in later H4/H5 formalization. **Root causes:** - Local witnesses (Lift(B12)-scoped) were not exportable into a versioned, machine-checkable clause artefact. **Correctifs:** - Add deterministic extraction with minimal stable modulus lifting for D_exact/F and local encoding for D_brother dependencies. - Add deterministic verifier checking arithmetic consistency, lifting stability, and brother↔mate relation. **Evolutions:** - Version universal clause artefacts (JSON/MD) under `docs/artefacts/collatz/universal_clauses/`. - Document the feature and reproduction steps in `docs/features/`. **Pages affectées:** - applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py - applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py - docs/artefacts/collatz/universal_clauses/* - docs/features/collatz_universal_clause_extraction_optionA.md
This commit is contained in:
ncantu
parent
523fa25fef
commit
94280b93fd
@ -0,0 +1,392 @@
|
||||
#!/usr/bin/env python3
|
||||
# -*- coding: utf-8 -*-
|
||||
"""
|
||||
collatz_extract_universal_clauses.py
|
||||
|
||||
Option A (Lift(B12)-scoped): convert deterministic *local witnesses* from the C3
|
||||
verification artefact into *universal clause candidates* (D/F) by lifting each
|
||||
witnessed residue to the minimal modulus that fixes its prefix of valuations.
|
||||
|
||||
Inputs:
|
||||
- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json
|
||||
|
||||
Outputs (versionable, no transcripts):
|
||||
- docs/artefacts/collatz/universal_clauses/clauses_universelles.json
|
||||
- docs/artefacts/collatz/universal_clauses/clauses_universelles.md
|
||||
|
||||
Notes:
|
||||
- D_exact and F witnesses are lifted to modulus 2^(A+1) where A is the prefix sum.
|
||||
- D_brother witnesses are preserved as *local* dependencies (mate_exact) at the
|
||||
domain palier; they are not asserted as standalone universal reductions here.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import json
|
||||
from dataclasses import dataclass
|
||||
from pathlib import Path
|
||||
from typing import Literal
|
||||
|
||||
from collatz_k_core import prefix_data
|
||||
|
||||
|
||||
ClauseKind = Literal["D_exact", "F", "D_brother_local"]
|
||||
|
||||
|
||||
def _read_json(path: Path) -> object:
|
||||
return json.loads(path.read_text(encoding="utf-8", errors="strict"))
|
||||
|
||||
|
||||
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)
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class ExtractedClause:
|
||||
kind: ClauseKind
|
||||
domain_palier: int
|
||||
source_n: int
|
||||
stable_modulus_power: int | None
|
||||
stable_residue_mod_2p: int | None
|
||||
# shared: prefix length + affine constants
|
||||
k_or_t: int | None
|
||||
A: int | None
|
||||
C: int | None
|
||||
word: tuple[int, ...] | None
|
||||
# D
|
||||
N0: int | None
|
||||
# F
|
||||
a: int | None
|
||||
y: int | None
|
||||
preimage_m: int | None
|
||||
DeltaF: int | None
|
||||
Nf: int | None
|
||||
source_csv: str | None
|
||||
# brother
|
||||
mate_exact: int | None
|
||||
|
||||
def to_json(self) -> dict[str, object]:
|
||||
return {
|
||||
"kind": self.kind,
|
||||
"domain_palier": self.domain_palier,
|
||||
"source_n": self.source_n,
|
||||
"stable_modulus_power": self.stable_modulus_power,
|
||||
"stable_residue_mod_2p": self.stable_residue_mod_2p,
|
||||
"k_or_t": self.k_or_t,
|
||||
"A": self.A,
|
||||
"C": self.C,
|
||||
"word": list(self.word) if self.word is not None else None,
|
||||
"N0": self.N0,
|
||||
"a": self.a,
|
||||
"y": self.y,
|
||||
"preimage_m": self.preimage_m,
|
||||
"DeltaF": self.DeltaF,
|
||||
"Nf": self.Nf,
|
||||
"source_csv": self.source_csv,
|
||||
"mate_exact": self.mate_exact,
|
||||
}
|
||||
|
||||
|
||||
def _lift_to_stable_residue(
|
||||
*,
|
||||
n0: int,
|
||||
base_palier: int,
|
||||
target_palier: int,
|
||||
prefix_len: int,
|
||||
expected_word: tuple[int, ...],
|
||||
) -> int:
|
||||
"""
|
||||
Deterministically lift a residue from 2^base_palier to 2^target_palier by choosing,
|
||||
at each step, the unique child (r or r+2^m) that preserves the expected prefix word.
|
||||
"""
|
||||
if target_palier < base_palier:
|
||||
raise ValueError("target_palier must be >= base_palier")
|
||||
if prefix_len < 1:
|
||||
raise ValueError("prefix_len must be >= 1")
|
||||
r = n0
|
||||
for m in range(base_palier, target_palier):
|
||||
shift = 1 << m
|
||||
c0 = r
|
||||
c1 = r + shift
|
||||
w0 = prefix_data(c0, prefix_len).word
|
||||
w1 = prefix_data(c1, prefix_len).word
|
||||
ok0 = w0 == expected_word
|
||||
ok1 = w1 == expected_word
|
||||
if ok0 and not ok1:
|
||||
r = c0
|
||||
elif ok1 and not ok0:
|
||||
r = c1
|
||||
else:
|
||||
raise ValueError(
|
||||
"Ambiguous lift (expected exactly one child to preserve the prefix word): "
|
||||
f"m={m}, base_palier={base_palier}, target_palier={target_palier}, n0={n0}, ok0={ok0}, ok1={ok1}"
|
||||
)
|
||||
return r
|
||||
|
||||
|
||||
def _format_int_list(values: list[int], per_line: int = 16) -> list[str]:
|
||||
lines: list[str] = []
|
||||
for i in range(0, len(values), per_line):
|
||||
lines.append(", ".join(str(x) for x in values[i : i + per_line]))
|
||||
return lines
|
||||
|
||||
|
||||
def run(*, verification_json: Path, output_dir: Path, repo_root: Path) -> None:
|
||||
obj = _read_json(verification_json)
|
||||
if not isinstance(obj, dict):
|
||||
raise ValueError("Invalid C3 verification JSON: expected object")
|
||||
domain = obj.get("domain")
|
||||
records = obj.get("records")
|
||||
if not isinstance(domain, dict) or not isinstance(records, list):
|
||||
raise ValueError("Invalid C3 verification JSON: missing domain/records")
|
||||
palier = domain.get("palier")
|
||||
if not isinstance(palier, int):
|
||||
raise ValueError("Invalid C3 verification JSON: domain.palier must be int")
|
||||
|
||||
extracted: list[ExtractedClause] = []
|
||||
for rec in records:
|
||||
if not isinstance(rec, dict):
|
||||
raise ValueError("Invalid C3 record: expected object")
|
||||
n = rec.get("n")
|
||||
kind = rec.get("kind")
|
||||
if not isinstance(n, int) or not isinstance(kind, str):
|
||||
raise ValueError("Invalid C3 record: missing n/kind")
|
||||
|
||||
if kind == "D_exact":
|
||||
k = rec.get("k")
|
||||
A_k = rec.get("A_k")
|
||||
C_k = rec.get("C_k")
|
||||
N0 = rec.get("N0")
|
||||
if not all(isinstance(x, int) for x in [k, A_k, C_k, N0]):
|
||||
raise ValueError(f"Invalid D_exact record for n={n}: missing k/A_k/C_k/N0")
|
||||
pref = prefix_data(n, k)
|
||||
if pref.A != A_k or pref.C != C_k:
|
||||
raise ValueError(f"D_exact mismatch for n={n}: prefix_data differs from record")
|
||||
m_stab = A_k + 1
|
||||
r_stab = _lift_to_stable_residue(
|
||||
n0=n,
|
||||
base_palier=palier,
|
||||
target_palier=m_stab,
|
||||
prefix_len=k,
|
||||
expected_word=pref.word,
|
||||
)
|
||||
pref_stab = prefix_data(r_stab, k)
|
||||
if pref_stab.word != pref.word or pref_stab.A != pref.A or pref_stab.C != pref.C:
|
||||
raise ValueError(f"D_exact lift check failed for n={n} at modulus 2^{m_stab}")
|
||||
|
||||
extracted.append(
|
||||
ExtractedClause(
|
||||
kind="D_exact",
|
||||
domain_palier=palier,
|
||||
source_n=n,
|
||||
stable_modulus_power=m_stab,
|
||||
stable_residue_mod_2p=r_stab,
|
||||
k_or_t=k,
|
||||
A=A_k,
|
||||
C=C_k,
|
||||
word=pref.word,
|
||||
N0=N0,
|
||||
a=None,
|
||||
y=None,
|
||||
preimage_m=None,
|
||||
DeltaF=None,
|
||||
Nf=None,
|
||||
source_csv=None,
|
||||
mate_exact=None,
|
||||
)
|
||||
)
|
||||
continue
|
||||
|
||||
if kind == "F":
|
||||
t = rec.get("t")
|
||||
a = rec.get("a")
|
||||
y = rec.get("y")
|
||||
preimage_m = rec.get("preimage_m")
|
||||
A_t = rec.get("A_t")
|
||||
C_t = rec.get("C_t")
|
||||
DeltaF = rec.get("DeltaF")
|
||||
Nf = rec.get("Nf")
|
||||
source_csv = rec.get("source_csv")
|
||||
ints_ok = all(isinstance(x, int) for x in [t, a, y, preimage_m, A_t, C_t, DeltaF, Nf])
|
||||
if not ints_ok or not isinstance(source_csv, str):
|
||||
raise ValueError(f"Invalid F record for n={n}: missing fields")
|
||||
pref = prefix_data(n, t)
|
||||
if pref.A != A_t or pref.C != C_t or pref.y != y:
|
||||
raise ValueError(f"F mismatch for n={n}: prefix_data differs from record")
|
||||
m_stab = A_t + 1
|
||||
r_stab = _lift_to_stable_residue(
|
||||
n0=n,
|
||||
base_palier=palier,
|
||||
target_palier=m_stab,
|
||||
prefix_len=t,
|
||||
expected_word=pref.word,
|
||||
)
|
||||
pref_stab = prefix_data(r_stab, t)
|
||||
if pref_stab.word != pref.word or pref_stab.A != pref.A or pref_stab.C != pref.C or pref_stab.y != pref.y:
|
||||
raise ValueError(f"F lift check failed for n={n} at modulus 2^{m_stab}")
|
||||
|
||||
extracted.append(
|
||||
ExtractedClause(
|
||||
kind="F",
|
||||
domain_palier=palier,
|
||||
source_n=n,
|
||||
stable_modulus_power=m_stab,
|
||||
stable_residue_mod_2p=r_stab,
|
||||
k_or_t=t,
|
||||
A=A_t,
|
||||
C=C_t,
|
||||
word=pref.word,
|
||||
N0=None,
|
||||
a=a,
|
||||
y=y,
|
||||
preimage_m=preimage_m,
|
||||
DeltaF=DeltaF,
|
||||
Nf=Nf,
|
||||
source_csv=source_csv,
|
||||
mate_exact=None,
|
||||
)
|
||||
)
|
||||
continue
|
||||
|
||||
if kind == "D_brother":
|
||||
k = rec.get("k")
|
||||
A_k = rec.get("A_k")
|
||||
C_k = rec.get("C_k")
|
||||
mate = rec.get("mate_exact")
|
||||
if not all(isinstance(x, int) for x in [k, A_k, C_k, mate]):
|
||||
raise ValueError(f"Invalid D_brother record for n={n}: missing fields")
|
||||
pref = prefix_data(n, k)
|
||||
if pref.A != A_k or pref.C != C_k:
|
||||
raise ValueError(f"D_brother mismatch for n={n}: prefix_data differs from record")
|
||||
extracted.append(
|
||||
ExtractedClause(
|
||||
kind="D_brother_local",
|
||||
domain_palier=palier,
|
||||
source_n=n,
|
||||
stable_modulus_power=None,
|
||||
stable_residue_mod_2p=None,
|
||||
k_or_t=k,
|
||||
A=A_k,
|
||||
C=C_k,
|
||||
word=pref.word,
|
||||
N0=None,
|
||||
a=None,
|
||||
y=None,
|
||||
preimage_m=None,
|
||||
DeltaF=None,
|
||||
Nf=None,
|
||||
source_csv=None,
|
||||
mate_exact=mate,
|
||||
)
|
||||
)
|
||||
continue
|
||||
|
||||
raise ValueError(f"Unknown record kind in C3 verification JSON: {kind}")
|
||||
|
||||
extracted = sorted(extracted, key=lambda c: (c.kind, c.source_n))
|
||||
max_stab = max([c.stable_modulus_power for c in extracted if c.stable_modulus_power is not None], default=None)
|
||||
|
||||
out_json = output_dir / "clauses_universelles.json"
|
||||
out_md = output_dir / "clauses_universelles.md"
|
||||
output_dir.mkdir(parents=True, exist_ok=True)
|
||||
|
||||
summary = {
|
||||
"inputs": {
|
||||
"verification_c3_local_descent_json": _display_path(verification_json, repo_root),
|
||||
},
|
||||
"domain": {"palier": palier, "max_stable_modulus_power": max_stab},
|
||||
"counts": {
|
||||
"total": len(extracted),
|
||||
"D_exact": sum(1 for c in extracted if c.kind == "D_exact"),
|
||||
"F": sum(1 for c in extracted if c.kind == "F"),
|
||||
"D_brother_local": sum(1 for c in extracted if c.kind == "D_brother_local"),
|
||||
},
|
||||
"clauses": [c.to_json() for c in extracted],
|
||||
}
|
||||
out_json.write_text(json.dumps(summary, indent=2, ensure_ascii=False) + "\n", encoding="utf-8")
|
||||
|
||||
# Markdown output (short, human-checkable)
|
||||
lines: list[str] = []
|
||||
lines.append("**Auteur** : Équipe 4NK")
|
||||
lines.append("")
|
||||
lines.append("# Clauses universelles extraites — Option A (Lift(B12))")
|
||||
lines.append("")
|
||||
lines.append("## Entrée")
|
||||
lines.append("")
|
||||
lines.append(f"- C3 vérification JSON : `{_display_path(verification_json, repo_root)}`")
|
||||
lines.append("")
|
||||
lines.append("## Domaine")
|
||||
lines.append("")
|
||||
lines.append(f"- palier (domaine des témoins) : 2^{palier}")
|
||||
if max_stab is not None:
|
||||
lines.append(f"- max(2^m_stable) observé : 2^{max_stab}")
|
||||
lines.append("")
|
||||
lines.append("## Compteurs")
|
||||
lines.append("")
|
||||
lines.append(f"- total : {summary['counts']['total']}")
|
||||
lines.append(f"- D_exact : {summary['counts']['D_exact']}")
|
||||
lines.append(f"- F : {summary['counts']['F']}")
|
||||
lines.append(f"- D_brother_local : {summary['counts']['D_brother_local']}")
|
||||
lines.append("")
|
||||
lines.append("## Table (extrait)")
|
||||
lines.append("")
|
||||
header = ["kind", "source_n", "m_stable", "residue_mod_2^m", "k/t", "A", "N0/Nf", "mate_exact"]
|
||||
lines.append("| " + " | ".join(header) + " |")
|
||||
lines.append("| " + " | ".join(["---"] * len(header)) + " |")
|
||||
for c in extracted:
|
||||
m_st = "" if c.stable_modulus_power is None else str(c.stable_modulus_power)
|
||||
r_st = "" if c.stable_residue_mod_2p is None else str(c.stable_residue_mod_2p)
|
||||
kt = "" if c.k_or_t is None else str(c.k_or_t)
|
||||
A = "" if c.A is None else str(c.A)
|
||||
if c.kind == "D_exact":
|
||||
thr = "" if c.N0 is None else f"N0={c.N0}"
|
||||
elif c.kind == "F":
|
||||
thr = "" if c.Nf is None else f"Nf={c.Nf}"
|
||||
else:
|
||||
thr = ""
|
||||
mate = "" if c.mate_exact is None else str(c.mate_exact)
|
||||
lines.append(f"| {c.kind} | {c.source_n} | {m_st} | {r_st} | {kt} | {A} | {thr} | {mate} |")
|
||||
lines.append("")
|
||||
lines.append("## Notes")
|
||||
lines.append("")
|
||||
lines.append("- `D_exact` et `F` sont relevées au module minimal \\(2^{A+1}\\) qui fige le mot de valuations du témoin.")
|
||||
lines.append("- `D_brother_local` encode une dépendance locale (palier du domaine) vers un `mate_exact` ; elle n’est pas utilisée ici comme clause universelle autonome.")
|
||||
lines.append("")
|
||||
out_md.write_text("\n".join(lines) + "\n", encoding="utf-8")
|
||||
|
||||
|
||||
def main() -> None:
|
||||
ap = argparse.ArgumentParser(description="Extract universal clause candidates from deterministic C3 witnesses (Option A)")
|
||||
ap.add_argument(
|
||||
"--verification-json",
|
||||
default="docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json",
|
||||
help="Path to deterministic C3 verification JSON",
|
||||
)
|
||||
ap.add_argument(
|
||||
"--output-dir",
|
||||
default="docs/artefacts/collatz/universal_clauses",
|
||||
help="Output directory for extracted clause artefacts (JSON + MD)",
|
||||
)
|
||||
ap.add_argument(
|
||||
"--repo-root",
|
||||
default="",
|
||||
help="Repository root used to display relative paths in outputs (defaults to current working directory)",
|
||||
)
|
||||
args = ap.parse_args()
|
||||
|
||||
repo_root = Path(args.repo_root).resolve() if args.repo_root.strip() else Path.cwd().resolve()
|
||||
run(
|
||||
verification_json=Path(args.verification_json).resolve(),
|
||||
output_dir=Path(args.output_dir).resolve(),
|
||||
repo_root=repo_root,
|
||||
)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
|
||||
@ -0,0 +1,339 @@
|
||||
#!/usr/bin/env python3
|
||||
# -*- coding: utf-8 -*-
|
||||
"""
|
||||
collatz_verify_universal_clauses.py
|
||||
|
||||
Deterministic verifier for the extracted clause artefact produced by
|
||||
collatz_extract_universal_clauses.py.
|
||||
|
||||
Scope (Option A):
|
||||
- check internal arithmetic consistency for each extracted D_exact / F clause
|
||||
against the originating C3 witness record
|
||||
- check deterministic lifting (stable residue) preserves the prefix word and
|
||||
affine constants on the canonical representative
|
||||
- check D_brother_local records point to an existing D_exact mate and match the
|
||||
"sister" relation at the domain palier (xor 2^(m-1))
|
||||
|
||||
Outputs:
|
||||
- docs/artefacts/collatz/universal_clauses/verification_universal_clauses.json
|
||||
- docs/artefacts/collatz/universal_clauses/verification_universal_clauses.md
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import json
|
||||
from pathlib import Path
|
||||
|
||||
from collatz_k_core import (
|
||||
N0_D,
|
||||
Nf_F,
|
||||
U_step,
|
||||
delta_F,
|
||||
fusion_choice_a,
|
||||
prefix_data,
|
||||
preimage_m,
|
||||
)
|
||||
|
||||
|
||||
def _read_json(path: Path) -> object:
|
||||
return json.loads(path.read_text(encoding="utf-8", errors="strict"))
|
||||
|
||||
|
||||
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 _req_int(obj: dict[str, object], key: str) -> int:
|
||||
v = obj.get(key)
|
||||
if not isinstance(v, int):
|
||||
raise ValueError(f"Expected int for {key}")
|
||||
return v
|
||||
|
||||
|
||||
def _opt_int(obj: dict[str, object], key: str) -> int | None:
|
||||
v = obj.get(key)
|
||||
if v is None:
|
||||
return None
|
||||
if not isinstance(v, int):
|
||||
raise ValueError(f"Expected int|null for {key}")
|
||||
return v
|
||||
|
||||
|
||||
def _opt_str(obj: dict[str, object], key: str) -> str | None:
|
||||
v = obj.get(key)
|
||||
if v is None:
|
||||
return None
|
||||
if not isinstance(v, str):
|
||||
raise ValueError(f"Expected str|null for {key}")
|
||||
return v
|
||||
|
||||
|
||||
def _opt_word(obj: dict[str, object], key: str) -> tuple[int, ...] | None:
|
||||
v = obj.get(key)
|
||||
if v is None:
|
||||
return None
|
||||
if not isinstance(v, list) or not all(isinstance(x, int) for x in v):
|
||||
raise ValueError(f"Expected list[int]|null for {key}")
|
||||
return tuple(v)
|
||||
|
||||
|
||||
def run(
|
||||
*,
|
||||
verification_json: Path,
|
||||
clauses_json: Path,
|
||||
output_dir: Path,
|
||||
repo_root: Path,
|
||||
) -> None:
|
||||
vobj = _read_json(verification_json)
|
||||
if not isinstance(vobj, dict):
|
||||
raise ValueError("Invalid C3 verification JSON: expected object")
|
||||
domain = vobj.get("domain")
|
||||
records = vobj.get("records")
|
||||
if not isinstance(domain, dict) or not isinstance(records, list):
|
||||
raise ValueError("Invalid C3 verification JSON: missing domain/records")
|
||||
palier = domain.get("palier")
|
||||
if not isinstance(palier, int):
|
||||
raise ValueError("Invalid C3 verification JSON: domain.palier must be int")
|
||||
|
||||
cobj = _read_json(clauses_json)
|
||||
if not isinstance(cobj, dict):
|
||||
raise ValueError("Invalid clauses JSON: expected object")
|
||||
clauses = cobj.get("clauses")
|
||||
if not isinstance(clauses, list) or not all(isinstance(x, dict) for x in clauses):
|
||||
raise ValueError("Invalid clauses JSON: missing clauses list")
|
||||
|
||||
by_source_n: dict[int, dict[str, object]] = {}
|
||||
for c in clauses:
|
||||
sn = c.get("source_n")
|
||||
if not isinstance(sn, int):
|
||||
raise ValueError("Invalid clause: missing source_n")
|
||||
if sn in by_source_n:
|
||||
raise ValueError(f"Duplicate source_n in clauses JSON: {sn}")
|
||||
by_source_n[sn] = c
|
||||
|
||||
by_record_n: dict[int, dict[str, object]] = {}
|
||||
for r in records:
|
||||
if not isinstance(r, dict):
|
||||
raise ValueError("Invalid C3 record: expected object")
|
||||
n = r.get("n")
|
||||
if not isinstance(n, int):
|
||||
raise ValueError("Invalid C3 record: missing n")
|
||||
if n in by_record_n:
|
||||
raise ValueError(f"Duplicate n in C3 records: {n}")
|
||||
by_record_n[n] = r
|
||||
|
||||
missing = sorted(set(by_record_n.keys()) - set(by_source_n.keys()))
|
||||
if missing:
|
||||
raise ValueError(f"Missing extracted clauses for {len(missing)} records (e.g. {missing[:20]})")
|
||||
|
||||
ok_records = 0
|
||||
kind_counts: dict[str, int] = {"D_exact": 0, "F": 0, "D_brother_local": 0}
|
||||
max_stable_mod: int | None = None
|
||||
|
||||
for n, r in by_record_n.items():
|
||||
c = by_source_n[n]
|
||||
kind = c.get("kind")
|
||||
if not isinstance(kind, str):
|
||||
raise ValueError(f"Invalid clause for n={n}: missing kind")
|
||||
if kind not in kind_counts:
|
||||
raise ValueError(f"Unknown clause kind for n={n}: {kind}")
|
||||
kind_counts[kind] += 1
|
||||
|
||||
domain_palier = _req_int(c, "domain_palier")
|
||||
if domain_palier != palier:
|
||||
raise ValueError(f"Clause domain_palier mismatch for n={n}: {domain_palier} != {palier}")
|
||||
|
||||
word = _opt_word(c, "word")
|
||||
A = _opt_int(c, "A")
|
||||
C = _opt_int(c, "C")
|
||||
k_or_t = _opt_int(c, "k_or_t")
|
||||
m_stab = _opt_int(c, "stable_modulus_power")
|
||||
r_stab = _opt_int(c, "stable_residue_mod_2p")
|
||||
if m_stab is not None:
|
||||
max_stable_mod = m_stab if max_stable_mod is None else max(max_stable_mod, m_stab)
|
||||
|
||||
if kind == "D_exact":
|
||||
if r.get("kind") != "D_exact":
|
||||
raise ValueError(f"Record kind mismatch for n={n}: expected D_exact")
|
||||
k = _req_int(r, "k")
|
||||
A_k = _req_int(r, "A_k")
|
||||
C_k = _req_int(r, "C_k")
|
||||
N0 = _req_int(r, "N0")
|
||||
if k_or_t != k or A != A_k or C != C_k:
|
||||
raise ValueError(f"D_exact clause params mismatch for n={n}")
|
||||
if m_stab is None or r_stab is None or word is None:
|
||||
raise ValueError(f"D_exact clause missing stability fields for n={n}")
|
||||
if m_stab != A_k + 1:
|
||||
raise ValueError(f"D_exact stable modulus mismatch for n={n}: {m_stab} != {A_k+1}")
|
||||
pref = prefix_data(n, k)
|
||||
if pref.word != word or pref.A != A_k or pref.C != C_k:
|
||||
raise ValueError(f"D_exact prefix mismatch for n={n}")
|
||||
pref_stab = prefix_data(r_stab, k)
|
||||
if pref_stab.word != word or pref_stab.A != A_k or pref_stab.C != C_k:
|
||||
raise ValueError(f"D_exact lift mismatch for n={n}")
|
||||
N0_calc = N0_D(C_k, A_k, k)
|
||||
if N0_calc != N0:
|
||||
raise ValueError(f"D_exact N0 mismatch for n={n}: {N0_calc} != {N0}")
|
||||
if n >= N0:
|
||||
next_n = prefix_data(n, k).y
|
||||
if not next_n < n:
|
||||
raise ValueError(f"D_exact descent failed on representative for n={n}: U^k(n)={next_n} not < n")
|
||||
ok_records += 1
|
||||
continue
|
||||
|
||||
if kind == "F":
|
||||
if r.get("kind") != "F":
|
||||
raise ValueError(f"Record kind mismatch for n={n}: expected F")
|
||||
t = _req_int(r, "t")
|
||||
a = _req_int(r, "a")
|
||||
y = _req_int(r, "y")
|
||||
pre_m = _req_int(r, "preimage_m")
|
||||
A_t = _req_int(r, "A_t")
|
||||
C_t = _req_int(r, "C_t")
|
||||
dF = _req_int(r, "DeltaF")
|
||||
Nf = _req_int(r, "Nf")
|
||||
src = r.get("source_csv")
|
||||
if not isinstance(src, str):
|
||||
raise ValueError(f"F record missing source_csv for n={n}")
|
||||
|
||||
a2 = _opt_int(c, "a")
|
||||
y2 = _opt_int(c, "y")
|
||||
pre2 = _opt_int(c, "preimage_m")
|
||||
dF2 = _opt_int(c, "DeltaF")
|
||||
Nf2 = _opt_int(c, "Nf")
|
||||
src2 = _opt_str(c, "source_csv")
|
||||
if (k_or_t, A, C, a2, y2, pre2, dF2, Nf2, src2) != (t, A_t, C_t, a, y, pre_m, dF, Nf, src):
|
||||
raise ValueError(f"F clause params mismatch for n={n}")
|
||||
if m_stab is None or r_stab is None or word is None:
|
||||
raise ValueError(f"F clause missing stability fields for n={n}")
|
||||
if m_stab != A_t + 1:
|
||||
raise ValueError(f"F stable modulus mismatch for n={n}: {m_stab} != {A_t+1}")
|
||||
|
||||
pref = prefix_data(n, t)
|
||||
if pref.word != word or pref.A != A_t or pref.C != C_t or pref.y != y:
|
||||
raise ValueError(f"F prefix mismatch for n={n}")
|
||||
pref_stab = prefix_data(r_stab, t)
|
||||
if pref_stab.word != word or pref_stab.A != A_t or pref_stab.C != C_t or pref_stab.y != y:
|
||||
raise ValueError(f"F lift mismatch for n={n}")
|
||||
|
||||
a_calc = fusion_choice_a(y)
|
||||
if a_calc is None or a_calc != a:
|
||||
raise ValueError(f"F a mismatch for n={n}: fusion_choice_a(y)={a_calc} != {a}")
|
||||
dF_calc = delta_F(A_t, t, a)
|
||||
if dF_calc != dF:
|
||||
raise ValueError(f"F DeltaF mismatch for n={n}: {dF_calc} != {dF}")
|
||||
Nf_calc = Nf_F(C_t, A_t, t, a)
|
||||
if Nf_calc != Nf:
|
||||
raise ValueError(f"F Nf mismatch for n={n}: {Nf_calc} != {Nf}")
|
||||
pre_calc = preimage_m(y, a)
|
||||
if pre_calc != pre_m:
|
||||
raise ValueError(f"F preimage mismatch for n={n}: {pre_calc} != {pre_m}")
|
||||
um, _ = U_step(pre_m)
|
||||
if um != y:
|
||||
raise ValueError(f"F witness failed for n={n}: U(preimage_m)={um} != y={y}")
|
||||
if n >= Nf and not (pre_m < n):
|
||||
raise ValueError(f"F m<n failed on representative for n={n}: m={pre_m} >= n")
|
||||
ok_records += 1
|
||||
continue
|
||||
|
||||
if kind == "D_brother_local":
|
||||
if r.get("kind") != "D_brother":
|
||||
raise ValueError(f"Record kind mismatch for n={n}: expected D_brother")
|
||||
mate = _req_int(r, "mate_exact")
|
||||
mate2 = _opt_int(c, "mate_exact")
|
||||
if mate2 != mate:
|
||||
raise ValueError(f"D_brother_local mate mismatch for n={n}")
|
||||
shift = 1 << (palier - 1)
|
||||
if (n ^ shift) != mate:
|
||||
raise ValueError(f"D_brother_local mate relation mismatch for n={n}: n^2^(m-1) != mate_exact")
|
||||
mate_rec = by_record_n.get(mate)
|
||||
if not isinstance(mate_rec, dict) or mate_rec.get("kind") != "D_exact":
|
||||
raise ValueError(f"D_brother_local mate is not a D_exact record for n={n}: mate={mate}")
|
||||
ok_records += 1
|
||||
continue
|
||||
|
||||
raise ValueError(f"Unhandled kind for n={n}: {kind}")
|
||||
|
||||
output_dir.mkdir(parents=True, exist_ok=True)
|
||||
out_json = output_dir / "verification_universal_clauses.json"
|
||||
out_md = output_dir / "verification_universal_clauses.md"
|
||||
|
||||
summary = {
|
||||
"inputs": {
|
||||
"verification_c3_local_descent_json": _display_path(verification_json, repo_root),
|
||||
"clauses_universelles_json": _display_path(clauses_json, repo_root),
|
||||
},
|
||||
"domain": {"palier": palier, "max_stable_modulus_power": max_stable_mod},
|
||||
"counts": {"ok_records": ok_records, **kind_counts},
|
||||
"ok": True,
|
||||
}
|
||||
out_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 — clauses universelles extraites (Option A)")
|
||||
lines.append("")
|
||||
lines.append("## Entrées")
|
||||
lines.append("")
|
||||
lines.append(f"- C3 vérification JSON : `{_display_path(verification_json, repo_root)}`")
|
||||
lines.append(f"- clauses JSON : `{_display_path(clauses_json, repo_root)}`")
|
||||
lines.append("")
|
||||
lines.append("## Résultat")
|
||||
lines.append("")
|
||||
lines.append(f"- ok : {summary['ok']}")
|
||||
lines.append(f"- palier (domaine) : 2^{palier}")
|
||||
if max_stable_mod is not None:
|
||||
lines.append(f"- max(2^m_stable) observé : 2^{max_stable_mod}")
|
||||
lines.append("")
|
||||
lines.append("## Compteurs")
|
||||
lines.append("")
|
||||
lines.append(f"- ok_records : {ok_records}")
|
||||
lines.append(f"- D_exact : {kind_counts['D_exact']}")
|
||||
lines.append(f"- F : {kind_counts['F']}")
|
||||
lines.append(f"- D_brother_local : {kind_counts['D_brother_local']}")
|
||||
lines.append("")
|
||||
out_md.write_text("\n".join(lines) + "\n", encoding="utf-8")
|
||||
|
||||
|
||||
def main() -> None:
|
||||
ap = argparse.ArgumentParser(description="Verify extracted universal clauses (Option A)")
|
||||
ap.add_argument(
|
||||
"--verification-json",
|
||||
default="docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json",
|
||||
help="Path to deterministic C3 verification JSON",
|
||||
)
|
||||
ap.add_argument(
|
||||
"--clauses-json",
|
||||
default="docs/artefacts/collatz/universal_clauses/clauses_universelles.json",
|
||||
help="Path to extracted clauses JSON",
|
||||
)
|
||||
ap.add_argument(
|
||||
"--output-dir",
|
||||
default="docs/artefacts/collatz/universal_clauses",
|
||||
help="Output directory for verification artefacts (JSON + MD)",
|
||||
)
|
||||
ap.add_argument(
|
||||
"--repo-root",
|
||||
default="",
|
||||
help="Repository root used to display relative paths in outputs (defaults to current working directory)",
|
||||
)
|
||||
args = ap.parse_args()
|
||||
|
||||
repo_root = Path(args.repo_root).resolve() if args.repo_root.strip() else Path.cwd().resolve()
|
||||
run(
|
||||
verification_json=Path(args.verification_json).resolve(),
|
||||
clauses_json=Path(args.clauses_json).resolve(),
|
||||
output_dir=Path(args.output_dir).resolve(),
|
||||
repo_root=repo_root,
|
||||
)
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
main()
|
||||
|
||||
13360
docs/artefacts/collatz/universal_clauses/clauses_universelles.json
Normal file
13360
docs/artefacts/collatz/universal_clauses/clauses_universelles.json
Normal file
File diff suppressed because it is too large
Load Diff
414
docs/artefacts/collatz/universal_clauses/clauses_universelles.md
Normal file
414
docs/artefacts/collatz/universal_clauses/clauses_universelles.md
Normal file
@ -0,0 +1,414 @@
|
||||
**Auteur** : Équipe 4NK
|
||||
|
||||
# Clauses universelles extraites — Option A (Lift(B12))
|
||||
|
||||
## Entrée
|
||||
|
||||
- C3 vérification JSON : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`
|
||||
|
||||
## Domaine
|
||||
|
||||
- palier (domaine des témoins) : 2^13
|
||||
- max(2^m_stable) observé : 2^85
|
||||
|
||||
## Compteurs
|
||||
|
||||
- total : 384
|
||||
- D_exact : 27
|
||||
- F : 330
|
||||
- D_brother_local : 27
|
||||
|
||||
## Table (extrait)
|
||||
|
||||
| kind | source_n | m_stable | residue_mod_2^m | k/t | A | N0/Nf | mate_exact |
|
||||
| --- | --- | --- | --- | --- | --- | --- | --- |
|
||||
| D_brother_local | 127 | | | 8 | 12 | | 4223 |
|
||||
| D_brother_local | 359 | | | 8 | 12 | | 4455 |
|
||||
| D_brother_local | 763 | | | 8 | 12 | | 4859 |
|
||||
| D_brother_local | 831 | | | 8 | 12 | | 4927 |
|
||||
| D_brother_local | 1095 | | | 8 | 12 | | 5191 |
|
||||
| D_brother_local | 1275 | | | 8 | 12 | | 5371 |
|
||||
| D_brother_local | 1343 | | | 8 | 12 | | 5439 |
|
||||
| D_brother_local | 1775 | | | 8 | 12 | | 5871 |
|
||||
| D_brother_local | 2119 | | | 8 | 12 | | 6215 |
|
||||
| D_brother_local | 2651 | | | 8 | 12 | | 6747 |
|
||||
| D_brother_local | 2719 | | | 8 | 12 | | 6815 |
|
||||
| D_brother_local | 2983 | | | 8 | 12 | | 7079 |
|
||||
| D_brother_local | 3163 | | | 8 | 12 | | 7259 |
|
||||
| D_brother_local | 3303 | | | 8 | 12 | | 7399 |
|
||||
| D_brother_local | 3815 | | | 8 | 12 | | 7911 |
|
||||
| D_brother_local | 4007 | | | 8 | 12 | | 8103 |
|
||||
| D_brother_local | 4351 | | | 8 | 12 | | 255 |
|
||||
| D_brother_local | 4635 | | | 8 | 12 | | 539 |
|
||||
| D_brother_local | 4775 | | | 8 | 12 | | 679 |
|
||||
| D_brother_local | 5287 | | | 8 | 12 | | 1191 |
|
||||
| D_brother_local | 5659 | | | 8 | 12 | | 1563 |
|
||||
| D_brother_local | 6079 | | | 8 | 12 | | 1983 |
|
||||
| D_brother_local | 6171 | | | 8 | 12 | | 2075 |
|
||||
| D_brother_local | 6191 | | | 8 | 12 | | 2095 |
|
||||
| D_brother_local | 6703 | | | 8 | 12 | | 2607 |
|
||||
| D_brother_local | 7135 | | | 8 | 12 | | 3039 |
|
||||
| D_brother_local | 7647 | | | 8 | 12 | | 3551 |
|
||||
| D_exact | 255 | 14 | 255 | 8 | 13 | N0=4 | |
|
||||
| D_exact | 539 | 14 | 539 | 8 | 13 | N0=7 | |
|
||||
| D_exact | 679 | 14 | 679 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 1191 | 14 | 1191 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 1563 | 14 | 1563 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 1983 | 14 | 1983 | 8 | 13 | N0=5 | |
|
||||
| D_exact | 2075 | 14 | 2075 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 2095 | 14 | 2095 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 2607 | 14 | 2607 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 3039 | 14 | 3039 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 3551 | 14 | 3551 | 8 | 13 | N0=5 | |
|
||||
| D_exact | 4223 | 14 | 4223 | 8 | 13 | N0=4 | |
|
||||
| D_exact | 4455 | 14 | 4455 | 8 | 13 | N0=5 | |
|
||||
| D_exact | 4859 | 14 | 4859 | 8 | 13 | N0=8 | |
|
||||
| D_exact | 4927 | 14 | 4927 | 8 | 13 | N0=5 | |
|
||||
| D_exact | 5191 | 14 | 5191 | 8 | 13 | N0=8 | |
|
||||
| D_exact | 5371 | 14 | 5371 | 8 | 13 | N0=7 | |
|
||||
| D_exact | 5439 | 14 | 5439 | 8 | 13 | N0=5 | |
|
||||
| D_exact | 5871 | 14 | 5871 | 8 | 13 | N0=5 | |
|
||||
| D_exact | 6215 | 14 | 6215 | 8 | 13 | N0=7 | |
|
||||
| D_exact | 6747 | 14 | 6747 | 8 | 13 | N0=7 | |
|
||||
| D_exact | 6815 | 14 | 6815 | 8 | 13 | N0=5 | |
|
||||
| D_exact | 7079 | 14 | 7079 | 8 | 13 | N0=8 | |
|
||||
| D_exact | 7259 | 14 | 7259 | 8 | 13 | N0=7 | |
|
||||
| D_exact | 7399 | 14 | 7399 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 7911 | 14 | 7911 | 8 | 13 | N0=6 | |
|
||||
| D_exact | 8103 | 14 | 8103 | 8 | 13 | N0=7 | |
|
||||
| F | 27 | 60 | 27 | 37 | 59 | Nf=2 | |
|
||||
| F | 31 | 57 | 31 | 35 | 56 | Nf=2 | |
|
||||
| F | 47 | 56 | 47 | 34 | 55 | Nf=1 | |
|
||||
| F | 63 | 58 | 63 | 35 | 57 | Nf=1 | |
|
||||
| F | 71 | 55 | 71 | 33 | 54 | Nf=1 | |
|
||||
| F | 91 | 46 | 91 | 28 | 45 | Nf=16 | |
|
||||
| F | 103 | 43 | 103 | 26 | 42 | Nf=8 | |
|
||||
| F | 111 | 32 | 111 | 19 | 31 | Nf=4 | |
|
||||
| F | 159 | 23 | 159 | 13 | 22 | Nf=1 | |
|
||||
| F | 167 | 31 | 167 | 18 | 30 | Nf=2 | |
|
||||
| F | 191 | 18 | 191 | 9 | 17 | Nf=1 | |
|
||||
| F | 223 | 33 | 223 | 19 | 32 | Nf=1 | |
|
||||
| F | 239 | 22 | 239 | 12 | 21 | Nf=1 | |
|
||||
| F | 251 | 30 | 251 | 17 | 29 | Nf=1 | |
|
||||
| F | 283 | 27 | 283 | 15 | 26 | Nf=1 | |
|
||||
| F | 303 | 19 | 303 | 9 | 18 | Nf=1 | |
|
||||
| F | 319 | 24 | 319 | 13 | 23 | Nf=1 | |
|
||||
| F | 327 | 23 | 327 | 13 | 22 | Nf=1 | |
|
||||
| F | 415 | 17 | 415 | 9 | 16 | Nf=1 | |
|
||||
| F | 447 | 42 | 447 | 25 | 41 | Nf=1 | |
|
||||
| F | 479 | 19 | 479 | 11 | 18 | Nf=15 | |
|
||||
| F | 495 | 29 | 495 | 17 | 28 | Nf=1 | |
|
||||
| F | 511 | 20 | 511 | 11 | 19 | Nf=1 | |
|
||||
| F | 559 | 19 | 559 | 11 | 18 | Nf=14 | |
|
||||
| F | 603 | 17 | 603 | 10 | 16 | Nf=2 | |
|
||||
| F | 623 | 19 | 623 | 9 | 18 | Nf=1 | |
|
||||
| F | 639 | 24 | 639 | 14 | 23 | Nf=1 | |
|
||||
| F | 667 | 27 | 667 | 15 | 26 | Nf=1 | |
|
||||
| F | 671 | 23 | 671 | 14 | 22 | Nf=4 | |
|
||||
| F | 703 | 84 | 703 | 51 | 83 | Nf=1 | |
|
||||
| F | 743 | 28 | 743 | 16 | 27 | Nf=1 | |
|
||||
| F | 751 | 24 | 751 | 13 | 23 | Nf=1 | |
|
||||
| F | 767 | 19 | 767 | 10 | 18 | Nf=1 | |
|
||||
| F | 795 | 28 | 795 | 17 | 27 | Nf=3 | |
|
||||
| F | 839 | 16 | 839 | 9 | 15 | Nf=6 | |
|
||||
| F | 859 | 20 | 859 | 10 | 19 | Nf=1 | |
|
||||
| F | 871 | 36 | 871 | 22 | 35 | Nf=2 | |
|
||||
| F | 895 | 25 | 895 | 15 | 24 | Nf=2 | |
|
||||
| F | 927 | 38 | 927 | 23 | 37 | Nf=28 | |
|
||||
| F | 959 | 23 | 959 | 13 | 22 | Nf=1 | |
|
||||
| F | 991 | 27 | 991 | 16 | 26 | Nf=10 | |
|
||||
| F | 1007 | 22 | 1007 | 13 | 21 | Nf=2 | |
|
||||
| F | 1023 | 21 | 1023 | 11 | 20 | Nf=1 | |
|
||||
| F | 1051 | 20 | 1051 | 12 | 19 | Nf=3 | |
|
||||
| F | 1055 | 83 | 1055 | 50 | 82 | Nf=1 | |
|
||||
| F | 1115 | 24 | 1115 | 14 | 23 | Nf=6 | |
|
||||
| F | 1127 | 23 | 1127 | 12 | 22 | Nf=1 | |
|
||||
| F | 1135 | 16 | 1135 | 9 | 15 | Nf=1 | |
|
||||
| F | 1151 | 18 | 1151 | 9 | 17 | Nf=1 | |
|
||||
| F | 1179 | 20 | 1179 | 10 | 19 | Nf=1 | |
|
||||
| F | 1183 | 17 | 1183 | 10 | 16 | Nf=1 | |
|
||||
| F | 1215 | 16 | 1215 | 9 | 15 | Nf=1 | |
|
||||
| F | 1247 | 20 | 1247 | 9 | 19 | Nf=1 | |
|
||||
| F | 1255 | 21 | 1255 | 12 | 20 | Nf=3 | |
|
||||
| F | 1263 | 27 | 1263 | 16 | 26 | Nf=6 | |
|
||||
| F | 1279 | 25 | 1279 | 14 | 24 | Nf=1 | |
|
||||
| F | 1307 | 35 | 1307 | 21 | 34 | Nf=1 | |
|
||||
| F | 1327 | 21 | 1327 | 9 | 20 | Nf=1 | |
|
||||
| F | 1351 | 15 | 1351 | 9 | 14 | Nf=5 | |
|
||||
| F | 1383 | 43 | 1383 | 24 | 42 | Nf=1 | |
|
||||
| F | 1407 | 85 | 1407 | 51 | 84 | Nf=1 | |
|
||||
| F | 1439 | 22 | 1439 | 12 | 21 | Nf=1 | |
|
||||
| F | 1471 | 32 | 1471 | 19 | 31 | Nf=1 | |
|
||||
| F | 1503 | 25 | 1503 | 13 | 24 | Nf=1 | |
|
||||
| F | 1519 | 18 | 1519 | 10 | 17 | Nf=2 | |
|
||||
| F | 1535 | 20 | 1535 | 10 | 19 | Nf=1 | |
|
||||
| F | 1567 | 20 | 1567 | 9 | 19 | Nf=1 | |
|
||||
| F | 1583 | 82 | 1583 | 49 | 81 | Nf=1 | |
|
||||
| F | 1639 | 37 | 1639 | 23 | 36 | Nf=25 | |
|
||||
| F | 1663 | 18 | 1663 | 11 | 17 | Nf=7 | |
|
||||
| F | 1691 | 22 | 1691 | 11 | 21 | Nf=1 | |
|
||||
| F | 1695 | 34 | 1695 | 20 | 33 | Nf=1 | |
|
||||
| F | 1727 | 20 | 1727 | 9 | 19 | Nf=1 | |
|
||||
| F | 1767 | 20 | 1767 | 12 | 19 | Nf=3 | |
|
||||
| F | 1791 | 19 | 1791 | 11 | 18 | Nf=1 | |
|
||||
| F | 1819 | 62 | 1819 | 38 | 61 | Nf=1 | |
|
||||
| F | 1883 | 20 | 1883 | 11 | 19 | Nf=2 | |
|
||||
| F | 1895 | 26 | 1895 | 15 | 25 | Nf=2 | |
|
||||
| F | 1919 | 24 | 1919 | 13 | 23 | Nf=1 | |
|
||||
| F | 1951 | 18 | 1951 | 11 | 17 | Nf=12 | |
|
||||
| F | 1959 | 28 | 1959 | 16 | 27 | Nf=1 | |
|
||||
| F | 2043 | 20 | 2043 | 11 | 19 | Nf=2 | |
|
||||
| F | 2047 | 59 | 2047 | 36 | 58 | Nf=1 | |
|
||||
| F | 2079 | 17 | 2079 | 9 | 16 | Nf=1 | |
|
||||
| F | 2111 | 84 | 2111 | 50 | 83 | Nf=1 | |
|
||||
| F | 2139 | 21 | 2139 | 12 | 20 | Nf=1 | |
|
||||
| F | 2151 | 42 | 2151 | 26 | 41 | Nf=7 | |
|
||||
| F | 2159 | 21 | 2159 | 11 | 20 | Nf=1 | |
|
||||
| F | 2175 | 21 | 2175 | 12 | 20 | Nf=1 | |
|
||||
| F | 2207 | 31 | 2207 | 18 | 30 | Nf=1 | |
|
||||
| F | 2215 | 45 | 2215 | 27 | 44 | Nf=2 | |
|
||||
| F | 2271 | 17 | 2271 | 9 | 16 | Nf=1 | |
|
||||
| F | 2287 | 54 | 2287 | 31 | 53 | Nf=1 | |
|
||||
| F | 2299 | 17 | 2299 | 9 | 16 | Nf=1 | |
|
||||
| F | 2303 | 19 | 2303 | 9 | 18 | Nf=1 | |
|
||||
| F | 2331 | 17 | 2331 | 9 | 16 | Nf=1 | |
|
||||
| F | 2367 | 18 | 2367 | 10 | 17 | Nf=1 | |
|
||||
| F | 2375 | 29 | 2375 | 18 | 28 | Nf=49 | |
|
||||
| F | 2407 | 18 | 2407 | 10 | 17 | Nf=1 | |
|
||||
| F | 2463 | 23 | 2463 | 13 | 22 | Nf=2 | |
|
||||
| F | 2495 | 17 | 2495 | 10 | 16 | Nf=1 | |
|
||||
| F | 2527 | 28 | 2527 | 16 | 27 | Nf=1 | |
|
||||
| F | 2543 | 30 | 2543 | 18 | 29 | Nf=59 | |
|
||||
| F | 2559 | 41 | 2559 | 25 | 40 | Nf=1 | |
|
||||
| F | 2663 | 16 | 2663 | 9 | 15 | Nf=1 | |
|
||||
| F | 2671 | 20 | 2671 | 10 | 19 | Nf=1 | |
|
||||
| F | 2687 | 18 | 2687 | 10 | 17 | Nf=1 | |
|
||||
| F | 2715 | 34 | 2715 | 20 | 33 | Nf=1 | |
|
||||
| F | 2727 | 16 | 2727 | 9 | 15 | Nf=5 | |
|
||||
| F | 2751 | 44 | 2751 | 27 | 43 | Nf=3 | |
|
||||
| F | 2791 | 19 | 2791 | 10 | 18 | Nf=1 | |
|
||||
| F | 2799 | 17 | 2799 | 9 | 16 | Nf=1 | |
|
||||
| F | 2811 | 19 | 2811 | 11 | 18 | Nf=2 | |
|
||||
| F | 2815 | 15 | 2815 | 9 | 14 | Nf=3 | |
|
||||
| F | 2843 | 25 | 2843 | 14 | 24 | Nf=1 | |
|
||||
| F | 2879 | 18 | 2879 | 11 | 17 | Nf=10 | |
|
||||
| F | 2887 | 17 | 2887 | 10 | 16 | Nf=3 | |
|
||||
| F | 2919 | 18 | 2919 | 11 | 17 | Nf=10 | |
|
||||
| F | 2943 | 30 | 2943 | 18 | 29 | Nf=36 | |
|
||||
| F | 3007 | 23 | 3007 | 14 | 22 | Nf=5 | |
|
||||
| F | 3055 | 31 | 3055 | 18 | 30 | Nf=1 | |
|
||||
| F | 3067 | 18 | 3067 | 9 | 17 | Nf=1 | |
|
||||
| F | 3071 | 50 | 3071 | 31 | 49 | Nf=3 | |
|
||||
| F | 3099 | 20 | 3099 | 12 | 19 | Nf=3 | |
|
||||
| F | 3103 | 20 | 3103 | 11 | 19 | Nf=1 | |
|
||||
| F | 3135 | 21 | 3135 | 9 | 20 | Nf=1 | |
|
||||
| F | 3175 | 43 | 3175 | 26 | 42 | Nf=11 | |
|
||||
| F | 3183 | 22 | 3183 | 11 | 21 | Nf=1 | |
|
||||
| F | 3199 | 18 | 3199 | 11 | 17 | Nf=7 | |
|
||||
| F | 3227 | 41 | 3227 | 25 | 40 | Nf=3 | |
|
||||
| F | 3231 | 24 | 3231 | 14 | 23 | Nf=3 | |
|
||||
| F | 3239 | 15 | 3239 | 9 | 14 | Nf=5 | |
|
||||
| F | 3263 | 20 | 3263 | 11 | 19 | Nf=1 | |
|
||||
| F | 3311 | 27 | 3311 | 16 | 26 | Nf=9 | |
|
||||
| F | 3323 | 44 | 3323 | 26 | 43 | Nf=2 | |
|
||||
| F | 3327 | 19 | 3327 | 11 | 18 | Nf=1 | |
|
||||
| F | 3355 | 25 | 3355 | 13 | 24 | Nf=1 | |
|
||||
| F | 3375 | 20 | 3375 | 11 | 19 | Nf=1 | |
|
||||
| F | 3391 | 30 | 3391 | 18 | 29 | Nf=61 | |
|
||||
| F | 3399 | 49 | 3399 | 30 | 48 | Nf=3 | |
|
||||
| F | 3431 | 37 | 3431 | 23 | 36 | Nf=17 | |
|
||||
| F | 3455 | 21 | 3455 | 9 | 20 | Nf=1 | |
|
||||
| F | 3487 | 17 | 3487 | 10 | 16 | Nf=2 | |
|
||||
| F | 3519 | 25 | 3519 | 15 | 24 | Nf=2 | |
|
||||
| F | 3567 | 31 | 3567 | 19 | 30 | Nf=4 | |
|
||||
| F | 3583 | 20 | 3583 | 11 | 19 | Nf=1 | |
|
||||
| F | 3611 | 17 | 3611 | 9 | 16 | Nf=1 | |
|
||||
| F | 3615 | 21 | 3615 | 11 | 20 | Nf=1 | |
|
||||
| F | 3631 | 29 | 3631 | 18 | 28 | Nf=37 | |
|
||||
| F | 3687 | 19 | 3687 | 9 | 18 | Nf=1 | |
|
||||
| F | 3711 | 38 | 3711 | 23 | 37 | Nf=1 | |
|
||||
| F | 3739 | 41 | 3739 | 24 | 40 | Nf=1 | |
|
||||
| F | 3743 | 16 | 3743 | 9 | 15 | Nf=1 | |
|
||||
| F | 3775 | 22 | 3775 | 11 | 21 | Nf=1 | |
|
||||
| F | 3823 | 26 | 3823 | 16 | 25 | Nf=10 | |
|
||||
| F | 3839 | 37 | 3839 | 23 | 36 | Nf=10 | |
|
||||
| F | 3867 | 25 | 3867 | 14 | 24 | Nf=1 | |
|
||||
| F | 3931 | 27 | 3931 | 15 | 26 | Nf=1 | |
|
||||
| F | 3943 | 46 | 3943 | 25 | 45 | Nf=1 | |
|
||||
| F | 3967 | 20 | 3967 | 9 | 19 | Nf=1 | |
|
||||
| F | 3999 | 20 | 3999 | 12 | 19 | Nf=2 | |
|
||||
| F | 4031 | 17 | 4031 | 9 | 16 | Nf=1 | |
|
||||
| F | 4079 | 18 | 4079 | 9 | 17 | Nf=1 | |
|
||||
| F | 4091 | 16 | 4091 | 9 | 15 | Nf=2 | |
|
||||
| F | 4095 | 52 | 4095 | 32 | 51 | Nf=2 | |
|
||||
| F | 4123 | 15 | 4123 | 9 | 14 | Nf=5 | |
|
||||
| F | 4127 | 43 | 4127 | 26 | 42 | Nf=2 | |
|
||||
| F | 4143 | 15 | 4143 | 9 | 14 | Nf=5 | |
|
||||
| F | 4159 | 18 | 4159 | 9 | 17 | Nf=1 | |
|
||||
| F | 4167 | 21 | 4167 | 12 | 20 | Nf=4 | |
|
||||
| F | 4187 | 18 | 4187 | 9 | 17 | Nf=1 | |
|
||||
| F | 4199 | 18 | 4199 | 9 | 17 | Nf=1 | |
|
||||
| F | 4207 | 38 | 4207 | 22 | 37 | Nf=1 | |
|
||||
| F | 4255 | 71 | 4255 | 44 | 70 | Nf=2 | |
|
||||
| F | 4263 | 58 | 4263 | 35 | 57 | Nf=1 | |
|
||||
| F | 4287 | 20 | 4287 | 9 | 19 | Nf=1 | |
|
||||
| F | 4319 | 17 | 4319 | 10 | 16 | Nf=2 | |
|
||||
| F | 4335 | 18 | 4335 | 11 | 17 | Nf=12 | |
|
||||
| F | 4347 | 48 | 4347 | 30 | 47 | Nf=138 | |
|
||||
| F | 4379 | 17 | 4379 | 10 | 16 | Nf=2 | |
|
||||
| F | 4399 | 34 | 4399 | 20 | 33 | Nf=1 | |
|
||||
| F | 4415 | 29 | 4415 | 17 | 28 | Nf=3 | |
|
||||
| F | 4423 | 24 | 4423 | 13 | 23 | Nf=1 | |
|
||||
| F | 4511 | 21 | 4511 | 12 | 20 | Nf=2 | |
|
||||
| F | 4543 | 15 | 4543 | 9 | 14 | Nf=3 | |
|
||||
| F | 4575 | 39 | 4575 | 24 | 38 | Nf=4 | |
|
||||
| F | 4591 | 66 | 4591 | 41 | 65 | Nf=4 | |
|
||||
| F | 4607 | 49 | 4607 | 30 | 48 | Nf=1 | |
|
||||
| F | 4655 | 16 | 4655 | 9 | 15 | Nf=4 | |
|
||||
| F | 4699 | 23 | 4699 | 13 | 22 | Nf=1 | |
|
||||
| F | 4719 | 26 | 4719 | 14 | 25 | Nf=1 | |
|
||||
| F | 4735 | 18 | 4735 | 11 | 17 | Nf=7 | |
|
||||
| F | 4763 | 26 | 4763 | 16 | 25 | Nf=10 | |
|
||||
| F | 4767 | 24 | 4767 | 14 | 23 | Nf=5 | |
|
||||
| F | 4799 | 17 | 4799 | 10 | 16 | Nf=1 | |
|
||||
| F | 4839 | 20 | 4839 | 12 | 19 | Nf=4 | |
|
||||
| F | 4847 | 23 | 4847 | 13 | 22 | Nf=1 | |
|
||||
| F | 4863 | 36 | 4863 | 21 | 35 | Nf=1 | |
|
||||
| F | 4891 | 45 | 4891 | 28 | 44 | Nf=22 | |
|
||||
| F | 4935 | 24 | 4935 | 14 | 23 | Nf=6 | |
|
||||
| F | 4955 | 17 | 4955 | 9 | 16 | Nf=2 | |
|
||||
| F | 4967 | 26 | 4967 | 15 | 25 | Nf=3 | |
|
||||
| F | 4991 | 18 | 4991 | 10 | 17 | Nf=1 | |
|
||||
| F | 5023 | 18 | 5023 | 9 | 17 | Nf=1 | |
|
||||
| F | 5055 | 24 | 5055 | 13 | 23 | Nf=1 | |
|
||||
| F | 5087 | 15 | 5087 | 9 | 14 | Nf=5 | |
|
||||
| F | 5103 | 18 | 5103 | 9 | 17 | Nf=1 | |
|
||||
| F | 5119 | 39 | 5119 | 24 | 38 | Nf=2 | |
|
||||
| F | 5147 | 36 | 5147 | 22 | 35 | Nf=3 | |
|
||||
| F | 5151 | 34 | 5151 | 21 | 33 | Nf=7 | |
|
||||
| F | 5211 | 22 | 5211 | 12 | 21 | Nf=1 | |
|
||||
| F | 5223 | 18 | 5223 | 11 | 17 | Nf=11 | |
|
||||
| F | 5231 | 16 | 5231 | 9 | 15 | Nf=1 | |
|
||||
| F | 5247 | 23 | 5247 | 12 | 22 | Nf=1 | |
|
||||
| F | 5275 | 17 | 5275 | 9 | 16 | Nf=2 | |
|
||||
| F | 5279 | 24 | 5279 | 14 | 23 | Nf=1 | |
|
||||
| F | 5311 | 16 | 5311 | 9 | 15 | Nf=1 | |
|
||||
| F | 5343 | 21 | 5343 | 10 | 20 | Nf=1 | |
|
||||
| F | 5351 | 30 | 5351 | 18 | 29 | Nf=2 | |
|
||||
| F | 5359 | 23 | 5359 | 14 | 22 | Nf=4 | |
|
||||
| F | 5375 | 19 | 5375 | 10 | 18 | Nf=1 | |
|
||||
| F | 5403 | 22 | 5403 | 13 | 21 | Nf=2 | |
|
||||
| F | 5423 | 20 | 5423 | 10 | 19 | Nf=1 | |
|
||||
| F | 5447 | 28 | 5447 | 17 | 27 | Nf=3 | |
|
||||
| F | 5479 | 26 | 5479 | 16 | 25 | Nf=8 | |
|
||||
| F | 5503 | 42 | 5503 | 26 | 41 | Nf=11 | |
|
||||
| F | 5535 | 28 | 5535 | 17 | 27 | Nf=2 | |
|
||||
| F | 5567 | 37 | 5567 | 22 | 36 | Nf=1 | |
|
||||
| F | 5599 | 18 | 5599 | 9 | 17 | Nf=1 | |
|
||||
| F | 5615 | 17 | 5615 | 9 | 16 | Nf=1 | |
|
||||
| F | 5631 | 16 | 5631 | 9 | 15 | Nf=1 | |
|
||||
| F | 5663 | 21 | 5663 | 10 | 20 | Nf=1 | |
|
||||
| F | 5679 | 21 | 5679 | 12 | 20 | Nf=1 | |
|
||||
| F | 5735 | 25 | 5735 | 15 | 24 | Nf=3 | |
|
||||
| F | 5759 | 36 | 5759 | 22 | 35 | Nf=2 | |
|
||||
| F | 5787 | 17 | 5787 | 9 | 16 | Nf=1 | |
|
||||
| F | 5791 | 33 | 5791 | 20 | 32 | Nf=2 | |
|
||||
| F | 5823 | 24 | 5823 | 10 | 23 | Nf=1 | |
|
||||
| F | 5863 | 19 | 5863 | 10 | 18 | Nf=1 | |
|
||||
| F | 5887 | 27 | 5887 | 15 | 26 | Nf=1 | |
|
||||
| F | 5915 | 45 | 5915 | 24 | 44 | Nf=1 | |
|
||||
| F | 5979 | 16 | 5979 | 9 | 15 | Nf=2 | |
|
||||
| F | 5991 | 29 | 5991 | 16 | 28 | Nf=1 | |
|
||||
| F | 6015 | 23 | 6015 | 13 | 22 | Nf=1 | |
|
||||
| F | 6047 | 17 | 6047 | 9 | 16 | Nf=1 | |
|
||||
| F | 6055 | 19 | 6055 | 11 | 18 | Nf=14 | |
|
||||
| F | 6139 | 20 | 6139 | 11 | 19 | Nf=1 | |
|
||||
| F | 6143 | 51 | 6143 | 31 | 50 | Nf=1 | |
|
||||
| F | 6175 | 17 | 6175 | 9 | 16 | Nf=1 | |
|
||||
| F | 6207 | 18 | 6207 | 10 | 17 | Nf=2 | |
|
||||
| F | 6235 | 18 | 6235 | 11 | 17 | Nf=12 | |
|
||||
| F | 6247 | 18 | 6247 | 10 | 17 | Nf=2 | |
|
||||
| F | 6255 | 17 | 6255 | 9 | 16 | Nf=1 | |
|
||||
| F | 6271 | 15 | 6271 | 9 | 14 | Nf=3 | |
|
||||
| F | 6303 | 29 | 6303 | 15 | 28 | Nf=1 | |
|
||||
| F | 6311 | 37 | 6311 | 21 | 36 | Nf=1 | |
|
||||
| F | 6367 | 23 | 6367 | 11 | 22 | Nf=1 | |
|
||||
| F | 6383 | 70 | 6383 | 43 | 69 | Nf=2 | |
|
||||
| F | 6395 | 23 | 6395 | 14 | 22 | Nf=6 | |
|
||||
| F | 6399 | 19 | 6399 | 11 | 18 | Nf=1 | |
|
||||
| F | 6427 | 25 | 6427 | 13 | 24 | Nf=1 | |
|
||||
| F | 6463 | 25 | 6463 | 14 | 24 | Nf=1 | |
|
||||
| F | 6471 | 51 | 6471 | 31 | 50 | Nf=1 | |
|
||||
| F | 6503 | 16 | 6503 | 9 | 15 | Nf=4 | |
|
||||
| F | 6559 | 16 | 6559 | 9 | 15 | Nf=1 | |
|
||||
| F | 6591 | 45 | 6591 | 28 | 44 | Nf=8 | |
|
||||
| F | 6623 | 28 | 6623 | 16 | 27 | Nf=2 | |
|
||||
| F | 6639 | 18 | 6639 | 11 | 17 | Nf=12 | |
|
||||
| F | 6655 | 42 | 6655 | 22 | 41 | Nf=1 | |
|
||||
| F | 6759 | 16 | 6759 | 9 | 15 | Nf=1 | |
|
||||
| F | 6767 | 20 | 6767 | 11 | 19 | Nf=1 | |
|
||||
| F | 6783 | 16 | 6783 | 9 | 15 | Nf=3 | |
|
||||
| F | 6811 | 29 | 6811 | 18 | 28 | Nf=45 | |
|
||||
| F | 6823 | 38 | 6823 | 23 | 37 | Nf=18 | |
|
||||
| F | 6847 | 21 | 6847 | 11 | 20 | Nf=1 | |
|
||||
| F | 6887 | 58 | 6887 | 36 | 57 | Nf=4 | |
|
||||
| F | 6895 | 22 | 6895 | 13 | 21 | Nf=1 | |
|
||||
| F | 6907 | 17 | 6907 | 9 | 16 | Nf=1 | |
|
||||
| F | 6911 | 48 | 6911 | 29 | 47 | Nf=1 | |
|
||||
| F | 6939 | 29 | 6939 | 15 | 28 | Nf=1 | |
|
||||
| F | 6975 | 15 | 6975 | 9 | 14 | Nf=4 | |
|
||||
| F | 6983 | 18 | 6983 | 9 | 17 | Nf=1 | |
|
||||
| F | 7015 | 15 | 7015 | 9 | 14 | Nf=4 | |
|
||||
| F | 7039 | 18 | 7039 | 11 | 17 | Nf=8 | |
|
||||
| F | 7103 | 17 | 7103 | 10 | 16 | Nf=1 | |
|
||||
| F | 7151 | 23 | 7151 | 13 | 22 | Nf=2 | |
|
||||
| F | 7163 | 20 | 7163 | 9 | 19 | Nf=1 | |
|
||||
| F | 7167 | 34 | 7167 | 21 | 33 | Nf=4 | |
|
||||
| F | 7195 | 20 | 7195 | 12 | 19 | Nf=3 | |
|
||||
| F | 7199 | 16 | 7199 | 9 | 15 | Nf=1 | |
|
||||
| F | 7231 | 22 | 7231 | 11 | 21 | Nf=1 | |
|
||||
| F | 7271 | 22 | 7271 | 12 | 21 | Nf=1 | |
|
||||
| F | 7279 | 58 | 7279 | 36 | 57 | Nf=4 | |
|
||||
| F | 7295 | 32 | 7295 | 19 | 31 | Nf=3 | |
|
||||
| F | 7323 | 31 | 7323 | 17 | 30 | Nf=1 | |
|
||||
| F | 7327 | 23 | 7327 | 14 | 22 | Nf=4 | |
|
||||
| F | 7335 | 25 | 7335 | 15 | 24 | Nf=2 | |
|
||||
| F | 7359 | 45 | 7359 | 27 | 44 | Nf=1 | |
|
||||
| F | 7407 | 31 | 7407 | 13 | 30 | Nf=1 | |
|
||||
| F | 7419 | 15 | 7419 | 9 | 14 | Nf=6 | |
|
||||
| F | 7423 | 39 | 7423 | 23 | 38 | Nf=1 | |
|
||||
| F | 7451 | 18 | 7451 | 11 | 17 | Nf=16 | |
|
||||
| F | 7471 | 20 | 7471 | 11 | 19 | Nf=1 | |
|
||||
| F | 7487 | 17 | 7487 | 9 | 16 | Nf=1 | |
|
||||
| F | 7495 | 19 | 7495 | 9 | 18 | Nf=1 | |
|
||||
| F | 7527 | 75 | 7527 | 46 | 74 | Nf=1 | |
|
||||
| F | 7551 | 23 | 7551 | 11 | 22 | Nf=1 | |
|
||||
| F | 7583 | 23 | 7583 | 12 | 22 | Nf=1 | |
|
||||
| F | 7615 | 23 | 7615 | 12 | 22 | Nf=1 | |
|
||||
| F | 7663 | 26 | 7663 | 16 | 25 | Nf=8 | |
|
||||
| F | 7679 | 38 | 7679 | 23 | 37 | Nf=1 | |
|
||||
| F | 7707 | 21 | 7707 | 12 | 20 | Nf=3 | |
|
||||
| F | 7711 | 21 | 7711 | 11 | 20 | Nf=1 | |
|
||||
| F | 7727 | 33 | 7727 | 20 | 32 | Nf=3 | |
|
||||
| F | 7783 | 18 | 7783 | 9 | 17 | Nf=1 | |
|
||||
| F | 7807 | 26 | 7807 | 13 | 25 | Nf=1 | |
|
||||
| F | 7835 | 17 | 7835 | 10 | 16 | Nf=2 | |
|
||||
| F | 7839 | 26 | 7839 | 15 | 25 | Nf=1 | |
|
||||
| F | 7871 | 22 | 7871 | 11 | 21 | Nf=1 | |
|
||||
| F | 7919 | 15 | 7919 | 9 | 14 | Nf=4 | |
|
||||
| F | 7935 | 43 | 7935 | 25 | 42 | Nf=1 | |
|
||||
| F | 7963 | 76 | 7963 | 45 | 75 | Nf=1 | |
|
||||
| F | 8027 | 26 | 8027 | 16 | 25 | Nf=13 | |
|
||||
| F | 8039 | 21 | 8039 | 12 | 20 | Nf=2 | |
|
||||
| F | 8063 | 18 | 8063 | 9 | 17 | Nf=1 | |
|
||||
| F | 8095 | 17 | 8095 | 10 | 16 | Nf=2 | |
|
||||
| F | 8127 | 47 | 8127 | 27 | 46 | Nf=1 | |
|
||||
| F | 8175 | 26 | 8175 | 15 | 25 | Nf=1 | |
|
||||
| F | 8187 | 16 | 8187 | 9 | 15 | Nf=1 | |
|
||||
| F | 8191 | 45 | 8191 | 27 | 44 | Nf=1 | |
|
||||
|
||||
## Notes
|
||||
|
||||
- `D_exact` et `F` sont relevées au module minimal \(2^{A+1}\) qui fige le mot de valuations du témoin.
|
||||
- `D_brother_local` encode une dépendance locale (palier du domaine) vers un `mate_exact` ; elle n’est pas utilisée ici comme clause universelle autonome.
|
||||
|
||||
@ -0,0 +1,17 @@
|
||||
{
|
||||
"inputs": {
|
||||
"verification_c3_local_descent_json": "docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json",
|
||||
"clauses_universelles_json": "docs/artefacts/collatz/universal_clauses/clauses_universelles.json"
|
||||
},
|
||||
"domain": {
|
||||
"palier": 13,
|
||||
"max_stable_modulus_power": 85
|
||||
},
|
||||
"counts": {
|
||||
"ok_records": 384,
|
||||
"D_exact": 27,
|
||||
"F": 330,
|
||||
"D_brother_local": 27
|
||||
},
|
||||
"ok": true
|
||||
}
|
||||
@ -0,0 +1,22 @@
|
||||
**Auteur** : Équipe 4NK
|
||||
|
||||
# Vérification déterministe — clauses universelles extraites (Option A)
|
||||
|
||||
## Entrées
|
||||
|
||||
- C3 vérification JSON : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`
|
||||
- clauses JSON : `docs/artefacts/collatz/universal_clauses/clauses_universelles.json`
|
||||
|
||||
## Résultat
|
||||
|
||||
- ok : True
|
||||
- palier (domaine) : 2^13
|
||||
- max(2^m_stable) observé : 2^85
|
||||
|
||||
## Compteurs
|
||||
|
||||
- ok_records : 384
|
||||
- D_exact : 27
|
||||
- F : 330
|
||||
- D_brother_local : 27
|
||||
|
||||
64
docs/features/collatz_universal_clause_extraction_optionA.md
Normal file
64
docs/features/collatz_universal_clause_extraction_optionA.md
Normal file
@ -0,0 +1,64 @@
|
||||
**Auteur** : Équipe 4NK
|
||||
|
||||
# Collatz — Extraction de clauses universelles (Option A : Lift(B12))
|
||||
|
||||
## Objectif
|
||||
|
||||
Industrialiser la conversion « témoin local → clause universelle candidate » (H4/H5) dans le périmètre **Option A** :
|
||||
|
||||
- domaine des témoins : une instance locale de clôture (C3) sur \(L=\mathrm{Lift}_{12\to 13}(B_{12})\) ;
|
||||
- entrée standard : un artefact déterministe `verification_c3_local_descent.json` contenant, pour chaque \(n\in L\), un témoin \(D\) (exact / brother) ou \(F\) (fusion) ;
|
||||
- sortie : un ensemble versionné de **clauses candidates** \(D/F\) relevées au module minimal \(2^{A+1}\) qui fige le préfixe de valuations, plus une vérification déterministe de cohérence.
|
||||
|
||||
Le but est de rendre la notion « certificat ⇒ clause universelle utilisable dans une induction bien fondée » exploitable de manière répétable, sans transcript, et sans dépendre d’un seul représentant.
|
||||
|
||||
## Impacts
|
||||
|
||||
- Ajoute un format d’artefacts versionnés `docs/artefacts/collatz/universal_clauses/` pour stocker :
|
||||
- clauses extraites (JSON + MD),
|
||||
- vérification (JSON + MD).
|
||||
- N’altère pas la pipeline de génération de certificats ; le flux est en lecture seule vis‑à‑vis des artefacts C3.
|
||||
|
||||
## Modifications
|
||||
|
||||
### Scripts
|
||||
|
||||
- `applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py`
|
||||
- lit `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`,
|
||||
- pour chaque témoin `D_exact` ou `F`, calcule le module minimal \(2^{A+1}\) et relève le résidu au palier stable par un relèvement déterministe (choix unique du bon enfant à chaque palier),
|
||||
- conserve `D_brother` sous forme de dépendance locale `D_brother_local` (référence `mate_exact`).
|
||||
|
||||
- `applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py`
|
||||
- vérifie la cohérence arithmétique et la cohérence de relèvement avec le fichier source C3,
|
||||
- vérifie aussi les dépendances `D_brother_local` (relation de sœur au palier de domaine, et existence du `mate_exact` en `D_exact`).
|
||||
|
||||
### Artefacts
|
||||
|
||||
- `docs/artefacts/collatz/universal_clauses/clauses_universelles.{json,md}`
|
||||
- `docs/artefacts/collatz/universal_clauses/verification_universal_clauses.{json,md}`
|
||||
|
||||
## Modalités de déploiement
|
||||
|
||||
Pas de déploiement : scripts exécutés localement, artefacts versionnés.
|
||||
|
||||
## Modalités d’analyse / reproduction
|
||||
|
||||
Commande d’extraction :
|
||||
|
||||
```bash
|
||||
python3 applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py --repo-root /home/ncantu/code/algo
|
||||
```
|
||||
|
||||
Commande de vérification :
|
||||
|
||||
```bash
|
||||
python3 applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py --repo-root /home/ncantu/code/algo
|
||||
```
|
||||
|
||||
Entrée attendue :
|
||||
- `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`
|
||||
|
||||
Sorties attendues :
|
||||
- `docs/artefacts/collatz/universal_clauses/clauses_universelles.json`
|
||||
- `docs/artefacts/collatz/universal_clauses/verification_universal_clauses.json`
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user