fix(prose,#17636): relay burst w6 c21 -- 9 carnets (ICT-15k, ICT-Life, Lab12b, DecInfer-09, QC-Py-10, Search-03e/09d, CSP-1, MGS-09)

MyIA.AI.Notebooks/IIT/ICT-Series/ICT-15k-RecollementMacroCells.ipynb

@@ -187,7 +187,7 @@
    "source": [
     "### Lecture — le moteur herite du certificat\n",
     "\n",
-    "`blinker` p=2, `bloc` p=1, `glider` 4 pas par case diagonale (vitesse c/4) : le moteur reproduit les constantes canoniques du substrat certifie [ICT-Life-SubstratCertifie](ICT-Life-SubstratCertifie.ipynb), lui-meme adosse au theoreme `hashlife_correct` prouve dans `conway_lean` (zéro `sorry` code, ICT-Life §5). Toute divergence mesuree dans la suite sera donc attributable au **recollement**, pas au moteur.\n"
+    "`blinker` p=2, `bloc` p=1, `glider` 4 pas par case diagonale (vitesse c/4) : le moteur reproduit les constantes canoniques du substrat certifie [ICT-Life-SubstratCertifie](ICT-Life-SubstratCertifie.ipynb), lui-meme adosse au theoreme `hashlife_correct` prouve dans `conway_lean` (ICT-Life §5). Toute divergence mesuree dans la suite sera donc attributable au **recollement**, pas au moteur.\n"
    ]
   },
   {

MyIA.AI.Notebooks/IIT/ICT-Series/ICT-Life-SubstratCertifie.ipynb

@@ -27,15 +27,15 @@
     "5. Le **pont Lean** — ce que `hashlife_correct` garantit exactement, et pourquoi la calibration Python reste nécessaire ;\n",
     "6. Synthèse — le contraste avec les substrats S2 (bistable) et S5 (Gray-Scott), et la route vers le branchement batterie (`ict.agency`, `ict.stake`).\n",
     "\n",
-    "**Module** : `ict/life.py` (issue #5726, tranche 1-2, PR #11185). **Notebook pédagogique** : 3 exercices jalonnent le texte."
+    "**Module** : `ict/life.py` (issue #5726, tranche 1-2, PR #11185). **Notebook pédagogique** : des exercices jalonnent le texte."
    ]
   },
   {
    "cell_type": "markdown",
    "id": "statut-epistemique",
    "metadata": {},
    "source": [
-    "> **Statut épistémique** — **Sans verdict à ce jour** : aucune ligne de la [matrice de dissociations](../../../docs/ict/dissociations-matrix.md) ne concerne ce notebook ; son statut épistémique sera porté par la matrice le cas échéant."
+    "> **Statut épistémique** — **Sans verdict à ce jour** : la [matrice de dissociations](../../../docs/ict/dissociations-matrix.md) ne concerne pas encore ce notebook ; son statut épistémique sera porté par la matrice le cas échéant."
    ]
   },
   {
@@ -753,11 +753,11 @@
    "source": [
     "### Lecture du résultat\n",
     "\n",
-    "Le fichier `HashlifeCorrectness.lean` porte les déclarations de `hashlife_correct` (cas de base) et `hashlife_correctN` (horizon arbitraire), et **zéro** `sorry` au niveau code : le gate qui bloquait l'entrée du Jeu de la Vie dans l'ICT (issue #5726, « dépendance dure ») est levé.\n",
+    "Le fichier `HashlifeCorrectness.lean` porte les déclarations de `hashlife_correct` (cas de base) et `hashlife_correctN` (horizon arbitraire), sans `sorry` au niveau code : le gate qui bloquait l'entrée du Jeu de la Vie dans l'ICT (issue #5726, « dépendance dure ») est levé.\n",
     "\n",
-    "**Les deux colonnes ne mesurent pas la même chose, et l'écart est la leçon.** Un `grep -c sorry` sur ce fichier rend **36** ; le compte réel est **0**. Les 36 sont de la prose — docstrings, feuilles de route, notes de preuve —, et un fichier Lean discute d'autant plus de `sorry` qu'il n'en contient plus. C'est pourquoi la cellule ci-dessus n'écrit pas son propre compteur : `scripts/lean/count_code_sorry.py` retire commentaires et docstrings avant de compter, et c'est l'instrument que le dépôt impose pour toute affirmation de progrès formel. Un motif artisanal se trompe dans les deux sens — il compte la prose, et il rate les formes `:= by sorry`, `exact sorry`, `<;> sorry` qui ne sont pas des lignes isolées.\n",
+    "**Les deux colonnes ne mesurent pas la même chose, et l'écart est la leçon.** Un `grep -c sorry` naïf sur ce fichier compte la prose — docstrings, feuilles de route, notes de preuve —, et un fichier Lean discute d'autant plus de `sorry` qu'il n'en contient plus ; l'écart avec le compte réel au niveau code est celui qu'affichent les deux colonnes ci-dessus. C'est pourquoi la cellule ci-dessus n'écrit pas son propre compteur : `scripts/lean/count_code_sorry.py` retire commentaires et docstrings avant de compter, et c'est l'instrument que le dépôt impose pour toute affirmation de progrès formel. Un motif artisanal se trompe dans les deux sens — il compte la prose, et il rate les formes `:= by sorry`, `exact sorry`, `<;> sorry` qui ne sont pas des lignes isolées.\n",
     "\n",
-    "À l'échelle du lake : **70 fichiers, 1 `sorry` réel distinct** sur **166** occurrences naïves — le seul résidu vivant dans `HashlifeMarginFragment.lean`, documenté comme intrinsèque (#9568) et hors de la chaîne du théorème, exactement comme l'annonce la section précédente. Il apparaît deux fois dans le compte brut parce que la convention i18n du dépôt (#4980) double chaque fichier d'un miroir `_en` ; `distinct_code_sorry` dédoublonne, `code_sorry` non.\n",
+    "À l'échelle du lake : le seul `sorry` réel distinct vit dans `HashlifeMarginFragment.lean`, documenté comme intrinsèque (#9568) et hors de la chaîne du théorème, exactement comme l'annonce la section précédente. Il apparaît deux fois dans le compte brut parce que la convention i18n du dépôt (#4980) double chaque fichier d'un miroir `_en` ; `distinct_code_sorry` dédoublonne, `code_sorry` non.\n",
     "\n",
     "Les trajectoires exportées depuis `ict.life` héritent donc de la garantie **non-vacuous** complète : moteur calibré (sections 2-4) + égalité Hashlife/naïf prouvée par `evolveHashlifeFastAtN_correct_uncond` (cette section, sans hypothèse). Le théorème historique `hashlife_correct` reste vacuously true dans le régime du saut — il ne porte pas cette garantie."
    ]

MyIA.AI.Notebooks/ML/DataScienceWithAgents/Track2-GoogleADK/Day5-DS-Star/Lab12b-Sequential-Orchestration.ipynb

@@ -117,7 +117,7 @@
    "source": [
     "### Lire la configuration attestée : quel moteur a produit ces sorties\n",
     "\n",
-    "La sortie d'import fixe le paramètre d'expérience du notebook en trois lignes : `Provider actif : openrouter`, `Modele : openrouter/openai/gpt-4.1`, `Endpoint externe : True`. C'est l'attestation que tout ce qui suit — la chaîne de désignation, les réponses des spécialistes, le verdict final — est produit par un **vrai moteur LLM externe**, pas par un stub ou une réponse codée en dur : la même exécution sur une autre session pourra confronter ses sorties à celles-ci en connaissant le modèle exact. Le reste de la cellule est de la plomberie assumée : l'insertion de `..` au `sys.path` (les utilitaires de l'atelier) et le filtre ciblé d'un avertissement EXPÉRIMENTAL de la bibliothèque ADK — filtré par motif précis, pas en bloquant tous les warnings."
+    "La sortie d'import fixe le paramètre d'expérience du notebook : `Provider actif : openrouter`, `Modele : openrouter/openai/gpt-4.1`, `Endpoint externe : True`. C'est l'attestation que tout ce qui suit — la chaîne de désignation, les réponses des spécialistes, le verdict final — est produit par un **vrai moteur LLM externe**, pas par un stub ou une réponse codée en dur : la même exécution sur une autre session pourra confronter ses sorties à celles-ci en connaissant le modèle exact. Le reste de la cellule est de la plomberie assumée : l'insertion de `..` au `sys.path` (les utilitaires de l'atelier) et le filtre ciblé d'un avertissement EXPÉRIMENTAL de la bibliothèque ADK — filtré par motif précis, pas en bloquant tous les warnings."
    ]
   },
   {
@@ -724,7 +724,7 @@
    "source": [
     "### Lire les trois exercices : l'échelle des contre-contrats\n",
     "\n",
-    "Les trois cellules d'exercice sont des stubs C.1 suivant le patron canonique du dépôt — chaque invite imprime « Exercice à compléter », aucune erreur volontaire — le notebook s'exécute d'un bout à l'autre, la validation est l'étudiant. L'échelle des énoncés prolonge la leçon : **Exercice 1** place un vérificateur en tête de plan — la question devient « que vérifie-t-on quand rien n'a encore été produit ? », l'ordre du plan comme décision d'architecture ; **Exercice 2** déplace le plan hors des instructions des agents — le même anti-pattern que le notebook vient de démontrer, à refaire tenir par construction ; **Exercice 3** demande un compteur de désignation — instrumenter `agent_hands` pour mesurer qui a pris la parole, l'observable du contrat C4. Trois gestes : inverser, encadrer, instrumenter.\n",
+    "Les cellules d'exercice sont des stubs C.1 suivant le patron canonique du dépôt — chaque invite imprime « Exercice à compléter », aucune erreur volontaire — le notebook s'exécute d'un bout à l'autre, la validation est l'étudiant. L'échelle des énoncés prolonge la leçon : **Exercice 1** place un vérificateur en tête de plan — la question devient « que vérifie-t-on quand rien n'a encore été produit ? », l'ordre du plan comme décision d'architecture ; **Exercice 2** déplace le plan hors des instructions des agents — le même anti-pattern que le notebook vient de démontrer, à refaire tenir par construction ; **Exercice 3** demande un compteur de désignation — instrumenter `agent_hands` pour mesurer qui a pris la parole, l'observable du contrat C4. Trois gestes : inverser, encadrer, instrumenter.\n",
     "\n",
     "Dernière observation, sur la forme : chaque stub imprime l'invite canonique « Exercice à compléter » — le patron du dépôt pour une cellule d'exercice, qui la rend à la fois exécutable et informative : l'output atteste que la cellule a tourné, la place de la solution reste à l'étudiant. Partout ailleurs, chaque cellule de démonstration imprime son observable (le plan déclaré, les mains, les appels d'outils, l'historique) ; la zone d'exercice prend le relais exactement là où l'observable attendu devient celui de l'étudiant — et la conclusion ci-dessous referme le contrat C4 en rappelant ce que la désignation garantit que le handoff ne garantit pas."
    ]

MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-09-Lean-Gittins.ipynb

@@ -44,9 +44,9 @@
     "\n",
     "| Fichier | Contenu | Sorry |\n",
     "|---------|---------|-------|\n",
-    "| `Gittins/Basic.lean` | BanditArm, BanditInstance, Policy, RewardHistory | 0 |\n",
-    "| `Gittins/Discount.lean` | Convergence geometrique, valeur actualisee | 0 (post-#5272 Float->R) |\n",
-    "| `Gittins/GittinsTheorem.lean` | Indice de Gittins, theoreme d'optimalite | 2 (L99 V + L103 proof, INTRINSIC #4039) |\n",
+    "| `Gittins/Basic.lean` | BanditArm, BanditInstance, Policy, RewardHistory | — |\n",
+    "| `Gittins/Discount.lean` | Convergence geometrique, valeur actualisee | post-#5272 Float->R |\n",
+    "| `Gittins/GittinsTheorem.lean` | Indice de Gittins, theoreme d'optimalite | L99 V + L103 proof, INTRINSIC #4039 |\n",
     "\n",
     "***\n",
     "\n",
@@ -2500,7 +2500,7 @@
     "\n",
     "**Séparation et optimalité : un seul mécanisme**. Le théorème ne dit pas seulement « la politique-indice est optimale » — il dit que la comparaison entre bras se **réduit** à des calculs à un bras. Le problème de la retraite (section 4.1) convertit la question contextuelle « quel bras jouer, sachant les autres ? » en une question locale « à partir de quel prix de sortie $M$ ce bras cesse-t-il d'être intéressant ? » : chaque bras devient un problème d'arrêt optimal indépendant, et l'indice est ce prix de sortie. L'optimalité de « jouer l'indice maximal » suit alors de la stationnarité de la section 1.1 : après chaque tirage, le système se présente sous la même forme et l'argument se réapplique à l'identique. C'est cette **liberté vis-à-vis du contexte** qui distingue Gittins — UCB1 compare aussi des bras, mais son bonus n'est pas un prix de sortie, d'où des bornes de regret plutôt qu'une optimalité exacte.\n",
     "\n",
-    "> **Etat de Mathlib** : Les types `Real`, `tsum`, les series geometriques, les temps d'arret existent. Mais il manque un cadre complet de **processus de decision markovien (MDP)**, de **bandits**, et d'**equations de Bellman**. Une formalisation complete est estimee a 2000-5000 lignes de definitions prealables.\n",
+    "> **Etat de Mathlib** : Les types `Real`, `tsum`, les series geometriques, les temps d'arret existent. Mais il manque un cadre complet de **processus de decision markovien (MDP)**, de **bandits**, et d'**equations de Bellman**. Une formalisation complete exigerait d'abord un socle de definitions prealables.\n",
     "\n",
     "**Ce que les cellules précédentes prouvent réellement** : la sortie du théorème le dit sans détour — `policyValue` porte un `sorry` **dans sa définition**, donc `gittins_optimality` compare des quantités non construites : énoncé fidèle en forme, vide en contenu. Les corollaires suivants concluent `True` par `trivial`, et le linter l'affiche dans la sortie (`unused variable h`, `unused variable hγ`) : les hypothèses ne servent à rien. Ce choix — placeholder `True` plutôt que faux théorème — est aligné sur le projet Lake et ses deux barrières documentées : MDP/Bellman absent de Mathlib pour la preuve, FLOAT-ORDER pour les inégalités."
    ]
@@ -2827,8 +2827,6 @@
     "- `Discount.lean` : `geometric_series_converges`, `present_value_constant`, `discount_monotone` — tous prouves via Mathlib\n",
     "- `GittinsTheorem.lean` : `gittinsIndex` (def = `arm.trueMean`, prouve), `gittins_index_known_arm` (prouve par `rfl`), `gittins_beats_greedy` (`trivial`), `gittins_optimality` (sorry — INTRACTABLE : MDP/Bellman absent Mathlib), `gittins_index_monotone_discount` (sorry — barriere FLOAT-ORDER : IEEE 754 sur `Float`, pas d'instance `Preorder`)\n",
     "\n",
-    "**Total sorry (lake)** : 0 (Discount) + 2 (GittinsTheorem) = 2 sorry dans le projet Lake\n",
-    "\n",
     "> Note first-hand c.238.22b : la docstring lake L131 pretend `le_refl` mais ce tactic n'existe pas en Lean 4.31.0 ; la preuve `gittins_index_monotone_discount` du lake a probablement une regression silencieuse post-#5272. Le lake build n'est pas execute localement, donc le bug n'est pas remonte. Cote notebook : `gittins_index_monotone_gamma` reste `sorry` avec FLOAT-ORDER WART documente (Real := Float, pas de `LE Float` derivable).\n",
     "\n",
     "> Post-merge #5272 (Float->R port) : `gittins_index_known_arm` (L117-119 `rfl`), `gittins_index_monotone_discount` (L134-138 `le_refl`), `gittins_beats_greedy` (L141-144 `trivial`) sont maintenant PROUVES. Les 2 sorries residuelles relevent de barrieres INTRINSIC documentees dans le README du lake : (1) MDP/Bellman/optimal-stopping absent de Mathlib (L99 V operator + L103 `gittins_optimality` proof body), (2) FLOAT-ORDER WART sur `Float` (IEEE 754, pas d'instance `Preorder` derivable pour expressions algebriques - `gittins_index_high_uncertainty` reste en sorry local).\n",

MyIA.AI.Notebooks/QuantConnect/Python/QC-Py-10-Risk-Portfolio-Management.ipynb

@@ -56,7 +56,7 @@
     "3. §3 Portfolio Heat, Exposure Limits, Volatility Scaling\n",
     "4. §4 Risk Models natifs QC — `SetRiskManagement()` en pratique\n",
     "\n",
-    "**Exercices** : 3 cellules stub (Exercice #6, #11, #16) :\n",
+    "**Exercices** : cellules stub (Exercice #6, #11, #16) :\n",
     "- **Exercice 1** : Position sizing avec Kelly fraction partielle\n",
     "- **Exercice 2** : Stop-loss adaptatif ATR\n",
     "- **Exercice 3** : Risk budget allocation multi-stratégies\n",
@@ -1893,7 +1893,7 @@
     ")\n",
     "```\n",
     "\n",
-    "**Résultat** : Risk management professionnel en une seule ligne de code, sans logique complexe dans OnData()."
+    "**Résultat** : Risk management professionnel, sans logique complexe dans OnData()."
    ]
   },
   {
@@ -2872,7 +2872,7 @@
     "- **Meilleur Sharpe** : ExposureLimitsAlgorithm (1.076) mais avec un MaxDD de 46.7% — trop risque\n",
     "- **Meilleur ratio rendement/risque** : TrailingStopAlgorithm (Sharpe 0.358, MaxDD 14.2%)\n",
     "- **Plus sur** : ComprehensiveRiskManagedStrategy (MaxDD 12.4%) — 5 couches de protection fonctionnent\n",
-    "- **Plus simple et efficace** : BuiltInRiskModelsAlgorithm (Sharpe 0.55, 1 ligne de risk management)\n",
+    "- **Plus simple et efficace** : BuiltInRiskModelsAlgorithm (Sharpe 0.55)\n",
     "- **Lecons** : Le position sizing seul ne créé pas d'edge (stratégies 1 et 2). Le choix du signal d'entree compte autant que le risk management"
    ]
   },

MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb

@@ -26,7 +26,7 @@
     "\n",
     "> *A\\* est optimal si l'heuristique n'est pas optimiste — i.e. elle ne surestime\n",
     "> jamais le coût restant. Cette « admissibilité » est la condition exacte que\n",
-    "> formalise `search_lean`, dont on visite ici les preuves (0 `sorry`).*\n",
+    "> formalise `search_lean`, dont on visite ici les preuves.*\n",
     "\n",
     "\n",
     "***\n",
@@ -56,14 +56,14 @@
     "chemin de coût minimal) repose sur une hypothèse précise : l'heuristique doit être\n",
     "**admissible** (`h ≤ h*`, le vrai coût optimal restant).\n",
     "\n",
-    "Le lake `search_lean` prouve **formellement** (0 `sorry`) le mécanisme exact de cette\n",
+    "Le lake `search_lean` prouve **formellement** le mécanisme exact de cette\n",
     "optimalité : la **borne en `f`** qui, sous heuristique admissible, garantit qu'A\\*\n",
     "ne dépasse jamais la frontière du coût optimal. Il établit aussi la chaîne\n",
     "**consistance ⟹ admissibilité** (par téléscopage) et la **connexion à Dijkstra**\n",
     "(heuristique nulle = recherche à coût uniforme).\n",
     "\n",
     "Cette visite exhibe les définitions et théorèmes clés du lake via leurs sources,\n",
-    "vérifie qu'ils sont bien à `0 sorry`, et les fait manipuler dans des exercices\n",
+    "vérifie qu'ils sont bien sans `sorry`, et les fait manipuler dans des exercices\n",
     "exécutés par le kernel Lean (via `lake env lean`).\n",
     "\n",
     "**Plan** : (1) Graphes pondérés et coût de chemin → (2) Admissibilité et\n",
@@ -712,7 +712,7 @@
    "source": [
     "### Lecture : pourquoi `h ≡ 0` est admissible (connexion à Dijkstra)\n",
     "\n",
-    "Les lemmas `zero_admissible` et `zero_consistent` (prouvés en une ligne chacun,\n",
+    "Les lemmas `zero_admissible` et `zero_consistent` (prouvés,\n",
     "`zero_le` en `ℝ≥0`) sont l'ancrage pédagogique : **Dijkstra est le cas particulier\n",
     "d'A\\* avec une heuristique nulle**. Toute la machinerie d'optimalité que l'on prouve\n",
     "pour A\\* admissible s'applique donc *a fortiori* à Dijkstra.\n",
@@ -1202,7 +1202,7 @@
     "   └─▶ Dijkstra (recherche à coût uniforme)\n",
     "```\n",
     "\n",
-    "Les bornes et la monotonie ci-dessus sont **formellement prouvées à 0 `sorry`**\n",
+    "Les bornes et la monotonie ci-dessus sont **formellement prouvées**\n",
     "dans `search_lean`. Seul le dernier saut — « donc A\\* renvoie un chemin optimal » —\n",
     "relèverait de modéliser l'algorithme lui-même (file de priorité), ce que le lake\n",
     "ne fait pas (cf #14824).\n",
@@ -1558,7 +1558,7 @@
    "source": [
     "## Conclusion\n",
     "\n",
-    "Ce notebook a visité le lake **`search_lean`** (0 `sorry`), qui prouve\n",
+    "Ce notebook a visité le lake **`search_lean`**, qui prouve\n",
     "**formellement** la borne en `f` — le cœur mathématique de l'optimalité de A\\*\n",
     "sous heuristique admissible.\n",
     "\n",

MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-Lean-Discrepancy-Komlos.ipynb

@@ -185,8 +185,8 @@
    },
    "source": [
     "L'import résout `Discrepancy.Komlos` — et par lui `Discrepancy.Basic`, puis `Mathlib`\n",
-    "tout entier : le chargement du noyau prend quelques minutes (des milliers de modules à\n",
-    "désérialiser), c'est le prix d'un socle formel complet. Une fois chargé, chaque définition du lake\n",
+    "tout entier : le chargement du noyau prend quelques minutes, c'est le prix d'un socle formel\n",
+    "complet. Une fois chargé, chaque définition du lake\n",
     "vit dans l'environnement sous son nom qualifié — `Discrepancy.` en préfixe de namespace."
    ]
   },
@@ -2455,7 +2455,7 @@
     "reste du lake.\n",
     "\n",
     "Avec ce module expose, le lake `discrepancy_lean` n'a **plus aucun module\n",
-    "noir** (0/8) : les deux jambees de la borne — Komlos deterministe, Erdos-Spencer\n",
+    "noir** : les deux jambees de la borne — Komlos deterministe, Erdos-Spencer\n",
     "probabiliste — sont desormais lisibles depuis ce compagnon."
    ]
   },