diff --git a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py b/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
index 1b5a749..55b56c2 100644
--- a/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
+++ b/applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
@@ -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}")
 
 
diff --git a/applications/collatz/conjoncture_collatz.md b/applications/collatz/conjoncture_collatz.md
index f7973ab..66d39f6 100644
--- a/applications/collatz/conjoncture_collatz.md
+++ b/applications/collatz/conjoncture_collatz.md
@@ -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)
diff --git a/applications/collatz/démonstration collatz.md b/applications/collatz/démonstration collatz.md
index 4445f00..19768a2 100644
--- a/applications/collatz/démonstration collatz.md	
+++ b/applications/collatz/démonstration collatz.md	
@@ -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`
diff --git a/docs/collatz_conjoncture_collatz_cartographie.md b/docs/collatz_conjoncture_collatz_cartographie.md
new file mode 100644
index 0000000..e1c296c
--- /dev/null
+++ b/docs/collatz_conjoncture_collatz_cartographie.md
@@ -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).
+
diff --git a/docs/collatz_run_report_2026-03-09_universal_clauses.md b/docs/collatz_run_report_2026-03-09_universal_clauses.md
new file mode 100644
index 0000000..b42ef45
--- /dev/null
+++ b/docs/collatz_run_report_2026-03-09_universal_clauses.md
@@ -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`
+
diff --git a/docs/collatz_run_report_format.md b/docs/collatz_run_report_format.md
index 8c49d4c..72baef9 100644
--- a/docs/collatz_run_report_format.md
+++ b/docs/collatz_run_report_format.md
@@ -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)
diff --git a/docs/features/collatz_run_report_generator.md b/docs/features/collatz_run_report_generator.md
index a4dd4f0..bd56410 100644
--- a/docs/features/collatz_run_report_generator.md
+++ b/docs/features/collatz_run_report_generator.md
@@ -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