**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`