ncantu 94280b93fd collatz: extract and verify universal clause candidates (Option A)

**Motivations:**
- Produce a deterministic bridge from C3 local witnesses to universal-clause candidates (D/F) usable in later H4/H5 formalization.

**Root causes:**
- Local witnesses (Lift(B12)-scoped) were not exportable into a versioned, machine-checkable clause artefact.

**Correctifs:**
- Add deterministic extraction with minimal stable modulus lifting for D_exact/F and local encoding for D_brother dependencies.
- Add deterministic verifier checking arithmetic consistency, lifting stability, and brother↔mate relation.

**Evolutions:**
- Version universal clause artefacts (JSON/MD) under `docs/artefacts/collatz/universal_clauses/`.
- Document the feature and reproduction steps in `docs/features/`.

**Pages affectées:**
- applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py
- applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py
- docs/artefacts/collatz/universal_clauses/*
- docs/features/collatz_universal_clause_extraction_optionA.md

2026-03-09 03:26:07 +01:00

2.9 KiB

Raw Blame History

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 :

python3 applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py --repo-root /home/ncantu/code/algo

Commande de vérification :

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

2.9 KiB Raw Blame History Unescape Escape