fix(lean,#17357): Lean-21c -- substrat A lu comme violation d'hstrict, tableau et exercice 1 alignes sur les sorties committes

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb

@@ -263,15 +263,15 @@
     "tags": []
    },
    "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 : deux relevent du theoreme, un non -\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)** - le run atteint la cible en `len = 3` flips, mais la colonne `stric. decr. = False` dit l'essentiel : `hstrict` **ne tient pas** sur ce substrat. Les couts `2 -> 3 -> 4 -> 5` croissent vers la cible `a` par construction (`rafinement_cost = {a:5, b:4, c:3, d:2}`). Le theoreme `descent_target_before_ceiling` ne s'applique donc **pas** au run A : confronter son observation a la borne `rest.length <= cost s0` n'a pas de sens - quand l'hypothese tombe, la garantie tombe avec elle (la section 2 fait de ces violations son sujet). Le run atteit malgre tout sa cible : une **dissociation positive** - l'atteinte sans garantie, comme la variante 2 du code 2.1.\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** verifie, la cible atteinte avant `M_N = 8` - et `len = 4 <= cost s0 = 4` : la borne du **Lemme 3** (`rest.length <= cost s0`) porte sur le **nombre de pas**, pas sur le cout restant, et elle est satisfaite.\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** : seule la colonne `stric. decr.` du tableau decide quelles lignes relevent du theoreme. A ne releve pas de `descent_target_before_ceiling` (`hstrict` violee par construction) ; B et C satisfont les hypotheses et leurs longueurs tiennent dans le budget (`4 <= 4`, `50 <= 100`)."
    ]
   },
   {
@@ -486,7 +486,7 @@
     "|---|---|---|---|---|\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",
-    "| 3 (cout croissant) | violee | **violee** | divergence du cout | OUI triviale (s=10) |\n",
+    "| 3 (cout croissant) | violee | **violee** | divergence du cout : 0 -> 18 en 6 pas | **NON** au cap 6 - le cout saute de 9 a 12, la valeur cible `s = 10` n'est jamais visitee |\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."
    ]
@@ -1842,7 +1842,7 @@
     "\n",
     "**Indice 1 (RNG)** : `numpy.random.default_rng(7)` pour la reproductibilite ; les perturbations peuvent etre (a) une permutation des transitions (autre ordre `d -> b -> c -> a`), ou (b) un saut qui augmente le score (`d -> a` direct) qui viole `hstrict`.\n",
     "\n",
-    "**Indice 2 (mesures)** : `result = {\"n_runs\": 100, \"n_hstrict\": ..., \"n_target_atteinte\": ..., \"ratio_hstrict_a_target\": ..., \"longueur_moyenne_run\": ...}`. Le ratio attendu proche de 1 si toutes les permutations sont elles aussi strictement decroissantes, proche de 0.5 si les permutations preservent 50 pourcent des decroissances."
+    "**Indice 2 (mesures)** : `result = {\"n_runs\": 100, \"n_hstrict\": ..., \"n_target_atteinte\": ..., \"ratio_hstrict_a_target\": ..., \"longueur_moyenne_run\": ...}`. Attendu : `n_hstrict = 0` - le cout du substrat A **croit vers la cible par construction** (`{a:5, b:4, c:3, d:2}`, la cible etant `a` ; le tableau du code 1.1 affiche `stric. decr. = False` pour le run de reference), aucune permutation ne peut rendre la marche strictement decroissante. La mesure qui discrimine est l'autre colonne : `n_target_atteinte` proche de 100 signifierait que la cible est atteinte *malgre* la violation d'hstrict (dissociation positive, comme la variante 2 du code 2.1) ; si un saut non monotone pousse des runs hors de la barriere, ce taux baisse - c'est cela que tes 100 trajectoires mesurent."
    ]
   },
   {
@@ -2160,4 +2160,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}