collatz: add universal_clauses run report profile and conjoncture cartography
**Motivations:** - Cite universal clause extraction/verification as a first-class deterministic run in the standard reporting flow. - Provide a measurable cartography of `conjoncture_collatz.md` duplication to enable later rationalization without immediate content moves. **Root causes:** - Universal clauses artefacts were not covered by the run report generator, making citations inconsistent with other C1/C2/C3 artefacts. - `conjoncture_collatz.md` contains multiple repeated trunks and generic headings, preventing unambiguous internal referencing. **Correctifs:** - Add `universal_clauses` profile to `collatz_generate_run_report.py` parsing and reporting counts/ok from versioned artefacts. - Add a versioned run report for the universal clauses artefacts. **Evolutions:** - Extend `docs/collatz_run_report_format.md` and `docs/features/collatz_run_report_generator.md` with the new profile. - Link the new artefacts and report in `démonstration collatz.md` and `conjoncture_collatz.md`. - Add `docs/collatz_conjoncture_collatz_cartographie.md` (livrable 1) with headings/duplication cartography and a no-deletion plan. **Pages affectées:** - applications/collatz/collatz_k_scripts/collatz_generate_run_report.py - docs/collatz_run_report_2026-03-09_universal_clauses.md - docs/collatz_run_report_format.md - docs/features/collatz_run_report_generator.md - applications/collatz/démonstration collatz.md - applications/collatz/conjoncture_collatz.md - docs/collatz_conjoncture_collatz_cartographie.md
This commit is contained in:
ncantu
parent
94280b93fd
commit
cb87e55ed4
@ -156,6 +156,18 @@ class C3LocalDescentMetrics:
|
||||
base_checked_up_to: int
|
||||
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class UniversalClausesMetrics:
|
||||
domain_palier: int
|
||||
max_stable_modulus_power: int
|
||||
total: int
|
||||
d_exact: int
|
||||
f: int
|
||||
d_brother_local: int
|
||||
ok_records: int
|
||||
ok: bool
|
||||
|
||||
|
||||
def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics:
|
||||
obj = read_json(Path(verification_json))
|
||||
if not isinstance(obj, dict):
|
||||
@ -273,6 +285,67 @@ def parse_c3_local_descent_metrics(verification_json: str) -> C3LocalDescentMetr
|
||||
)
|
||||
|
||||
|
||||
def parse_universal_clauses_metrics(
|
||||
*,
|
||||
clauses_json_path: Path,
|
||||
verification_json_path: Path,
|
||||
) -> UniversalClausesMetrics:
|
||||
clauses_obj = read_json(clauses_json_path)
|
||||
if not isinstance(clauses_obj, dict):
|
||||
raise ValueError("Invalid universal clauses JSON: expected object")
|
||||
counts = clauses_obj.get("counts")
|
||||
domain = clauses_obj.get("domain")
|
||||
if not isinstance(counts, dict) or not isinstance(domain, dict):
|
||||
raise ValueError("Invalid universal clauses JSON: missing counts/domain")
|
||||
|
||||
def req_int(d: dict, k: str) -> int:
|
||||
v = d.get(k)
|
||||
if not isinstance(v, int):
|
||||
raise ValueError(f"Invalid universal clauses JSON: {k} must be int")
|
||||
return v
|
||||
|
||||
max_stable = req_int(domain, "max_stable_modulus_power")
|
||||
total = req_int(counts, "total")
|
||||
d_exact = req_int(counts, "D_exact")
|
||||
f = req_int(counts, "F")
|
||||
d_brother_local = req_int(counts, "D_brother_local")
|
||||
|
||||
vobj = read_json(verification_json_path)
|
||||
if not isinstance(vobj, dict):
|
||||
raise ValueError("Invalid universal clauses verification JSON: expected object")
|
||||
vdomain = vobj.get("domain")
|
||||
vcounts = vobj.get("counts")
|
||||
ok = vobj.get("ok")
|
||||
if not isinstance(vdomain, dict) or not isinstance(vcounts, dict) or not isinstance(ok, bool):
|
||||
raise ValueError("Invalid universal clauses verification JSON: missing domain/counts/ok")
|
||||
|
||||
domain_palier = req_int(vdomain, "palier")
|
||||
v_max_stable = req_int(vdomain, "max_stable_modulus_power")
|
||||
if v_max_stable != max_stable:
|
||||
raise ValueError("Universal clauses: max_stable_modulus_power mismatch between clauses and verification")
|
||||
|
||||
ok_records = req_int(vcounts, "ok_records")
|
||||
if req_int(vcounts, "D_exact") != d_exact:
|
||||
raise ValueError("Universal clauses: D_exact count mismatch between clauses and verification")
|
||||
if req_int(vcounts, "F") != f:
|
||||
raise ValueError("Universal clauses: F count mismatch between clauses and verification")
|
||||
if req_int(vcounts, "D_brother_local") != d_brother_local:
|
||||
raise ValueError("Universal clauses: D_brother_local count mismatch between clauses and verification")
|
||||
if ok_records != total:
|
||||
raise ValueError("Universal clauses: ok_records must equal total clauses (Option A)")
|
||||
|
||||
return UniversalClausesMetrics(
|
||||
domain_palier=domain_palier,
|
||||
max_stable_modulus_power=max_stable,
|
||||
total=total,
|
||||
d_exact=d_exact,
|
||||
f=f,
|
||||
d_brother_local=d_brother_local,
|
||||
ok_records=ok_records,
|
||||
ok=ok,
|
||||
)
|
||||
|
||||
|
||||
def write_c2_projective_run_report(
|
||||
*,
|
||||
output_path: Path,
|
||||
@ -388,6 +461,60 @@ def write_c3_local_descent_run_report(
|
||||
output_path.write_text("\n".join(lines) + "\n", encoding="utf-8")
|
||||
|
||||
|
||||
def write_universal_clauses_run_report(
|
||||
*,
|
||||
output_path: Path,
|
||||
report_title: str,
|
||||
command: str,
|
||||
git_commit: str,
|
||||
sha_entries: list[Sha256Entry],
|
||||
metrics: UniversalClausesMetrics,
|
||||
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** : extraire des clauses universelles candidates (Option A : Lift(B12)) depuis l’artefact C3 local, et vérifier leur cohérence déterministe.")
|
||||
lines.append("- **Assertion vérifiée** : cohérence arithmétique des clauses extraites et cohérence des relèvements au module minimal \\(2^{A+1}\\).")
|
||||
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 (domaine des témoins) : 2^{metrics.domain_palier}")
|
||||
lines.append(f"- max(2^m_stable) observé : 2^{metrics.max_stable_modulus_power}")
|
||||
lines.append(f"- total clauses : {metrics.total}")
|
||||
lines.append(f"- D_exact : {metrics.d_exact}")
|
||||
lines.append(f"- F : {metrics.f}")
|
||||
lines.append(f"- D_brother_local : {metrics.d_brother_local}")
|
||||
lines.append(f"- ok_records : {metrics.ok_records}")
|
||||
lines.append(f"- ok : {metrics.ok}")
|
||||
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:
|
||||
@ -970,6 +1097,7 @@ def main() -> None:
|
||||
"local_H6_E1",
|
||||
"c2_projective",
|
||||
"c3_local_descent",
|
||||
"universal_clauses",
|
||||
],
|
||||
help="Report profile",
|
||||
)
|
||||
@ -996,6 +1124,11 @@ def main() -> None:
|
||||
default="",
|
||||
help="For profile c3_local_descent: path to deterministic artefacts directory (e.g. docs/artefacts/collatz/c3_local_descent)",
|
||||
)
|
||||
ap.add_argument(
|
||||
"--universal-clauses-artefacts-dir",
|
||||
default="",
|
||||
help="For profile universal_clauses: path to deterministic artefacts directory (e.g. docs/artefacts/collatz/universal_clauses)",
|
||||
)
|
||||
args = ap.parse_args()
|
||||
|
||||
repo_root = Path(args.repo_root).resolve() if args.repo_root else Path.cwd().resolve()
|
||||
@ -1289,6 +1422,53 @@ def main() -> None:
|
||||
print(f"Wrote: {output_path}")
|
||||
return
|
||||
|
||||
if args.profile == "universal_clauses":
|
||||
command = (
|
||||
args.command.strip()
|
||||
if args.command.strip()
|
||||
else "--profile universal_clauses --scope universal_clauses "
|
||||
"--universal-clauses-artefacts-dir docs/artefacts/collatz/universal_clauses "
|
||||
"--out-dir applications/collatz/out --docs-dir docs"
|
||||
)
|
||||
artefacts_dir = (
|
||||
Path(args.universal_clauses_artefacts_dir).resolve()
|
||||
if args.universal_clauses_artefacts_dir.strip()
|
||||
else (docs_dir / "artefacts" / "collatz" / "universal_clauses")
|
||||
)
|
||||
clauses_json = artefacts_dir / "clauses_universelles.json"
|
||||
clauses_md = artefacts_dir / "clauses_universelles.md"
|
||||
verification_json = artefacts_dir / "verification_universal_clauses.json"
|
||||
verification_md = artefacts_dir / "verification_universal_clauses.md"
|
||||
metrics = parse_universal_clauses_metrics(
|
||||
clauses_json_path=clauses_json,
|
||||
verification_json_path=verification_json,
|
||||
)
|
||||
date_str = pick_report_date_from_mtime([clauses_json, clauses_md, verification_json, verification_md])
|
||||
|
||||
sha_paths: list[Path] = [
|
||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_generate_run_report.py",
|
||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_extract_universal_clauses.py",
|
||||
repo_root / "applications" / "collatz" / "collatz_k_scripts" / "collatz_verify_universal_clauses.py",
|
||||
repo_root / "docs" / "artefacts" / "collatz" / "c3_local_descent" / "verification_c3_local_descent.json",
|
||||
clauses_json,
|
||||
clauses_md,
|
||||
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_universal_clauses_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}")
|
||||
|
||||
|
||||
|
||||
@ -67,6 +67,36 @@ où:
|
||||
- **Théorème 1**: démontré sous hypothèses (H1)-(H4).
|
||||
- **Proposition 1**: démontrée par calcul fini, indexée par ses paramètres.
|
||||
|
||||
## Trajectoire hybride instrumentée (C1→C2→C3) et artefacts déterministes
|
||||
|
||||
Cette trajectoire isole une chaîne de vérifications citable (sans transcript) et distingue explicitement les points qui restent des obligations de preuve (clauses universelles et itération au-delà d’un palier).
|
||||
|
||||
- C1 (complétude locale H6(E) sur les états de \(B_{12}\)) :
|
||||
- index : `docs/artefacts/collatz/local_H6_index.md`
|
||||
- rapports : `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p13.md`
|
||||
|
||||
- C2 (réduction projective par complétion “one” et stabilité \(B_m\bmod 2^{12}=B_{12}\)) :
|
||||
- script : `applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py`
|
||||
- sorties : `docs/artefacts/collatz/c2_projective/verification_c2_projective.{json,md}`
|
||||
- rapport : `docs/collatz_run_report_2026-03-09_c2_projective.md`
|
||||
- documents de complétion intégrés automatiquement (actuellement) :
|
||||
- `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`
|
||||
- `applications/collatz/collatz_k_scripts/complétion_minorée_m16_vers_m17.md`
|
||||
|
||||
- C3 (instance locale au palier \(2^{13}\) sur \(L=\mathrm{Lift}_{12\to 13}(B_{12})\)) :
|
||||
- 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 : `docs/collatz_run_report_2026-03-09_c3_local_descent.md`
|
||||
|
||||
- Extraction de clauses universelles candidates (Option A : Lift(\(B_{12}\))) :
|
||||
- scripts : `applications/collatz/collatz_k_scripts/{collatz_extract_universal_clauses.py,collatz_verify_universal_clauses.py}`
|
||||
- sorties : `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}`
|
||||
- rapport : `docs/collatz_run_report_2026-03-09_universal_clauses.md`
|
||||
|
||||
Le verrou restant est la transformation des témoins observés en clauses universelles valides “pour tout \(n\) dans une classe modulo \(2^m\), pour tout \(n\ge N\)”, et l’itération du schéma \(C1+C2\to C3\) à paliers arbitraires. La formalisation minimale visée est donnée dans :
|
||||
- `applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md`.
|
||||
|
||||
## Énoncés démontrés
|
||||
|
||||
### Lemme 1 (Forme affine le long d'un préfixe de valuations)
|
||||
|
||||
@ -89,7 +89,7 @@ Théorème (conditionnel).
|
||||
Sous l’hypothèse \(H_{\mathrm{ext}}(M)\), la conjecture de Collatz est vraie : pour tout entier \(n\ge 1\), il existe \(k\) tel que \(T^{(k)}(n)=1\).
|
||||
|
||||
Schéma de preuve.
|
||||
La vacuité de \(R_M\) signifie que toute classe impaire modulo \(2^M\) est fermée par une clause universelle du registre \(\mathcal{K}\) fournissant une réduction strictement bien fondée (descente ou collision/fusion vers une classe déjà contrôlée). Par bon ordre de \(\mathbb{N}\), aucune trajectoire ne peut éviter indéfiniment une réduction stricte, ce qui entraîne la terminaison.
|
||||
La vacuité de \(R_M\) signifie que toute classe impaire modulo \(2^M\) est fermée par une clause universelle du registre \(\mathcal{K}\) fournissant une réduction strictement bien fondée (descente \(D\) avec seuil \(N_0\), ou fusion \(F\) vers un impair strictement plus petit avec seuil \(N_F\)). Par bon ordre de \(\mathbb{N}\), aucune trajectoire ne peut éviter indéfiniment une réduction stricte, ce qui entraîne la terminaison.
|
||||
|
||||
Statut au regard des artefacts computationnels.
|
||||
Les artefacts D18→D21 (avec F15/F16) produisent un noyau résiduel non vide au dernier palier audité (par exemple `out/noyaux/noyau_post_D21.json`). En l’absence d’un artefact final attestant \(|R_M|=0\) pour un certain \(M\), la clôture par extinction n’est pas établie dans ce cadre. Une continuation standard suit l’une des trajectoires suivantes :
|
||||
@ -97,3 +97,63 @@ Les artefacts D18→D21 (avec F15/F16) produisent un noyau résiduel non vide au
|
||||
- branche « extinction par certificat total » : obtenir un palier \(2^M\) tel que \(|R_M|=0\), et produire un artefact de vérification citable (fichier + empreintes + script reproductible) ;
|
||||
- branche « analytique » : prouver un lemme global transformant les tendances observées (par exemple les coefficients de survie \(q_m\)) en extinction universelle, ce qui requiert une redéfinition/raffinement de \(R_m\) ou un renforcement de la grammaire des clauses tant que \(q_m\) reste proche de \(0{,}88\)–\(0{,}91\).
|
||||
- branche « hybride » : réduire \(R_M\) par certificats, caractériser structurellement les résidus survivants (invariants, contraintes, formes normales), puis prouver un lemme spécifique éliminant le noyau restant.
|
||||
|
||||
6. Trajectoire hybride (C1→C2→C3) : artefacts déterministes et verrou restant
|
||||
|
||||
Le schéma hybride se formule comme une chaîne de réductions citable, où chaque étape est indexée par ses choix (palier, domaines, certificats) et vérifiée par un artefact déterministe.
|
||||
|
||||
6.1. C2 (réduction projective par complétion « one »)
|
||||
|
||||
But.
|
||||
Réduire l’étude de la transition \(m\to m+1\) à un noyau “parents both” \(B_m\) et établir, après complétion par frères des cas “one”, l’égalité d’ensembles
|
||||
\[
|
||||
R_{m+1}^{\mathrm{comp}}=\{\,r,\ r+2^m\;:\; r\in B_m\,\}
|
||||
\]
|
||||
ainsi que la stabilité projective \(B_m\bmod 2^{12}=B_{12}\) sur les transitions auditées.
|
||||
|
||||
Artefact déterministe (C2).
|
||||
- script : `applications/collatz/collatz_k_scripts/collatz_verify_c2_projective.py`
|
||||
- sorties versionnées : `docs/artefacts/collatz/c2_projective/verification_c2_projective.{json,md}`
|
||||
- rapport d’exécution : `docs/collatz_run_report_2026-03-09_c2_projective.md`
|
||||
|
||||
Les transitions détectées dans les documents de complétion sont intégrées automatiquement dans la table multi‑transitions, à partir des fichiers :
|
||||
- `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`
|
||||
- `applications/collatz/collatz_k_scripts/complétion_minorée_m16_vers_m17.md`
|
||||
|
||||
6.2. C1 (complétude locale H6(E) sur les états de \(B_{12}\))
|
||||
|
||||
But.
|
||||
Pour chaque état \(E\) (mot de valuations sur \(B_{12}\) à horizon fixé), établir qu’un relèvement fini \(\Delta m(E)\) suffit à couvrir \(\mathrm{Lift}_{12\to 12+\Delta m(E)}(B_{12}(E))\) par une union finie de certificats \(D/F\).
|
||||
|
||||
Artefacts (H6 locale).
|
||||
- index agrégé : `docs/artefacts/collatz/local_H6_index.md`
|
||||
- répertoires par état : `docs/artefacts/collatz/local_E*_palier2p13/`
|
||||
- rapports d’exécution : `docs/collatz_run_report_2026-03-09_local_H6_E*_palier2p13.md`
|
||||
|
||||
6.3. C3 (instance locale : clôture sur Lift(\(B_{12}\)) au palier \(2^{13}\))
|
||||
|
||||
But.
|
||||
Sur le domaine \(L=\mathrm{Lift}_{12\to 13}(B_{12})\), exhiber pour chaque classe un témoin \(D\) (descente exacte ou frère) ou \(F\) (fusion vers un impair strictement plus petit) et fermer l’instance par validation de base finie.
|
||||
|
||||
Artefact déterministe (C3 local).
|
||||
- script : `applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py`
|
||||
- sorties versionnées : `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`
|
||||
|
||||
6.4. Verrou formel restant (au-delà de \(2^{13}\))
|
||||
|
||||
La transition de l’instance locale à une clôture globale requiert de transformer les témoins observés en **clauses universelles** utilisables dans une induction bien fondée (au sens : “pour tout \(n\) dans une classe modulo \(2^m\), pour tout \(n\ge N\)”), et d’itérer le schéma \(C1+C2\to C3\) à paliers arbitraires.
|
||||
|
||||
La formalisation minimale de ces clauses universelles (formes D/F, seuils \(N_0/N_F\), et schéma d’induction) est donnée dans :
|
||||
- `applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md` (section “Verrou technique précis”, puis “Formalisation minimale attendue (clauses universelles)”).
|
||||
|
||||
6.5. Extraction déterministe de clauses universelles candidates (Option A : Lift(\(B_{12}\)))
|
||||
|
||||
À partir de l’artefact déterministe C3 (témoins locaux sur \(L=\mathrm{Lift}_{12\to 13}(B_{12})\)), une procédure de relèvement transforme chaque témoin \(D\) exact ou \(F\) en une clause candidate stabilisée au module minimal \(2^{A+1}\) où le préfixe de valuations est figé.
|
||||
|
||||
Artefacts déterministes :
|
||||
- extraction : `applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py`
|
||||
- vérification : `applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py`
|
||||
- sorties versionnées : `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}`
|
||||
- rapport d’exécution : `docs/collatz_run_report_2026-03-09_universal_clauses.md`
|
||||
|
||||
111
docs/collatz_conjoncture_collatz_cartographie.md
Normal file
111
docs/collatz_conjoncture_collatz_cartographie.md
Normal file
@ -0,0 +1,111 @@
|
||||
**Auteur** : Équipe 4NK
|
||||
|
||||
# Cartographie — `applications/collatz/conjoncture_collatz.md` (rationalisation, sans suppression)
|
||||
|
||||
## Périmètre
|
||||
|
||||
Ce document cartographie les doublons structuraux et les zones hétérogènes de `applications/collatz/conjoncture_collatz.md`, afin de préparer une rationalisation **sans suppression ni restructuration immédiate**.
|
||||
|
||||
## Statistiques brutes (mesurables)
|
||||
|
||||
- **Lignes** : 23828
|
||||
- **Headings** (`##` à `######`) : 1456
|
||||
- **Groupes de headings dupliqués** (même niveau, titre normalisé) : 525
|
||||
|
||||
## Doublons structuraux majeurs (tronc répété)
|
||||
|
||||
Le “tronc formel” (cadre, définitions, lemmes D/F, théorème-cadre, protocoles, limites, conclusion, références) apparaît sous plusieurs variantes très proches :
|
||||
|
||||
- **Bloc A (accentué)** : commence à `L5` (ex. `## Introduction de l'objet mathématique`) et couvre la séquence :
|
||||
- `## Introduction de l'objet mathématique`
|
||||
- `## Prérequis de lecture`
|
||||
- `## Cadre de référence et notations`
|
||||
- `### Définition 1..4`
|
||||
- `## Statut des énoncés`
|
||||
- `## Énoncés démontrés` + `### Lemme 1..3`
|
||||
- `## Théorème-cadre conditionnel` + `### Théorème 1`
|
||||
- `## État quantifié actuel`
|
||||
- `## Protocoles de sensibilité`
|
||||
- `## Limites explicites du cadre`
|
||||
- `## Conclusion de l'état de preuve`
|
||||
- `## Références`
|
||||
|
||||
- **Blocs B/C/D (non accentués / variantes)** : commencent aux environs de :
|
||||
- `L274` (`## Introduction de l'objet mathematique`)
|
||||
- `L518` (`## Introduction de l'objet mathematique`)
|
||||
- `L762` (`## Introduction de l'objet mathématique`)
|
||||
|
||||
Indicateurs objectifs (extraits de doublons de headings) :
|
||||
- `## Prérequis de lecture` : 4 occurrences (`L15`, `L284`, `L528`, `L772`)
|
||||
- `## Cadre de référence et notations` : 4 occurrences (`L24`, `L293`, `L537`, `L781`)
|
||||
- `## Énoncés démontrés / Enonces demontres` : 4 occurrences (`L95`, `L339`, `L583`, `L820`)
|
||||
- `## Théorème-cadre conditionnel / Theoreme-cadre conditionnel` : 4 occurrences (`L173`, `L417`, `L661`, `L898`)
|
||||
- `## Protocoles de sensibilité / Protocoles de sensibilite` : 4 occurrences (`L215`, `L459`, `L703`, `L940`)
|
||||
- `## Limites explicites du cadre` : 4 occurrences (`L252`, `L496`, `L740`, `L977`)
|
||||
- `## Références / References` : 4 occurrences (`L262`, `L506`, `L750`, `L987`)
|
||||
- `## Conclusion de l'état de preuve` : 5 occurrences (`L258`, `L502`, `L746`, `L983`, `L23815`)
|
||||
|
||||
## Doublons récurrents (titres “génériques”)
|
||||
|
||||
Certains titres sont répétés de façon massive, ce qui empêche une indexation univoque des dépendances logiques :
|
||||
|
||||
- `## Conclusion de la section précédente` : 62 occurrences (premières : `L1831`, `L2002`, `L2073`, `L2190`, `L2626`, `L3374`, …)
|
||||
- `## Conclusion de l'étape` : 26 occurrences (premières : `L8774`, `L9513`, `L9645`, `L9752`, `L9788`, `L9824`, …)
|
||||
- `### Énoncé` : 6 occurrences (`L4514`, `L4552`, `L12582`, `L14087`, `L14125`, `L22155`)
|
||||
|
||||
Conséquence : un renvoi interne de type “voir la Conclusion de l’étape” n’est pas traçable sans un identifiant supplémentaire (numérotation ou titre spécialisé).
|
||||
|
||||
## Hétérogénéité de registre (hors tronc formel)
|
||||
|
||||
Des zones longues ne relèvent pas du cadre de preuve et mélangent :
|
||||
- vulgarisation (style non neutre, citations),
|
||||
- narration externe,
|
||||
- contenu sans statut mathématique (pas de lemmes/propositions indexés).
|
||||
|
||||
Exemple (détection par lecture ponctuelle du bas de fichier) :
|
||||
- présence de sections de vulgarisation et d’analogies qui ne sont pas indexées comme “annexe” et cohabitent avec les références.
|
||||
|
||||
## Risques actuels (liés à la rationalisation)
|
||||
|
||||
- **Traçabilité des hypothèses** : duplication du tronc rend ambigu l’endroit “canonique” des hypothèses (H1..H4/H5).
|
||||
- **Numérotation / renvois** : impossibilité de renvoyer à une section sans collision de titres.
|
||||
- **Maintenance** : tout ajout (ex. C1/C2/C3 instrumentés) doit être répliqué dans plusieurs blocs, sinon divergence.
|
||||
|
||||
## Plan de rationalisation (sans suppression/restructuration immédiate)
|
||||
|
||||
### Étape 1 — Définir un “tronc canonique” (sans déplacer)
|
||||
|
||||
Choisir un seul bloc comme canonique (recommandé : le tout premier bloc accentué, à partir de `L5`), et introduire un marqueur explicite au début :
|
||||
|
||||
- “Version canonique : sections X–Y”
|
||||
- “Les répétitions ultérieures sont des variantes / brouillons (à déplacer en annexe lors d’une étape dédiée).”
|
||||
|
||||
Cette étape ne supprime rien, ne déplace rien, mais fixe la référence.
|
||||
|
||||
### Étape 2 — Indexer les variantes (sans déplacer)
|
||||
|
||||
Au début de chaque bloc redondant (ex. à `L274`, `L518`, `L762`), ajouter une ligne de statut :
|
||||
|
||||
- “Variante / duplicat du tronc canonique (voir L5…)”
|
||||
|
||||
Objectif : éliminer l’ambiguïté de lecture.
|
||||
|
||||
### Étape 3 — Préparer l’atterrissage en annexes (sans exécuter ici)
|
||||
|
||||
Préparer un plan de migration qui, dans une étape ultérieure validée :
|
||||
- déplace les variantes du tronc en annexes (même fichier en bas, ou fichier `*_annexes.md`),
|
||||
- renvoie depuis le tronc canonique,
|
||||
- conserve une seule occurrence des définitions/lemmes/théorème.
|
||||
|
||||
### Étape 4 — Traiter les titres “génériques”
|
||||
|
||||
Établir une règle :
|
||||
- interdiction de titres dupliqués non indexés (“Conclusion de l’étape”, “Conclusion de la section précédente”) dans le tronc canonique,
|
||||
- remplacement par des titres spécialisés (ex. “Conclusion de la section X : …”) et/ou numérotation.
|
||||
|
||||
## Décisions à valider avant toute suppression/restructuration
|
||||
|
||||
- où placer les annexes (même fichier vs fichier annexe),
|
||||
- politique de numérotation (globale vs par chapitre),
|
||||
- traitement des contenus de vulgarisation (annexe dédiée, séparée du cadre formel).
|
||||
|
||||
52
docs/collatz_run_report_2026-03-09_universal_clauses.md
Normal file
52
docs/collatz_run_report_2026-03-09_universal_clauses.md
Normal file
@ -0,0 +1,52 @@
|
||||
**Auteur** : Équipe 4NK
|
||||
|
||||
# Rapport d’exécution — universal_clauses
|
||||
|
||||
## Contexte
|
||||
|
||||
- **But du run** : extraire des clauses universelles candidates (Option A : Lift(B12)) depuis l’artefact C3 local, et vérifier leur cohérence déterministe.
|
||||
- **Assertion vérifiée** : cohérence arithmétique des clauses extraites et cohérence des relèvements au module minimal \(2^{A+1}\).
|
||||
|
||||
## Code et reproductibilité
|
||||
|
||||
- **Commit Git** : `523fa25fefc9f12e1de9991d41fdb171850458bc`
|
||||
- **Commande** :
|
||||
|
||||
```bash
|
||||
--profile universal_clauses --scope universal_clauses --universal-clauses-artefacts-dir docs/artefacts/collatz/universal_clauses --out-dir applications/collatz/out --docs-dir docs
|
||||
```
|
||||
|
||||
## Empreintes sha256 (scripts, artefacts)
|
||||
|
||||
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py`
|
||||
- sha256: `dc14461dc91bf32a77cd35c2a598a628072075f1afe58eafcbaf07acee5a79b4`
|
||||
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py`
|
||||
- sha256: `a3de82a8b2b4e2579e2a4f94141711254629961ad8ea7746545a566c4ff4490f`
|
||||
- `/home/ncantu/code/algo/applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py`
|
||||
- sha256: `d7e0248c2096ce603166761b0cc78e6984d5995aba7c49ae6fa071b36d81df1e`
|
||||
- `/home/ncantu/code/algo/docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`
|
||||
- sha256: `cad483cab3a6db3693dc6130e68f61e99350515719bf52fc63370f4287e7ef97`
|
||||
- `/home/ncantu/code/algo/docs/artefacts/collatz/universal_clauses/clauses_universelles.json`
|
||||
- sha256: `45da7b5bb606ebe03a5bc596a0629f4762ca960dc675fe6fe55504c2bdc3ea9f`
|
||||
- `/home/ncantu/code/algo/docs/artefacts/collatz/universal_clauses/clauses_universelles.md`
|
||||
- sha256: `30d5da014aeae447f9904ba5135bd6c7a52d5de5b4c32d6ba52705d962efd274`
|
||||
- `/home/ncantu/code/algo/docs/artefacts/collatz/universal_clauses/verification_universal_clauses.json`
|
||||
- sha256: `a45f5a6279febe00a8c723718e935d45481c1c4e2ec60b4664c7a506321121c5`
|
||||
- `/home/ncantu/code/algo/docs/artefacts/collatz/universal_clauses/verification_universal_clauses.md`
|
||||
- sha256: `a40e151dc81c004009030b0749c9025cc5f74526ae0bf60fecd72d11fe20f5e3`
|
||||
|
||||
## Compteurs et métriques
|
||||
|
||||
- palier (domaine des témoins) : 2^13
|
||||
- max(2^m_stable) observé : 2^85
|
||||
- total clauses : 384
|
||||
- D_exact : 27
|
||||
- F : 330
|
||||
- D_brother_local : 27
|
||||
- ok_records : 384
|
||||
- ok : True
|
||||
|
||||
## Chemins d’artefacts (versionnés)
|
||||
|
||||
- ARTEFACTS : `/home/ncantu/code/algo/docs/artefacts/collatz/universal_clauses`
|
||||
|
||||
@ -116,6 +116,28 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
|
||||
--docs-dir docs
|
||||
```
|
||||
|
||||
Pour l’extraction/vérification de clauses universelles candidates (Option A : Lift(\(B_{12}\))), à partir de l’artefact C3 (artefacts déterministes versionnés) :
|
||||
|
||||
```bash
|
||||
python3 applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py \
|
||||
--repo-root /home/ncantu/code/algo \
|
||||
--verification-json docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json \
|
||||
--output-dir docs/artefacts/collatz/universal_clauses
|
||||
|
||||
python3 applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py \
|
||||
--repo-root /home/ncantu/code/algo \
|
||||
--verification-json docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json \
|
||||
--clauses-json docs/artefacts/collatz/universal_clauses/clauses_universelles.json \
|
||||
--output-dir docs/artefacts/collatz/universal_clauses
|
||||
|
||||
python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py \
|
||||
--profile universal_clauses \
|
||||
--scope universal_clauses \
|
||||
--universal-clauses-artefacts-dir docs/artefacts/collatz/universal_clauses \
|
||||
--out-dir applications/collatz/out \
|
||||
--docs-dir docs
|
||||
```
|
||||
|
||||
### Contexte
|
||||
|
||||
- **But du run** : (énoncé court)
|
||||
|
||||
@ -23,10 +23,11 @@ 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`, `c3_local_descent`.
|
||||
- Profils supportés : `extend_finale`, `validation_section7`, `pipeline_d16_d17`, `fusion_palier2p25`, `local_H6_E1`, `local_H6`, `c2_projective`, `c3_local_descent`, `universal_clauses`.
|
||||
- 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}`.
|
||||
- Pour `universal_clauses`, le rapport cite les artefacts déterministes `docs/artefacts/collatz/universal_clauses/{clauses_universelles,verification_universal_clauses}.{json,md}` et l’entrée `docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json`.
|
||||
|
||||
## Modalités d’analyse
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user