Contradictions, interdits et dettes
Ce que le programme sait de faux chez lui, ce qu'il s'interdit de conclure, et ce qu'il doit encore payer. Cette page n'est pas un aveu de faiblesse : c'est l'appareil qui empêche une erreur corrigée de revenir par la porte de derrière.
ERRATUM OFFICIEL F-001 · 9 OCTOBRE 2026
PUBLIC FALSIFICATION
Rectification sur la proportion des premiers {1, 11, 29} mod 30 : À x = 10⁹, la proportion recalculée vaut environ 0,3749982, proche de 3/8. L'ancienne valeur rapportée proche de 0,378 était erronée. La limite 3/8 est classique et n'est pas un nouveau résultat.
L'appellation « température des premiers » appliquée au produit eulérien associé aux entiers sans facteur carré (μ²) est formellement proscrite.
Traçabilité complète au registre public : PUBLIC_FALSIFICATIONS.md (F-001)
Contradictions ouvertes
Conflits identifiés entre documents ou versions, avec l'état retenu et l'action due.
| ID | Conflit | État courant | Action |
|---|---|---|---|
| C-001 | U(30)≅C2×C4 versus ancienne formule C2×C4×C2 | C2×C4 retenu; ancienne formule réfutée | corriger sources dérivées |
| C-002 / F-001 | Proportion des premiers {1,11,29} mod 30 : ancienne valeur ≈ 0,378 versus recalcul 0,3749982 (limite 3/8 classique) | 0,3749982 retenu à x=10⁹ (proche de 3/8 classique) ; ancien 0,378 réfuté ; terme « température des premiers » interdit | erratum F-001 publié |
| C-003 | d_eff→7 / isotropie versus covariance RS anisotrope et d_eff≈5.15 | isotropie non établie | quarantaine de la route isotrope |
| C-004 | P_- présenté comme QR/NR complet versus χ5∈E3 | P_- ne voit que χ3,χ15 | corriger terminologie |
| C-005 | V(χ3)=0.157314 et V(χ15)=0.435740 versus recalculs 0.11322997 et 0.45936479 | anciennes valeurs retirées | reproduire χ15 en PARI/Sage |
| C-006 | c_log≈0.324 versus candidat≈0.3215743451 | ancien chiffre retiré | vérification certifiée à faire |
| C-007 | loi limite T10 sous GRH+LI versus existence sous GRH seule | GRH suffit pour existence; LI/GSH pour description renforcée | refactorer T10/T11 |
| C-008 | antichaîne exponentielle ⇒ NP-hard versus audit | inférence réfutée | supprimer des rapports antérieurs |
| C-009 | complexité m≥2,v≥2 ouverte dans audit puis NP-complétude proposée dans note plus récente | preuve nouvelle plausible, dépend d’une clause externe non pinée | vérifier Dor–Tarsi et restriction bipartite |
| C-010 | « Lean 0-sorry » dans certains documents versus snippets explicitement non build-vérifiés / axiomes d’interface | aucune certification à partir des DOCX seuls | exiger build réel du dépôt |
| C-011 | « temps linéaire » pour MM-CM-007 versus modèle de coût non fixé | statut robuste: polynomial et simple; linéaire à qualifier | fixer représentation des c_j et stratégie de recherche en v avant titre de complexité |
Transitions interdites
Les raccourcis que le programme se refuse — chacun né d'une tentation réelle, et inscrit en append-only.
| ID | Transition interdite | Pourquoi |
|---|---|---|
| FT-CM-001 | |Min(B*)| exponentiel ⇒ NP-hard | La taille de l’espace de recherche n’implique aucune classe de complexité. |
| FT-CM-002 | THM-source ⇒ THM-vérifié | Un document peut énoncer un théorème sans que sa preuve ait été auditée. |
| FT-CM-003 | THM-vérifié ⇒ THM-formalisé | La preuve papier et la formalisation machine sont deux artefacts distincts. |
| FT-CM-004 | THM-formalisé ⇒ THM-nouveau | La vérité/formalisation ne décide pas l’antériorité. |
| FT-CM-005 | Attestation computationnelle ⇒ preuve générale | 279/279, 134/134 ou des témoins C4 soutiennent une preuve; ils ne la remplacent pas. |
| FT-CM-006 | Réduction interne + source externe non vérifiée ⇒ NP-complétude fermée | Le théorème de départ de la réduction doit être piné dans sa version exacte, notamment la restriction bipartite. |
| FT-CM-007 | INTERP / ANALOGY_ONLY ⇒ conséquence formelle | Une résonance philosophique ne monte pas le statut mathématique. |
Dépromotions — l'historique conservé
Un état antérieur n'est jamais effacé. Voici des promotions et des chutes, datées.
| Événement | Entrée | Avant | Après | Motif |
|---|---|---|---|---|
| H-CM-001 2026-08-17 |
MM-REF-006 | NP-Hard local inféré de l’antichaîne exponentielle | [R] | L’inférence est un non sequitur; un espace de solutions exponentiel n’implique pas NP-hard. |
| H-CM-002 2026-08-17 |
MM-CM-010a | Complexité m≥2,v≥2 non démontrée | [O-historique] | Audit reformule correctement le sous-problème f_j(v). |
| H-CM-003 2026-08-17 |
MM-CM-010b | Ouvert | [D-reduction | C-source] | Nouvelle réduction C4 interne; dette externe sur Dor–Tarsi / hôtes bipartis. |
| H-CM-004 2026-08-19 |
MM-CM-007 | « temps linéaire » non qualifié | Polynomial, très simple; linéaire seulement sous modèle explicite | La somme est linéaire à v fixé; la recherche du plus petit v doit être comptabilisée dans un modèle algorithmique déclaré. |
Dettes en cours — conditions de promotion
Ce qu'il faudrait obtenir pour qu'un chantier monte en statut. Rien ne monte sans ça.
| Rang | Chantier | Condition de promotion |
|---|---|---|
| 1 | T8–T11 corrigé (χ3, χ15, Rubinstein–Sarnak, c_log) | reproduction numérique indépendante + preuve papier complète + formalisation conditionnelle sans axiomes opaques |
| 2 | Centres minimax / spectre comportemental | vérification primaire de la réduction C4 + septième passe d’antériorité ciblée |
| 3 | Formalisation Lean du noyau fini TC | build courant réel, 0 sorry dans les modules concernés, artefact piné |
| 4 | Registre Mathématique Maître | poursuivre jusqu’à couverture exhaustive des sources |
| 5 | Routes H3/HP, cosmologie, Collatz/NS | garder en aval jusqu’à théorème local nouveau et indépendant |
| 2 | Septième passe d’antériorité — sous-problème f_j(v) | audit primaire; comparer au literature on labeled partition / diversity-bounded clustering / graph decomposition |
Règle de conservation : ne jamais effacer un état antérieur. Une entrée réfutée
reste lisible avec son motif de chute, pour qu'aucun claim déclassé ne puisse être réactivé
silencieusement.
Extrait du Registre Mathématique Maître v0.2 consolidé au 9 octobre 2026. Les identifiants renvoient aux entrées du registre complet.