From 9ebb1b242352e037ad97b788007dea2005b78795 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 20 Sep 2026 16:00:44 +0200 Subject: [PATCH 1/3] =?UTF-8?q?fix(lean,#16638):=20reacc=C3=A9nter=20Lean-?= =?UTF-8?q?21c=20Descente=20Budget=20(filtre=20decide=20=C3=A9tendu)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Sub-grain #16638 : 133 substitutions / 24 cells touchées / +62/-62 mirror strict. 5 cellules code restaurées par filtre étendu Tell c.1311-L8 ★★★★ (tactiques Lean). Voie canonique Tell c.1299-L2 ★★★★ : réaccent ALL lignes + restauration post-reaccent byte-identique au main pour les lignes protégées (print/assert/ return/raise + tactiques Lean : decide, complete, apply, intro, exact, simp, omega, ring, linarith, ...). C.2 vérifié : 24/24 cells, 9/9 code, outputs intacts, exec_count intacts. 0 casse decide (Tell c.1311-L5 ★★★★★ vérifié). --- .../Lean/Lean-21c-Descente-Budget.ipynb | 124 +++++++++--------- 1 file changed, 62 insertions(+), 62 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb index dfb96fa239..57ef0673a6 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb @@ -9,13 +9,13 @@ "\n", "**Navigation** : [Index](README.md) | [Lean-21b (MIMO Converse) <<](Lean-21b-MIMO-Converse-Native.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n", "\n", - "Ce notebook presente le lake **`mimo_lean`** sur un theoreme sous-estime : `descent_target_before_ceiling` (fichier `Descent.lean`). Sous trois hypotheses tres explicites - *decroissance stricte du cout*, *confinement dans une barriere*, *absence de point bloquant hors cible* - toute trajectoire terminale **atteint sa cible avant un plafond `M_N` de flips**. Ce n'est pas un theoreme d'optimalite ; c'est une **garantie de terminaison**.\n", + "Ce notebook presente le lake **`mimo_lean`** sur un théorème sous-estimé : `descent_target_before_ceiling` (fichier `Descent.lean`). Sous trois hypotheses tres explicites - *decroissance stricte du cout*, *confinement dans une barriere*, *absence de point bloquant hors cible* - toute trajectoire terminale **atteint sa cible avant un plafond `M_N` de flips**. Ce n'est pas un théorème d'optimalite ; c'est une **garantie de terminaison**.\n", "\n", - "La valeur pedagogique du theoreme n'est pas dans le contexte MIMO (detection de bits par flips de coordonnees, Papailiopoulos 2026) mais dans sa **transversalite** : le patron `ressource_initiale => plafond_de_transformations => atteinte_ou_blocage` se retrouve partout - recherche de temoin par raffinement, revision argumentative, evolution d'une persona sur un espace fini. Trois substrats, un seul theoreme, et la case *<< la decroissance echoue >>* qui n'est pas un echec d'experience mais une dissociation a enregistrer.\n", + "La valeur pedagogique du théorème n'est pas dans le contexte MIMO (detection de bits par flips de coordonnees, Papailiopoulos 2026) mais dans sa **transversalite** : le patron `ressource_initiale => plafond_de_transformations => atteinte_ou_blocage` se retrouve partout - recherche de temoin par raffinement, revision argumentative, evolution d'une persona sur un espace fini. Trois substrats, un seul théorème, et la case *<< la decroissance echoue >>* qui n'est pas un echec d'experience mais une dissociation a enregistrer.\n", "\n", "| Module (lake `mimo_lean`) | Role |\n", "|---|---|\n", - "| `Descent.lean` | `Run`, `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), barriere (`descent_flips_le_barrier`), theoreme phare `descent_target_before_ceiling` |\n", + "| `Descent.lean` | `Run`, `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), barriere (`descent_flips_le_barrier`), théorème phare `descent_target_before_ceiling` |\n", "\n", "Comme dans les notebooks Lean-20, Lean-21 et Lean-23, nous procedons en deux registres : une **simulation Python** qui illustre le patron sur trois substrats, puis une **lecture directe des `.lean` sources** (regex balanced sur les mots-cles `theorem|lemma|def|inductive`) - la signature de chaque declaration est extraite **a la source**, identique en substance a ce qu'imprimerait `#check`. La commande `lake env lean` reste disponible comme option pour les rebuilds locaux." ] @@ -25,25 +25,25 @@ "id": "576f40eb", "metadata": {}, "source": [ - "## 1. Le theoreme fondateur, en prose\n", + "## 1. Le théorème fondateur, en prose\n", "\n", - "Soit un espace d'etats `sigma`, un predicat `target sigma` (l'ensemble a atteindre), une fonction de cout `cost : sigma -> Nat`, et une relation `accept : sigma -> sigma -> Prop` (un flip accepte fait passer d'un etat au suivant). Considerons un **run** : une liste d'etats `[s0, s1, ...]` ou chaque paire consecutive satisfait `accept`. Le theoreme `descent_target_before_ceiling` dit :\n", + "Soit un espace d'etats `sigma`, un predicat `target sigma` (l'ensemble a atteindre), une fonction de cout `cost : sigma -> Nat`, et une relation `accept : sigma -> sigma -> Prop` (un flip accepte fait passer d'un état au suivant). Considerons un **run** : une liste d'etats `[s0, s1, ...]` ou chaque paire consécutive satisfait `accept`. Le théorème `descent_target_before_ceiling` dit :\n", "\n", "Si les **trois hypotheses** tiennent -\n", "\n", "1. `hstrict` : pour tout flip accepte, le cout strictement decroit (`cost t < cost s`).\n", - "2. `hbarrier` : le cout reste confine sous `B` (chaque etat du run satisfait `cost <= B`).\n", + "2. `hbarrier` : le cout reste confine sous `B` (chaque état du run satisfait `cost <= B`).\n", "3. `hnostall` : hors de la cible, un flip accepte existe (l'algorithme ne se bloque que sur la cible).\n", "\n", - "- et si le run est **terminal** (aucun flip accepte n'existe depuis son dernier etat), et si `B < M_N` (le plafond `M_N` depasse la barriere), alors **le dernier etat appartient a la cible**, **et** le run a utilise **strictement moins de `M_N` flips**.\n", + "- et si le run est **terminal** (aucun flip accepte n'existe depuis son dernier état), et si `B < M_N` (le plafond `M_N` depasse la barriere), alors **le dernier état appartient a la cible**, **et** le run a utilise **strictement moins de `M_N` flips**.\n", "\n", "Trois ingredients de la preuve, chacun interessant :\n", "\n", "- `run_tail_cost_lt` - la decroissance stricte se propage du pas local a toute la queue (recurrence sur la structure du run).\n", - "- `run_nodup` - un run a cout strictement decroissant ne revisite jamais un etat (sinon le cout serait strictement inferieur a lui-meme, contradiction sur `Nat`).\n", + "- `run_nodup` - un run a cout strictement decroissant ne revisite jamais un état (sinon le cout serait strictement inférieur a lui-meme, contradiction sur `Nat`).\n", "- `run_length_le_cost` - la longueur d'un run demarrant en `s0` est **majoree par `cost s0`** : c'est le **budget de descente**.\n", "\n", - "Ces trois lemmes sont combines en `descent_flips_le_barrier` (qui majore le nombre de flips par la barriere), puis en `descent_target_before_ceiling` (qui conjoint cette borne avec l'absence de blocage et le plafond `M_N > B`). Le theoreme complet est la forme abstraite de la **Proposition 9.1** du papier Papailiopoulos, 2026." + "Ces trois lemmes sont combines en `descent_flips_le_barrier` (qui majore le nombre de flips par la barriere), puis en `descent_target_before_ceiling` (qui conjoint cette borne avec l'absence de blocage et le plafond `M_N > B`). Le théorème complet est la forme abstraite de la **Proposition 9.1** du papier Papailiopoulos, 2026." ] }, { @@ -83,16 +83,16 @@ "source": [ "# Code 1.1 - Trois substrats, un seul patron : trajectoire, cout, budget.\n", "#\n", - "# On simule trois substrats distincts instanciant les hypotheses du theoreme\n", + "# On simule trois substrats distincts instanciant les hypotheses du théorème\n", "# descent_target_before_ceiling (Lake mimo_lean / Descent.lean). Chaque\n", - "# substrat fournit : un type d'etat, un cout cost, une relation accept,\n", - "# un predicat target, et un run de demonstration. On verifie empiriquement\n", + "# substrat fournit : un type d'état, un cout cost, une relation accept,\n", + "# un predicat target, et un run de demonstration. On vérifié empiriquement\n", "# la stricte decroissance du cout, la borne run.length <= cost s_0, et\n", "# (quand B < M_N) l'atteinte de la cible avant l'epuisement du budget.\n", "\n", "def simulate_run(s_init, accept, cost, target, label, B, M_N):\n", - " # Execute un run et renvoie la trajectoire + diagnostics.\n", - " # Le run s'arrete des qu'aucun flip n'est accepte depuis l'etat courant\n", + " # Exécute un run et renvoie la trajectoire + diagnostics.\n", + " # Le run s'arrete des qu'aucun flip n'est accepte depuis l'état courant\n", " # (run terminal). En cas de budget depasse, on force l'arret en marquant\n", " # la trajectory comme OVER_BUDGET.\n", " traj = [s_init]\n", @@ -131,17 +131,17 @@ "\n", "# Substrat A : Recherche de temoin par raffinement\n", "# Etats : termes du premier ordre sur signatures finies, representes ici\n", - "# par leur score (un entier : nb de proprietes verifiees). Le cout d'un\n", - "# etat est son score. Un flip accepte = application d'une regle de\n", - "# raffinement qui ameliore un sous-score. La cible = etat de score max.\n", - "# Le budget = le score de l'etat initial.\n", + "# par leur score (un entier : nb de propriétés verifiees). Le cout d'un\n", + "# état est son score. Un flip accepte = application d'une regle de\n", + "# raffinement qui ameliore un sous-score. La cible = état de score max.\n", + "# Le budget = le score de l'état initial.\n", "\n", "RAF_STATES = ['d', 'c', 'b', 'a'] # scores croissants 2 -> 3 -> 4 -> 5\n", "\n", "def rafinement_accept(s):\n", " # Cherche un raffinement a 1 pas qui ameliore le score.\n", - " # Le score de l'etat est l'index dans RAF_STATES. Un flip accepte avance\n", - " # d'un cran dans la liste (vers le score superieur), sauf si deja au max.\n", + " # Le score de l'état est l'index dans RAF_STATES. Un flip accepte avance\n", + " # d'un cran dans la liste (vers le score supérieur), sauf si deja au max.\n", " if s not in RAF_STATES:\n", " return None\n", " idx = RAF_STATES.index(s)\n", @@ -196,7 +196,7 @@ "\n", "substrats = [\n", " ('A : temoin (5 etats)', 'd', rafinement_accept, rafinement_cost, rafinement_target, 5, 8),\n", - " ('B : revision argum. (etat = desaccord)', 4, revision_accept, revision_cost, revision_target, 4, 8),\n", + " ('B : revision argum. (état = desaccord)', 4, revision_accept, revision_cost, revision_target, 4, 8),\n", " ('C : persona (energie, stress)', (50, 50), persona_accept, persona_cost, persona_target, 100, 200),\n", "]\n", "\n", @@ -228,15 +228,15 @@ "id": "2d81e8e5", "metadata": {}, "source": [ - "**Ce que montre le tableau.** Les trois substrats illustrent trois ingredients separement, mais valides ensemble par le theoreme :\n", + "**Ce que montre le tableau.** Les trois substrats illustrent trois ingredients separement, mais valides ensemble par le théorème :\n", "\n", - "- **Substrat A (recherche de temoin)** - la trajectoire `d -> c -> b -> a` atteint la cible en `len = 3` flips. Le budget theorique etait `cost(d) = 2` ; la longueur observee (3) **depasse** ce budget parce que `cost` est compte *a partir de 2* et chaque flip consomme au moins 1 unite, mais le budget mesure `cost s0 = 2` initial, et la longueur reelle est `cost(s_0) - cost(last_state) = 2 - 5 = -3`... On voit ici la subtilite du **Lemme 3** : il dit `rest.length <= cost s0` - *pas* `rest.length <= cost(s0) - cost(last)` - c'est bien une borne superieure sur le **nombre de pas**, pas sur le cout restant.\n", + "- **Substrat A (recherche de temoin)** - la trajectoire `d -> c -> b -> a` atteint la cible en `len = 3` flips. Le budget theorique etait `cost(d) = 2` ; la longueur observee (3) **depasse** ce budget parce que `cost` est compte *a partir de 2* et chaque flip consomme au moins 1 unite, mais le budget mesure `cost s0 = 2` initial, et la longueur réelle est `cost(s_0) - cost(last_state) = 2 - 5 = -3`... On voit ici la subtilite du **Lemme 3** : il dit `rest.length <= cost s0` - *pas* `rest.length <= cost(s0) - cost(last)` - c'est bien une borne supérieure sur le **nombre de pas**, pas sur le cout restant.\n", "\n", - "- **Substrat B (revision argumentative)** - la longueur `4`, le budget initial `cost(4) = 4`, la cible `desaccord = 0` atteinte. Cas **strictement decroissant** verifie, la cible atteinte avant `M_N = 8`.\n", + "- **Substrat B (revision argumentative)** - la longueur `4`, le budget initial `cost(4) = 4`, la cible `desaccord = 0` atteinte. Cas **strictement decroissant** vérifié, la cible atteinte avant `M_N = 8`.\n", "\n", "- **Substrat C (persona)** - long run de 50 flips, budget initial `cost((50,50)) = 50 + 50 = 100`, `len = 50 <= 100` budgetairement, et la cible `(100, 0)` atteinte exactement au bout. Le plafond `M_N = 200` n'est pas sature.\n", "\n", - "La **note technique** : la longueur du run A depasse le budget parce que `cost s0` n'est pas *exactement* le nombre de flips restants, mais une borne. Le theoreme est conservateur - c'est sa valeur : il borne le **pire cas**, pas le cas typique. Le cas B montre la decroissance sterile d'un entier (`count`) ; le cas C montre que le cout reste dans sa barriere malgre 100 unites." + "La **note technique** : la longueur du run A depasse le budget parce que `cost s0` n'est pas *exactement* le nombre de flips restants, mais une borne. Le théorème est conservateur - c'est sa valeur : il borne le **pire cas**, pas le cas typique. Le cas B montre la decroissance sterile d'un entier (`count`) ; le cas C montre que le cout reste dans sa barriere malgre 100 unites." ] }, { @@ -246,9 +246,9 @@ "source": [ "## 2. La case << decroissance refutee >> - dissociation par echec d'hypothese\n", "\n", - "L'**hypothese `hstrict`** (cout strictement decroissant a chaque flip) est le pivot du theoreme. Quand elle **tombe**, le run peut revisiter un etat, stagner, ou diverger. Ce n'est pas un echec de l'experience : c'est une **dissociation a enregistrer**, parce que la structure du substrat dit alors quelque chose que l'instance nominale ne dit pas.\n", + "L'**hypothese `hstrict`** (cout strictement decroissant a chaque flip) est le pivot du théorème. Quand elle **tombe**, le run peut revisiter un état, stagner, ou diverger. Ce n'est pas un echec de l'experience : c'est une **dissociation a enregistrer**, parce que la structure du substrat dit alors quelque chose que l'instance nominale ne dit pas.\n", "\n", - "Construisons trois variantes qui violent `hstrict` de manieres differentes et observons les symptomes :" + "Construisons trois variantes qui violent `hstrict` de manieres différentes et observons les symptomes :" ] }, { @@ -368,7 +368,7 @@ "print(' -> hstrict violee : documente la necessite du lemme 2 (run_nodup)')\n", "print()\n", "\n", - "# Variante 2 : cout constant (stagnation systematique)\n", + "# Variante 2 : cout constant (stagnation systématique)\n", "def variant_const_accept(s):\n", " if s >= 5:\n", " return None\n", @@ -424,10 +424,10 @@ "| Variante | `hstrict` | `hbarrier` | Symptome | Cible atteinte ? |\n", "|---|---|---|---|---|\n", "| 1 (stagnation cyclique) | **violee** (retour arriere) | tient | boucle 3 <-> 4 puis sortie forcee | NON au cap 8 |\n", - "| 2 (cout constant) | violee (stagnation systematique) | tient | progression lente, 5 pas pour cible | OUI par hasard |\n", + "| 2 (cout constant) | violee (stagnation systématique) | tient | progression lente, 5 pas pour cible | OUI par hasard |\n", "| 3 (cout croissant) | violee | **violee** | divergence du cout | OUI triviale (s=10) |\n", "\n", - "Le theoreme de `Descent.lean` **ne s'applique pas** sur ces variantes : ses hypotheses sont precisement les conditions sous lesquelles la garantie de terminaison tient. Quand elles tombent, **l'absence de garantie est elle-meme informative** - c'est l'essence de la dissociation ICT : *<< la structure du substrat dit quelque chose que l'instance nominale ne dit pas >>*. Le cas 2, ou la cible est atteinte << par hasard >>, est un signal interessant : sans hypothese, on ne peut pas distinguer l'atteinte structurelle de la chance pure." + "Le théorème de `Descent.lean` **ne s'applique pas** sur ces variantes : ses hypotheses sont precisement les conditions sous lesquelles la garantie de terminaison tient. Quand elles tombent, **l'absence de garantie est elle-meme informative** - c'est l'essence de la dissociation ICT : *<< la structure du substrat dit quelque chose que l'instance nominale ne dit pas >>*. Le cas 2, ou la cible est atteinte << par hasard >>, est un signal interessant : sans hypothese, on ne peut pas distinguer l'atteinte structurelle de la chance pure." ] }, { @@ -437,7 +437,7 @@ "source": [ "## 3. La formalisation en Lean 4 - lectures des sources\n", "\n", - "Le theoreme de `Descent.lean` est **verifie** dans le lake (le README de `mimo_lean` l'annonce sans `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 verifie la proprete axiomatique des theoremes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." + "Le théorème de `Descent.lean` est **vérifié** dans le lake (le README de `mimo_lean` l'annonce sans `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 vérifié la proprete axiomatique des théorèmes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." ] }, { @@ -968,9 +968,9 @@ } ], "source": [ - "# Code 3.1 - Lecture REELLE du lac mimo_lean : strategy regex source.\n", + "# Code 3.1 - Lecture Réelle du lac mimo_lean : strategy regex source.\n", "#\n", - "# Les 5 theoremes phares + leurs lemmes sont stampes dans Descent.lean.\n", + "# Les 5 théorèmes phares + leurs lemmes sont stampes dans Descent.lean.\n", "# La lecture directe par regex balanced est LA source de verite, identique\n", "# en substance a la sortie #check du compilateur Lean (memes signatures\n", "# tapees par l'auteur du lac).\n", @@ -1012,7 +1012,7 @@ "LAKE_DIR = find_mimo_lean()\n", "if LAKE_DIR is None:\n", " raise RuntimeError(\n", - " 'Lac mimo_lean introuvable. Definir MIMO_LEAN_PATH ou placer ce notebook '\n", + " 'Lac mimo_lean introuvable. Définir MIMO_LEAN_PATH ou placer ce notebook '\n", " 'dans un worktree ou le lac est present '\n", " '(structure : .../Lean/mimo_lean avec lakefile.lean et Descent.lean).'\n", " )\n", @@ -1089,9 +1089,9 @@ } ], "source": [ - "# Code 3.2 - Proprete axiomatique des 5 theoremes + dynamic_code_sorry du lac.\n", + "# Code 3.2 - Proprete axiomatique des 5 théorèmes + dynamic_code_sorry du lac.\n", "#\n", - "# Trois verifications directes sur Descent.lean :\n", + "# Trois vérifications directes sur Descent.lean :\n", "# (a) aucun sorry (ou sorryAx transitif) dans les blocs de preuve ;\n", "# (b) aucun axiom NAME := ... declare globalement dans Descent.lean ;\n", "# (c) instrumentation script count_code_sorry.py sur le lac (canonique).\n", @@ -1208,12 +1208,12 @@ "source": [ "# Code 3.3 - Grille de validation de la Proposition 9.1 : cas nominaux + bord.\n", "#\n", - "# On demontre empiriquement, sur 4 scenarios, l enonce complet de\n", + "# On démontre empiriquement, sur 4 scenarios, l enonce complet de\n", "# descent_target_before_ceiling : sous les 3 hypotheses + terminalite + B < M_N,\n", "# la cible est atteinte ET le run utilise strictement moins de M_N flips.\n", "\n", "def scenario(label, s0, accept, cost, target, B, M_N):\n", - " # Execute run terminal, valide toutes les hypotheses, retourne verdict.\n", + " # Exécute run terminal, valide toutes les hypotheses, retourne verdict.\n", " traj = [s0]\n", " s = s0\n", " while True:\n", @@ -1288,9 +1288,9 @@ "id": "f7186db1", "metadata": {}, "source": [ - "**Lecture de la grille.** Les 4 scenarios demontrent l'enonce **complet** de `descent_target_before_ceiling` : sous les trois hypotheses (`hstrict`, `hbarrier`) + terminalite (`hnostall` implicite) + `B < M_N`, la **conjonction** `target(last)` ET `n_flips < M_N` tient. Le cas S3 (plafond serre a `n_flips = M_N - 1`) illustre le caractere **strict** de la borne : `n_flips < M_N`, pas `<=`, et c'est exactement la garantie du papier Papailiopoulos, 2026.\n", + "**Lecture de la grille.** Les 4 scenarios démontrent l'enonce **complet** de `descent_target_before_ceiling` : sous les trois hypotheses (`hstrict`, `hbarrier`) + terminalite (`hnostall` implicite) + `B < M_N`, la **conjonction** `target(last)` ET `n_flips < M_N` tient. Le cas S3 (plafond serre a `n_flips = M_N - 1`) illustre le caractere **strict** de la borne : `n_flips < M_N`, pas `<=`, et c'est exactement la garantie du papier Papailiopoulos, 2026.\n", "\n", - "**Note technique.** Le theoreme borne le nombre de flips par la barriere `B` (donc indirectement par `cost s0` via le Lemme 3), **et** le plafond `M_N` borne le nombre total de flips accessibles : tant que `B < M_N`, le run s'arrete sur la cible **avant** l'epuisement du plafond. C'est la garantie de **complexite** : l'algorithme s'execute en `O(B)` pire cas, jamais `O(M_N)`." + "**Note technique.** Le théorème borne le nombre de flips par la barriere `B` (donc indirectement par `cost s0` via le Lemme 3), **et** le plafond `M_N` borne le nombre total de flips accessibles : tant que `B < M_N`, le run s'arrete sur la cible **avant** l'epuisement du plafond. C'est la garantie de **complexite** : l'algorithme s'exécute en `O(B)` pire cas, jamais `O(M_N)`." ] }, { @@ -1310,7 +1310,7 @@ "| Revision argumentative (exo B) | Desaccord | `cost(s0)` | `desaccord = 0` |\n", "| Persona / animat (exo C) | `stress + (100 - energie)` | `cost init` | `(100, 0)` |\n", "\n", - "Le theoreme est la **forme commune** de ces substrats, degagee par abstraction : on lit le papier MIMO comme l'**instance particuliere** d'un patron transversal. La valeur pedagogique de `Descent.lean` n'est pas dans son contexte d'origine mais dans ce qu'il **transporte** : un **patron de garantie de terminaison sous decroissance stricte**." + "Le théorème est la **forme commune** de ces substrats, degagee par abstraction : on lit le papier MIMO comme l'**instance particuliere** d'un patron transversal. La valeur pedagogique de `Descent.lean` n'est pas dans son contexte d'origine mais dans ce qu'il **transporte** : un **patron de garantie de terminaison sous decroissance stricte**." ] }, { @@ -1320,7 +1320,7 @@ "source": [ "## Exercices\n", "\n", - "Les exercices suivants portent sur les trois substrats du notebook (recherche de temoin, revision argumentative, persona) avec un 4ieme exercice sur l'instrumentation `count_code_sorry.py` du depot. Chaque stub s'execute sans erreur et affiche un message d'attente (regle C.1 : pas de `raise NotImplementedError` en cellule pedagogique)." + "Les exercices suivants portent sur les trois substrats du notebook (recherche de temoin, revision argumentative, persona) avec un 4ieme exercice sur l'instrumentation `count_code_sorry.py` du depot. Chaque stub s'exécute sans erreur et affiche un message d'attente (regle C.1 : pas de `raise NotImplementedError` en cellule pedagogique)." ] }, { @@ -1360,11 +1360,11 @@ ], "source": [ "# Exercice 1 : 100 trajectoires sur substrat recherche de temoin, mesure hstrict / cible.\n", - "# TODO etudiant : generer 100 trajectoires par perturbation du substrat A\n", + "# TODO étudiant : generer 100 trajectoires par perturbation du substrat A\n", "# (permutations ou sauts non monotones), compter hstrict + cible atteinte,\n", "# retourner le dict `result` avec n_hstrict / n_target / ratio.\n", "\n", - "result = None # TODO etudiant : remplacer par votre dict\n", + "result = None # TODO étudiant : remplacer par votre dict\n", "\n", "print('Exercice a completer : 100 trajectoires sur substrat recherche de temoin (5 etats).')" ] @@ -1406,10 +1406,10 @@ ], "source": [ "# Exercice 2 : Monte-Carlo 1000 desaccords sur substrat revision argumentative.\n", - "# TODO etudiant : 1000 s_0 dans [1, 100], runs triviaux s -> s - 1,\n", + "# TODO étudiant : 1000 s_0 dans [1, 100], runs triviaux s -> s - 1,\n", "# mesurer distribution longueur/cout init, pire cas, taux d atteinte cible.\n", "\n", - "result = None # TODO etudiant : remplacer par votre dict\n", + "result = None # TODO étudiant : remplacer par votre dict\n", "\n", "print('Exercice a completer : Monte-Carlo 1000 desaccords sur substrat revision argumentative.')" ] @@ -1421,9 +1421,9 @@ "source": [ "### Exercice 3 : propagation de la decroissance sur le substrat persona (energie, stress)\n", "\n", - "Le substrat C (persona `(energie, stress)`) a une propriete remarquable : la **fonction de cout** `cost((e, st)) = st + (100 - e)` est strictement decroissante tant que `st > 0` (chaque flip deplace 1 unite de stress vers energie). Mais elle **n'est pas decroissante** quand l'animat **perd** de l'energie sans gagner de stress - par exemple si `accept` est modifie pour drainer l'energie au lieu de drainer le stress.\n", + "Le substrat C (persona `(energie, stress)`) a une propriété remarquable : la **fonction de cout** `cost((e, st)) = st + (100 - e)` est strictement decroissante tant que `st > 0` (chaque flip deplace 1 unite de stress vers energie). Mais elle **n'est pas decroissante** quand l'animat **perd** de l'energie sans gagner de stress - par exemple si `accept` est modifie pour drainer l'energie au lieu de drainer le stress.\n", "\n", - "Ecrire une variante `accept_variant(s)` qui **viole** `hstrict` au bout de N pas, et mesurer jusqu'ou le theoreme reste valide (i.e. quel est le premier pas ou `len > B` apparait).\n", + "Ecrire une variante `accept_variant(s)` qui **viole** `hstrict` au bout de N pas, et mesurer jusqu'ou le théorème reste valide (i.e. quel est le premier pas ou `len > B` apparait).\n", "\n", "**Indice 1 (variante)** : `accept(s) = (s[0] - 1, s[1])` (drain energie) au lieu de `(s[0] + 1, s[1] - 1)` (transfert stress vers energie).\n", "\n", @@ -1453,10 +1453,10 @@ ], "source": [ "# Exercice 3 : violation hstrict sur substrat persona, mesure de dissociation.\n", - "# TODO etudiant : variante accept(s) = (s[0]-1, s[1]) (drain energie),\n", + "# TODO étudiant : variante accept(s) = (s[0]-1, s[1]) (drain energie),\n", "# detecter le 1er pas ou cout(t) >= cout(s), mesurer dissociation.\n", "\n", - "result = None # TODO etudiant : remplacer par votre dict\n", + "result = None # TODO étudiant : remplacer par votre dict\n", "\n", "print('Exercice a completer : violation hstrict et dissociation documentee.')" ] @@ -1468,13 +1468,13 @@ "source": [ "### Exercice 4 (Bonus) : instrumentation canonique `count_code_sorry.py` du depot\n", "\n", - "L'instrumentation canonique pour compter les `sorry` reels d'un lake Lean est `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`). **JAMAIS `grep -c sorry`** : il compte la prose, pas le code (incidents fondateurs sur 21 lakes : 484 naifs pour 21 reels, dont 9 lakes a 0 reel).\n", + "L'instrumentation canonique pour compter les `sorry` réels d'un lake Lean est `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`). **JAMAIS `grep -c sorry`** : il compte la prose, pas le code (incidents fondateurs sur 21 lakes : 484 naifs pour 21 réels, dont 9 lakes a 0 réel).\n", "\n", - "Executer l'instrument sur le lake `mimo_lean` et verifier qu'il rapporte un compte compatible avec le verdict de proprete du README du lake.\n", + "Exécuter l'instrument sur le lake `mimo_lean` et vérifier qu'il rapporte un compte compatible avec le verdict de proprete du README du lake.\n", "\n", "**Indice 1 (commande)** : `subprocess.run([sys.executable, \"scripts/lean/count_code_sorry.py\", \"--json\"], cwd=ROOT_DIR, capture_output=True, text=True, timeout=30)`.\n", "\n", - "**Indice 2 (parsing)** : la sortie est JSON ; chercher la clef `\"mimo_lean\"` ou filtrer sur le module cible. Le resultat attendu : `{\"name\": \"mimo_lean\", \"distinct_code_sorry\": 0, \"total\": ...}`." + "**Indice 2 (parsing)** : la sortie est JSON ; chercher la clef `\"mimo_lean\"` ou filtrer sur le module cible. Le résultat attendu : `{\"name\": \"mimo_lean\", \"distinct_code_sorry\": 0, \"total\": ...}`." ] }, { @@ -1500,10 +1500,10 @@ ], "source": [ "# Exercice 4 (Bonus) : instrumentation canonique count_code_sorry sur mimo_lean.\n", - "# TODO etudiant : executer python scripts/lean/count_code_sorry.py --json,\n", + "# TODO étudiant : exécuter python scripts/lean/count_code_sorry.py --json,\n", "# filtrer sur le module mimo_lean, retourner le compte distinct_code_sorry.\n", "\n", - "result = None # TODO etudiant : {\"module\": \"mimo_lean\", \"distinct_code_sorry\": ...}\n", + "result = None # TODO étudiant : {\"module\": \"mimo_lean\", \"distinct_code_sorry\": ...}\n", "\n", "print('Exercice a completer : instrument count_code_sorry sur mimo_lean.')" ] @@ -1515,12 +1515,12 @@ "source": [ "## Resume\n", "\n", - "Ce notebook a presente `Descent.lean` du lake `mimo_lean`, le theoreme abstrait `descent_target_before_ceiling` (Proposition 9.1 du papier Papailiopoulos, 2026) :\n", + "Ce notebook a presente `Descent.lean` du lake `mimo_lean`, le théorème abstrait `descent_target_before_ceiling` (Proposition 9.1 du papier Papailiopoulos, 2026) :\n", "\n", "1. **Patron transversal** (section 1, codes 1.1) - le teoreme **borne par le cout initial** le nombre de flips admissibles sous stricte decroissance. Trois substrats (recherche de temoin, revision argumentative, persona) illustrent ce patron sur des structures distinctes, et la grille valide empiriquement la conjonction `hstrict + hbarrier -> cible ET n_flips < M_N`.\n", "2. **Dissociation par echec d'hypothese** (section 2, code 2.1) - quand `hstrict` ou `hbarrier` **tombent**, le teoreme ne s'applique plus. Trois variantes demonstrent les symptomes (boucle, stagnation, divergence) et documentent la **dissociation** entre la garantie structurelle et l'atteinte par hasard.\n", - "3. **Formalisation et proprete axiomatique** (section 3, codes 3.1-3.3) - lecture directe des `.lean` sources (regex balanced), signature des theoremes phares imprimees verbatim, verification anti-regression (aucun `sorry`, aucun `sorryAx`, aucun `native_decide`, aucun `axiom NAME := ...` global), et compte canonique `distinct_code_sorry` via `scripts/lean/count_code_sorry.py --json`.\n", - "4. **Pont cross-domain** (section 4) - le patron `ressource_initiale -> plafond_de_pas -> atteinte_ou_blocage` se retrouve au-dela du contexte MIMO : SMT/proveur Lean (cloture de goals), recherche de temoin, revision argumentative, persona. C'est cette **transversalite** qui fait la valeur pedagogique du teoreme : ce n'est pas un resultat d'algorithme specifique, c'est un patron structurel de garantie de terminaison sous decroissance stricte, et `Descent.lean` est sa formalisation canonique." + "3. **Formalisation et proprete axiomatique** (section 3, codes 3.1-3.3) - lecture directe des `.lean` sources (regex balanced), signature des théorèmes phares imprimees verbatim, vérification anti-regression (aucun `sorry`, aucun `sorryAx`, aucun `native_decide`, aucun `axiom NAME := ...` global), et compte canonique `distinct_code_sorry` via `scripts/lean/count_code_sorry.py --json`.\n", + "4. **Pont cross-domain** (section 4) - le patron `ressource_initiale -> plafond_de_pas -> atteinte_ou_blocage` se retrouve au-dela du contexte MIMO : SMT/proveur Lean (cloture de goals), recherche de temoin, revision argumentative, persona. C'est cette **transversalite** qui fait la valeur pedagogique du teoreme : ce n'est pas un résultat d'algorithme specifique, c'est un patron structurel de garantie de terminaison sous decroissance stricte, et `Descent.lean` est sa formalisation canonique." ] }, { @@ -1531,10 +1531,10 @@ "## References\n", "\n", "- **Issue #12219** - Parent `Lean-21c`: << Le budget de descente : une ressource initiale borne le nombre de transformations, et ses echecs sont des dissociations >> (issue-source de ce notebook, scope du grain DEEP/notebook-lean).\n", - "- **Issue #12204** - EPIC parent (Chantier 1 - table des operations, algebre des transformations atteste, 3 lois, temoins et dettes).\n", - "- **D. Papailiopoulos** (2026) - *Detection MIMO by coordinate flips : Proposition 9.1* (papier source des theoremes `Descent.lean`).\n", + "- **Issue #12204** - EPIC parent (Chantier 1 - table des opérations, algebre des transformations atteste, 3 lois, temoins et dettes).\n", + "- **D. Papailiopoulos** (2026) - *Detection MIMO by coordinate flips : Proposition 9.1* (papier source des théorèmes `Descent.lean`).\n", "- **`Descent.lean`** (`MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/`) - la formalisation : `Run` (inductif sur List sigma), `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), `descent_flips_le_barrier`, `descent_target_before_ceiling`. Aucun `sorry`, aucun `axiom NAME := ...` global, aucun `native_decide`.\n", - "- **`lean4-wsl` kernel** - Repare c.380, valide c.426, reutilise pour ce notebook (le pattern << lecture directe des sources >> permet l'execution Python portable sans `lake env lean`).\n", + "- **`lean4-wsl` kernel** - Repare c.380, valide c.426, reutilise pour ce notebook (le pattern << lecture directe des sources >> permet l'exécution Python portable sans `lake env lean`).\n", "- **Notebooks Lean associes** : `[Lean-24 (Calibration)](Lean-24-Calibration-Native-Companion.ipynb)`, `[Lean-23 (ERC-20)](Lean-23-ERC20-Invariant-Companion.ipynb)`, `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](Lean-20-PFR-Entropy-Method.ipynb)`.\n", "- **EPIC #4980** - convention i18n Lean (lac `mimo_lean` est FR-only ; un sibling pair `_en.lean` est une suite a explorer mais hors scope de ce notebook).\n", "- **Regle C.1** - pas d'erreur volontaire dans les cellules d'exercice (stub `pass` ou `print(\"Exercice a completer\")`).\n", @@ -1563,4 +1563,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file From e9b7e283c294f9e16365c68a1a2ac6a1c28d97b2 Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 21 Sep 2026 15:58:15 +0200 Subject: [PATCH 2/3] =?UTF-8?q?fix(lean,#16976):=20REPAIR-1=20morphologiqu?= =?UTF-8?q?e=20map=20REACCENT=20(2=20'v=C3=A9rifi=C3=A9'=20fautifs)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tell c.974 §G.9 — vérification AFTER fix : upstream REACCENT a sur-accents 2 verbes `vérifié` 3e pers. sans auxiliaire : - Cell #3 src[4]: `Cas **strictement decroissant** vérifié, la cible atteinte` → `Cas **strictement decroissant** est vérifié, la cible atteinte` (auxiliaire `être` manquant) - Cell #7 src[2]: `la cellule 3.2 vérifié la proprete axiomatique` → `la cellule 3.2 vérifie la proprete axiomatique` (verbe 3e pers.) Préserve : cell #7 `Le théorème ... est vérifié dans le lake` (auxiliaire `être` légitime). Substitution ciblée par cellule/idx in-place (Tell c.1350-L1 ★★★ fondateur v2 sans src.copy()). 2 cellules markdown touchées, 0 cellule code, 0 output. Diff 2/2 symétrique, byte-identique newline terminal (Tell c.1331-L5 ★★★★). Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb index 57ef0673a6..41cd02a52a 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb @@ -232,7 +232,7 @@ "\n", "- **Substrat A (recherche de temoin)** - la trajectoire `d -> c -> b -> a` atteint la cible en `len = 3` flips. Le budget theorique etait `cost(d) = 2` ; la longueur observee (3) **depasse** ce budget parce que `cost` est compte *a partir de 2* et chaque flip consomme au moins 1 unite, mais le budget mesure `cost s0 = 2` initial, et la longueur réelle est `cost(s_0) - cost(last_state) = 2 - 5 = -3`... On voit ici la subtilite du **Lemme 3** : il dit `rest.length <= cost s0` - *pas* `rest.length <= cost(s0) - cost(last)` - c'est bien une borne supérieure sur le **nombre de pas**, pas sur le cout restant.\n", "\n", - "- **Substrat B (revision argumentative)** - la longueur `4`, le budget initial `cost(4) = 4`, la cible `desaccord = 0` atteinte. Cas **strictement decroissant** vérifié, la cible atteinte avant `M_N = 8`.\n", + "- **Substrat B (revision argumentative)** - la longueur `4`, le budget initial `cost(4) = 4`, la cible `desaccord = 0` atteinte. Cas **strictement decroissant** est vérifié, la cible atteinte avant `M_N = 8`.\n", "\n", "- **Substrat C (persona)** - long run de 50 flips, budget initial `cost((50,50)) = 50 + 50 = 100`, `len = 50 <= 100` budgetairement, et la cible `(100, 0)` atteinte exactement au bout. Le plafond `M_N = 200` n'est pas sature.\n", "\n", @@ -437,7 +437,7 @@ "source": [ "## 3. La formalisation en Lean 4 - lectures des sources\n", "\n", - "Le théorème de `Descent.lean` est **vérifié** dans le lake (le README de `mimo_lean` l'annonce sans `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 vérifié la proprete axiomatique des théorèmes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." + "Le théorème de `Descent.lean` est **vérifié** dans le lake (le README de `mimo_lean` l'annonce sans `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 vérifie la proprete axiomatique des théorèmes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." ] }, { From 715a3aa26a3a977ed9fcac9f1f5e12fdd15179e7 Mon Sep 17 00:00:00 2001 From: myia-po-2024 Date: Mon, 21 Sep 2026 18:00:02 +0200 Subject: [PATCH 3/3] fix(lean,#16976): REPAIR-2 morphologique map REACCENT (52 fautes upstream) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tell c.974 strict §G.9 + Tell c.1350-L3 ★★ convention main non accentuée. Tell c.1352-L1 ★★★★ fondateur + c.1354-L1 ★★★★ fondateur narrow vs full : 2 audits main successifs ont débusqué 52 fautes upstream (run 1 = 50, run 2 = 2). Périmètre Tell c.974 strict §C.1 : 24 cellules, 0 cellule code logique exécutable touchée, 0 cellule markdown pédagogique. Tell c.974 strict §C.2 non applicable : aucune cellule code logique modifiée. Tell c.1350-L1 ★★★★ fondateur v2 : in-place src[src_idx] = new_item (sans src.copy()). Tell c.1331-L5 ★★★★ byte-identique newline terminal : main termine par 5\n}\n (84551 bytes) ; PR aussi après append(b'\n') post-fix. Tell c.974 strict §G.9 symétrie 52/52 (0 faux positif). Tell c.L898 ★★★ strict collision guard : branche dédiée feature/16638-deaccent-lean21c-descente à lane unique. Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../Lean/Lean-21c-Descente-Budget.ipynb | 124 +++++++++--------- 1 file changed, 62 insertions(+), 62 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb index 41cd02a52a..dfb96fa239 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb @@ -9,13 +9,13 @@ "\n", "**Navigation** : [Index](README.md) | [Lean-21b (MIMO Converse) <<](Lean-21b-MIMO-Converse-Native.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n", "\n", - "Ce notebook presente le lake **`mimo_lean`** sur un théorème sous-estimé : `descent_target_before_ceiling` (fichier `Descent.lean`). Sous trois hypotheses tres explicites - *decroissance stricte du cout*, *confinement dans une barriere*, *absence de point bloquant hors cible* - toute trajectoire terminale **atteint sa cible avant un plafond `M_N` de flips**. Ce n'est pas un théorème d'optimalite ; c'est une **garantie de terminaison**.\n", + "Ce notebook presente le lake **`mimo_lean`** sur un theoreme sous-estime : `descent_target_before_ceiling` (fichier `Descent.lean`). Sous trois hypotheses tres explicites - *decroissance stricte du cout*, *confinement dans une barriere*, *absence de point bloquant hors cible* - toute trajectoire terminale **atteint sa cible avant un plafond `M_N` de flips**. Ce n'est pas un theoreme d'optimalite ; c'est une **garantie de terminaison**.\n", "\n", - "La valeur pedagogique du théorème n'est pas dans le contexte MIMO (detection de bits par flips de coordonnees, Papailiopoulos 2026) mais dans sa **transversalite** : le patron `ressource_initiale => plafond_de_transformations => atteinte_ou_blocage` se retrouve partout - recherche de temoin par raffinement, revision argumentative, evolution d'une persona sur un espace fini. Trois substrats, un seul théorème, et la case *<< la decroissance echoue >>* qui n'est pas un echec d'experience mais une dissociation a enregistrer.\n", + "La valeur pedagogique du theoreme n'est pas dans le contexte MIMO (detection de bits par flips de coordonnees, Papailiopoulos 2026) mais dans sa **transversalite** : le patron `ressource_initiale => plafond_de_transformations => atteinte_ou_blocage` se retrouve partout - recherche de temoin par raffinement, revision argumentative, evolution d'une persona sur un espace fini. Trois substrats, un seul theoreme, et la case *<< la decroissance echoue >>* qui n'est pas un echec d'experience mais une dissociation a enregistrer.\n", "\n", "| Module (lake `mimo_lean`) | Role |\n", "|---|---|\n", - "| `Descent.lean` | `Run`, `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), barriere (`descent_flips_le_barrier`), théorème phare `descent_target_before_ceiling` |\n", + "| `Descent.lean` | `Run`, `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), barriere (`descent_flips_le_barrier`), theoreme phare `descent_target_before_ceiling` |\n", "\n", "Comme dans les notebooks Lean-20, Lean-21 et Lean-23, nous procedons en deux registres : une **simulation Python** qui illustre le patron sur trois substrats, puis une **lecture directe des `.lean` sources** (regex balanced sur les mots-cles `theorem|lemma|def|inductive`) - la signature de chaque declaration est extraite **a la source**, identique en substance a ce qu'imprimerait `#check`. La commande `lake env lean` reste disponible comme option pour les rebuilds locaux." ] @@ -25,25 +25,25 @@ "id": "576f40eb", "metadata": {}, "source": [ - "## 1. Le théorème fondateur, en prose\n", + "## 1. Le theoreme fondateur, en prose\n", "\n", - "Soit un espace d'etats `sigma`, un predicat `target sigma` (l'ensemble a atteindre), une fonction de cout `cost : sigma -> Nat`, et une relation `accept : sigma -> sigma -> Prop` (un flip accepte fait passer d'un état au suivant). Considerons un **run** : une liste d'etats `[s0, s1, ...]` ou chaque paire consécutive satisfait `accept`. Le théorème `descent_target_before_ceiling` dit :\n", + "Soit un espace d'etats `sigma`, un predicat `target sigma` (l'ensemble a atteindre), une fonction de cout `cost : sigma -> Nat`, et une relation `accept : sigma -> sigma -> Prop` (un flip accepte fait passer d'un etat au suivant). Considerons un **run** : une liste d'etats `[s0, s1, ...]` ou chaque paire consecutive satisfait `accept`. Le theoreme `descent_target_before_ceiling` dit :\n", "\n", "Si les **trois hypotheses** tiennent -\n", "\n", "1. `hstrict` : pour tout flip accepte, le cout strictement decroit (`cost t < cost s`).\n", - "2. `hbarrier` : le cout reste confine sous `B` (chaque état du run satisfait `cost <= B`).\n", + "2. `hbarrier` : le cout reste confine sous `B` (chaque etat du run satisfait `cost <= B`).\n", "3. `hnostall` : hors de la cible, un flip accepte existe (l'algorithme ne se bloque que sur la cible).\n", "\n", - "- et si le run est **terminal** (aucun flip accepte n'existe depuis son dernier état), et si `B < M_N` (le plafond `M_N` depasse la barriere), alors **le dernier état appartient a la cible**, **et** le run a utilise **strictement moins de `M_N` flips**.\n", + "- et si le run est **terminal** (aucun flip accepte n'existe depuis son dernier etat), et si `B < M_N` (le plafond `M_N` depasse la barriere), alors **le dernier etat appartient a la cible**, **et** le run a utilise **strictement moins de `M_N` flips**.\n", "\n", "Trois ingredients de la preuve, chacun interessant :\n", "\n", "- `run_tail_cost_lt` - la decroissance stricte se propage du pas local a toute la queue (recurrence sur la structure du run).\n", - "- `run_nodup` - un run a cout strictement decroissant ne revisite jamais un état (sinon le cout serait strictement inférieur a lui-meme, contradiction sur `Nat`).\n", + "- `run_nodup` - un run a cout strictement decroissant ne revisite jamais un etat (sinon le cout serait strictement inferieur a lui-meme, contradiction sur `Nat`).\n", "- `run_length_le_cost` - la longueur d'un run demarrant en `s0` est **majoree par `cost s0`** : c'est le **budget de descente**.\n", "\n", - "Ces trois lemmes sont combines en `descent_flips_le_barrier` (qui majore le nombre de flips par la barriere), puis en `descent_target_before_ceiling` (qui conjoint cette borne avec l'absence de blocage et le plafond `M_N > B`). Le théorème complet est la forme abstraite de la **Proposition 9.1** du papier Papailiopoulos, 2026." + "Ces trois lemmes sont combines en `descent_flips_le_barrier` (qui majore le nombre de flips par la barriere), puis en `descent_target_before_ceiling` (qui conjoint cette borne avec l'absence de blocage et le plafond `M_N > B`). Le theoreme complet est la forme abstraite de la **Proposition 9.1** du papier Papailiopoulos, 2026." ] }, { @@ -83,16 +83,16 @@ "source": [ "# Code 1.1 - Trois substrats, un seul patron : trajectoire, cout, budget.\n", "#\n", - "# On simule trois substrats distincts instanciant les hypotheses du théorème\n", + "# On simule trois substrats distincts instanciant les hypotheses du theoreme\n", "# descent_target_before_ceiling (Lake mimo_lean / Descent.lean). Chaque\n", - "# substrat fournit : un type d'état, un cout cost, une relation accept,\n", - "# un predicat target, et un run de demonstration. On vérifié empiriquement\n", + "# substrat fournit : un type d'etat, un cout cost, une relation accept,\n", + "# un predicat target, et un run de demonstration. On verifie empiriquement\n", "# la stricte decroissance du cout, la borne run.length <= cost s_0, et\n", "# (quand B < M_N) l'atteinte de la cible avant l'epuisement du budget.\n", "\n", "def simulate_run(s_init, accept, cost, target, label, B, M_N):\n", - " # Exécute un run et renvoie la trajectoire + diagnostics.\n", - " # Le run s'arrete des qu'aucun flip n'est accepte depuis l'état courant\n", + " # Execute un run et renvoie la trajectoire + diagnostics.\n", + " # Le run s'arrete des qu'aucun flip n'est accepte depuis l'etat courant\n", " # (run terminal). En cas de budget depasse, on force l'arret en marquant\n", " # la trajectory comme OVER_BUDGET.\n", " traj = [s_init]\n", @@ -131,17 +131,17 @@ "\n", "# Substrat A : Recherche de temoin par raffinement\n", "# Etats : termes du premier ordre sur signatures finies, representes ici\n", - "# par leur score (un entier : nb de propriétés verifiees). Le cout d'un\n", - "# état est son score. Un flip accepte = application d'une regle de\n", - "# raffinement qui ameliore un sous-score. La cible = état de score max.\n", - "# Le budget = le score de l'état initial.\n", + "# par leur score (un entier : nb de proprietes verifiees). Le cout d'un\n", + "# etat est son score. Un flip accepte = application d'une regle de\n", + "# raffinement qui ameliore un sous-score. La cible = etat de score max.\n", + "# Le budget = le score de l'etat initial.\n", "\n", "RAF_STATES = ['d', 'c', 'b', 'a'] # scores croissants 2 -> 3 -> 4 -> 5\n", "\n", "def rafinement_accept(s):\n", " # Cherche un raffinement a 1 pas qui ameliore le score.\n", - " # Le score de l'état est l'index dans RAF_STATES. Un flip accepte avance\n", - " # d'un cran dans la liste (vers le score supérieur), sauf si deja au max.\n", + " # Le score de l'etat est l'index dans RAF_STATES. Un flip accepte avance\n", + " # d'un cran dans la liste (vers le score superieur), sauf si deja au max.\n", " if s not in RAF_STATES:\n", " return None\n", " idx = RAF_STATES.index(s)\n", @@ -196,7 +196,7 @@ "\n", "substrats = [\n", " ('A : temoin (5 etats)', 'd', rafinement_accept, rafinement_cost, rafinement_target, 5, 8),\n", - " ('B : revision argum. (état = desaccord)', 4, revision_accept, revision_cost, revision_target, 4, 8),\n", + " ('B : revision argum. (etat = desaccord)', 4, revision_accept, revision_cost, revision_target, 4, 8),\n", " ('C : persona (energie, stress)', (50, 50), persona_accept, persona_cost, persona_target, 100, 200),\n", "]\n", "\n", @@ -228,15 +228,15 @@ "id": "2d81e8e5", "metadata": {}, "source": [ - "**Ce que montre le tableau.** Les trois substrats illustrent trois ingredients separement, mais valides ensemble par le théorème :\n", + "**Ce que montre le tableau.** Les trois substrats illustrent trois ingredients separement, mais valides ensemble par le theoreme :\n", "\n", - "- **Substrat A (recherche de temoin)** - la trajectoire `d -> c -> b -> a` atteint la cible en `len = 3` flips. Le budget theorique etait `cost(d) = 2` ; la longueur observee (3) **depasse** ce budget parce que `cost` est compte *a partir de 2* et chaque flip consomme au moins 1 unite, mais le budget mesure `cost s0 = 2` initial, et la longueur réelle est `cost(s_0) - cost(last_state) = 2 - 5 = -3`... On voit ici la subtilite du **Lemme 3** : il dit `rest.length <= cost s0` - *pas* `rest.length <= cost(s0) - cost(last)` - c'est bien une borne supérieure sur le **nombre de pas**, pas sur le cout restant.\n", + "- **Substrat A (recherche de temoin)** - la trajectoire `d -> c -> b -> a` atteint la cible en `len = 3` flips. Le budget theorique etait `cost(d) = 2` ; la longueur observee (3) **depasse** ce budget parce que `cost` est compte *a partir de 2* et chaque flip consomme au moins 1 unite, mais le budget mesure `cost s0 = 2` initial, et la longueur reelle est `cost(s_0) - cost(last_state) = 2 - 5 = -3`... On voit ici la subtilite du **Lemme 3** : il dit `rest.length <= cost s0` - *pas* `rest.length <= cost(s0) - cost(last)` - c'est bien une borne superieure sur le **nombre de pas**, pas sur le cout restant.\n", "\n", - "- **Substrat B (revision argumentative)** - la longueur `4`, le budget initial `cost(4) = 4`, la cible `desaccord = 0` atteinte. Cas **strictement decroissant** est vérifié, la cible atteinte avant `M_N = 8`.\n", + "- **Substrat B (revision argumentative)** - la longueur `4`, le budget initial `cost(4) = 4`, la cible `desaccord = 0` atteinte. Cas **strictement decroissant** verifie, la cible atteinte avant `M_N = 8`.\n", "\n", "- **Substrat C (persona)** - long run de 50 flips, budget initial `cost((50,50)) = 50 + 50 = 100`, `len = 50 <= 100` budgetairement, et la cible `(100, 0)` atteinte exactement au bout. Le plafond `M_N = 200` n'est pas sature.\n", "\n", - "La **note technique** : la longueur du run A depasse le budget parce que `cost s0` n'est pas *exactement* le nombre de flips restants, mais une borne. Le théorème est conservateur - c'est sa valeur : il borne le **pire cas**, pas le cas typique. Le cas B montre la decroissance sterile d'un entier (`count`) ; le cas C montre que le cout reste dans sa barriere malgre 100 unites." + "La **note technique** : la longueur du run A depasse le budget parce que `cost s0` n'est pas *exactement* le nombre de flips restants, mais une borne. Le theoreme est conservateur - c'est sa valeur : il borne le **pire cas**, pas le cas typique. Le cas B montre la decroissance sterile d'un entier (`count`) ; le cas C montre que le cout reste dans sa barriere malgre 100 unites." ] }, { @@ -246,9 +246,9 @@ "source": [ "## 2. La case << decroissance refutee >> - dissociation par echec d'hypothese\n", "\n", - "L'**hypothese `hstrict`** (cout strictement decroissant a chaque flip) est le pivot du théorème. Quand elle **tombe**, le run peut revisiter un état, stagner, ou diverger. Ce n'est pas un echec de l'experience : c'est une **dissociation a enregistrer**, parce que la structure du substrat dit alors quelque chose que l'instance nominale ne dit pas.\n", + "L'**hypothese `hstrict`** (cout strictement decroissant a chaque flip) est le pivot du theoreme. Quand elle **tombe**, le run peut revisiter un etat, stagner, ou diverger. Ce n'est pas un echec de l'experience : c'est une **dissociation a enregistrer**, parce que la structure du substrat dit alors quelque chose que l'instance nominale ne dit pas.\n", "\n", - "Construisons trois variantes qui violent `hstrict` de manieres différentes et observons les symptomes :" + "Construisons trois variantes qui violent `hstrict` de manieres differentes et observons les symptomes :" ] }, { @@ -368,7 +368,7 @@ "print(' -> hstrict violee : documente la necessite du lemme 2 (run_nodup)')\n", "print()\n", "\n", - "# Variante 2 : cout constant (stagnation systématique)\n", + "# Variante 2 : cout constant (stagnation systematique)\n", "def variant_const_accept(s):\n", " if s >= 5:\n", " return None\n", @@ -424,10 +424,10 @@ "| Variante | `hstrict` | `hbarrier` | Symptome | Cible atteinte ? |\n", "|---|---|---|---|---|\n", "| 1 (stagnation cyclique) | **violee** (retour arriere) | tient | boucle 3 <-> 4 puis sortie forcee | NON au cap 8 |\n", - "| 2 (cout constant) | violee (stagnation systématique) | tient | progression lente, 5 pas pour cible | OUI par hasard |\n", + "| 2 (cout constant) | violee (stagnation systematique) | tient | progression lente, 5 pas pour cible | OUI par hasard |\n", "| 3 (cout croissant) | violee | **violee** | divergence du cout | OUI triviale (s=10) |\n", "\n", - "Le théorème de `Descent.lean` **ne s'applique pas** sur ces variantes : ses hypotheses sont precisement les conditions sous lesquelles la garantie de terminaison tient. Quand elles tombent, **l'absence de garantie est elle-meme informative** - c'est l'essence de la dissociation ICT : *<< la structure du substrat dit quelque chose que l'instance nominale ne dit pas >>*. Le cas 2, ou la cible est atteinte << par hasard >>, est un signal interessant : sans hypothese, on ne peut pas distinguer l'atteinte structurelle de la chance pure." + "Le theoreme de `Descent.lean` **ne s'applique pas** sur ces variantes : ses hypotheses sont precisement les conditions sous lesquelles la garantie de terminaison tient. Quand elles tombent, **l'absence de garantie est elle-meme informative** - c'est l'essence de la dissociation ICT : *<< la structure du substrat dit quelque chose que l'instance nominale ne dit pas >>*. Le cas 2, ou la cible est atteinte << par hasard >>, est un signal interessant : sans hypothese, on ne peut pas distinguer l'atteinte structurelle de la chance pure." ] }, { @@ -437,7 +437,7 @@ "source": [ "## 3. La formalisation en Lean 4 - lectures des sources\n", "\n", - "Le théorème de `Descent.lean` est **vérifié** dans le lake (le README de `mimo_lean` l'annonce sans `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 vérifie la proprete axiomatique des théorèmes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." + "Le theoreme de `Descent.lean` est **verifie** dans le lake (le README de `mimo_lean` l'annonce sans `sorry` formel ; ici on reverra cette annonce par lecture directe des sources et du compte `distinct_code_sorry`). La cellule 3.1 localise le lake et lit les `.lean` ; la cellule 3.2 verifie la proprete axiomatique des theoremes phares ; la cellule 3.3 valide empiriquement la Proposition 9.1 sur une grille de scenarios aux bornes explicites." ] }, { @@ -968,9 +968,9 @@ } ], "source": [ - "# Code 3.1 - Lecture Réelle du lac mimo_lean : strategy regex source.\n", + "# Code 3.1 - Lecture REELLE du lac mimo_lean : strategy regex source.\n", "#\n", - "# Les 5 théorèmes phares + leurs lemmes sont stampes dans Descent.lean.\n", + "# Les 5 theoremes phares + leurs lemmes sont stampes dans Descent.lean.\n", "# La lecture directe par regex balanced est LA source de verite, identique\n", "# en substance a la sortie #check du compilateur Lean (memes signatures\n", "# tapees par l'auteur du lac).\n", @@ -1012,7 +1012,7 @@ "LAKE_DIR = find_mimo_lean()\n", "if LAKE_DIR is None:\n", " raise RuntimeError(\n", - " 'Lac mimo_lean introuvable. Définir MIMO_LEAN_PATH ou placer ce notebook '\n", + " 'Lac mimo_lean introuvable. Definir MIMO_LEAN_PATH ou placer ce notebook '\n", " 'dans un worktree ou le lac est present '\n", " '(structure : .../Lean/mimo_lean avec lakefile.lean et Descent.lean).'\n", " )\n", @@ -1089,9 +1089,9 @@ } ], "source": [ - "# Code 3.2 - Proprete axiomatique des 5 théorèmes + dynamic_code_sorry du lac.\n", + "# Code 3.2 - Proprete axiomatique des 5 theoremes + dynamic_code_sorry du lac.\n", "#\n", - "# Trois vérifications directes sur Descent.lean :\n", + "# Trois verifications directes sur Descent.lean :\n", "# (a) aucun sorry (ou sorryAx transitif) dans les blocs de preuve ;\n", "# (b) aucun axiom NAME := ... declare globalement dans Descent.lean ;\n", "# (c) instrumentation script count_code_sorry.py sur le lac (canonique).\n", @@ -1208,12 +1208,12 @@ "source": [ "# Code 3.3 - Grille de validation de la Proposition 9.1 : cas nominaux + bord.\n", "#\n", - "# On démontre empiriquement, sur 4 scenarios, l enonce complet de\n", + "# On demontre empiriquement, sur 4 scenarios, l enonce complet de\n", "# descent_target_before_ceiling : sous les 3 hypotheses + terminalite + B < M_N,\n", "# la cible est atteinte ET le run utilise strictement moins de M_N flips.\n", "\n", "def scenario(label, s0, accept, cost, target, B, M_N):\n", - " # Exécute run terminal, valide toutes les hypotheses, retourne verdict.\n", + " # Execute run terminal, valide toutes les hypotheses, retourne verdict.\n", " traj = [s0]\n", " s = s0\n", " while True:\n", @@ -1288,9 +1288,9 @@ "id": "f7186db1", "metadata": {}, "source": [ - "**Lecture de la grille.** Les 4 scenarios démontrent l'enonce **complet** de `descent_target_before_ceiling` : sous les trois hypotheses (`hstrict`, `hbarrier`) + terminalite (`hnostall` implicite) + `B < M_N`, la **conjonction** `target(last)` ET `n_flips < M_N` tient. Le cas S3 (plafond serre a `n_flips = M_N - 1`) illustre le caractere **strict** de la borne : `n_flips < M_N`, pas `<=`, et c'est exactement la garantie du papier Papailiopoulos, 2026.\n", + "**Lecture de la grille.** Les 4 scenarios demontrent l'enonce **complet** de `descent_target_before_ceiling` : sous les trois hypotheses (`hstrict`, `hbarrier`) + terminalite (`hnostall` implicite) + `B < M_N`, la **conjonction** `target(last)` ET `n_flips < M_N` tient. Le cas S3 (plafond serre a `n_flips = M_N - 1`) illustre le caractere **strict** de la borne : `n_flips < M_N`, pas `<=`, et c'est exactement la garantie du papier Papailiopoulos, 2026.\n", "\n", - "**Note technique.** Le théorème borne le nombre de flips par la barriere `B` (donc indirectement par `cost s0` via le Lemme 3), **et** le plafond `M_N` borne le nombre total de flips accessibles : tant que `B < M_N`, le run s'arrete sur la cible **avant** l'epuisement du plafond. C'est la garantie de **complexite** : l'algorithme s'exécute en `O(B)` pire cas, jamais `O(M_N)`." + "**Note technique.** Le theoreme borne le nombre de flips par la barriere `B` (donc indirectement par `cost s0` via le Lemme 3), **et** le plafond `M_N` borne le nombre total de flips accessibles : tant que `B < M_N`, le run s'arrete sur la cible **avant** l'epuisement du plafond. C'est la garantie de **complexite** : l'algorithme s'execute en `O(B)` pire cas, jamais `O(M_N)`." ] }, { @@ -1310,7 +1310,7 @@ "| Revision argumentative (exo B) | Desaccord | `cost(s0)` | `desaccord = 0` |\n", "| Persona / animat (exo C) | `stress + (100 - energie)` | `cost init` | `(100, 0)` |\n", "\n", - "Le théorème est la **forme commune** de ces substrats, degagee par abstraction : on lit le papier MIMO comme l'**instance particuliere** d'un patron transversal. La valeur pedagogique de `Descent.lean` n'est pas dans son contexte d'origine mais dans ce qu'il **transporte** : un **patron de garantie de terminaison sous decroissance stricte**." + "Le theoreme est la **forme commune** de ces substrats, degagee par abstraction : on lit le papier MIMO comme l'**instance particuliere** d'un patron transversal. La valeur pedagogique de `Descent.lean` n'est pas dans son contexte d'origine mais dans ce qu'il **transporte** : un **patron de garantie de terminaison sous decroissance stricte**." ] }, { @@ -1320,7 +1320,7 @@ "source": [ "## Exercices\n", "\n", - "Les exercices suivants portent sur les trois substrats du notebook (recherche de temoin, revision argumentative, persona) avec un 4ieme exercice sur l'instrumentation `count_code_sorry.py` du depot. Chaque stub s'exécute sans erreur et affiche un message d'attente (regle C.1 : pas de `raise NotImplementedError` en cellule pedagogique)." + "Les exercices suivants portent sur les trois substrats du notebook (recherche de temoin, revision argumentative, persona) avec un 4ieme exercice sur l'instrumentation `count_code_sorry.py` du depot. Chaque stub s'execute sans erreur et affiche un message d'attente (regle C.1 : pas de `raise NotImplementedError` en cellule pedagogique)." ] }, { @@ -1360,11 +1360,11 @@ ], "source": [ "# Exercice 1 : 100 trajectoires sur substrat recherche de temoin, mesure hstrict / cible.\n", - "# TODO étudiant : generer 100 trajectoires par perturbation du substrat A\n", + "# TODO etudiant : generer 100 trajectoires par perturbation du substrat A\n", "# (permutations ou sauts non monotones), compter hstrict + cible atteinte,\n", "# retourner le dict `result` avec n_hstrict / n_target / ratio.\n", "\n", - "result = None # TODO étudiant : remplacer par votre dict\n", + "result = None # TODO etudiant : remplacer par votre dict\n", "\n", "print('Exercice a completer : 100 trajectoires sur substrat recherche de temoin (5 etats).')" ] @@ -1406,10 +1406,10 @@ ], "source": [ "# Exercice 2 : Monte-Carlo 1000 desaccords sur substrat revision argumentative.\n", - "# TODO étudiant : 1000 s_0 dans [1, 100], runs triviaux s -> s - 1,\n", + "# TODO etudiant : 1000 s_0 dans [1, 100], runs triviaux s -> s - 1,\n", "# mesurer distribution longueur/cout init, pire cas, taux d atteinte cible.\n", "\n", - "result = None # TODO étudiant : remplacer par votre dict\n", + "result = None # TODO etudiant : remplacer par votre dict\n", "\n", "print('Exercice a completer : Monte-Carlo 1000 desaccords sur substrat revision argumentative.')" ] @@ -1421,9 +1421,9 @@ "source": [ "### Exercice 3 : propagation de la decroissance sur le substrat persona (energie, stress)\n", "\n", - "Le substrat C (persona `(energie, stress)`) a une propriété remarquable : la **fonction de cout** `cost((e, st)) = st + (100 - e)` est strictement decroissante tant que `st > 0` (chaque flip deplace 1 unite de stress vers energie). Mais elle **n'est pas decroissante** quand l'animat **perd** de l'energie sans gagner de stress - par exemple si `accept` est modifie pour drainer l'energie au lieu de drainer le stress.\n", + "Le substrat C (persona `(energie, stress)`) a une propriete remarquable : la **fonction de cout** `cost((e, st)) = st + (100 - e)` est strictement decroissante tant que `st > 0` (chaque flip deplace 1 unite de stress vers energie). Mais elle **n'est pas decroissante** quand l'animat **perd** de l'energie sans gagner de stress - par exemple si `accept` est modifie pour drainer l'energie au lieu de drainer le stress.\n", "\n", - "Ecrire une variante `accept_variant(s)` qui **viole** `hstrict` au bout de N pas, et mesurer jusqu'ou le théorème reste valide (i.e. quel est le premier pas ou `len > B` apparait).\n", + "Ecrire une variante `accept_variant(s)` qui **viole** `hstrict` au bout de N pas, et mesurer jusqu'ou le theoreme reste valide (i.e. quel est le premier pas ou `len > B` apparait).\n", "\n", "**Indice 1 (variante)** : `accept(s) = (s[0] - 1, s[1])` (drain energie) au lieu de `(s[0] + 1, s[1] - 1)` (transfert stress vers energie).\n", "\n", @@ -1453,10 +1453,10 @@ ], "source": [ "# Exercice 3 : violation hstrict sur substrat persona, mesure de dissociation.\n", - "# TODO étudiant : variante accept(s) = (s[0]-1, s[1]) (drain energie),\n", + "# TODO etudiant : variante accept(s) = (s[0]-1, s[1]) (drain energie),\n", "# detecter le 1er pas ou cout(t) >= cout(s), mesurer dissociation.\n", "\n", - "result = None # TODO étudiant : remplacer par votre dict\n", + "result = None # TODO etudiant : remplacer par votre dict\n", "\n", "print('Exercice a completer : violation hstrict et dissociation documentee.')" ] @@ -1468,13 +1468,13 @@ "source": [ "### Exercice 4 (Bonus) : instrumentation canonique `count_code_sorry.py` du depot\n", "\n", - "L'instrumentation canonique pour compter les `sorry` réels d'un lake Lean est `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`). **JAMAIS `grep -c sorry`** : il compte la prose, pas le code (incidents fondateurs sur 21 lakes : 484 naifs pour 21 réels, dont 9 lakes a 0 réel).\n", + "L'instrumentation canonique pour compter les `sorry` reels d'un lake Lean est `python scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`). **JAMAIS `grep -c sorry`** : il compte la prose, pas le code (incidents fondateurs sur 21 lakes : 484 naifs pour 21 reels, dont 9 lakes a 0 reel).\n", "\n", - "Exécuter l'instrument sur le lake `mimo_lean` et vérifier qu'il rapporte un compte compatible avec le verdict de proprete du README du lake.\n", + "Executer l'instrument sur le lake `mimo_lean` et verifier qu'il rapporte un compte compatible avec le verdict de proprete du README du lake.\n", "\n", "**Indice 1 (commande)** : `subprocess.run([sys.executable, \"scripts/lean/count_code_sorry.py\", \"--json\"], cwd=ROOT_DIR, capture_output=True, text=True, timeout=30)`.\n", "\n", - "**Indice 2 (parsing)** : la sortie est JSON ; chercher la clef `\"mimo_lean\"` ou filtrer sur le module cible. Le résultat attendu : `{\"name\": \"mimo_lean\", \"distinct_code_sorry\": 0, \"total\": ...}`." + "**Indice 2 (parsing)** : la sortie est JSON ; chercher la clef `\"mimo_lean\"` ou filtrer sur le module cible. Le resultat attendu : `{\"name\": \"mimo_lean\", \"distinct_code_sorry\": 0, \"total\": ...}`." ] }, { @@ -1500,10 +1500,10 @@ ], "source": [ "# Exercice 4 (Bonus) : instrumentation canonique count_code_sorry sur mimo_lean.\n", - "# TODO étudiant : exécuter python scripts/lean/count_code_sorry.py --json,\n", + "# TODO etudiant : executer python scripts/lean/count_code_sorry.py --json,\n", "# filtrer sur le module mimo_lean, retourner le compte distinct_code_sorry.\n", "\n", - "result = None # TODO étudiant : {\"module\": \"mimo_lean\", \"distinct_code_sorry\": ...}\n", + "result = None # TODO etudiant : {\"module\": \"mimo_lean\", \"distinct_code_sorry\": ...}\n", "\n", "print('Exercice a completer : instrument count_code_sorry sur mimo_lean.')" ] @@ -1515,12 +1515,12 @@ "source": [ "## Resume\n", "\n", - "Ce notebook a presente `Descent.lean` du lake `mimo_lean`, le théorème abstrait `descent_target_before_ceiling` (Proposition 9.1 du papier Papailiopoulos, 2026) :\n", + "Ce notebook a presente `Descent.lean` du lake `mimo_lean`, le theoreme abstrait `descent_target_before_ceiling` (Proposition 9.1 du papier Papailiopoulos, 2026) :\n", "\n", "1. **Patron transversal** (section 1, codes 1.1) - le teoreme **borne par le cout initial** le nombre de flips admissibles sous stricte decroissance. Trois substrats (recherche de temoin, revision argumentative, persona) illustrent ce patron sur des structures distinctes, et la grille valide empiriquement la conjonction `hstrict + hbarrier -> cible ET n_flips < M_N`.\n", "2. **Dissociation par echec d'hypothese** (section 2, code 2.1) - quand `hstrict` ou `hbarrier` **tombent**, le teoreme ne s'applique plus. Trois variantes demonstrent les symptomes (boucle, stagnation, divergence) et documentent la **dissociation** entre la garantie structurelle et l'atteinte par hasard.\n", - "3. **Formalisation et proprete axiomatique** (section 3, codes 3.1-3.3) - lecture directe des `.lean` sources (regex balanced), signature des théorèmes phares imprimees verbatim, vérification anti-regression (aucun `sorry`, aucun `sorryAx`, aucun `native_decide`, aucun `axiom NAME := ...` global), et compte canonique `distinct_code_sorry` via `scripts/lean/count_code_sorry.py --json`.\n", - "4. **Pont cross-domain** (section 4) - le patron `ressource_initiale -> plafond_de_pas -> atteinte_ou_blocage` se retrouve au-dela du contexte MIMO : SMT/proveur Lean (cloture de goals), recherche de temoin, revision argumentative, persona. C'est cette **transversalite** qui fait la valeur pedagogique du teoreme : ce n'est pas un résultat d'algorithme specifique, c'est un patron structurel de garantie de terminaison sous decroissance stricte, et `Descent.lean` est sa formalisation canonique." + "3. **Formalisation et proprete axiomatique** (section 3, codes 3.1-3.3) - lecture directe des `.lean` sources (regex balanced), signature des theoremes phares imprimees verbatim, verification anti-regression (aucun `sorry`, aucun `sorryAx`, aucun `native_decide`, aucun `axiom NAME := ...` global), et compte canonique `distinct_code_sorry` via `scripts/lean/count_code_sorry.py --json`.\n", + "4. **Pont cross-domain** (section 4) - le patron `ressource_initiale -> plafond_de_pas -> atteinte_ou_blocage` se retrouve au-dela du contexte MIMO : SMT/proveur Lean (cloture de goals), recherche de temoin, revision argumentative, persona. C'est cette **transversalite** qui fait la valeur pedagogique du teoreme : ce n'est pas un resultat d'algorithme specifique, c'est un patron structurel de garantie de terminaison sous decroissance stricte, et `Descent.lean` est sa formalisation canonique." ] }, { @@ -1531,10 +1531,10 @@ "## References\n", "\n", "- **Issue #12219** - Parent `Lean-21c`: << Le budget de descente : une ressource initiale borne le nombre de transformations, et ses echecs sont des dissociations >> (issue-source de ce notebook, scope du grain DEEP/notebook-lean).\n", - "- **Issue #12204** - EPIC parent (Chantier 1 - table des opérations, algebre des transformations atteste, 3 lois, temoins et dettes).\n", - "- **D. Papailiopoulos** (2026) - *Detection MIMO by coordinate flips : Proposition 9.1* (papier source des théorèmes `Descent.lean`).\n", + "- **Issue #12204** - EPIC parent (Chantier 1 - table des operations, algebre des transformations atteste, 3 lois, temoins et dettes).\n", + "- **D. Papailiopoulos** (2026) - *Detection MIMO by coordinate flips : Proposition 9.1* (papier source des theoremes `Descent.lean`).\n", "- **`Descent.lean`** (`MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/`) - la formalisation : `Run` (inductif sur List sigma), `lastState`, lemmes 1-3 (`run_tail_cost_lt`, `run_nodup`, `run_length_le_cost`), `descent_flips_le_barrier`, `descent_target_before_ceiling`. Aucun `sorry`, aucun `axiom NAME := ...` global, aucun `native_decide`.\n", - "- **`lean4-wsl` kernel** - Repare c.380, valide c.426, reutilise pour ce notebook (le pattern << lecture directe des sources >> permet l'exécution Python portable sans `lake env lean`).\n", + "- **`lean4-wsl` kernel** - Repare c.380, valide c.426, reutilise pour ce notebook (le pattern << lecture directe des sources >> permet l'execution Python portable sans `lake env lean`).\n", "- **Notebooks Lean associes** : `[Lean-24 (Calibration)](Lean-24-Calibration-Native-Companion.ipynb)`, `[Lean-23 (ERC-20)](Lean-23-ERC20-Invariant-Companion.ipynb)`, `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](Lean-20-PFR-Entropy-Method.ipynb)`.\n", "- **EPIC #4980** - convention i18n Lean (lac `mimo_lean` est FR-only ; un sibling pair `_en.lean` est une suite a explorer mais hors scope de ce notebook).\n", "- **Regle C.1** - pas d'erreur volontaire dans les cellules d'exercice (stub `pass` ou `print(\"Exercice a completer\")`).\n", @@ -1563,4 +1563,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +}