nicolas.cantu/algo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add deterministic C3 local descent verification and run report profile

Browse Source 
**Motivations:**
- Instrument the C3 “final lock” as a citeable deterministic artefact
- Provide a reproducible check over Lift(B12) at palier 2^13 using D8/Fusion witnesses

**Root causes:**
- C3 lacked a machine-checkable artefact aligned with the run-report standard

**Correctifs:**
- Add a deterministic verifier that checks fusion witnesses (m<n and U(m)=U^t(n)) and aggregates N* where computable

**Evolutions:**
- Version C3 verification artefacts under docs/artefacts
- Add run report profile c3_local_descent (sha256 + metrics)
- Document the new profile and reference the artefacts in the proof plan

**Pages affectées:**
- applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py
- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json
- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md
- applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
- docs/collatz_run_report_2026-03-09_c3_local_descent.md
- docs/collatz_run_report_format.md
- docs/features/collatz_run_report_generator.md
- docs/features/collatz_c3_local_descent_verification.md
- applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md
This commit is contained in:
ncantu 2026-03-09 01:44:01 +01:00
parent c29bbaec4b
commit 071da20b19
9 changed files with 5860 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

140
applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
View File

@ -132,6 +132,18 @@ class C2ProjectiveMetrics:
proj_both15_equals_b12: bool
@dataclass(frozen=True)
class C3LocalDescentMetrics:
palier: int
lifted_domain_size: int
d8_nodes: int
d8_exact_nodes: int
d8_brother_nodes: int
fusion_nodes: int
n_star: int
base_checked_up_to: int
def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics:
obj = read_json(Path(verification_json))
if not isinstance(obj, dict):
@ -172,6 +184,35 @@ def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics:
)
def parse_c3_local_descent_metrics(verification_json: str) -> C3LocalDescentMetrics:
obj = read_json(Path(verification_json))
if not isinstance(obj, dict):
raise ValueError("Invalid C3 verification JSON: expected object")
domain = obj.get("domain")
elim = obj.get("elimination")
base = obj.get("base_validation")
if not isinstance(domain, dict) or not isinstance(elim, dict) or not isinstance(base, dict):
raise ValueError("Invalid C3 verification JSON: missing domain/elimination/base_validation blocks")
def req_int(d: dict, k: str) -> int:
v = d.get(k)
if not isinstance(v, int):
raise ValueError(f"Invalid C3 verification JSON: {k} must be int")
return v
return C3LocalDescentMetrics(
palier=req_int(domain, "palier"),
lifted_domain_size=req_int(domain, "lifted_domain_size"),
d8_nodes=req_int(elim, "d8_nodes"),
d8_exact_nodes=req_int(elim, "d8_exact_nodes"),
d8_brother_nodes=req_int(elim, "d8_brother_nodes"),
fusion_nodes=req_int(elim, "fusion_nodes"),
n_star=req_int(elim, "N_star"),
base_checked_up_to=req_int(base, "checked_up_to"),
)
def write_c2_projective_run_report(
*,
output_path: Path,
@ -224,6 +265,58 @@ def write_c2_projective_run_report(
output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
def write_c3_local_descent_run_report(
*,
output_path: Path,
report_title: str,
command: str,
git_commit: str,
sha_entries: list[Sha256Entry],
metrics: C3LocalDescentMetrics,
artefacts_dir: Path,
) -> None:
lines: list[str] = []
lines.append("**Auteur** : Équipe 4NK")
lines.append("")
lines.append(f"# {report_title}")
lines.append("")
lines.append("## Contexte")
lines.append("")
lines.append("- **But du run** : vérifier C3 (clôture locale sur Lift(B12) au palier 2^13) via témoins D8/Fusion.")
lines.append("- **Assertion vérifiée** : cohérence arithmétique des témoins (U(m)=U^t(n), m<n) et agrégats (N*).")
lines.append("")
lines.append("## Code et reproductibilité")
lines.append("")
if git_commit:
lines.append(f"- **Commit Git** : `{git_commit}`")
if command:
lines.append("- **Commande** :")
lines.append("")
lines.append("```bash")
lines.append(command)
lines.append("```")
lines.append("")
lines.append("## Empreintes sha256 (scripts, artefacts)")
lines.append("")
lines.extend(format_sha256_list(sha_entries))
lines.append("")
lines.append("## Compteurs et métriques")
lines.append("")
lines.append(f"- palier : 2^{metrics.palier}")
lines.append(f"- |Lift(B12)| : {metrics.lifted_domain_size}")
lines.append(f"- D8 : {metrics.d8_nodes} (exact={metrics.d8_exact_nodes}, brothers={metrics.d8_brother_nodes})")
lines.append(f"- Fusion : {metrics.fusion_nodes}")
lines.append(f"- N* (max seuils N0/Nf calculés) : {metrics.n_star}")
lines.append(f"- base validation checked up to : {metrics.base_checked_up_to}")
lines.append("")
lines.append("## Chemins d’artefacts (versionnés)")
lines.append("")
lines.append(f"- ARTEFACTS : `{artefacts_dir}`")
lines.append("")
output_path.parent.mkdir(parents=True, exist_ok=True)
output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
def _discover_base_noyau_path(artefacts_dir: Path) -> Path:
candidates = sorted((artefacts_dir / "noyaux").glob("noyau_*_B12.json"))
if len(candidates) != 1:
@ -805,6 +898,7 @@ def main() -> None:
"local_H6",
"local_H6_E1",
"c2_projective",
"c3_local_descent",
],
help="Report profile",
)
@ -826,6 +920,11 @@ def main() -> None:
default="",
help="For profile c2_projective: path to deterministic artefacts directory (e.g. docs/artefacts/collatz/c2_projective)",
)
ap.add_argument(
"--c3-artefacts-dir",
default="",
help="For profile c3_local_descent: path to deterministic artefacts directory (e.g. docs/artefacts/collatz/c3_local_descent)",
)
args = ap.parse_args()
repo_root = Path(args.repo_root).resolve() if args.repo_root else Path.cwd().resolve()
@ -1078,6 +1177,47 @@ def main() -> None:
print(f"Wrote: {output_path}")
return
if args.profile == "c3_local_descent":
command = args.command.strip()
if not command:
command = (
"python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py "
"--profile c3_local_descent --scope c3_local_descent "
"--out-dir applications/collatz/out --docs-dir docs "
"--c3-artefacts-dir docs/artefacts/collatz/c3_local_descent"
)
artefacts_dir = (
Path(args.c3_artefacts_dir).resolve()
if args.c3_artefacts_dir.strip()
else (docs_dir / "artefacts" / "collatz" / "c3_local_descent")
)
verification_json = artefacts_dir / "verification_c3_local_descent.json"
verification_md = artefacts_dir / "verification_c3_local_descent.md"
metrics = parse_c3_local_descent_metrics(str(verification_json))
date_str = pick_report_date_from_mtime([verification_json, verification_md])
sha_paths: list[Path] = [
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_verify_c3_local_descent.py",
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_k_core.py",
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_k_fusion.py",
verification_json,
verification_md,
]
sha_entries = compute_sha256_entries(sha_paths)
output_path = docs_dir / f"collatz_run_report_{date_str}_{args.scope}.md"
write_c3_local_descent_run_report(
output_path=output_path,
report_title=f"Rapport d’exécution — {args.scope}",
command=command,
git_commit=commit_hash,
sha_entries=sha_entries,
metrics=metrics,
artefacts_dir=artefacts_dir,
)
print(f"Wrote: {output_path}")
return
raise ValueError(f"Unknown profile: {args.profile}")

421
applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py Normal file
View File

@ -0,0 +1,421 @@
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
"""
collatz_verify_c3_local_descent.py
Deterministic verification artefact for the C3 step, starting from the
instrumented C1 (local H6 cover) and C2 (projective reduction).
Scope of this verifier:
- domain L := Lift_{12->13}(B12) (represented by the versioned local H6 artefacts)
- for each n in L, select a witnessed elimination:
- D8 branch: verify U^8(n) < n (direct check on the representative n)
- Fusion branch: verify the row witnesses a fusion to a strictly smaller preimage m < n,
and that U^t(n) == U(m) (shared suffix) using U_step computations.
- additionally, verify that every reached integer <= max_seen terminates to 1
under the standard Collatz map (accelerated on odds), so the local descent
proof for representatives is closed unconditionally at this finite bound.
Inputs:
- docs/artefacts/collatz/local_E*_palier2p13/** (generated by collatz_generate_local_h6_artefacts.py)
Outputs:
- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json
- docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md
"""
from __future__ import annotations
import argparse
import csv
import json
import re
from dataclasses import dataclass
from pathlib import Path
from collatz_k_core import U_step, prefix_data, N0_D, fusion_choice_a, delta_F, Nf_F
def _read_json(path: Path) -> object:
return json.loads(path.read_text(encoding="utf-8", errors="strict"))
def _discover_state_dirs(root: Path) -> list[Path]:
dirs = sorted([p for p in root.glob("local_E*_palier2p13") if p.is_dir()])
if not dirs:
raise ValueError(f"No local_E*_palier2p13 directories found under {root}")
return dirs
def _load_covered_from_cert(cert_path: Path) -> set[int]:
obj = _read_json(cert_path)
if not isinstance(obj, dict) or "covered" not in obj:
raise ValueError(f"Invalid certificate JSON (missing covered): {cert_path}")
cov = obj["covered"]
if not isinstance(cov, list) or not all(isinstance(x, int) for x in cov):
raise ValueError(f"Invalid certificate JSON covered list: {cert_path}")
return set(cov)
@dataclass(frozen=True)
class FusionWitness:
n: int
t: int
a: int
y: int
preimage_m: int
source_csv: str
def _parse_int_field(row: dict[str, str], key: str, source: Path) -> int:
if key not in row:
raise ValueError(f"Missing column {key} in {source}")
raw = row[key].strip()
if not raw:
raise ValueError(f"Empty column {key} in {source}")
try:
return int(raw)
except ValueError as e:
raise ValueError(f"Invalid int for {key} in {source}: {raw}") from e
def _load_fusion_witnesses(state_dir: Path) -> list[FusionWitness]:
candidats_dir = state_dir / "candidats"
paths = sorted(candidats_dir.glob("candidats_F9to*_E*_palier2p13.csv"))
if not paths:
return []
witnesses: list[FusionWitness] = []
for p in paths:
if p.stat().st_size == 0:
continue
with p.open("r", encoding="utf-8") as f:
r = csv.DictReader(f)
for row in r:
n = _parse_int_field(row, "classe_mod_2^m", p)
t = _parse_int_field(row, "t", p)
a = _parse_int_field(row, "a", p)
y = _parse_int_field(row, "y", p)
m = _parse_int_field(row, "preimage_m", p)
witnesses.append(
FusionWitness(n=n, t=t, a=a, y=y, preimage_m=m, source_csv=str(p))
)
return witnesses
def _u_iter(n: int, k: int) -> int:
x = n
for _ in range(k):
x, _ = U_step(x)
return x
def _collatz_terminates(n: int) -> bool:
x = n
seen = 0
while x != 1:
if x <= 0:
return False
if x % 2 == 0:
x //= 2
else:
x, _ = U_step(x)
seen += 1
if seen > 10_000_000:
return False
return True
def _pick_best_witness(witnesses: list[FusionWitness]) -> dict[int, FusionWitness]:
"""
For each n, choose a canonical witness: minimal t, then minimal preimage_m,
then lexical source_csv (for determinism).
"""
out: dict[int, FusionWitness] = {}
for w in witnesses:
prev = out.get(w.n)
if prev is None:
out[w.n] = w
continue
if (w.t, w.preimage_m, w.source_csv) < (prev.t, prev.preimage_m, prev.source_csv):
out[w.n] = w
return out
def _infer_state_id(state_dir: Path) -> int:
m = re.search(r"local_E(\d+)_palier2p13", state_dir.name)
if not m:
raise ValueError(f"Cannot infer state id from {state_dir}")
return int(m.group(1))
def run(
*,
artefacts_root: Path,
output_dir: Path,
) -> None:
state_dirs = _discover_state_dirs(artefacts_root)
# Domain L as union of per-state lifted noyaux
L: set[int] = set()
d8_covered: set[int] = set()
fusion_witnesses_all: list[FusionWitness] = []
for sd in state_dirs:
sid = _infer_state_id(sd)
lift_candidates = sorted((sd / "noyaux").glob(f"noyau_Lift_E{sid}_palier2p13.json"))
if len(lift_candidates) != 1:
raise ValueError(f"Expected exactly one lift noyau for {sd}, got {len(lift_candidates)}")
lift_obj = _read_json(lift_candidates[0])
if not isinstance(lift_obj, dict) or "noyau" not in lift_obj:
raise ValueError(f"Invalid lift noyau JSON: {lift_candidates[0]}")
lift_list = lift_obj["noyau"]
if not isinstance(lift_list, list) or not all(isinstance(x, int) for x in lift_list):
raise ValueError(f"Invalid lift noyau list: {lift_candidates[0]}")
L |= set(lift_list)
cert_d8 = sd / "certificats" / f"certificat_D8_E{sid}_palier2p13.json"
if cert_d8.exists():
d8_covered |= _load_covered_from_cert(cert_d8)
fusion_witnesses_all.extend(_load_fusion_witnesses(sd))
if not L:
raise ValueError("Empty domain L")
fusion_by_n = _pick_best_witness(fusion_witnesses_all)
d8_nodes = sorted([n for n in L if n in d8_covered])
f_nodes = sorted([n for n in L if n not in d8_covered])
missing_f = [n for n in f_nodes if n not in fusion_by_n]
if missing_f:
raise ValueError(f"Missing fusion witness for {len(missing_f)} residues (e.g. {missing_f[:20]})")
records: list[dict[str, object]] = []
next_values: list[int] = []
thresholds: list[int] = []
d8_exact_nodes = 0
d8_brother_nodes = 0
d8_exact_base_cases = 0
d8_exact_descent_witnesses = 0
shift = 1 << (13 - 1)
d8_exact_set: set[int] = set()
d8_brother_set: set[int] = set()
for n in d8_nodes:
pref = prefix_data(n, 8)
if pref.A == 13:
d8_exact_set.add(n)
else:
d8_brother_set.add(n)
for n in sorted(L):
if n in d8_covered:
pref = prefix_data(n, 8)
if n in d8_exact_set:
d8_exact_nodes += 1
N0 = N0_D(pref.C, pref.A, 8)
thresholds.append(N0)
if n >= N0:
y = pref.y
if y >= n:
raise ValueError(f"D8 descent check failed for n={n}: U^8(n)={y} not < n (N0={N0})")
next_values.append(y)
d8_exact_descent_witnesses += 1
records.append(
{
"n": n,
"kind": "D_exact",
"k": 8,
"A_k": pref.A,
"C_k": pref.C,
"N0": N0,
"next": y,
"base_case": False,
}
)
else:
d8_exact_base_cases += 1
records.append(
{
"n": n,
"kind": "D_exact",
"k": 8,
"A_k": pref.A,
"C_k": pref.C,
"N0": N0,
"next": None,
"base_case": True,
}
)
else:
d8_brother_nodes += 1
mate = n ^ shift
if mate not in d8_exact_set:
raise ValueError(
f"D8 brother check failed for n={n}: expected mate={mate} to be an exact D8 candidate (A8=13)"
)
records.append(
{
"n": n,
"kind": "D_brother",
"k": 8,
"A_k": pref.A,
"C_k": pref.C,
"mate_exact": mate,
}
)
else:
w = fusion_by_n[n]
pref = prefix_data(n, w.t)
y = pref.y
if y != w.y:
raise ValueError(f"Fusion witness y mismatch for n={n}: computed U^{w.t}(n)={y}, row y={w.y}")
m = w.preimage_m
if m >= n:
raise ValueError(f"Fusion witness preimage not smaller for n={n}: m={m} >= n")
y2, _ = U_step(m)
if y2 != y:
raise ValueError(f"Fusion witness invalid: U(m) != U^t(n) for n={n}: U({m})={y2}, U^{w.t}({n})={y}")
a = fusion_choice_a(y)
if a is None:
raise ValueError(f"Fusion witness invalid: y mod 3 == 0 for n={n}, y={y}")
if a != w.a:
raise ValueError(f"Fusion witness a mismatch for n={n}: computed a={a}, row a={w.a}")
dF = delta_F(pref.A, w.t, a)
if dF <= 0:
raise ValueError(f"Fusion witness invalid: DeltaF<=0 for n={n}: DeltaF={dF}")
Nf = Nf_F(pref.C, pref.A, w.t, a)
thresholds.append(Nf)
if n < Nf:
raise ValueError(f"Fusion witness invalid: n < Nf for n={n}: Nf={Nf}")
records.append(
{
"n": n,
"kind": "F",
"t": w.t,
"a": a,
"y": y,
"preimage_m": m,
"A_t": pref.A,
"C_t": pref.C,
"DeltaF": dF,
"Nf": Nf,
"source_csv": w.source_csv,
"next": m,
}
)
next_values.append(m)
max_n = max(L)
max_next = max(next_values) if next_values else 0
max_seen = max(max_n, max_next)
N_star = max(thresholds) if thresholds else 0
base_check_up_to = max(max_seen, N_star)
# Base validation at finite bound
non_terminating: list[int] = []
for x in range(1, base_check_up_to + 1):
if not _collatz_terminates(x):
non_terminating.append(x)
break
if non_terminating:
raise ValueError(f"Base validation failed at n={non_terminating[0]}")
summary = {
"inputs": {
"artefacts_root": str(artefacts_root),
"states": len(state_dirs),
},
"domain": {
"palier": 13,
"lifted_domain_size": len(L),
"min_n": min(L),
"max_n": max_n,
},
"elimination": {
"d8_nodes": len(d8_nodes),
"d8_exact_nodes": d8_exact_nodes,
"d8_exact_descent_witnesses": d8_exact_descent_witnesses,
"d8_exact_base_cases": d8_exact_base_cases,
"d8_brother_nodes": d8_brother_nodes,
"fusion_nodes": len(f_nodes),
"max_next": max_next,
"N_star": N_star,
},
"base_validation": {
"checked_up_to": base_check_up_to,
"ok": True,
},
"records": records,
}
output_dir.mkdir(parents=True, exist_ok=True)
out_json = output_dir / "verification_c3_local_descent.json"
out_md = output_dir / "verification_c3_local_descent.md"
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 — C3 (clôture locale par descente/fusion)")
lines.append("")
lines.append("## Entrées")
lines.append("")
lines.append(f"- ARTEFACTS ROOT : `{artefacts_root}`")
lines.append("")
lines.append("## Domaine")
lines.append("")
lines.append(f"- palier : 2^13")
lines.append(f"- |L| (Lift(B12) à 2^13) : {len(L)}")
lines.append(f"- min(L) : {min(L)}, max(L) : {max_n}")
lines.append("")
lines.append("## Élimination (témoins)")
lines.append("")
lines.append(
f"- D8 : {len(d8_nodes)} (exact A8=13 : {d8_exact_nodes}, "
f"descente vérifiée pour n>=N0 : {d8_exact_descent_witnesses}, "
f"cas de base n<N0 : {d8_exact_base_cases}, "
f"frères (mate exact requis) : {d8_brother_nodes})"
)
lines.append(f"- Fusion : {len(f_nodes)} (m<n, U(m)=U^t(n) vérifié)")
lines.append(f"- max(next) : {max_next}")
lines.append(f"- N* (max des seuils N0/Nf calculés) : {N_star}")
lines.append("")
lines.append("## Validation de base (finie)")
lines.append("")
lines.append(f"- Trajectoires vérifiées jusqu’à : {max_seen}")
lines.append("- Résultat : True (toutes atteignent 1)")
lines.append("")
lines.append("## Sorties")
lines.append("")
lines.append(f"- JSON : `{out_json}`")
lines.append(f"- Markdown : `{out_md}`")
lines.append("")
out_md.write_text("\n".join(lines) + "\n", encoding="utf-8")
def main() -> None:
ap = argparse.ArgumentParser(description="Deterministic C3 verification from local H6 artefacts (palier 2^13)")
ap.add_argument(
"--local-h6-root",
default="docs/artefacts/collatz",
help="Root directory containing local_E*_palier2p13 directories",
)
ap.add_argument(
"--output-dir",
default="docs/artefacts/collatz/c3_local_descent",
help="Output directory for deterministic artefacts (JSON + MD)",
)
args = ap.parse_args()
run(
artefacts_root=Path(args.local_h6_root),
output_dir=Path(args.output_dir),
)
if __name__ == "__main__":
main()

17
applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md
View File

@ -261,6 +261,23 @@ Lemme C3 (impossibilité d’orbite infinie sous contraintes).
Sous un paquet explicite de contraintes arithmétiques \(P\) (congruences, bornes sur sommes de valuations sur des horizons, contraintes modulo \(3^k\), etc.) extraites comme invariants des survivants, aucune orbite de la dynamique accélérée \(U\) ne peut être infinie.
Objectif : fournir une mesure de rang ou une contradiction directe stable sous \(U\) sur le sous-ensemble défini par \(P\).
### Instance instrumentée (palier \(2^{13}\), domaine Lift(\(B_{12}\)))
On pose \(L=\mathrm{Lift}_{12\to 13}(B_{12})\subset(\mathbb{Z}/2^{13}\mathbb{Z})^\times\).
Une instance vérifiable de C3 consiste à exhiber, pour chaque \(n\in L\), un témoin d’élimination de type :
- **fusion** : un entier impair \(m<n\) et un \(t\ge 1\) tels que \(U(m)=U^{(t)}(n)\) (donc la terminaison de \(n\) se réduit à celle de \(m\)) ;
- **descente exacte** : un \(k\ge 1\) (ici \(k=8\)) tel que la clause exacte est contractante (\(\Delta_D=2^{A_k}-3^k>0\)) et fournit un seuil \(N_0\) ; pour \(n\ge N_0\), on a \(U^{(k)}(n)<n\) ;
- **frère** : une réduction au cas “descente exacte” via l’égalité “sœur” (structure de complétion par frères), indexée par un `mate_exact`.
Artefact déterministe (script + sorties courtes) :
- script : `applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py`
- sorties : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}`
- rapport d’exécution : `docs/collatz_run_report_2026-03-09_c3_local_descent.md`
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.
## 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).

5134
docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json Normal file
View File

File diff suppressed because it is too large Load Diff

31
docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md Normal file
View File

@ -0,0 +1,31 @@
**Auteur** : Équipe 4NK
# Vérification déterministe — C3 (clôture locale par descente/fusion)
## Entrées
- ARTEFACTS ROOT : `docs/artefacts/collatz`
## Domaine
- palier : 2^13
- |L| (Lift(B12) à 2^13) : 384
- min(L) : 27, max(L) : 8191
## Élimination (témoins)
- D8 : 54 (exact A8=13 : 27, descente vérifiée pour n>=N0 : 27, cas de base n<N0 : 0, frères (mate exact requis) : 27)
- Fusion : 330 (m<n, U(m)=U^t(n) vérifié)
- max(next) : 6867
- N* (max des seuils N0/Nf calculés) : 138
## Validation de base (finie)
- Trajectoires vérifiées jusqu’à : 8191
- Résultat : True (toutes atteignent 1)
## Sorties
- JSON : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`
- Markdown : `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md`

44
docs/collatz_run_report_2026-03-09_c3_local_descent.md Normal file
View File

@ -0,0 +1,44 @@
**Auteur** : Équipe 4NK
# Rapport d’exécution — c3_local_descent
## Contexte
- **But du run** : vérifier C3 (clôture locale sur Lift(B12) au palier 2^13) via témoins D8/Fusion.
- **Assertion vérifiée** : cohérence arithmétique des témoins (U(m)=U^t(n), m<n) et agrégats (N*).
## Code et reproductibilité
- **Commit Git** : `e3e68fe39c8ad466e5741e87d20311ca93b2456e`
- **Commande** :
```bash
python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py --profile c3_local_descent --scope c3_local_descent --out-dir applications/collatz/out --docs-dir docs --c3-artefacts-dir docs/artefacts/collatz/c3_local_descent
```
## Empreintes sha256 (scripts, artefacts)
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py`
- sha256: `8959c31332dc650040a434efd9ebfa7a604d2f436a1316cf36371a12578b2b34`
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_k_core.py`
- sha256: `2d5fb9fff733c37a2fa88334b034b70bfe23665d5a13bf4b2407bb13de7227dc`
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_k_fusion.py`
- sha256: `421d4384b501129a2039c67a327e57e0dd891cdf125c1d74499627bc20a3f62f`
- `/home/ncantu/code/algo/docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`
- sha256: `cad483cab3a6db3693dc6130e68f61e99350515719bf52fc63370f4287e7ef97`
- `/home/ncantu/code/algo/docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md`
- sha256: `5353489e85fca4ad3774a778e39b57e2994de8e4dfb937b62a8d41df31a952dd`
## Compteurs et métriques
- palier : 2^13
- |Lift(B12)| : 384
- D8 : 54 (exact=27, brothers=27)
- Fusion : 330
- N* (max seuils N0/Nf calculés) : 138
- base validation checked up to : 8191
## Chemins d’artefacts (versionnés)
- ARTEFACTS : `/home/ncantu/code/algo/docs/artefacts/collatz/c3_local_descent`

15
docs/collatz_run_report_format.md
View File

@ -101,6 +101,21 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
--docs-dir docs
```
Pour la vérification C3 (clôture locale au palier \(2^{13}\) sur Lift(\(B_{12}\)) via témoins D8/Fusion, artefacts déterministes versionnés) :
```bash
python3 applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py \
--local-h6-root docs/artefacts/collatz \
--output-dir docs/artefacts/collatz/c3_local_descent
python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
--profile c3_local_descent \
--scope c3_local_descent \
--c3-artefacts-dir docs/artefacts/collatz/c3_local_descent \
--out-dir applications/collatz/out \
--docs-dir docs
```
### Contexte
- **But du run** : (énoncé court)

56
docs/features/collatz_c3_local_descent_verification.md Normal file
View File

@ -0,0 +1,56 @@
**Auteur** : Équipe 4NK
# Collatz — Vérification déterministe de C3 (clôture locale)
## Objectif
Produire un artefact déterministe et citable (sans transcript terminal) vérifiant une instance de C3 sur un domaine fini contrôlé :
- domaine \(L=\mathrm{Lift}_{12\to 13}(B_{12})\) (384 résidus impairs modulo \(2^{13}\)),
- témoins :
- clauses de fusion F (avec `preimage_m < n` et égalité \(U(m)=U^{(t)}(n)\) vérifiée),
- et branche D8 (distinguée en “exact” \(A_8=13\) et “frère”, i.e. `mate_exact`).
Cet artefact vérifie la cohérence arithmétique des témoins et agrège les seuils \(N_0\) (D exact) et \(N_F\) (fusion) en une borne \(N^\star\) calculée sur ce domaine.
## Impacts
- Ajout d’un artefact versionné dans `docs/artefacts/` et d’un rapport d’exécution dans `docs/`, alignés sur le format standard des rapports.
## Modifications
- Script déterministe :
- `applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py`
- Artefacts versionnés (sortie du script) :
- `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`
- `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.md`
- Rapport d’exécution (sha256 + métriques) :
- `docs/collatz_run_report_2026-03-09_c3_local_descent.md`
- Extension du générateur de rapports :
- `applications/collatz/collatz_k_scripts/collatz_generate_run_report.py` (profil `c3_local_descent`)
## Modalités d’analyse
- Générer/mettre à jour les artefacts déterministes :
```bash
python3 applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py \
--local-h6-root docs/artefacts/collatz \
--output-dir docs/artefacts/collatz/c3_local_descent
```
- Produire le rapport d’exécution (empreintes sha256 + métriques) :
```bash
python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
--profile c3_local_descent \
--scope c3_local_descent \
--c3-artefacts-dir docs/artefacts/collatz/c3_local_descent \
--out-dir applications/collatz/out \
--docs-dir docs
```
## Modalités de déploiement
Aucun déploiement.

3
docs/features/collatz_run_report_generator.md
View File

@ -23,9 +23,10 @@ afin d’éviter toute insertion de transcript terminal dans les documents math
- Ajout d’un format standard : `docs/collatz_run_report_format.md`.
- Ajout d’un générateur : `applications/collatz/collatz_k_scripts/collatz_generate_run_report.py`.
- Ajout d’un exemple réel de rapport : `docs/collatz_run_report_2026-03-04_extend_D18_D21_resume_from_D20.md`.
- Profils supportés : `extend_finale`, `validation_section7`, `pipeline_d16_d17`, `fusion_palier2p25`, `local_H6_E1`, `local_H6`, `c2_projective`.
- Profils supportés : `extend_finale`, `validation_section7`, `pipeline_d16_d17`, `fusion_palier2p25`, `local_H6_E1`, `local_H6`, `c2_projective`, `c3_local_descent`.
- Pour `local_H6`/`local_H6_E1`, un audit automatique compare le **palier attendu** (artefacts) au **palier certifié** (certificats) et échoue en cas de désaccord.
- Pour `c2_projective`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/c2_projective/verification_c2_projective.{json,md}`.
- Pour `c3_local_descent`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.{json,md}`.
## Modalités d’analyse