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

475 B

Raw Blame History

Auteur : Équipe 4NK

Vérification déterministe — clauses universelles extraites (Option A)

Entrées

C3 vérification JSON : docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent.json
clauses JSON : docs/artefacts/collatz/universal_clauses/clauses_universelles.json

Résultat

ok : True
palier (domaine) : 2^13
max(2^m_stable) observé : 2^85

Compteurs

ok_records : 384
D_exact : 27
F : 330
D_brother_local : 27

475 B Raw Blame History

Vérification déterministe — clauses universelles extraites (Option A)

Entrées

Résultat

Compteurs

475 B

Raw Blame History