From 158222d3ea67ebad69c4b6a49cac6676e9160de4 Mon Sep 17 00:00:00 2001 From: jsboige self-bot Date: Thu, 3 Sep 2026 11:00:38 +0200 Subject: [PATCH] docs(lean,#13565): discrepancy_lean comme controle negatif de strate-advance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Doctrine formalisant le role du lake MyIA.AI.Notebooks/Search/discrepancy_lean/ comme controle negatif d'allegations d'extension d'espace (transition de strate, emancipation de niveau, decouverte d'un nouveau regime) : - Desambiguïsation explicitee : 'discrepancy' (combine, Spencer/Beck-Fiala/Banaszczyk) != 'Limited Discrepancy Search' (Harvey/Ginsberg) ; le geste se transporte, le mot ne voyage pas. - Patron certifie (lecture firsthand de Kernel/Progress/BeckFiala) : tant qu'il y a plus de variables flottantes que de contraintes dangereuses, il existe un noyau non trivial (carte lineaire sommes colorées -> Q^D non injective) ; suivre la direction de noyau jusqu'au premier contact avec la frontiere du cube [-1,1] fige au moins un flottant ; la recursion sur |X| strictement decroissant etablit la borne disc <= 2k-1. Resultat mesurable, certificat constructif, aucune possibilite nouvelle inventee. - Table 4-objets (ambient / admissible / liberte residuelle / politique) posee comme grille discriminante entre 'meilleure heuristique', 'descension guidee', 'Beck-Fiala', 'relaxation PDDL', 'macro-action', 'nouvelle regle'. - Obligation methodologique 5 etapes : caracteriser / chercher / ecrire / reformuler / falsifiable. - Perimetre d'application (5 terrains nommes) : ICT-Series, GameTheory, Probas, Planners, Lean. Mesure canonique du prerequis (lake comme certificat) : python scripts/lean/count_code_sorry.py --json -> discrepancy_lean/Discrepancy : distinct_code_sorry = 0 (mesure 2026-09-03). --- docs/lean/discrepancy-as-negative-control.md | 175 +++++++++++++++++++ 1 file changed, 175 insertions(+) create mode 100644 docs/lean/discrepancy-as-negative-control.md diff --git a/docs/lean/discrepancy-as-negative-control.md b/docs/lean/discrepancy-as-negative-control.md new file mode 100644 index 0000000000..1255831af0 --- /dev/null +++ b/docs/lean/discrepancy-as-negative-control.md @@ -0,0 +1,175 @@ +# Discrepancy_lean comme contrôle négatif d'allégation de strate-advance + +> Issue de référence : **#13565**. +> Lake : `MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/`. +> Mesure sorry (instrument canonique) : `python scripts/lean/count_code_sorry.py --json` +> → champ `distinct_code_sorry = 0` pour `discrepancy_lean` au 2026-09-03. +> Le lake est **un certificat** : zéro `sorry` réel, donc les théorèmes qu'il +> porte peuvent servir de base à un contrôle négatif sans risque que la +> chaîne d'inférence soit elle-même trouée. + +## L'idée + +Avant de conclure qu'un agent a **élargi son espace de possibles** (transition +de strate au sens de `ICT-Series`, émancipation de niveau), il faut éliminer +l'hypothèse concurrente : il existait un **degré de liberté latent** dans +l'ancien espace, et l'agent ne l'avait pas su exploiter. Élargir n'est pas la +seule lecture compatible avec les observations ; **exploiter** l'est aussi, et +l'attribution « extension » sur cette seule base est un **faux positif +structurel**. + +`discrepancy_lean` fournit un cas où ce degré de liberté latent existe, et il +est **certifié en Lean 4** (sans `sorry`, distinct_code_sorry = 0, lake +construit en `Basic → Kernel → Progress → BeckFiala`). C'est la +référence canonique pour rédiger le geste de contrôle négatif : **avant +d'écrire « l'agent a étendu son espace », chercher le noyau / le slack de +l'espace initial, et écrire ce qu'on a cherché.** + +## Désambiguïsation obligatoire + +`Basic.lean` ligne 13-19 avertit explicitement : la **discrépance combinatoire** +formalisée dans ce lake (sommes colorées signées, théorie de Spencer, Beck-Fiala, +Banaszczyk, Bansal-Jiang 2025) **n'a aucun rapport mathématique** avec la +**Limited Discrepancy Search** de Harvey & Ginsberg enseignée dans +`Search-13-LimitedDiscrepancySearch` (même série `Search/`). Confondre les deux +serait exactement le défaut de vocabulaire que ce document cherche à prévenir. +Le geste de contrôle négatif se transporte, le mot `discrepancy` ne voyage pas. + +## Le patron certifié + +Trois théorèmes, lus firsthand dans le lake, posent le patron : + +1. **`Kernel.lean` — `card_dangerous_lt_card_floating` + `exists_dangerous_kernel_vec`** + (b1, étapes 1 et 2). Tant qu'il y a plus de variables flottantes que de + contraintes dangereuses, le système linéaire `D × X` a un **noyau non + trivial** : il existe une direction de déplacement non nulle qui + **préserve exactement** toutes les sommes colorées des lignes dangereuses. + C'est ce degré de liberté qui permet de figer un flottant à chaque phase + sans déranger les lignes déjà sous contrôle. + +2. **`Progress.lean` — `exists_step_hits_boundary`** (b3). Suivre la direction + de noyau jusqu'au **premier contact** avec la frontière du cube `[-1, 1]` : + le pas est strictement positif, garde tout le monde dans le cube fermé, + et fige au moins un nouveau flottant en `±1`. + +3. **`BeckFiala.lean` — `beck_fiala_classic`** (b4). Boucle : chaque phase + préserve les invariants **et fait strictement décroître** le nombre de + flottants. La récursion est bien fondée sur `|X|`. Résultat : toute famille + de degré maximal `≤ k` (`k ≥ 1`) admet une coloration `±1` de discrépance + `≤ 2k−1`. + +**Lecture en contrôle négatif.** Beck-Fiala montre qu'on peut obtenir un +**résultat mesurable** (coloration `±1`, borne `2k−1`) sans qu'aucun pas +n'élargisse l'espace ambiant : `|X|` ne fait que décroître, l'espace actif se +**contracte**. Le progrès est réel, le certificat est constructif, et **aucune +possibilité nouvelle n'a été inventée**. C'est précisément la lecture +alternative à « l'agent a étendu son espace » qu'il faut avoir cherché avant de +claim l'élargissement. + +## Le vocabulaire que ça corrige + +Le contraste binaire « meilleure navigation » vs « espace élargi » est trop +grossier. Il faut au moins **quatre objets** pour discriminer les gestes : + +| Geste | ambiant | admissible | liberté résiduelle | politique | +|---|---|---|---|---| +| meilleure heuristique | = | = | = | change | +| descente guidée dans une taxonomie | = | = | = | change | +| **Beck-Fiala** | **=** | **préservé sous invariants** | **diminue** | exploite le noyau | +| relaxation PDDL | = | **s'élargit** | augmente | éventuellement = | +| ajout d'une macro-action | **change** | change | change | éventuellement = | +| nouvelle règle institutionnelle | **change de langage** | change | change | change | + +Beck-Fiala occupe **une ligne qu'aucune autre n'occupe**, et c'est la **seule +avec un certificat** vérifiable. Les autres lignes sont des gestes plausibles +mais **non-certifiés** : il est possible qu'ils étendent l'espace, il est aussi +possible qu'ils exploitent un noyau non documenté. + +## Obligation méthodologique proposée + +Avant de publier un témoin « l'agent a dû étendre son espace » : + +1. **Caractériser** l'espace initial (ambient + admissible + liberté + résiduelle, selon la table 4-objets). +2. **Chercher** le noyau ou le slack de cet espace (variables inactives, + contraintes redondantes, dimension cachée, colonnes de marge). +3. **Écrire** ce qu'on a cherché, ce qu'on a trouvé, et ce qu'on n'a **pas** + trouvé. **« Je n'ai pas cherché » n'est pas une option** — c'est + précisément le geste de contrôle négatif qui fait défaut. +4. **Si** un noyau est trouvé et exploité : reformuler le claim en + « exploitation d'un degré de liberté latent », pas en « extension ». +5. **Si** aucun noyau n'est trouvé : le claim « extension » reste sur la + table, mais avec la mention explicite que la recherche de noyau a été + conduite et est négative. **C'est cette mention qui transforme un + claim narratif en un résultat falsifiable.** + +Hors du cas linéaire, « noyau » devient analogique. Exemples de transport : + +- **Planning** : atteignabilité dans l'espace d'états, actions dominées non + explorées. +- **SAT** : backbone, nombre de modèles, littéraux gelés. +- **Jeux** : actions dominées ou symétriques, strates de profondeur jamais + atteinte. +- **ICT-Series** : variables latentes non contraintes, régime du modèle + jamais atteint, mode latent non sollicité. + +C'est le **geste** qui se transporte (« chercher la marge dans l'ancien +espace, écrire ce qu'on a cherché »), pas la formule. + +## Quand ce contrôle négatif s'applique + +| Terrain | Application concrète | Référence canonique | +|---|---|---| +| ICT-Series | Avant toute allégation de transition de strate (sortie ICT-19 vers 21/22) | `ICT-21-SAETrajectoires.ipynb`, `ICT-SAE-JLens-TeteATete.ipynb` | +| GameTheory | Avant toute allégation « le joueur découvre une nouvelle stratégie » | `game_theory_lean/`, identifier si la stratégie existait dans le réservoir initial | +| Probas / Infer.NET | Avant toute allégation « le modèle identifie un nouveau régime » | `discrepancy_lean` + transport au PBPI/Bande de Credibilité | +| Planners | Avant toute allégation « le solveur explore au-delà du domaine » | domaine relaxé (PDDL relaxation) vs domaine initial | +| Lean | Avant tout claim « le prouveur a découvert un nouveau fait » | tactics, casse-disjonctions, lemmes cachés dans le contexte | + +## Limites du contrôle négatif + +- **Le contrôle négatif ne ferme pas la question**, il élimine une classe + d'explication alternative. Beck-Fiala montre que l'**exploitation** est + compatible avec les observations de progrès sans extension. Cela n'établit + pas qu'**aucune extension** n'a eu lieu — cela déplace le fardeau de la + preuve vers celui qui claim l'extension. +- **Le transport analogique** (noyau → atteignabilité → backbone → mode + latent) est plus délicat que le cas linéaire. Le geste de chercher la marge + reste, mais la preuve d'absence de marge est rarement absolue. +- **Le coût de la recherche** est non-trivial. Une recherche exhaustive de + noyau sur un grand système linéaire est elle-même un calcul qu'il faut + borner. Le présent document ne tranche pas la question du **niveau + d'effort** minimal qui suffirait à écrire « j'ai cherché » honnêtement — + c'est une question ouverte que cette doctrine ne prétend pas résoudre. + +## Statut de la doctrine + +- **Source** : issue #13565 (po-2025), rédigée par po-2025 le 2026-09-XX, + claimée par `myia-po-2026:CoursIA-2` le 2026-09-03 dans le cadre du grain + c.911. +- **Référence interne au lake** : `Discrepancy/Basic.lean` (désambiguïsation + ligne 13-19) + `Kernel.lean` + `Progress.lean` + `BeckFiala.lean`. Aucun + `sorry` réel (`distinct_code_sorry = 0` au 2026-09-03, instrument + canonique `scripts/lean/count_code_sorry.py`). +- **Périmètre d'application** : tout allégation de transition de strate + (élargissement d'espace, émancipation de niveau, découverte d'un nouveau + régime) sur le dépôt. +- **Force normative** : **médium**. La doctrine pose un geste et un + vocabulaire ; elle ne crée pas un gate bloquant (qui exigerait une + couverture exhaustive et un coût de revue disproportionné). Le geste se + transporte d'abord, l'enforcement vient ensuite si l'usage s'avère. + +## Voir aussi + +- **Issue #13565** — source de la doctrine, motivation et désambiguïsation + (limitée à ce que la doctrine formalise). +- **`docs/lean/README.md`** — index des documents de doctrine Lean du + dépôt ; ce document s'y inscrit. +- **`.claude/rules/pr-review-discipline.md` §H** — Vrai outil SOTA, geste de + contrôle négatif compatible. +- **`scripts/lean/count_code_sorry.py`** — instrument canonique de mesure + des `sorry` réels, à utiliser **avant** d'invoquer un lake comme + certificat (un lake avec `distinct_code_sorry > 0` ne peut pas servir). +- **`docs/lean/i18n-sibling-patterns.md`** — convention i18n FR/EN siblings + appliquée au lake ; la version EN de ce document (`_en.md` suffixé) n'est + **pas** un livrable de ce grain mais reste un suivi possible.