diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-16d-Echange-de-Reins-Lean-Python.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-16d-Echange-de-Reins-Lean-Python.ipynb index 6696586fcd..6390c25cb3 100644 --- a/MyIA.AI.Notebooks/GameTheory/GameTheory-16d-Echange-de-Reins-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/GameTheory-16d-Echange-de-Reins-Lean-Python.ipynb @@ -567,7 +567,7 @@ "\n", "**Cohabitation pattern Lean/Python** : le notebook Python peut **lire** les sources Lean (regex balanced, cf lecon c.437-L1) et **citer** les theoremes, sans executer `lake env lean`. Le kernel Python suffit pour cette verification structurelle. La verification formelle (lake build) releve du notebook Lean side track `GameTheory-15b-Lean-CooperativeGames-Lean.ipynb`.\n", "\n", - "C'est le pattern transversal documente dans `GameTheory-15d-Mobius-Coalitions-Lean-Python.ipynb` (c.438) — la localisation par ancetres et le `raise` si introuvable y sont deja en place — et `Lean-21c-Descente-Budget.ipynb` (c.437). JAMAIS de simulation jouet - ou bien le vrai outil est invoque, ou bien l'absence est documentee.\n" + "**Pattern transversal** : la localisation par remontee d'ancetres et le `raise` si introuvable sont la regle de portage pour tout carnet qui depend d'une arborescence externe. JAMAIS de simulation jouet — ou bien le vrai outil est invoque, ou bien l'absence est documentee.\n" ] }, { @@ -1344,4 +1344,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03b-PatternDatabases.ipynb b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03b-PatternDatabases.ipynb index e54aa2cd1a..457a54881a 100644 --- a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03b-PatternDatabases.ipynb +++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03b-PatternDatabases.ipynb @@ -976,7 +976,7 @@ "\n", "> **Quotienter / fibrer** — changer l'échelle de description en projetant l'état sur un quotient. **Loi** : la règle de chaîne $H(X) = H(\\pi(X)) + H(X \\mid \\pi(X))$. **Témoin** : $I(X_i ; X_j \\mid Q)$ sur un quotient commun $Q$. **Dette** : Ruzsa exige une structure de groupe — sans elle, ce serait « le nouveau mapping affine ».\n", "\n", - "**Position dans la table.** Première attestation : [Lean-21b](../../SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb) (PR [#12252](https://github.com/jsboige/CoursIA/pull/12252), primitives PFR). Candidate non-indépendante : Infer-20 (PR [#12277](https://github.com/jsboige/CoursIA/pull/12277), née du même batch — son témoin **négatif** mesuré, ratio $I(X_1;X_2|Q)/I(X_1;X_2) = 1{,}684$, borne la classe des quotients naïfs). Cette section est la **seconde attestation, sur un substrat indépendant** (Search/Python), avec le cas **positif** que la table attend : un quotient commun sous lequel l'interaction disparaît **exactement**.\n", + "**Position dans la table.** Première attestation : [Lean-21b](../../SymbolicAI/Lean/MIMO/MIMO-03-Converse-Native-Lean.ipynb) (PR [#12252](https://github.com/jsboige/CoursIA/pull/12252), primitives PFR). Candidate non-indépendante : Infer-20 (PR [#12277](https://github.com/jsboige/CoursIA/pull/12277), née du même batch — son témoin **négatif** mesuré, ratio $I(X_1;X_2|Q)/I(X_1;X_2) = 1{,}684$, borne la classe des quotients naïfs). Cette section est la **seconde attestation, sur un substrat indépendant** (Search/Python), avec le cas **positif** que la table attend : un quotient commun sous lequel l'interaction disparaît **exactement**.\n", "\n", "**Les trois personnages :**\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb index 82f4438ddf..1d68c3ee93 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb @@ -21,7 +21,7 @@ "\n", "| Notebook précédent | Notebook suivant |\n", "|---|---|\n", - "| [ANALYSE-04 - PFR Primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [Lean-21 - MIMO Detection Flips](../Lean-21-MIMO-Detection-Flips.ipynb) |\n", + "| [ANALYSE-04 - PFR Primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [Lean-21 - MIMO Detection Flips](../MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb) |\n", "\n", "***\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md index 80b851303c..6319917f74 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md @@ -20,6 +20,6 @@ La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier **Prérequis d'entrée** : le tutoriel de la série principale (numéros 1 à 6, tactiques et Mathlib). Le point d'entrée réel documenté du carnet 01 est [Search-03e-AStar-Optimality](../../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) (heuristique A*, companion `search_lean`) — voir sa cellule d'ouverture. -**Marches nommées, à écrire** (règle 5 de la gradation) : entropie de Shannon avant ANALYSE-03, inégalités de concentration avant le converse MIMO ([Lean-21b](../Lean-21b-MIMO-Converse-Native.ipynb)). Elles vivront dans ce dossier ou la série principale selon la décision de renumérotation. +**Marches nommées, à écrire** (règle 5 de la gradation) : entropie de Shannon avant ANALYSE-03, inégalités de concentration avant le converse MIMO ([MIMO-03](../MIMO/MIMO-03-Converse-Native-Lean.ipynb)). Elles vivront dans ce dossier ou la série principale selon la décision de renumérotation. **Marches franchissables** : depuis la série principale, le tutoriel (1-14) suffit pour ANALYSE-01. ANALYSE-02 suppose la lecture d'un lac externe ; ANALYSE-03/04 supposent l'entropie de Shannon (marche nommée ci-dessus) ; ANALYSE-05 ne suppose rien au-delà du tutoriel : son lac est local, posé à côté du carnet. diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb index c8fc105bdc..e42891724f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb @@ -22,7 +22,7 @@ "\n", "| Notebook précédent | Notebook suivant |\n", "|---|---|\n", - "| [Lean-17c - Knots Companion Formel](KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb) | [ANALYSE-01 - Sendov](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) pour entrer dans la sous-série, ou [Lean-21 - MIMO Detection Flips](Lean-21-MIMO-Detection-Flips.ipynb) pour poursuivre le parcours principal |\n", + "| [Lean-17c - Knots Companion Formel](KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb) | [ANALYSE-01 - Sendov](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb) pour entrer dans la sous-série, ou [MIMO-01 - Descente Budget](MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb) pour poursuivre le parcours principal |\n", "\n", "***\n", "\n", @@ -686,7 +686,7 @@ "3. **Une marche montée.** La règle de chaîne et la distance de Ruzsa, calculées sur F₂³, suffisent pour lire l'énoncé entropique de PFR : une distance nulle est une structure, et une petite distance est une structure approchée.\n", "4. **Une surface mesurée, avec ses défauts.** Les titres, les exercices d'ANALYSE-04 et le nom du dossier sont suivis dans [#18408](https://github.com/jsboige/CoursIA/issues/18408).\n", "\n", - "**Suite.** Entrer par [ANALYSE-01](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb), ou poursuivre le parcours principal avec [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb). Ce dernier reprend les deux registres de la sous-série : des illustrations numériques, puis des `#check` réels sur un lac compilé. Les primitives entropiques de PFR ont aussi vocation à être greffées dans la série ICT ([#18405](https://github.com/jsboige/CoursIA/issues/18405))." + "**Suite.** Entrer par [ANALYSE-01](ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb), ou poursuivre le parcours principal avec [MIMO-01](MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb). Ce dernier reprend les deux registres de la sous-série : des illustrations numériques, puis des `#check` réels sur un lac compilé. Les primitives entropiques de PFR ont aussi vocation à être greffées dans la série ICT ([#18405](https://github.com/jsboige/CoursIA/issues/18405))." ] } ], diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb index 272a69057f..8fdd4c49df 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb @@ -18,7 +18,7 @@ "\n", "**Série** : SymbolicAI / Lean — Théorie des groupes sporadiques et problème inverse de Galois\n", "\n", - "**Navigation** : [<< Lean-21 MIMO](Lean-21-MIMO-Detection-Flips.ipynb) | [Index](README.md)\n", + "**Navigation** : [<< MIMO-04 Capstone](MIMO/MIMO-04-Capstone-Digestion-Python.ipynb) | [Index](README.md)\n", "\n", "**Kernel** : Python 3 (vérifications exécutables sympy + extraction Steiner) + Lean 4 via WSL\n", "(`galois_lean`, source de vérité formelle — sections 3 et 4)\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb index 2f4ece896d..f9291cf19f 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb @@ -948,7 +948,7 @@ "- **Lake `erc20_lean`** (`MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean/`) — la version Lean 4 + Mathlib : `ERC20/State.lean` (modèle), `ERC20/Ops.lean` (transitions), `ERC20/Invariant.lean` (préservation).\n", "- **EPIC #4980** — convention i18n Lean (aggrégateur bilingue inline FR-EN dans `ERC20.lean`, sibling pair dans `ERC20_en.lean`).\n", "- **Rule C.6** (mandat user 2026-08-19) — préférence pour un compagnon kernel `lean4-wsl` à côté du notebook Python ; le pattern actuel (subprocess `lake env lean`) reste mergeable, le kernel Lean natif est une suite à explorer.\n", - "- Notebooks associés : `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](Lean-21-MIMO-Detection-Flips.ipynb)`, `[Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb)`." + "- Notebooks associés : `[Lean-22 (Galois)](Lean-22-Galois-Probleme-Inverse-M23.ipynb)`, `[Lean-21 (MIMO)](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb)`, `[Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`, `[Lean-13 (Kochen-Specker)](Lean-13-Kochen-Specker.ipynb)`, `[A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb)`." ] } ], diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-29-Hecke-Operators-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-29-Hecke-Operators-Native.ipynb index 826e8a66b4..bee39a3c3c 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-29-Hecke-Operators-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-29-Hecke-Operators-Native.ipynb @@ -28,7 +28,7 @@ "\n", "**L'enjeu de ce que le lake porte.** Les opérateurs de Hecke ne sont pas un objet d'exposition : ils sont la charnière par laquelle une forme modulaire devient une **suite de nombres comparable à autre chose**. Une forme propre normalisée — un vecteur propre commun de tous les $T_p$ — a ses coefficients de Fourier $a(p)$ égaux à ses valeurs propres, et c'est cette suite que le théorème de modularité apparie aux comptages de points $\\#E(\\mathbb{F}_p)$ d'une courbe elliptique sur $\\mathbb{Q}$. La chaîne courbe de Frey $\\rightarrow$ abaissement du niveau $\\rightarrow$ modularité, qui clôt le dernier théorème de Fermat, passe donc par la relation $a(np) + p^{k-1} a(n/p)$ — celle que `coeffHeckeT` porte ici, et que la section 5 fait calculer. Le dépôt amont dont ce lake est un port, `anthropics/fermats-last-theorem`, est un chantier de formalisation de cette chaîne. **Le lake en formalise les opérateurs, pas la preuve** : c'est un fragment de fondation, et la section 8 en prouve la dernière étape — $S_2(\\Gamma_0(2)) = 0$ — pendant que la section 9 mesure exactement ce que le lake démontre et ce qu'il suppose.\n", "\n", - "**Pourquoi ce module parmi environ 15 000 théorèmes du corpus FLT.** Son choix n'est pas justifié par le seul fait qu'un énoncé non trivial puisse être soumis au noyau Lean — cet argument vaudrait pour n'importe quel module du corpus. Hecke prolonge deux objets déjà enseignés dans CoursIA. D'abord, [Lean-12](Lean-12-Sensitivity-Theorem.ipynb) et son [compagnon Lean-12b](Lean-12b-Lean-Sensitivity-Theorem.ipynb) introduisent les fonctions sur l'hypercube et le lake [`sensitivity_lean`](sensitivity_lean/) ; son module [`Sensitivity/Fourier.lean`](sensitivity_lean/Sensitivity/Fourier.lean) représente une fonction par une famille de coefficients de Walsh, établit leur orthogonalité puis une reconstruction par somme finie. Ensuite, ce même lake formalise dans [`Sensitivity/Operator.lean`](sensitivity_lean/Sensitivity/Operator.lean) un opérateur linéaire $f_n$ et la relation $f_n^2=n\\,\\mathrm{Id}$, tandis que [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb), son [compagnon Lean-21b](Lean-21b-MIMO-Converse-Native.ipynb) et le lake [`mimo_lean`](mimo_lean/) manipulent matrices, applications linéaires, actions scalaires et sommes finies. Le passage pédagogique devient alors lisible : **fonction décrite par des coefficients** $\\rightarrow$ **opérateur additif et homogène agissant sur une fonction** $\\rightarrow$ **transformation arithmétique explicite de ses coefficients**. Hecke est le fragment du corpus FLT où ces deux fils déjà familiers se rencontrent dans un nouvel objet : les formes modulaires sur le demi-plan supérieur, leurs slash actions et la formule de `coeffHeckeT`.\n", + "**Pourquoi ce module parmi environ 15 000 théorèmes du corpus FLT.** Son choix n'est pas justifié par le seul fait qu'un énoncé non trivial puisse être soumis au noyau Lean — cet argument vaudrait pour n'importe quel module du corpus. Hecke prolonge deux objets déjà enseignés dans CoursIA. D'abord, [Lean-12](Lean-12-Sensitivity-Theorem.ipynb) et son [compagnon Lean-12b](Lean-12b-Lean-Sensitivity-Theorem.ipynb) introduisent les fonctions sur l'hypercube et le lake [`sensitivity_lean`](sensitivity_lean/) ; son module [`Sensitivity/Fourier.lean`](sensitivity_lean/Sensitivity/Fourier.lean) représente une fonction par une famille de coefficients de Walsh, établit leur orthogonalité puis une reconstruction par somme finie. Ensuite, ce même lake formalise dans [`Sensitivity/Operator.lean`](sensitivity_lean/Sensitivity/Operator.lean) un opérateur linéaire $f_n$ et la relation $f_n^2=n\\,\\mathrm{Id}$, tandis que [Lean-21](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb), son [compagnon Lean-21b](MIMO/MIMO-03-Converse-Native-Lean.ipynb) et le lake [`mimo_lean`](mimo_lean/) manipulent matrices, applications linéaires, actions scalaires et sommes finies. Le passage pédagogique devient alors lisible : **fonction décrite par des coefficients** $\\rightarrow$ **opérateur additif et homogène agissant sur une fonction** $\\rightarrow$ **transformation arithmétique explicite de ses coefficients**. Hecke est le fragment du corpus FLT où ces deux fils déjà familiers se rencontrent dans un nouvel objet : les formes modulaires sur le demi-plan supérieur, leurs slash actions et la formule de `coeffHeckeT`.\n", "\n", "**Raccord conceptuel, dépendance réelle.** Ce passage est une analogie structurante, pas une identification mathématique : les coefficients de Fourier booléens de `Sensitivity/Fourier.lean` décrivent une fonction sur un hypercube fini à l'aide des caractères de Walsh ; les coefficients $a(n)$ manipulés ici sont ceux d'une $q$-expansion de forme modulaire. De même, `sensitivity_lean` et `mimo_lean` préparent la lecture des matrices, sommes finies, actions scalaires, additivité et homogénéité, mais **ne sont pas des dépendances Lean** de ce notebook. La cellule d'import charge réellement `Hecke.HeckeOperator`, et ce module importe directement `Mathlib.NumberTheory.ModularForms.SlashActions`. Aucun lien historique ou formel particulier avec Galois, Belyi ou la théorie de l'information n'est revendiqué à partir de cette seule proximité de vocabulaire.\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb similarity index 99% rename from MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb rename to MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb index 86e7ed8551..dbbc41baf2 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb @@ -14,9 +14,9 @@ "tags": [] }, "source": [ - "# Lean-21c : Le budget de descente - quand la decroissance borne le nombre de flips\n", + "# MIMO-01 : Le budget de descente - quand la decroissance borne le nombre de flips\n", "\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", + "**Navigation** : [Index](README.md) | [<< Lean-20 (Capstone Tao)](../Lean-20-Capstone-Digestions-Tao-Python.ipynb) | [MIMO-02 (Detection Flips) >>](MIMO-02-Detection-Flips-Lean-Python.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", "\n", @@ -26,7 +26,7 @@ "|---|---|\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." + "Comme dans les notebooks Lean-20, MIMO-02 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." ] }, { @@ -2120,10 +2120,10 @@ "- **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'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)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb)`.\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)`, `[MIMO-02 (Detection Flips)](MIMO-02-Detection-Flips-Lean-Python.ipynb)`, `[Lean-20 (PFR)](../ANALYSE/ANALYSE-03-PFR-Lean.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", - "- **Regle C.7 (count_code_sorry)** - l'instrument canonique `scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), jamais `grep -c sorry`. Cf [anti-regression.md](../../../.claude/rules/anti-regression.md)." + "- **Regle C.7 (count_code_sorry)** - l'instrument canonique `scripts/lean/count_code_sorry.py --json` (champ `distinct_code_sorry`), jamais `grep -c sorry`. Cf [anti-regression.md](../../../../.claude/rules/anti-regression.md)." ] } ], @@ -2151,8 +2151,8 @@ "end_time": "2026-10-08T19:43:36.553099+00:00", "environment_variables": {}, "exception": null, - "input_path": "Lean-21c-Descente-Budget.ipynb", - "output_path": "Lean-21c-Descente-Budget.ipynb", + "input_path": "MIMO-01-Descente-Budget-Lean-Python.ipynb", + "output_path": "MIMO-01-Descente-Budget-Lean-Python.ipynb", "parameters": {}, "start_time": "2026-10-08T19:43:32.305668+00:00", "version": "2.7.0" @@ -2160,4 +2160,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb similarity index 99% rename from MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb rename to MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb index 19cc0533bb..10dbd66a94 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb @@ -14,9 +14,9 @@ "tags": [] }, "source": [ - "# Lean-21 : Detection MIMO par flips -- le seuil 2 log N sous preuve Lean\n", + "# MIMO-02 : Detection MIMO par flips -- le seuil 2 log N sous preuve Lean\n", "\n", - "**Navigation** : [Index](README.md) | [<< Lean-20 (Capstone Tao)](Lean-20-Capstone-Digestions-Tao-Python.ipynb) | [Lean-22 (Galois) >>](Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n", + "**Navigation** : [Index](README.md) | [<< MIMO-01 (Descente-Budget)](MIMO-01-Descente-Budget-Lean-Python.ipynb) | [MIMO-03 (Converse-Native) >>](MIMO-03-Converse-Native-Lean.ipynb)\n", "\n", "Ce notebook presente le lake **`mimo_lean`** de ce depot (issue #10984) : le port\n", "formel de l'algorithme de detection MIMO par flips de coordonnées de\n", @@ -39,7 +39,7 @@ "`M·ε·φ(2) ≥ 2·log N − log log N`, `P(erreur ML) ≥ 1 − exp(−(2·log N − log log N))`\n", "(issues #11673, #11709).\n", "\n", - "Comme dans [ANALYSE-03 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb), nous procedons en deux\n", + "Comme dans [ANALYSE-03 (PFR)](../ANALYSE/ANALYSE-03-PFR-Lean.ipynb), nous procedons en deux\n", "registres : des **illustrations numeriques** (Python) qui montrent les phenomenes,\n", "puis des **`#check` reels** executes par `lake env lean` sur le lac compile --\n", "les enonces affiches sont ceux que le compilateur Lean 4 a verifies, pas des\n", @@ -2001,9 +2001,9 @@ "- **YuanheZ/lean-stat-learning-theory** (ICML 2026, Apache 2.0) :\n", " Hanson-Wright, mesures gaussiennes -- dependance externe de la Phase 3b.\n", "- **Mathlib 4** : `MeasureTheory`, `ProbabilityTheory`, espaces de Hilbert.\n", - "- Notebooks associes : [Lean-20 (PFR)](ANALYSE/ANALYSE-03-PFR-Lean.ipynb),\n", - " [A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb),\n", - " [Lean-6 (Mathlib)](Lean-06-Mathlib-Essentials-Lean.ipynb)." + "- Notebooks associes : [Lean-20 (PFR)](../ANALYSE/ANALYSE-03-PFR-Lean.ipynb),\n", + " [A* Optimalite (Search-03e)](../../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb),\n", + " [Lean-6 (Mathlib)](../Lean-06-Mathlib-Essentials-Lean.ipynb)." ] } ], @@ -2031,8 +2031,8 @@ "end_time": "2026-09-13T07:48:47.914424+00:00", "environment_variables": {}, "exception": null, - "input_path": "Lean-21-MIMO-Detection-Flips.ipynb", - "output_path": "Lean-21-MIMO-Detection-Flips.ipynb", + "input_path": "MIMO-02-Detection-Flips-Lean-Python.ipynb", + "output_path": "MIMO-02-Detection-Flips-Lean-Python.ipynb", "parameters": {}, "start_time": "2026-09-13T07:45:59.398354+00:00", "version": "2.6.0" @@ -2040,4 +2040,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-03-Converse-Native-Lean.ipynb similarity index 99% rename from MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb rename to MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-03-Converse-Native-Lean.ipynb index f8fc6b4206..23b9d197cb 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-03-Converse-Native-Lean.ipynb @@ -14,9 +14,11 @@ "tags": [] }, "source": [ - "# Lean-21b : le lake `mimo_lean` par ses énoncés — compagnon formel natif\n", + "# MIMO-03 : le lake `mimo_lean` par ses énoncés — compagnon formel natif\n", "\n", - "Compagnon **natif** du notebook Python [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb) : ici, plus de simulation — le lake `mimo_lean` est **importé et exécuté** dans un kernel Lean 4 réel, et chaque théorème est interrogé par `#check` / `#print axioms` avec sa signature rendue par le compilateur.\n", + "**Navigation** : [Index](README.md) | [<< MIMO-02 (Detection-Flips)](MIMO-02-Detection-Flips-Lean-Python.ipynb) | [MIMO-04 (Capstone) >>](MIMO-04-Capstone-Digestion-Python.ipynb)\n", + "\n", + "Compagnon **natif** du notebook Python [Lean-21](MIMO-02-Detection-Flips-Lean-Python.ipynb) : ici, plus de simulation — le lake `mimo_lean` est **importé et exécuté** dans un kernel Lean 4 réel, et chaque théorème est interrogé par `#check` / `#print axioms` avec sa signature rendue par le compilateur.\n", "\n", "Ce compagnon comble le point noir mesuré par l'instrument de visibilité de l'EPIC [#11703](https://github.com/jsboige/CoursIA/issues/11703) : le module **`NormTails.lean` n'était cité nulle part** — le seul module du lake entièrement invisible, alors qu'il porte la **Phase 3b**, la concentration gaussienne du bruit, c'est-à-dire le travail de preuve le plus exigeant du lake (cf [#11766](https://github.com/jsboige/CoursIA/issues/11766)).\n", "\n", @@ -541,7 +543,7 @@ "\n", "**Pourquoi `NormTails` etait invisible** : l'instrument de visibilite de l'EPIC #11703 a comptabilise aucune citation de `NormTails` dans le corpus Python/Lean, alors que `Descent`, `Objective`, `Lmmse` etaient cites plusieurs fois chacun. La raison est que `NormTails` est apparu tard dans le developpement du lake (Phase 3b), apres que la majorite du corpus Python ait ete ecrite. Ce compagnon comble ce trou documentaire : les declarations de `NormTails` sont maintenant interrogees par `#check` et leur role est explicite.\n", "\n", - "**Difference avec le notebook Python** : le notebook [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb) simule Monte-Carlo la queue de `‖w‖` et la compare a la borne. Ce compagnon-ci montre la borne elle-meme, signee par le compilateur Lean, sans simulation numerique. Les deux lectures sont complementaires : l'une pedagogique (intuition), l'autre formelle (certificat).\n", + "**Difference avec le notebook Python** : le notebook [Lean-21](MIMO-02-Detection-Flips-Lean-Python.ipynb) simule Monte-Carlo la queue de `‖w‖` et la compare a la borne. Ce compagnon-ci montre la borne elle-meme, signee par le compilateur Lean, sans simulation numerique. Les deux lectures sont complementaires : l'une pedagogique (intuition), l'autre formelle (certificat).\n", "\n", "**Trois ajouts spécifiques au lac** :\n", "\n", @@ -1077,7 +1079,7 @@ "source": [ "### 2.1 La borne en chiffres\n", "\n", - "La queue `2·exp(−t²/2)` décroît très vite. La cellule suivante l'évalue sur les premiers écarts-types, par quatre `#eval` consécutifs sur `t = 1, 2, 3, 4` (la vérification Monte-Carlo empirique — la queue simulée sous la courbe — vit dans le notebook Python [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb)).\n", + "La queue `2·exp(−t²/2)` décroît très vite. La cellule suivante l'évalue sur les premiers écarts-types, par quatre `#eval` consécutifs sur `t = 1, 2, 3, 4` (la vérification Monte-Carlo empirique — la queue simulée sous la courbe — vit dans le notebook Python [Lean-21](MIMO-02-Detection-Flips-Lean-Python.ipynb)).\n", "\n", "**Les quatre ordres de grandeur a attendre** — la lecture verbatim de la sortie est faite plus bas, une fois la cellule executee :\n", "\n", @@ -1088,7 +1090,7 @@ "| 3 | ≈ 0,022 | sous 2,5 % |\n", "| 4 | ≈ 0,00067 | sous 0,1 % |\n", "\n", - "**Implication pour le decodeur ML** : si le decodeur est cense tolerer un bruit `‖w‖` qui s'ecarte de sa moyenne de `t` ecarts-types avec probabilite au plus `p`, alors la borne de concentration donne directement cette probabilite. Le notebook Python [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb) superpose la queue empirique a la borne theorique pour un `n = M = 64` typique (64 antennes MIMO).\n", + "**Implication pour le decodeur ML** : si le decodeur est cense tolerer un bruit `‖w‖` qui s'ecarte de sa moyenne de `t` ecarts-types avec probabilite au plus `p`, alors la borne de concentration donne directement cette probabilite. Le notebook Python [Lean-21](MIMO-02-Detection-Flips-Lean-Python.ipynb) superpose la queue empirique a la borne theorique pour un `n = M = 64` typique (64 antennes MIMO).\n", "\n", "**Pourquoi `Float` plutot que `Real`** : `#eval` a besoin d'un type **computable**, et `Float` (IEEE 754 double precision) rend directement la valeur. L'affichage donne six decimales, ce qui laisse encore trois chiffres significatifs sur la plus petite des quatre valeurs (`0.000671`). Pour des evaluations plus precises, le lake utilise `Real.exp` (non affiche dans ce compagnon).\n", "\n", @@ -3264,7 +3266,7 @@ "1. **la frontière SLT** — le lake compose avec une bibliothèque externe vérifiée ; la concentration de Lipschitz et Hanson–Wright sont empruntées, tout le reste (l'instanciation MIMO, le converse chi-carré, le pont ML) est prouvé ici ;\n", "2. **deux routes pour une même queue** — la route légère (Lipschitz, `NormTails`) borne la norme, la route lourde (Hanson–Wright, `Converse`) borne la forme quadratique ; le pont `Bridge` convertit ces queues en borne sur l'erreur du décodeur ML.\n", "\n", - "La contrepartie expérimentale — Monte-Carlo de la queue de `‖w‖` superposée à la borne prouvée — vit dans le notebook Python [Lean-21](Lean-21-MIMO-Detection-Flips.ipynb). Les modules `Descent`, `Objective` et `Lmmse` (Phases 1–3a) y sont également visités par leurs énoncés.\n", + "La contrepartie expérimentale — Monte-Carlo de la queue de `‖w‖` superposée à la borne prouvée — vit dans le notebook Python [Lean-21](MIMO-02-Detection-Flips-Lean-Python.ipynb). Les modules `Descent`, `Objective` et `Lmmse` (Phases 1–3a) y sont également visités par leurs énoncés.\n", "\n", "Le lac `mimo_lean` est un exemple de **stratification propre** : Mathlib (base\n", "arithmétique) → SLT (concentration statistique) → `mimo_lean/NormTails`\n", @@ -3292,10 +3294,13 @@ " de Lean (`propext`, `Classical.choice`, `Quot.sound`). Aucun `sorry`, aucun\n", " axiome exotique. C'est la *garantie de correction*.\n", "\n", - "**Vers la suite** : le notebook Python `Lean-21` (déjà publié) montre la\n", - "*vérification empirique* des bornes de `NormTails` via simulation Monte-Carlo.\n", - "Les bornes théoriques y sont comparées aux fréquences empiriques — un bon\n", - "test de cohérence entre théorie et simulation.\n", + "**Pour la vérification empirique** : le notebook Python `MIMO-02`\n", + "(étape précédente de la sous-série) confronte les bornes de `NormTails` à\n", + "une simulation Monte-Carlo — les bornes théoriques y sont comparées aux\n", + "fréquences empiriques, un bon test de cohérence entre théorie et simulation.\n", + "**Vers la suite** : le notebook `MIMO-04` (Capstone) digère les trois\n", + "marches de la sous-série et met les énoncés à l'épreuve sur des instances\n", + "calculées.\n", "\n", "**Coût global du notebook** : ~10 secondes (lecture du lakefile +\n", "`#check` + `#print axioms` + `#eval Float`)." @@ -3320,8 +3325,8 @@ "end_time": "2026-09-28T15:22:13.582122+00:00", "environment_variables": {}, "exception": null, - "input_path": "Lean-21b-MIMO-Converse-Native.ipynb", - "output_path": "Lean-21b-MIMO-Converse-Native.ipynb", + "input_path": "MIMO-03-Converse-Native-Lean.ipynb", + "output_path": "MIMO-03-Converse-Native-Lean.ipynb", "parameters": {}, "start_time": "2026-09-28T15:21:59.101528+00:00", "version": "2.7.0" @@ -3329,4 +3334,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-04-Capstone-Digestion-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-04-Capstone-Digestion-Python.ipynb new file mode 100644 index 0000000000..a1c0f23b4c --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-04-Capstone-Digestion-Python.ipynb @@ -0,0 +1,1212 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "1b83a2b6", + "metadata": { + "papermill": { + "duration": 0.004844, + "end_time": "2026-10-11T12:50:13.453538+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.448694+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# MIMO-04 : Capstone — digérer la détection MIMO par flips\n", + "\n", + "**Navigation** : [Index](README.md) | [<< MIMO-03 (Converse-Native)](MIMO-03-Converse-Native-Lean.ipynb) | [Lean-22 (Galois) >>](../Lean-22-Galois-Probleme-Inverse-M23.ipynb)\n", + "\n", + "Ce carnet **digère** la sous-série MIMO plutôt que d'en ajouter une marche : il\n", + "reprend le théorème de tête, la borne de queue de norme et le seuil `2·log N`\n", + "que les trois carnets prouvent séparément, et il les met **à l'épreuve sur des\n", + "instances calculées**. C'est le pendant, pour MIMO, du capstone\n", + "[Lean-20](../Lean-20-Capstone-Digestions-Tao-Python.ipynb) de la série\n", + "principale : le même geste de digestion, un autre objet.\n", + "\n", + "Il est **exécutable seul** : noyau Python, aucune dépendance au lake, aucune\n", + "commande Lean.\n" + ] + }, + { + "cell_type": "markdown", + "id": "fd396938", + "metadata": { + "papermill": { + "duration": 0.004449, + "end_time": "2026-10-11T12:50:13.463403+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.458954+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. Le geste : digérer, pas seulement vérifier\n", + "\n", + "Les trois marches de la sous-série remplissent trois fonctions distinctes :\n", + "**lire** un théorème et ses hypothèses (MIMO-01), **simuler** le détecteur réel\n", + "et sa borne (MIMO-02), **exécuter** le lake dans un noyau Lean (MIMO-03). Aucune\n", + "ne fait le geste de synthèse : prendre un énoncé formel, en instancier les\n", + "hypothèses sur un objet calculable, et **constater** si la conclusion tient.\n", + "\n", + "C'est ce que ce carnet fait, sur deux énoncés qui portent tout le résultat :\n", + "\n", + "| Énoncé formel | Où il vit | Ce qu'on en fait ici |\n", + "|---|---|---|\n", + "| `descent_target_before_ceiling` | `Descent.lean` (Prop. 9.1) | on instancie la descente à flips sur une instance MIMO et on **mesure** les quatre faits de sa preuve |\n", + "| `norm_concentration` / `column_norm_tail` | `NormTails.lean` | on **confronte** la queue `2·exp(−t²/2)` à un tirage Monte-Carlo, puis on en dérive le seuil `2·log N` par union bound |\n", + "\n", + "Le carnet ne redémontre rien : il **relie** un énoncé à un nombre. Là où\n", + "l'expérience ne peut pas décider, il le dit.\n" + ] + }, + { + "cell_type": "markdown", + "id": "396e80cf", + "metadata": { + "papermill": { + "duration": 0.004995, + "end_time": "2026-10-11T12:50:13.472560+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.467565+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. Où entrer : les trois marches\n", + "\n", + "| Marche | Carnet | Geste | Prérequis |\n", + "|---|---|---|---|\n", + "| base | [MIMO-01 — Descente-Budget](MIMO-01-Descente-Budget-Lean-Python.ipynb) | lire le squelette combinatoire (`Descent.lean`, **sans Mathlib**) | aucun Lean — le carnet s'ouvre sur du texte |\n", + "| milieu | [MIMO-02 — Detection-Flips](MIMO-02-Detection-Flips-Lean-Python.ipynb) | simuler le détecteur, confronter la borne `NormTails` | noyau Python, disposition à lire un énoncé |\n", + "| sommet | [MIMO-03 — Converse-Native](MIMO-03-Converse-Native-Lean.ipynb) | exécuter le lake entier, énoncé par énoncé | WSL + Lean 4 + le lake |\n", + "\n", + "La progression est **monotone en prérequis** : c'est le contrat d'un escalier.\n", + "Ce carnet se place **après** les trois, et n'exige que le noyau Python.\n" + ] + }, + { + "cell_type": "markdown", + "id": "08dd1cbf", + "metadata": { + "papermill": { + "duration": 0.005383, + "end_time": "2026-10-11T12:50:13.483007+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.477624+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. La marche faite à la main : la descente à flips\n", + "\n", + "`Descent.lean` prouve la Proposition 9.1 sur un espace d'états **abstrait** :\n", + "`accept : σ → σ → Prop`, `cost : σ → ℕ`, et quatre faits enchaînés —\n", + "la décroissance se propage à toute la queue du run, un run ne se répète jamais,\n", + "le nombre de flips est majoré par le coût de départ, et sous une barrière `B` il\n", + "est majoré par `B`.\n", + "\n", + "On instancie `σ` par les `2^N` vecteurs de signes d'un petit canal MIMO et\n", + "`cost` par le **rang** de l'objectif `‖y − Hx‖²`. Le rang est un entier : la\n", + "décroissance stricte de l'objectif devient une décroissance stricte d'au moins\n", + "une unité, ce qui est **exactement** l'hypothèse `cost : σ → ℕ` du module. Un\n", + "coût réel ne la fournirait pas — on y revient en section 4.\n", + "\n", + "Le flip `x_i → −x_i` a pour variation de coût `4·x_i·(rᵀh_i) + 4·‖h_i‖²` avec\n", + "`r = y − Hx` : le flip est accepté si cette quantité est **strictement**\n", + "négative.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "a11ca8e1", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:13.494315Z", + "iopub.status.busy": "2026-10-11T12:50:13.493799Z", + "iopub.status.idle": "2026-10-11T12:50:13.882237Z", + "shell.execute_reply": "2026-10-11T12:50:13.880604Z" + }, + "papermill": { + "duration": 0.395801, + "end_time": "2026-10-11T12:50:13.883652+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.487851+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "canal 14x10, bruit sigma = 0.60, signal emis recupere : True\n", + "\n", + "pas | cout reel | cout entier\n", + " 0 | 308.745023 | 721\n", + " 1 | 145.193729 | 127\n", + " 2 | 74.455617 | 16\n", + " 3 | 45.950429 | 4\n", + " 4 | 2.667405 | 0\n", + "\n", + "flips acceptes : 4\n", + "aucun flip n'ameliore l'etat final : True\n" + ] + } + ], + "source": [ + "# La descente a flips, telle que `Descent.lean` la formalise : on ne suppose\n", + "# rien, on mesure. Instance MIMO jouet, entierement deterministe (graine fixe).\n", + "import numpy as np\n", + "from itertools import product\n", + "\n", + "rng = np.random.default_rng(20261011)\n", + "N, M, SIGMA = 10, 14, 0.6\n", + "\n", + "H = rng.normal(size=(M, N)) # canal, entrees i.i.d. N(0,1)\n", + "x_vrai = rng.choice(np.array([-1.0, 1.0]), size=N) # signal emis (BPSK)\n", + "bruit = SIGMA * rng.normal(size=M)\n", + "y = H @ x_vrai + bruit\n", + "\n", + "\n", + "def cout(x):\n", + " \"\"\"Objectif du detecteur : ||y - Hx||^2.\"\"\"\n", + " r = y - H @ x\n", + " return float(r @ r)\n", + "\n", + "\n", + "def gains_de_flip(x):\n", + " \"\"\"Variation de cout de chaque flip x_i -> -x_i.\n", + "\n", + " r' = r + 2*x_i*h_i, d'ou cout(x^i) - cout(x) = 4*x_i*(r . h_i) + 4*||h_i||^2.\n", + " \"\"\"\n", + " r = y - H @ x\n", + " return 4.0 * (x * (H.T @ r) + np.sum(H * H, axis=0))\n", + "\n", + "\n", + "# Le rang de l'objectif : un cout ENTIER, strictement monotone en l'objectif.\n", + "etats = np.array(list(product([-1.0, 1.0], repeat=N))) # les 2^N etats\n", + "objectifs = np.array([cout(x) for x in etats])\n", + "ordre = np.argsort(objectifs, kind=\"stable\")\n", + "rang = np.empty(len(etats), dtype=int)\n", + "rang[ordre] = np.arange(len(etats))\n", + "index = {tuple(s): k for k, s in enumerate(etats)}\n", + "\n", + "\n", + "def cout_entier(x):\n", + " \"\"\"cost : sigma -> N, au sens de `Descent.lean`.\"\"\"\n", + " return int(rang[index[tuple(x)]])\n", + "\n", + "\n", + "# La descente : a chaque pas, le meilleur flip s'il DECROIT strictement.\n", + "x0 = np.ones(N) # aucun signe exploite au depart\n", + "run = [x0.copy()]\n", + "while True:\n", + " delta = gains_de_flip(run[-1])\n", + " i = int(np.argmin(delta))\n", + " if delta[i] >= 0.0:\n", + " break # etat terminal : hterm\n", + " suivant = run[-1].copy()\n", + " suivant[i] = -suivant[i]\n", + " run.append(suivant)\n", + "\n", + "cout_reel = [cout(x) for x in run]\n", + "cout_nat = [cout_entier(x) for x in run]\n", + "\n", + "print(\"canal %dx%d, bruit sigma = %.2f, signal emis recupere : %s\"\n", + " % (M, N, SIGMA, np.array_equal(run[-1], x_vrai)))\n", + "print()\n", + "print(\"pas | cout reel | cout entier\")\n", + "for k, (cr, cn) in enumerate(zip(cout_reel, cout_nat)):\n", + " print(\"%3d | %11.6f | %5d\" % (k, cr, cn))\n", + "print()\n", + "print(\"flips acceptes : %d\" % (len(run) - 1))\n", + "print(\"aucun flip n'ameliore l'etat final : %s\"\n", + " % bool(np.all(gains_de_flip(run[-1]) >= 0.0)))" + ] + }, + { + "cell_type": "markdown", + "id": "decb7a6d", + "metadata": { + "papermill": { + "duration": 0.00504, + "end_time": "2026-10-11T12:50:13.894202+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.889162+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "La trajectoire descend de `cost = 721` à `cost = 0` en **4 flips acceptés**. Le\n", + "coût entier décroît strictement à chaque pas, ce qui est le contenu de\n", + "`run_tail_cost_lt` : le coût de tout état visité après le départ est strictement\n", + "inférieur à celui du départ.\n", + "\n", + "L'état terminal n'offre plus aucun flip améliorant — c'est l'hypothèse `hterm`\n", + "du théorème. Le théorème ne dit **pas** qu'un tel état est l'optimum global : il\n", + "dit que le run y arrive en moins de `M_N` flips. Ici il se trouve que le rang\n", + "final vaut `0`, donc que la descente a atteint l'optimum global — c'est une\n", + "observation sur cette instance, pas une conséquence de la Proposition 9.1.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "527c6bb2", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:13.907338Z", + "iopub.status.busy": "2026-10-11T12:50:13.906704Z", + "iopub.status.idle": "2026-10-11T12:50:13.916758Z", + "shell.execute_reply": "2026-10-11T12:50:13.915248Z" + }, + "papermill": { + "duration": 0.01853, + "end_time": "2026-10-11T12:50:13.918043+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.899513+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "run_tail_cost_lt (decroissance stricte) OK\n", + "run_nodup (aucune repetition) OK\n", + "run_length_le_cost (flips <= cout de depart) OK\n", + "descent_flips_le_barrier (flips <= B) OK\n", + "descent_target_before_ceiling (cible atteinte, flips < M_N) OK\n", + "\n", + "B = 721, M_N = 722, flips = 4, etats distincts = 5 sur 5 pas\n" + ] + } + ], + "source": [ + "# Les quatre faits de `Descent.lean`, verifies sur le run qui vient d'etre\n", + "# calcule. Chacun est un theoreme du module ; on les confronte un par un.\n", + "distincts = len(set(index[tuple(x)] for x in run))\n", + "B = cout_nat[0] # barriere de confinement : le cout ne remonte jamais\n", + "M_N = B + 1 # plafond de flips, strictement au-dessus de la barriere\n", + "n_flips = len(run) - 1\n", + "\n", + "faits = [\n", + " (\"run_tail_cost_lt (decroissance stricte)\",\n", + " all(b < a for a, b in zip(cout_nat, cout_nat[1:]))),\n", + " (\"run_nodup (aucune repetition)\",\n", + " distincts == len(run)),\n", + " (\"run_length_le_cost (flips <= cout de depart)\",\n", + " n_flips <= B),\n", + " (\"descent_flips_le_barrier (flips <= B)\",\n", + " n_flips <= B),\n", + " (\"descent_target_before_ceiling (cible atteinte, flips < M_N)\",\n", + " bool(np.all(gains_de_flip(run[-1]) >= 0.0)) and n_flips < M_N),\n", + "]\n", + "\n", + "for libelle, verdict in faits:\n", + " print(\"%-52s %s\" % (libelle, \"OK\" if verdict else \"ECHEC\"))\n", + "print()\n", + "print(\"B = %d, M_N = %d, flips = %d, etats distincts = %d sur %d pas\"\n", + " % (B, M_N, n_flips, distincts, len(run)))" + ] + }, + { + "cell_type": "markdown", + "id": "2a1a564d", + "metadata": { + "papermill": { + "duration": 0.005346, + "end_time": "2026-10-11T12:50:13.929154+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.923808+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "Les cinq lignes sont les cinq énoncés du module, sans exception. Le fait le plus\n", + "intéressant est `run_length_le_cost` : **`4 ≤ 721`**, une borne vraie mais\n", + "grossière. Elle est grossière *par construction* — la preuve n'utilise que le\n", + "fait que le coût est un entier qui décroît d'au moins `1` à chaque flip, jamais\n", + "la géométrie du problème. C'est la barrière `B` de la Phase 2 (`Objective.lean`)\n", + "qui resserre la borne ; ici on a pris `B = cost(s₀)`, le cas dégénéré où la\n", + "barrière ne contraint rien.\n" + ] + }, + { + "cell_type": "markdown", + "id": "39707a96", + "metadata": { + "papermill": { + "duration": 0.005251, + "end_time": "2026-10-11T12:50:13.939897+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.934646+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. Le défaut comme dissociation : le témoin d'échec\n", + "\n", + "La suite du module ne fait pas que prouver : elle **donne un nom au défaut**.\n", + "`DescentFailure` est un témoin — une paire d'états consécutifs dont le flip est\n", + "accepté sans que le coût décroisse strictement — et\n", + "`failure_witness_denies_global_strict` dit que ce témoin **réfute** l'hypothèse\n", + "globale. Le commentaire du module est explicite : un échec de décroissance n'est\n", + "pas un résidu numérique à écarter, c'est une dissociation à enregistrer.\n", + "\n", + "On construit ici le témoin **exactement**, sans flottement : un canal identité\n", + "sans bruit rend l'objectif `‖y − Hx‖² = ‖x‖² = M` **constant**. Tous les gains\n", + "de flip valent alors `0` — l'égalité, pas l'approximation.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "10f0b44b", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:13.953060Z", + "iopub.status.busy": "2026-10-11T12:50:13.952372Z", + "iopub.status.idle": "2026-10-11T12:50:13.979787Z", + "shell.execute_reply": "2026-10-11T12:50:13.978456Z" + }, + "papermill": { + "duration": 0.035396, + "end_time": "2026-10-11T12:50:13.980946+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.945550+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "objectif de tout etat : 14.0 (constant)\n", + "gains de flip possibles : [0.]\n", + "regle STRICTE (accepte si gain < 0) : 0 flip accepte\n", + "regle RELACHEE (accepte si gain <= 0) : 14 flips acceptes\n", + "\n", + "run relache : 6 pas, 2 etats distincts, 4 repetitions\n", + "cycle de periode 2 : l'etat de depart est retrouve au 2e pas : True\n", + "\n", + "temoin : accept(s, u) = True et cost(u) < cost(s) = False -> DescentFailure.here\n", + "donc 'pour tout flip accepte, le cout decroit strictement' est FAUX : True\n" + ] + } + ], + "source": [ + "# Temoin exact : objectif constant, donc variation de flip nulle partout.\n", + "H_sym = np.eye(M)\n", + "y_sym = np.zeros(M)\n", + "\n", + "\n", + "def gains_sym(x):\n", + " r = y_sym - H_sym @ x\n", + " return 4.0 * (x * (H_sym.T @ r) + np.sum(H_sym * H_sym, axis=0))\n", + "\n", + "\n", + "x_sym = np.ones(M)\n", + "cout_const = float((y_sym - H_sym @ x_sym) @ (y_sym - H_sym @ x_sym))\n", + "print(\"objectif de tout etat : %.1f (constant)\" % cout_const)\n", + "print(\"gains de flip possibles :\", np.unique(gains_sym(x_sym)))\n", + "print(\"regle STRICTE (accepte si gain < 0) : %d flip accepte\"\n", + " % int(np.sum(gains_sym(x_sym) < 0.0)))\n", + "print(\"regle RELACHEE (accepte si gain <= 0) : %d flips acceptes\"\n", + " % int(np.sum(gains_sym(x_sym) <= 0.0)))\n", + "\n", + "# Run sous la regle relachee : on accepte le premier flip non strict.\n", + "x_rel = x_sym.copy()\n", + "visites = []\n", + "for _ in range(6):\n", + " visites.append(tuple(x_rel))\n", + " delta = gains_sym(x_rel)\n", + " i = int(np.argmin(delta))\n", + " x_rel[i] = -x_rel[i]\n", + "print()\n", + "print(\"run relache : %d pas, %d etats distincts, %d repetitions\"\n", + " % (len(visites), len(set(visites)), len(visites) - len(set(visites))))\n", + "print(\"cycle de periode 2 : l'etat de depart est retrouve au 2e pas : %s\"\n", + " % (visites[0] == visites[2]))\n", + "\n", + "# Le temoin lui-meme : la paire (s, u) du constructeur `DescentFailure.here`.\n", + "s, u = np.ones(M), np.ones(M)\n", + "u[0] = -1.0\n", + "accepte = bool(np.all(gains_sym(s) <= 0.0))\n", + "decroit = bool(float((y_sym - H_sym @ u) @ (y_sym - H_sym @ u))\n", + " < float((y_sym - H_sym @ s) @ (y_sym - H_sym @ s)))\n", + "print()\n", + "print(\"temoin : accept(s, u) = %s et cost(u) < cost(s) = %s -> DescentFailure.here\"\n", + " % (accepte, decroit))\n", + "print(\"donc 'pour tout flip accepte, le cout decroit strictement' est FAUX : %s\"\n", + " % (accepte and not decroit))" + ] + }, + { + "cell_type": "markdown", + "id": "037e2e1d", + "metadata": { + "papermill": { + "duration": 0.005927, + "end_time": "2026-10-11T12:50:13.991817+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.985890+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "Le témoin est exhibé, et il fait exactement ce que le module annonce : il\n", + "**paie** l'hypothèse de stricte décroissance. Sous la règle relâchée, le run\n", + "revient sur son état de départ en deux pas — `run_nodup` tombe, et avec lui\n", + "`run_length_le_cost` : sans décroissance stricte, plus rien ne borne le nombre\n", + "de flips, et l'algorithme peut boucler indéfiniment.\n", + "\n", + "C'est la valeur pédagogique du témoin : au lieu de dire « l'hypothèse est\n", + "nécessaire », on **produit l'objet** qui la rend nécessaire. Le fichier ne\n", + "prouve pas seulement `descent_target_before_ceiling` sous `hstrict`, il montre\n", + "ce qui arrive quand `hstrict` tombe.\n" + ] + }, + { + "cell_type": "markdown", + "id": "adc97922", + "metadata": { + "papermill": { + "duration": 0.004851, + "end_time": "2026-10-11T12:50:14.001832+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:13.996981+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. La borne de queue et le seuil `2·log N`\n", + "\n", + "`NormTails.lean` ne prouve pas directement le seuil : il prouve une **queue de\n", + "norme**. Le bruit `w` et chaque colonne `hᵢ` du canal sont des vecteurs\n", + "gaussiens standards de dimension `M`, la norme euclidienne est `1`-Lipschitz, et\n", + "le théorème de concentration du lake externe SLT donne\n", + "\n", + " P(|‖X‖ − E‖X‖| ≥ t) ≤ 2·exp(−t²/2).\n", + "\n", + "Le seuil `2·log N` vient **après**, d'un union bound sur les `N` colonnes : la\n", + "probabilité qu'*une* colonne sorte de l'intervalle est majorée par\n", + "`N·2·exp(−t²/2)`, et demander que ce majorant passe sous `ε` donne\n", + "\n", + " t ≥ √(2·log(2N/ε)).\n", + "\n", + "On vérifie la borne d'abord, on en dérive le seuil ensuite.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "e6735307", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:14.014426Z", + "iopub.status.busy": "2026-10-11T12:50:14.013727Z", + "iopub.status.idle": "2026-10-11T12:50:14.199173Z", + "shell.execute_reply": "2026-10-11T12:50:14.197853Z" + }, + "papermill": { + "duration": 0.193024, + "end_time": "2026-10-11T12:50:14.200481+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.007457+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "M | E||X|| sqrt(M) | t | mesure | borne 2exp(-t2/2) | verdict\n", + "--------------------------------------------------------------------------\n", + " 4 | 1.879 2.000 | 1.0 | 0.14295 | 1.21306 | OK\n", + " 4 | 1.879 2.000 | 2.0 | 0.00360 | 0.27067 | OK\n", + " 4 | 1.879 2.000 | 3.0 | 0.00005 | 0.02222 | OK\n", + " 16 | 3.931 4.000 | 1.0 | 0.15480 | 1.21306 | OK\n", + " 16 | 3.931 4.000 | 2.0 | 0.00450 | 0.27067 | OK\n", + " 16 | 3.931 4.000 | 3.0 | 0.00005 | 0.02222 | OK\n", + " 64 | 7.967 8.000 | 1.0 | 0.15715 | 1.21306 | OK\n", + " 64 | 7.967 8.000 | 2.0 | 0.00490 | 0.27067 | OK\n", + " 64 | 7.967 8.000 | 3.0 | 0.00005 | 0.02222 | OK\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "256 | 15.991 16.000 | 1.0 | 0.15350 | 1.21306 | OK\n", + "256 | 15.991 16.000 | 2.0 | 0.00445 | 0.27067 | OK\n", + "256 | 15.991 16.000 | 3.0 | 0.00005 | 0.02222 | OK\n", + "\n", + "violations de norm_concentration / noise_norm_tail / column_norm_tail : 0\n" + ] + } + ], + "source": [ + "# La queue de norme, confrontee a l'experience. K tirages par dimension,\n", + "# plusieurs seuils t, et la borne `2*exp(-t^2/2)` du module.\n", + "K = 20000\n", + "gen = np.random.default_rng(7)\n", + "print(\"M | E||X|| sqrt(M) | t | mesure | borne 2exp(-t2/2) | verdict\")\n", + "print(\"-\" * 74)\n", + "violations = 0\n", + "for m in (4, 16, 64, 256):\n", + " X = gen.normal(size=(K, m))\n", + " norme = np.linalg.norm(X, axis=1)\n", + " moyenne = norme.mean()\n", + " for t in (1.0, 2.0, 3.0):\n", + " mesure = float(np.mean(np.abs(norme - moyenne) >= t))\n", + " borne = 2.0 * np.exp(-t * t / 2.0)\n", + " ok = mesure <= borne\n", + " violations += 0 if ok else 1\n", + " print(\"%3d | %7.3f %7.3f | %4.1f | %8.5f | %17.5f | %s\"\n", + " % (m, moyenne, np.sqrt(m), t, mesure, borne, \"OK\" if ok else \"VIOLATION\"))\n", + "print()\n", + "print(\"violations de norm_concentration / noise_norm_tail / column_norm_tail : %d\"\n", + " % violations)" + ] + }, + { + "cell_type": "markdown", + "id": "8b6bcbeb", + "metadata": { + "papermill": { + "duration": 0.004946, + "end_time": "2026-10-11T12:50:14.211035+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.206089+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Du union bound au seuil\n", + "\n", + "Une colonne qui sort de l'intervalle ne suffit pas à faire échouer le détecteur :\n", + "il faut qu'**aucune** des `N` colonnes n'en sorte. Le passage de « une » à\n", + "« toutes » est un union bound, et la colle qui le referme est\n", + "`one_sub_pow_le_exp_mul` — le module prouve `(1−p)^n ≤ exp(−n·p)`, ce qui\n", + "remplace un produit de `N` termes par une exponentielle. On vérifie les deux\n", + "ensemble.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "6df875c9", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:14.222804Z", + "iopub.status.busy": "2026-10-11T12:50:14.222354Z", + "iopub.status.idle": "2026-10-11T12:50:14.231555Z", + "shell.execute_reply": "2026-10-11T12:50:14.230460Z" + }, + "papermill": { + "duration": 0.016769, + "end_time": "2026-10-11T12:50:14.232472+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.215703+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "N | t requis (union bound) | sqrt(2 log N) | N*2exp(-t2/2)\n", + "------------------------------------------------------------------\n", + " 10 | 3.462 | 2.146 | 0.05000\n", + " 100 | 4.073 | 3.035 | 0.05000\n", + " 1000 | 4.604 | 3.717 | 0.05000\n", + "\n", + "(1-p)^n <= exp(-n p) sur une grille de p et n :\n", + " verifiee partout\n", + "\n", + "lecture : t croit comme sqrt(2 log N), donc LENTEMENT en N ;\n", + "a N=1000 le seuil vaut 4.60 contre 3.46 a N=10 (x1.3 pour x100 de colonnes).\n" + ] + } + ], + "source": [ + "# Du union bound sur les N colonnes au seuil `2 log N`, puis verification\n", + "# de la colle du module : `one_sub_pow_le_exp_mul`, (1-p)^n <= exp(-n p).\n", + "epsilon = 0.05\n", + "print(\"N | t requis (union bound) | sqrt(2 log N) | N*2exp(-t2/2)\")\n", + "print(\"-\" * 66)\n", + "for n_col in (10, 100, 1000):\n", + " t_req = np.sqrt(2.0 * np.log(2.0 * n_col / epsilon))\n", + " print(\"%5d | %22.3f | %13.3f | %.5f\"\n", + " % (n_col, t_req, np.sqrt(2 * np.log(n_col)), n_col * 2 * np.exp(-t_req ** 2 / 2)))\n", + "\n", + "print()\n", + "print(\"(1-p)^n <= exp(-n p) sur une grille de p et n :\")\n", + "colle_ok = True\n", + "for p in (0.01, 0.1, 0.3, 0.5):\n", + " for n_puis in (1, 5, 20, 100):\n", + " if not (1 - p) ** n_puis <= np.exp(-n_puis * p) + 1e-15:\n", + " colle_ok = False\n", + "print(\" %s\" % (\"verifiee partout\" if colle_ok else \"CONTREDITE\"))\n", + "\n", + "print()\n", + "print(\"lecture : t croit comme sqrt(2 log N), donc LENTEMENT en N ;\")\n", + "print(\"a N=1000 le seuil vaut %.2f contre %.2f a N=10 (x%.1f pour x%d de colonnes).\"\n", + " % (np.sqrt(2 * np.log(2 * 1000 / epsilon)),\n", + " np.sqrt(2 * np.log(2 * 10 / epsilon)),\n", + " np.sqrt(2 * np.log(2 * 1000 / epsilon)) / np.sqrt(2 * np.log(2 * 10 / epsilon)),\n", + " 100))" + ] + }, + { + "cell_type": "markdown", + "id": "9ccd82ae", + "metadata": { + "papermill": { + "duration": 0.004454, + "end_time": "2026-10-11T12:50:14.241999+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.237545+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "La borne tient sur les douze couples `(M, t)` testés : la queue de norme du\n", + "module est **vérifiée numériquement**, pas seulement énoncée. On lit aussi que\n", + "`E‖X‖ ≈ √M` (1.879 pour 2.000, 15.991 pour 16.000) — la constante que\n", + "`NormTails` laisse implicite dans `E‖X‖` et qui rend la borne exploitable : sans\n", + "elle, la queue porterait sur une quantité inconnue.\n", + "\n", + "Le seuil croit comme `√(2·log N)`, donc **très lentement** : multiplier le nombre\n", + "de colonnes par 100 (de 10 à 1000) ne fait passer le seuil que de 3.46 à 4.60.\n", + "C'est ce qui rend le détecteur utilisable à grande dimension, et c'est le\n", + "`2·log N` du titre de la sous-série.\n", + "\n", + "La colle `one_sub_pow_le_exp_mul` est vérifiée à part : c'est elle qui fait\n", + "passer du produit des `N` événements indépendants à l'exponentielle, sans quoi\n", + "le union bound ne se refermerait pas.\n" + ] + }, + { + "cell_type": "markdown", + "id": "f16b41ad", + "metadata": { + "papermill": { + "duration": 0.005318, + "end_time": "2026-10-11T12:50:14.252894+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.247576+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 6. Mesurer la surface du lake — et relire l'instrument\n", + "\n", + "Un théorème n'existe, pour un lecteur, que si un carnet le montre. La mesure de\n", + "cette exposition se fait d'ordinaire avec l'organe canonique\n", + "`scripts/lean/scan_lake_notebook_visibility.py --lake mimo_lean`. On le refait\n", + "ici **depuis les sources**, en regardant au passage ce que l'organe lui-même\n", + "compte.\n", + "\n", + "Deux chiffres vont apparaître, et l'écart entre les deux est le vrai résultat de\n", + "cette section.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "8635385e", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:14.266452Z", + "iopub.status.busy": "2026-10-11T12:50:14.265951Z", + "iopub.status.idle": "2026-10-11T12:50:14.308191Z", + "shell.execute_reply": "2026-10-11T12:50:14.306851Z" + }, + "papermill": { + "duration": 0.0512, + "end_time": "2026-10-11T12:50:14.309430+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.258230+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "module | organe | large\n", + "--------------------------------------\n", + "Bridge.lean | 15 | 15\n", + "Converse.lean | 16 | 16\n", + "Descent.lean | 10 | 10\n", + "lakefile.lean | 0 | 0\n", + "Lmmse.lean | 3 | 4 <<< ECART\n", + "NormTails.lean | 6 | 6\n", + "Objective.lean | 6 | 6\n", + "--------------------------------------\n", + "TOTAL | 56 | 57\n", + "\n", + "declarations invisibles au motif de l'organe (Lmmse.lean) : ['B_ρ', 'B_ρ_posSemidef']\n", + " l'organe les replie sur : ['B_']\n", + "\n", + "exposition des 10 declarations de Descent.lean dans la sous-serie :\n", + "carnets balayes : 01, 02, 03\n", + "(le capstone s'exclut de son propre balayage : il nomme ce qu'il mesure)\n", + "\n", + "declaration | source | sortie\n", + "------------------------------------------------------------------\n", + "DescentFailure | non | oui\n", + "Run | oui | oui\n", + "descent_flips_le_barrier | oui | oui\n", + "descent_target_before_ceiling | oui | oui\n", + "failure_witness_denies_global_strict | non | oui\n", + "lastState | oui | oui\n", + "run_length_le_cost | oui | oui\n", + "run_nodup | oui | oui\n", + "run_strictdescent_excludes_failure | non | oui\n", + "run_tail_cost_lt | oui | oui\n", + "\n", + "visibles seulement en sortie : ['DescentFailure', 'failure_witness_denies_global_strict', 'run_strictdescent_excludes_failure']\n" + ] + } + ], + "source": [ + "# La surface de `mimo_lean`, comptee depuis les sources, en francais\n", + "# (les jumeaux `_en.lean` portent la meme substance : convention i18n #4980).\n", + "import json\n", + "import pathlib\n", + "import re\n", + "\n", + "MODIF = r\"(?:private|protected|noncomputable|partial|unsafe|scoped|local)\"\n", + "# Le motif de l'organe canonique : pseudo-lettre ASCII pour le nom declare.\n", + "MOTIF_ORGANE = re.compile(\n", + " r\"^\\s*(?:@\\[[^\\]]*\\]\\s*)?(?:\" + MODIF + r\"\\s+)*\"\n", + " r\"(theorem|lemma|def|abbrev|instance|structure|inductive|class|opaque)\\s+\"\n", + " r\"([A-Za-z_][A-Za-z0-9_']*)\"\n", + ")\n", + "# Meme motif, mais nom lu jusqu'au premier delimiteur (accepte les grecques).\n", + "MOTIF_LARGE = re.compile(\n", + " r\"^\\s*(?:@\\[[^\\]]*\\]\\s*)?(?:\" + MODIF + r\"\\s+)*\"\n", + " r\"(theorem|lemma|def|abbrev|instance|structure|inductive|class|opaque)\\s+\"\n", + " r\"([^\\s({\\[:]+)\"\n", + ")\n", + "\n", + "\n", + "def racine_lake():\n", + " \"\"\"Le dossier qui contient `mimo_lean`, par remontee d'ancetres.\"\"\"\n", + " d = pathlib.Path.cwd()\n", + " for cand in [d, *d.parents]:\n", + " if (cand / \"mimo_lean\").is_dir():\n", + " return cand / \"mimo_lean\"\n", + " raise FileNotFoundError(\"mimo_lean introuvable depuis %s\" % d)\n", + "\n", + "\n", + "lake = racine_lake()\n", + "noms = {}\n", + "lignes_organe = 0\n", + "print(\"%-16s | %8s | %8s\" % (\"module\", \"organe\", \"large\"))\n", + "print(\"-\" * 38)\n", + "for f in sorted(lake.glob(\"*.lean\")):\n", + " if f.name.endswith(\"_en.lean\"):\n", + " continue\n", + " texte = f.read_text(encoding=\"utf-8\").splitlines()\n", + " s_organe = {m.group(2) for m in (MOTIF_ORGANE.match(l) for l in texte) if m}\n", + " s_large = {m.group(2) for m in (MOTIF_LARGE.match(l) for l in texte) if m}\n", + " noms[f.name] = s_large\n", + " lignes_organe += len(s_organe)\n", + " ecart = \" <<< ECART\" if len(s_organe) != len(s_large) else \"\"\n", + " print(\"%-16s | %8d | %8d%s\" % (f.name, len(s_organe), len(s_large), ecart))\n", + "total_large = sum(len(v) for v in noms.values())\n", + "print(\"-\" * 38)\n", + "print(\"%-16s | %8d | %8d\" % (\"TOTAL\", lignes_organe, total_large))\n", + "\n", + "# Qui l'organe perd-il, exactement ?\n", + "for f, s in noms.items():\n", + " perdues = {n for n in s if not re.fullmatch(r\"[A-Za-z_][A-Za-z0-9_']*\", n)}\n", + " if perdues:\n", + " print()\n", + " print(\"declarations invisibles au motif de l'organe (%s) : %s\"\n", + " % (f, sorted(perdues)))\n", + " autres = {m.group(2) for m in (MOTIF_ORGANE.match(l)\n", + " for l in lake.joinpath(f).read_text(encoding=\"utf-8\").splitlines()) if m}\n", + " print(\" l'organe les replie sur : %s\"\n", + " % sorted(n for n in autres if n.endswith(\"_\")))\n", + "\n", + "# Exposition des declarations de `Descent.lean` dans la sous-serie : citee dans\n", + "# la SOURCE d'une cellule, ou seulement lisible dans la SORTIE d'une autre ?\n", + "# Le capstone s'exclut de son propre balayage : il nomme les declarations qu'il\n", + "# mesure, donc s'il se comptait la mesure serait vraie par construction.\n", + "mimo_dir = lake.parent / \"MIMO\"\n", + "descent = noms[\"Descent.lean\"]\n", + "carnets = [q for q in sorted(mimo_dir.glob(\"MIMO-0*.ipynb\"))\n", + " if not q.name.startswith(\"MIMO-04\")]\n", + "\n", + "src_vu, out_vu = set(), set()\n", + "for nb_path in carnets:\n", + " don = json.loads(nb_path.read_text(encoding=\"utf-8\"))\n", + " for c in don[\"cells\"]:\n", + " src_txt = \"\".join(c[\"source\"])\n", + " for nom in descent:\n", + " if nom in src_txt:\n", + " src_vu.add(nom)\n", + " for o in c.get(\"outputs\", []):\n", + " blocs = o.get(\"text\", [])\n", + " if isinstance(blocs, str):\n", + " blocs = [blocs]\n", + " blocs = list(blocs) + list(o.get(\"data\", {}).get(\"text/plain\", []))\n", + " for bloc in blocs:\n", + " for nom in descent:\n", + " if nom in bloc:\n", + " out_vu.add(nom)\n", + "\n", + "print()\n", + "print(\"exposition des %d declarations de Descent.lean dans la sous-serie :\"\n", + " % len(descent))\n", + "print(\"carnets balayes : %s\" % \", \".join(q.name.split(\"-\")[1] for q in carnets))\n", + "print(\"(le capstone s'exclut de son propre balayage : il nomme ce qu'il mesure)\")\n", + "print()\n", + "print(\"%-38s | %-6s | %s\" % (\"declaration\", \"source\", \"sortie\"))\n", + "print(\"-\" * 66)\n", + "muettes = []\n", + "for nom in sorted(descent):\n", + " src = \"oui\" if nom in src_vu else \"non\"\n", + " out = \"oui\" if nom in out_vu else \"non\"\n", + " if src == \"non\" and out == \"oui\":\n", + " muettes.append(nom)\n", + " print(\"%-38s | %-6s | %s\" % (nom, src, out))\n", + "print()\n", + "print(\"visibles seulement en sortie : %s\" % (muettes or \"aucune\"))" + ] + }, + { + "cell_type": "markdown", + "id": "174be6de", + "metadata": { + "papermill": { + "duration": 0.004986, + "end_time": "2026-10-11T12:50:14.319953+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.314967+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture du résultat\n", + "\n", + "L'écart est net et il est **localisé** : l'organe rend `56` là où les sources en\n", + "portent `57`. La déclaration qu'il perd est nommée — `B_ρ`, dans `Lmmse.lean` —\n", + "et la raison est dans son motif : `[A-Za-z0-9_']*` s'arrête au premier caractère\n", + "non ASCII, donc `B_ρ` se lit `B_`, exactement comme `B_ρ_posSemidef`. Les deux\n", + "se replient sur le même nom et le compte en perd un.\n", + "\n", + "Rien dans le lake n'est faux : c'est **l'instrument** qui l'est, d'une seule\n", + "unité, sur les seuls noms qui portent une lettre grecque. Le chiffre `56`\n", + "recopié d'un rapport à l'autre hérite silencieusement de ce repli.\n", + "\n", + "Le tableau d'exposition sépare ensuite deux choses que le comptage confond : une\n", + "déclaration peut être **citée** dans le texte d'une sortie sans jamais être\n", + "**montrée** dans une cellule source. Trois des dix déclarations de `Descent.lean`\n", + "sont dans ce cas, et ce ne sont pas trois quelconques :\n", + "\n", + "- `DescentFailure`, le type du témoin d'échec ;\n", + "- `failure_witness_denies_global_strict`, qui l'exploite ;\n", + "- `run_strictdescent_excludes_failure`, le verrou que la sous-série raconte.\n", + "\n", + "Autrement dit, **le versant « échec » du chapitre n'est lisible dans aucune\n", + "cellule source** : il n'apparaît qu'en bloc, noyé dans le vidage de\n", + "`Descent.lean` qu'un carnet imprime. C'est exactement la famille que la section 4\n", + "exhibe à la main — et c'est donc ce carnet-ci qui la nomme pour la première fois\n", + "dans une cellule source.\n", + "\n", + "Une précaution compte ici autant que le chiffre : **le carnet s'exclut de son\n", + "propre balayage**. Il nomme les déclarations qu'il mesure ; s'il se comptait, la\n", + "mesure serait vraie par construction et ne dirait rien.\n" + ] + }, + { + "cell_type": "markdown", + "id": "faab2884", + "metadata": { + "papermill": { + "duration": 0.005395, + "end_time": "2026-10-11T12:50:14.330833+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.325438+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 7. Exercices\n", + "\n", + "### Exercice 1 — resserrer la barrière `B`\n", + "\n", + "La borne `4 ≤ 721` de la section 3 vient de `B = cost(s₀)`, la barrière la plus\n", + "lâche possible. Prenez `B` = le coût du **meilleur** état de l'instance, et\n", + "vérifiez que `descent_flips_le_barrier` tient toujours — puis expliquez pourquoi\n", + "`run_length_le_cost` ne peut pas, elle, se resserrer sans changer d'hypothèse.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "62d01e68", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:14.344620Z", + "iopub.status.busy": "2026-10-11T12:50:14.344116Z", + "iopub.status.idle": "2026-10-11T12:50:14.350269Z", + "shell.execute_reply": "2026-10-11T12:50:14.348919Z" + }, + "papermill": { + "duration": 0.015127, + "end_time": "2026-10-11T12:50:14.351723+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.336596+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer : resserrer la barriere B et reverifier le fait.\n" + ] + } + ], + "source": [ + "# Exercice 1 : reprendre la barriere de la section 3.\n", + "# Indice : `hbarrier` exige que le cout de TOUT etat du run reste sous B.\n", + "B_resserre = None # TODO etudiant : le cout du meilleur etat de l'instance\n", + "print(\"Exercice a completer : resserrer la barriere B et reverifier le fait.\")" + ] + }, + { + "cell_type": "markdown", + "id": "422d6701", + "metadata": { + "papermill": { + "duration": 0.005939, + "end_time": "2026-10-11T12:50:14.362517+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.356578+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 2 — rendre le plafond `M_N` serré\n", + "\n", + "`descent_target_before_ceiling` conclut `rest.length < M_N` dès que `B < M_N`.\n", + "Sur l'instance de la section 3 le run ne fait que 4 flips, très loin de la\n", + "borne. Construisez un état de départ dont le run consomme **exactement** `B`\n", + "flips — ou montrez que sur cette instance un tel départ n'existe pas.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "eaacc30e", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:14.376831Z", + "iopub.status.busy": "2026-10-11T12:50:14.376429Z", + "iopub.status.idle": "2026-10-11T12:50:14.382227Z", + "shell.execute_reply": "2026-10-11T12:50:14.380877Z" + }, + "papermill": { + "duration": 0.014422, + "end_time": "2026-10-11T12:50:14.383294+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.368872+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer : chercher un depart dont le run atteint B flips.\n" + ] + } + ], + "source": [ + "# Exercice 2 : chercher un depart dont le run epuise la barriere.\n", + "# Indice : parcourir les 2^N etats et garder celui dont le run est le plus long.\n", + "plus_long = None # TODO etudiant : (etat de depart, nombre de flips)\n", + "print(\"Exercice a completer : chercher un depart dont le run atteint B flips.\")" + ] + }, + { + "cell_type": "markdown", + "id": "a3b5e273", + "metadata": { + "papermill": { + "duration": 0.005866, + "end_time": "2026-10-11T12:50:14.395696+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.389830+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Exercice 3 — mesurer le seuil au lieu de le dériver\n", + "\n", + "La section 5 **dérive** `t ≥ √(2·log(2N/ε))` du union bound. Mesurez-le : pour\n", + "`N` colonnes simulées, estimez par Monte-Carlo la plus petite valeur de `t` telle\n", + "que la probabilité qu'**une** colonne sorte de l'intervalle passe sous `ε`, et\n", + "comparez au seuil dérivé. L'écart attendu est-il un défaut de la borne, ou son\n", + "caractère majorant ?\n" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "2f8b85f5", + "metadata": { + "execution": { + "iopub.execute_input": "2026-10-11T12:50:14.409360Z", + "iopub.status.busy": "2026-10-11T12:50:14.408971Z", + "iopub.status.idle": "2026-10-11T12:50:14.414484Z", + "shell.execute_reply": "2026-10-11T12:50:14.413082Z" + }, + "papermill": { + "duration": 0.01413, + "end_time": "2026-10-11T12:50:14.415611+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.401481+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer : mesurer le seuil par Monte-Carlo et le comparer.\n" + ] + } + ], + "source": [ + "# Exercice 3 : confronter le seuil derive a un seuil mesure.\n", + "# Indice : N colonnes = N vecteurs gaussiens de dimension M, un par experience.\n", + "seuil_mesure = None # TODO etudiant : plus petit t tel que P(une colonne sorte) < eps\n", + "print(\"Exercice a completer : mesurer le seuil par Monte-Carlo et le comparer.\")" + ] + }, + { + "cell_type": "markdown", + "id": "31489a75", + "metadata": { + "papermill": { + "duration": 0.006081, + "end_time": "2026-10-11T12:50:14.427947+00:00", + "exception": false, + "start_time": "2026-10-11T12:50:14.421866+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 8. Conclusion — ce que ce capstone laisse au lecteur\n", + "\n", + "Trois choses, dans l'ordre où elles se sont présentées :\n", + "\n", + "1. **La Proposition 9.1 est vraie et elle est grossière.** Les cinq énoncés de\n", + " `Descent.lean` se vérifient sur une instance réelle, et le plus utile est le\n", + " plus faible : `run_length_le_cost` ne borne les flips que par le coût de\n", + " départ, parce que sa preuve n'utilise que l'intégralité du coût. Resserrer\n", + " demande la géométrie de `Objective.lean`.\n", + "2. **Le défaut a un nom, et on peut le produire.** `DescentFailure` n'est pas une\n", + " clause de style : sur un canal identité sans bruit, le témoin s'exhibe à la\n", + " main, et le run revient sur son départ. La stricte décroissance n'est pas une\n", + " commodité de preuve, c'est ce qui borne l'algorithme.\n", + "3. **Les instruments aussi se relisent.** Le lake porte `57` déclarations ;\n", + " l'organe canonique en compte `56`, parce que son motif de nom s'arrête au\n", + " premier caractère grec. Le chiffre qui circule dans les rapports est faux\n", + " d'une unité, et il l'est resté parce que personne ne l'avait recompté depuis\n", + " les sources.\n", + "\n", + "Ce que ce carnet **ne fait pas** : il n'exécute pas Lean. Les énoncés formels\n", + "sont lus dans les sources, leur vérification native est le travail de\n", + "[MIMO-03](MIMO-03-Converse-Native-Lean.ipynb) ; ici, c'est l'**expérience** qui\n", + "répond, et la frontière entre les deux est marquée à chaque section.\n" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.13.7" + }, + "papermill": { + "default_parameters": {}, + "duration": 3.959211, + "end_time": "2026-10-11T12:50:14.778986+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "D:\\Dev\\CoursIA-2411-mimo\\MyIA.AI.Notebooks\\SymbolicAI\\Lean\\MIMO\\MIMO-04-Capstone-Digestion-Python.ipynb", + "output_path": "D:\\Dev\\CoursIA-2411-mimo\\MyIA.AI.Notebooks\\SymbolicAI\\Lean\\MIMO\\MIMO-04-Capstone-Digestion-Python.ipynb", + "parameters": {}, + "start_time": "2026-10-11T12:50:10.819775+00:00", + "version": "2.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} \ No newline at end of file diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/README.md new file mode 100644 index 0000000000..da1837160d --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/README.md @@ -0,0 +1,18 @@ +# MIMO — détection MIMO par flips, du budget de descente au converse + +Sous-série de la série [Lean](../README.md) (décision de gradation #17545, 24/09) : la détection MIMO par flips de coordonnées (Papailiopoulos 2026) descend ici avec son lac [`mimo_lean`](../mimo_lean/README.md). L'arc interne va du geste algorithmique nu — la descente et son budget — vers le problème réel et son seuil `2·log N`, puis vers le compagnon formel qui interroge le lac énoncé par énoncé, et se referme sur la digestion : ce que les énoncés valent une fois exécutés à la main. + +Les numéros de la table ci-dessous renvoient à l'ancien identifiant de série (`Lean-21c` → `MIMO-01`, `Lean-21` → `MIMO-02`, `Lean-21b` → `MIMO-03` — table de correspondance dans `docs/reference/rename-ledger.tsv`). + +**Escalier depuis la série principale** : le carnet d'entrée est [Lean-20 — Capstone](../Lean-20-Capstone-Digestions-Tao-Python.ipynb) ; la sous-série se referme sur MIMO-04, puis le parcours principal reprend à [Lean-22 — Galois](../Lean-22-Galois-Probleme-Inverse-M23.ipynb). + +| Carnet | Contenu | Durée | +|---|---|---| +| [MIMO-01-Descente-Budget-Lean-Python](MIMO-01-Descente-Budget-Lean-Python.ipynb) | Le budget de descente : quand la décroissance du coût borne le nombre de flips — l'analyse qui fonde le seuil `2·log N`. Le théorème `descent_target_before_ceiling` de `Descent.lean`, la case « décroissance réfutée » (trois variantes qui violent `hstrict`, avec leurs symptômes mesurés), la lecture des sources du lac et la propagation du substrat. Expose `Descent` seul. | 35 min | +| [MIMO-02-Detection-Flips-Lean-Python](MIMO-02-Detection-Flips-Lean-Python.ipynb) | Le problème réel et son seuil : détection MIMO par flips de coordonnées, descente simulée et comptage de flips, probabilité d'échappement du bruit (Monte-Carlo confronté à `e^{−np}`), puis `#check` réels des quatre phases du lac et du converse complet `ml_error_prob_ge_threshold`. Expose `Objective`, `Lmmse`, la glue `Converse`, `Bridge` (partiel) et `NormTails`. | 45 min | +| [MIMO-03-Converse-Native-Lean](MIMO-03-Converse-Native-Lean.ipynb) | Compagnon **natif** (kernel `lean4-wsl`) : le lac **importé et exécuté** dans un kernel Lean 4 réel. La frontière SLT est exhibée par `#check` (ce qui est prouvé ici vs emprunté à `YuanheZ/lean-stat-learning-theory`), puis chaque module est visité énoncé par énoncé et sondé par `#print axioms`. C'est le seul carnet qui montre le lake en entier. | 40 min | +| [MIMO-04-Capstone-Digestion-Python](MIMO-04-Capstone-Digestion-Python.ipynb) | **Capstone** : les énoncés du lac exécutés à la main sur une instance réelle, en Python. Les cinq faits de `Descent.lean` vérifiés un par un (le coût **entier** est ce qui rend `run_length_le_cost` vraie), le témoin d'échec `DescentFailure` exhibé sur un canal identité sans bruit (la règle stricte n'accepte aucun flip, la règle relâchée cycle de période 2), la borne de queue de `NormTails` vérifiée par Monte-Carlo, le seuil `√(2·log(2N/ε))` dérivé du union bound, et la **surface du lac recomptée depuis les sources** — où l'organe canonique rend `56` pour `57` déclarations, son motif de nom s'arrêtant au premier caractère grec. | 35 min | + +**Prérequis d'entrée** : MIMO-01 est autonome — `Descent.lean` n'a aucune dépendance Mathlib, le build est court, et la descente s'y lit sans prérequis formel. MIMO-02 et MIMO-03 supposent les tactiques et Mathlib du tutoriel de la série principale (numéros 1 à 6) et une disposition à lire des énoncés Lean. MIMO-04 ne demande que Python et NumPy : c'est le carnet de sortie, lisible après n'importe lequel des trois. + +**Statut du lac** : `mimo_lean` est **sorry-free** (baseline 0), sûr par les deux gates CI — build et intégrité de preuve (`lean-mimo.yml`, cibles dérivées au runtime, siblings i18n inclus). Il compose avec un lake externe vérifié (`YuanheZ/lean-stat-learning-theory`, épinglé via le fork `jsboige/lean-stat-learning-theory`) : la concentration de Lipschitz et Hanson–Wright sont empruntées, tout le reste — l'instanciation MIMO, le converse chi-carré, le pont vers l'erreur ML — est prouvé ici. Détail des phases et des énoncés : [`mimo_lean/README.md`](../mimo_lean/README.md). diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md index 51f402704a..054f81d2cf 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md @@ -154,9 +154,10 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet | ANALYSE-04 | [ANALYSE-04-PFR-Primitives-Python](ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb) | Trois primitives de PFR, et l'endroit exact où elles cessent de valoir — companion de digestion de ANALYSE-03 : ce qui se transporte hors du cadre d'origine (#12214) | 30 min | | ANALYSE-05 | [ANALYSE-05-KLS-Lean-Python](ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb) | La conjecture KLS démontrée (Bizeul–Klartag–Lehec 2026) : énoncé, chaîne de la preuve en cinq maillons, lac local `kls_lean` (six définitions, deux théorèmes prouvés, 0 sorry, axiomes vérifiés), thin-shell en Monte-Carlo avec saturation exacte à 8n par l'exponentielle produit, banc 1-lipschitzien minorant `poincareConstant` (#19729) | 45 min | | ANALYSE-09 | [ANALYSE-09-Tuilage-Aperiodique](ANALYSE/ANALYSE-09-Tuilage-Aperiodique.ipynb) (+ [jumeau _en](ANALYSE/ANALYSE-09-Tuilage-Aperiodique_en.ipynb)) | Contre-exemple au pavage périodique en dimension 3 (famille 155 du corpus openai/math) : un carreau fini de ℤ³ qui pave par translations sans **aucun** pavage totalement périodique — définitions (tuile, couverture exacte, rang du groupe de périodes), moteur borné exact-cover ancré sur la sémantique de `sudoku_lean`, quatre expériences mesurées dont deux pièges de fenêtre (rang mesuré 0 ou 2 pour des tuiles prouvées périodiques) et un théorème de non-pavage (prisme en L) | 30 min | -| 21 | [Lean-21-MIMO-Detection-Flips](Lean-21-MIMO-Detection-Flips.ipynb) | Détection MIMO par flips de coordonnées (Papailiopoulos 2026) : le seuil 2·log N — descente simulée et comptage de flips, probabilité d'échappement du bruit (Monte-Carlo vs `e^{−np}`), `#check` réels des quatre phases et du converse complet `ml_error_prob_ge_threshold` (P(erreur ML) ≥ 1 − e^{−(2·log N − log log N)}) du companion `mimo_lean` (sorry-free, lake externe SLT pour Hanson–Wright) | 45 min | -| 21b | [Lean-21b-MIMO-Converse-Native](Lean-21b-MIMO-Converse-Native.ipynb) | Compagnon **natif** (kernel `lean4-wsl`) du lac `mimo_lean` : le lac importé et exécuté dans un kernel Lean 4 réel — la frontière SLT exhibée par `#check` (ce qui est prouvé vs emprunté à `YuanheZ/lean-stat-learning-theory`), les six déclarations de `NormTails` (concentration de Lipschitz gaussienne), les seize briques du converse Hanson–Wright (dont `hanson_wright_noise` et la queue chi-carré `chisq_norm_concentration`), les treize du pont ML (`Bridge`), `#print axioms` sur les théorèmes clés — uniquement les axiomes standards, zéro `sorry` | 40 min | -| 21c | [Lean-21c-Descente-Budget](Lean-21c-Descente-Budget.ipynb) | Le budget de descente : quand la décroissance borne le nombre de flips — l'analyse qui fonde le seuil 2·log N de la détection MIMO (#12219) | 35 min | +| MIMO-01 | [MIMO-01-Descente-Budget-Lean-Python](MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb) | Le budget de descente : quand la décroissance borne le nombre de flips — l'analyse qui fonde le seuil 2·log N de la détection MIMO (#12219) | 35 min | +| MIMO-02 | [MIMO-02-Detection-Flips-Lean-Python](MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb) | Détection MIMO par flips de coordonnées (Papailiopoulos 2026) : le seuil 2·log N — descente simulée et comptage de flips, probabilité d'échappement du bruit (Monte-Carlo vs `e^{−np}`), `#check` réels des quatre phases et du converse complet `ml_error_prob_ge_threshold` (P(erreur ML) ≥ 1 − e^{−(2·log N − log log N)}) du companion `mimo_lean` (sorry-free, lake externe SLT pour Hanson–Wright) | 45 min | +| MIMO-03 | [MIMO-03-Converse-Native-Lean](MIMO/MIMO-03-Converse-Native-Lean.ipynb) | Compagnon **natif** (kernel `lean4-wsl`) du lac `mimo_lean` : le lac importé et exécuté dans un kernel Lean 4 réel — la frontière SLT exhibée par `#check` (ce qui est prouvé vs emprunté à `YuanheZ/lean-stat-learning-theory`), les six déclarations de `NormTails` (concentration de Lipschitz gaussienne), les seize briques du converse Hanson–Wright (dont `hanson_wright_noise` et la queue chi-carré `chisq_norm_concentration`), les treize du pont ML (`Bridge`), `#print axioms` sur les théorèmes clés — uniquement les axiomes standards, zéro `sorry` | 40 min | +| MIMO-04 | [MIMO-04-Capstone-Digestion-Python](MIMO/MIMO-04-Capstone-Digestion-Python.ipynb) | **Capstone** de la sous-série [MIMO](MIMO/README.md), et sa sortie : les énoncés du lac exécutés à la main sur une instance réelle — les cinq faits de `Descent.lean` vérifiés un par un (le coût **entier** est ce qui rend `run_length_le_cost` vraie), le témoin d'échec `DescentFailure` exhibé sur un canal identité sans bruit (la règle stricte n'accepte aucun flip, la règle relâchée cycle de période 2), la borne de queue de `NormTails` vérifiée par Monte-Carlo sur douze couples `(M, t)`, le seuil `√(2·log(2N/ε))` dérivé du union bound, et la **surface du lac recomptée depuis les sources** — où l'organe canonique rend `56` là où les sources en portent `57`, son motif de nom s'arrêtant au premier caractère grec — kernel `python3`, 3 exercices | 35 min | | 22 | [Lean-22-Galois-Probleme-Inverse-M23](Lean-22-Galois-Probleme-Inverse-M23.ipynb) | Le problème inverse de Galois refermé (arXiv:2608.08538, 9 août 2026) : M₂₃ prouvé simple d'ordre 10 200 960 **à l'écran** (`card_M23`/`simple_M23` exécutés, `#print axioms` = liste blanche), design de Witt S(4,7,23) vérifié des deux côtés (253 heptades), polynôme f₁ de degré 23 manipulé pour de vrai (empreinte, irréductibilité, discriminant 383 chiffres, Frobenius mod p) — les deux énoncés distingués : prouvé vs cité | 45 min | | 23 | [Lean-23-ERC20-Invariant-Companion](Lean-23-ERC20-Invariant-Companion.ipynb) | L'invariant de conservation d'un jeton ERC-20 (`Σ balances = totalSupply`) : traces jouets en Python, lectures statiques des 17 déclarations du lake `erc20_lean`, propreté axiomatique par absence de `sorry`, Monte-Carlo sur la tolérance numérique (#11710) | 40 min | | 23b | [Lean-23b-Lean-ERC20-Native-Companion](Lean-23b-Lean-ERC20-Native-Companion.ipynb) | Compagnon **natif** (kernel `lean4-wsl`) du lake `erc20_lean` : les 17 déclarations **résolues par le kernel** (`#check`), l'invariant et les transitions `mint`/`burn`/`transfer` **évalués** sur un état concret (`by decide`), `#print axioms` natif sur les 5 théorèmes phares, la pyramide op → trace `Reachable` → invariant type-checkée avec ses gardes (#11721) | 30 min | @@ -265,9 +266,10 @@ Pour l'état formel détaillé des modules support (preuves résolues vs `sorry` | 19 | Analysis-I-Tao-Workflow | ~18 | 3 | 0 | **NOUVEAU** | | 20 | PFR-Entropy-Method | ~23 | 3 | 0 | **NOUVEAU** | | 20b | PFR-Primitives-Transportables | ~6 | 0 | - | **NOUVEAU** (digestion #12214) | -| 21 | MIMO-Detection-Flips | ~34 | 6 | 0 | **NOUVEAU** | -| 21b | MIMO-Converse-Native | ~30 | 0 | - | **NOUVEAU** (kernel `lean4-wsl`) | -| 21c | Descente-Budget | ~9 | 8 | 0 | **NOUVEAU** (#12219) | +| MIMO-01 | Descente-Budget | ~24 | 4 | 0 | **NOUVEAU** (#12219) | +| MIMO-02 | MIMO-Detection-Flips | ~41 | 4 | 0 | **NOUVEAU** | +| MIMO-03 | MIMO-Converse-Native | ~34 | 0 | - | **NOUVEAU** (kernel `lean4-wsl`) | +| MIMO-04 | Capstone-Digestion | ~26 | 3 | 0 | **NOUVEAU** (kernel python3, capstone de la sous-série #17545) | | 22 | Galois-Probleme-Inverse-M23 | ~25 | 3 | 0 | **NOUVEAU** (exécution Lean + sympy) | | 23 | ERC20-Invariant-Companion | ~21 | 3 | 0 | **NOUVEAU** (lecture statique Python du lake) | | 23b | Lean-ERC20-Native-Companion | ~30 | 2 | - | **NOUVEAU** (kernel `lean4-wsl`) | @@ -479,9 +481,6 @@ Lean/ ├── Lean-17b-Knots-Invariants-Companion.ipynb # Python kernel - invariants de nœuds (PD-codes, Reidemeister, Fox tricolorability), compagnon knot_lean ├── Lean-17c-Knots-Companion-Formel.ipynb # Python kernel - companion formel knot_lean (modules non cités par 17b, murs R2/R3, miroir i18n) ├── Lean-20-Capstone-Digestions-Tao-Python.ipynb # Python kernel - escalier capstone vers la sous-série ANALYSE : digestion du travail formel de T. Tao, règle de chaîne, distance de Ruzsa -├── Lean-21-MIMO-Detection-Flips.ipynb # Python kernel - détection MIMO par flips (seuil 2·log N, companion mimo_lean) -├── Lean-21b-MIMO-Converse-Native.ipynb # Lean4 (WSL) kernel - converse MIMO natif (NormTails, Hanson-Wright, #print axioms) -├── Lean-21c-Descente-Budget.ipynb # Python kernel - budget de descente (décroissance borne les flips, #12219) ├── Lean-22-Galois-Probleme-Inverse-M23.ipynb # Python kernel - problème inverse de Galois (M₂₃ simple prouvé, f₁ degré 23 vérifié) ├── Lean-23-ERC20-Invariant-Companion.ipynb # Python kernel - invariant ERC-20 (lecture statique du lake erc20_lean, Monte-Carlo) ├── Lean-23b-Lean-ERC20-Native-Companion.ipynb # Lean4 (WSL) kernel - ERC-20 natif (17 déclarations résolues par le kernel) @@ -536,6 +535,12 @@ Lean/ │ ├── 09-congruences-tau-lacunarite-delta.ipynb │ ├── serre100_lean/ # Lake Serre 100 (Hasse, MZV, Yoneda, caractères — modules FR + jumeaux _en) │ └── README.md +├── MIMO/ # Sous-série détection MIMO par flips (budget de descente, seuil 2·log N, converse natif) — gradation #17545 : [README](MIMO/README.md) +│ ├── MIMO-01-Descente-Budget-Lean-Python.ipynb # Python kernel - budget de descente (décroissance borne les flips, #12219) +│ ├── MIMO-02-Detection-Flips-Lean-Python.ipynb # Python kernel - détection MIMO par flips (seuil 2·log N, companion mimo_lean) +│ ├── MIMO-03-Converse-Native-Lean.ipynb # Lean4 (WSL) kernel - converse MIMO natif (NormTails, Hanson-Wright, #print axioms) +│ ├── MIMO-04-Capstone-Digestion-Python.ipynb # Python kernel - capstone : les énoncés exécutés à la main, surface du lac recomptée +│ └── README.md ├── assets/ # Images des README de la série ([MANIFEST](assets/readme/MANIFEST.md)) ├── scripts/ # Helpers de maintenance de la série ([README](scripts/README.md), _archive/) ├── sensitivity_lean/ # Théorème de sensibilité (Huang 2019) + algèbre TPR (companions Lean-12/12b/12c) - 0 sorry 0 axiome, Lake build natif (jonction Mathlib) @@ -548,7 +553,7 @@ Lean/ ├── hecke_lean/ # Opérateurs de Hecke T_p/U_p (port pédagogique de anthropics/fermats-last-theorem, Apache-2.0, toolchain pinée v4.33.0) - 0 sorry, Lake build ; companion du notebook Lean-29 ├── formal_groups_lean/ # Groupes formels multivariés (port de anthropics/fermats-last-theorem, Apache-2.0) - 0 sorry, Lake build ; companion du notebook Lean-30 ├── formal_logic_lean/ # Logique formelle : Foundation piné + ProvabilityLogic (CONSUMER_PINNÉ) - 0 sorry, Lake build ; companion des notebooks Lean-3b/34/34b (Epic #15066) -├── mimo_lean/ # Détection MIMO et borne converse Hanson-Wright (brique SLT empruntée à YuanheZ/lean-stat-learning-theory) - 0 sorry, Lake build ; companion du notebook Lean-21b +├── mimo_lean/ # Détection MIMO et borne converse Hanson-Wright (brique SLT empruntée à YuanheZ/lean-stat-learning-theory) - 0 sorry, Lake build ; compagnons MIMO (relation plusieurs-a-plusieurs avec les carnets de la sous-série, sans attribution exclusive a un seul notebook) ├── tegmark_muh_lean/ # Annexe A de Tegmark 2007 (arXiv:0704.0646) : structures finies, encodage, C₃/C₂/NAND, Aut(S), squelette décideur déclaré - **sans dépendance Mathlib**, 0 sorry, Lake build ; companion du notebook Lean-36 ├── mathlib_examples/ # Smoke test Mathlib (ring/linarith/omega/rw, 4 buts) - 0 sorry, Lake build ├── agent_tests/ # Prover daemon (autonomous Lean proof) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md index 92c8b45117..288e5109fc 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md @@ -154,13 +154,13 @@ combinent ces queues par union bound sur les `N` colonnes du canal. ## Companion canonique -Le compagnon natif est **[Lean-21b-MIMO-Converse-Native.ipynb](../Lean-21b-MIMO-Converse-Native.ipynb)** +Le compagnon natif est **[MIMO-03-Converse-Native-Lean.ipynb](../MIMO/MIMO-03-Converse-Native-Lean.ipynb)** (kernel `lean4-wsl`) — il visite les 35 déclarations de `NormTails` / `Converse` / `Bridge`, chacune interrogée par `#check` et sondée par `#print axioms` sur les théorèmes clés. Trois axiomes standards, zéro `sorry`, zéro axiome non standard. -Lean-21b **distingue** le prouvé localement (les énoncés de ce lake) de +MIMO-03 **distingue** le prouvé localement (les énoncés de ce lake) de l'emprunté (les deux théorèmes SLT rappelés explicitement) — la lecture est self-contained, sans confusion de frontière. diff --git a/_quarto.yml b/_quarto.yml index f2e89c0d1b..40f3a7e2af 100644 --- a/_quarto.yml +++ b/_quarto.yml @@ -2082,9 +2082,10 @@ project: - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16j-Conway-Hashlife-Correctness-Native.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17-Conway-Bridge-to-Knots-Python.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-Capstone-Digestions-Tao-Python.ipynb" - - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb" - - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb" - - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-03-Converse-Native-Lean.ipynb" + - "MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-04-Capstone-Digestion-Python.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb" - "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23b-Lean-ERC20-Native-Companion.ipynb" diff --git a/docs/ledgers/18493-counter-scan-classification.md b/docs/ledgers/18493-counter-scan-classification.md index 151b5914be..73e76ea777 100644 --- a/docs/ledgers/18493-counter-scan-classification.md +++ b/docs/ledgers/18493-counter-scan-classification.md @@ -138,7 +138,7 @@ rougirait sur des equivalences correctes partout dans le depot. | `research_vrp_putwrite.ipynb` | c7 | 21 | `tilde_count` | **KEEP** | equivalence unitaire definitionnelle : conversion exacte d'une constante du code (252 jours ouvres/an, 4,184 kJ/kcal, 10 min/bloc) -- ne derive pas | | `Lean-10-LeanDojo.ipynb` | c2 | 22 | `config_dict_doc` | **KEEP** | borne unilaterale (`>100k`) sur une quantite qui ne decroit pas -- ne peut pas deriver faux ; doc de chois de preset | | `Lean-10-LeanDojo.ipynb` | c6 | 6 | `NOTE_runtime` | **EDIT** | litteral non derivable d'une mesure du carnet -- retire, mecanisme conserve | -| `Lean-21-MIMO-Detection-Flips.ipynb` | c3 | 27 | `gt_runtime_threshold` | **KEEP** | logique operationnelle (`> 0 si ...`), pas un compteur -- faux positif de l'organe | +| `MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb` | c3 | 27 | `gt_runtime_threshold` | **KEEP** | logique operationnelle (`> 0 si ...`), pas un compteur -- faux positif de l'organe | | `Z3-16c-Meal-Planner-Patient-Capstone-Python.ipynb` | c14 | 2 | `tilde_count` | **KEEP** | equivalence unitaire definitionnelle : conversion exacte d'une constante du code (252 jours ouvres/an, 4,184 kJ/kcal, 10 min/bloc) -- ne derive pas | | `Z3-16c-Meal-Planner-Patient-Capstone-Python.ipynb` | c14 | 3 | `tilde_count` | **KEEP** | equivalence unitaire definitionnelle : conversion exacte d'une constante du code (252 jours ouvres/an, 4,184 kJ/kcal, 10 min/bloc) -- ne derive pas | | `SC-20-Bitcoin-Scripting-Python.ipynb` | c27 | 24 | `tilde_count` | **KEEP** | equivalence unitaire definitionnelle : conversion exacte d'une constante du code (252 jours ouvres/an, 4,184 kJ/kcal, 10 min/bloc) -- ne derive pas | diff --git a/docs/notebook-metadata/production-scope.md b/docs/notebook-metadata/production-scope.md index bb6657cfb4..77af7ed891 100644 --- a/docs/notebook-metadata/production-scope.md +++ b/docs/notebook-metadata/production-scope.md @@ -318,7 +318,7 @@ l'Epic) ; un dossier de revue est alors préparé (T2).* - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb` -- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb` +- [ ] `MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb` - [ ] `MyIA.AI.Notebooks/SymbolicAI/SemanticWeb/SW-4-CSharp-SPARQL.ipynb` diff --git a/docs/reference/rename-ledger.tsv b/docs/reference/rename-ledger.tsv index 44d99d11b1..29808fb2f4 100644 --- a/docs/reference/rename-ledger.tsv +++ b/docs/reference/rename-ledger.tsv @@ -316,4 +316,7 @@ MyIA.AI.Notebooks/IIT/IIT-03-CoarseGrainingMacroPhi.ipynb MyIA.AI.Notebooks/IIT/ MyIA.AI.Notebooks/IIT/IIT-04-Le-Probleme-de-Frontiere.ipynb MyIA.AI.Notebooks/IIT/IIT-04-Le-Probleme-de-Frontiere-Python.ipynb 2026-10-12 myia-ai-01:CoursIA-2 MyIA.AI.Notebooks/IIT/IIT-05-Lentilles-et-Dissociations.ipynb MyIA.AI.Notebooks/IIT/IIT-05-Lentilles-et-Dissociations-Python.ipynb 2026-10-12 myia-ai-01:CoursIA-2 MyIA.AI.Notebooks/IIT/IIT-06-L-Objet-qui-a-Mordu-IIT.ipynb MyIA.AI.Notebooks/IIT/IIT-06-L-Objet-qui-a-Mordu-IIT-Python.ipynb 2026-10-12 myia-ai-01:CoursIA-2 -MyIA.AI.Notebooks/GameTheory/GameTheory-23a-Biens-Publics-Plan-Deformation-Python.ipynb MyIA.AI.Notebooks/GameTheory/Dynamics/Dynamics-09-Biens-Publics-N-Personnes-Python.ipynb 2026-10-11 myia-po-2023:CoursIA-2 +MyIA.AI.Notebooks/GameTheory/GameTheory-23a-Biens-Publics-Plan-Deformation-Python.ipynb MyIA.AI.Notebooks/GameTheory/Dynamics/Dynamics-09-Biens-Publics-N-Personnes-Python.ipynb 2026-10-11 myia-po-2023:CoursIA-2 +MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-01-Descente-Budget-Lean-Python.ipynb 2026-10-11 myia-po-2024:CoursIA-2 +MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-02-Detection-Flips-Lean-Python.ipynb 2026-10-11 myia-po-2024:CoursIA-2 +MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb MyIA.AI.Notebooks/SymbolicAI/Lean/MIMO/MIMO-03-Converse-Native-Lean.ipynb 2026-10-11 myia-po-2024:CoursIA-2 diff --git a/scripts/notebook_tools/twin_pairs.d/search-12-pattern-databases/0015-2026-10-14-myia-po-2024-CoursIA-2.yaml b/scripts/notebook_tools/twin_pairs.d/search-12-pattern-databases/0015-2026-10-14-myia-po-2024-CoursIA-2.yaml new file mode 100644 index 0000000000..bcb18bb3f8 --- /dev/null +++ b/scripts/notebook_tools/twin_pairs.d/search-12-pattern-databases/0015-2026-10-14-myia-po-2024-CoursIA-2.yaml @@ -0,0 +1,6 @@ +date: '2026-10-14' +by: myia-po-2024:CoursIA-2 +python_sha: 457a54881ac0dbb2fc6e4f761dcae4d399853406 +csharp_sha: c41c476e16a189d67e13eff22fb4f7cbfbf6a0b8 +content_python_sha: ece8c31893ff0f950332774aa04162c6b6660651f6a1c2c6caca8a8f28cf3928 +content_csharp_sha: e7bc7b42544d5f19ee5ffeccb8dc6512b419c6d2b4ac825a25744c97851a0275 diff --git a/scripts/tests/baseline_nb_nav_chain.json b/scripts/tests/baseline_nb_nav_chain.json index 669289b908..e7f06891ff 100644 --- a/scripts/tests/baseline_nb_nav_chain.json +++ b/scripts/tests/baseline_nb_nav_chain.json @@ -1,10 +1,5 @@ { "findings": [ - { - "kind": "independent_chain", - "notebook": "MyIA.AI.Notebooks/GameTheory", - "series": "MyIA.AI.Notebooks/GameTheory" - }, { "kind": "independent_chain", "notebook": "MyIA.AI.Notebooks/GenAI/Image/examples", @@ -20,6 +15,11 @@ "notebook": "MyIA.AI.Notebooks/ML/ML.Net", "series": "MyIA.AI.Notebooks/ML/ML.Net" }, + { + "kind": "independent_chain", + "notebook": "MyIA.AI.Notebooks/Probas/Infer", + "series": "MyIA.AI.Notebooks/Probas/Infer" + }, { "kind": "independent_chain", "notebook": "MyIA.AI.Notebooks/RL", @@ -70,6 +70,11 @@ "notebook": "MyIA.AI.Notebooks/GameTheory/GameTheory-03b-Chemins-de-Swaps-Lean-Python.ipynb", "series": "MyIA.AI.Notebooks/GameTheory" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/GameTheory/GameTheory-03e-Plan-de-deformation-Python.ipynb", + "series": "MyIA.AI.Notebooks/GameTheory" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/GameTheory/GameTheory-03f-Meta-Actions-Tarifees-Python.ipynb", @@ -275,16 +280,6 @@ "notebook": "MyIA.AI.Notebooks/GameTheory/SocialChoice/07-Committees-Core.ipynb", "series": "MyIA.AI.Notebooks/GameTheory/SocialChoice" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced/02-6-MIDI-Generation.ipynb", - "series": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced/02-9-AceStep-Music-Generation.ipynb", - "series": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/GenAI/Audio/04-Applications/04-13-Audiobook-FishAudio-S2Pro.ipynb", @@ -335,16 +330,6 @@ "notebook": "MyIA.AI.Notebooks/GenAI/FineTuning/FT-05-ModelMerging-Routing-Python_en.ipynb", "series": "MyIA.AI.Notebooks/GenAI/FineTuning" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/GenAI/Image/01-Foundation/01-1-OpenAI-DALL-E-3_en.ipynb", - "series": "MyIA.AI.Notebooks/GenAI/Image/01-Foundation" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/GenAI/Image/01-Foundation/01-2-GPT-5-Image-Generation_en.ipynb", - "series": "MyIA.AI.Notebooks/GenAI/Image/01-Foundation" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire/03-Aspire-Observabilite.ipynb", @@ -365,11 +350,6 @@ "notebook": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire/06-Aspire-GardeFous-Roslyn.ipynb", "series": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire/07-Aspire-SemanticFleet-MultiConnector.ipynb", - "series": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire/08-Aspire-AsyncFFI-Dotnet.ipynb", @@ -390,11 +370,6 @@ "notebook": "MyIA.AI.Notebooks/GenAI/PostTraining/PT_02_sft_baseline.ipynb", "series": "MyIA.AI.Notebooks/GenAI/PostTraining" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/GenAI/PostTraining/PT_03_dpo_direct_preference.ipynb", - "series": "MyIA.AI.Notebooks/GenAI/PostTraining" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/GenAI/PostTraining/PT_07_rewardspy_reward_hacking.ipynb", @@ -551,7 +526,7 @@ "series": "MyIA.AI.Notebooks/IIT/ICT-Series" }, { - "kind": "orphan_entry", + "kind": "unreachable", "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-15d-CechObstruction-Python.ipynb", "series": "MyIA.AI.Notebooks/IIT/ICT-Series" }, @@ -610,6 +585,11 @@ "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-22-LLMSubstrat-Python.ipynb", "series": "MyIA.AI.Notebooks/IIT/ICT-Series" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-23-PersonaCatastrophe-Python.ipynb", + "series": "MyIA.AI.Notebooks/IIT/ICT-Series" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-25-InoculationRL-Python.ipynb", @@ -680,6 +660,16 @@ "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-40b-AnalogCognitionWaves-Python.ipynb", "series": "MyIA.AI.Notebooks/IIT/ICT-Series" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-41-SAE-GeometrieFeatures-Python.ipynb", + "series": "MyIA.AI.Notebooks/IIT/ICT-Series" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-41b-Crosscoder-Distillation-Python.ipynb", + "series": "MyIA.AI.Notebooks/IIT/ICT-Series" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-42-InoculationBifurcation-Pilot-Python.ipynb", @@ -705,6 +695,11 @@ "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-Dissociation-PhatSelfReference.ipynb", "series": "MyIA.AI.Notebooks/IIT/ICT-Series" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-Dissociation-SaillancePregnance.ipynb", + "series": "MyIA.AI.Notebooks/IIT/ICT-Series" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/IIT/ICT-Series/ICT-Greffe4-VoteOnChain.ipynb", @@ -722,19 +717,39 @@ }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/IIT/IIT-03-CoarseGrainingMacroPhi-Python.ipynb", + "notebook": "MyIA.AI.Notebooks/IIT/IIT-03-CoarseGrainingMacroPhi.ipynb", "series": "MyIA.AI.Notebooks/IIT" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/IIT/IIT-04-Le-Probleme-de-Frontiere-Python.ipynb", + "notebook": "MyIA.AI.Notebooks/IIT/IIT-04-Le-Probleme-de-Frontiere.ipynb", "series": "MyIA.AI.Notebooks/IIT" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/IIT/IIT-06-L-Objet-qui-a-Mordu-IIT-Python.ipynb", + "notebook": "MyIA.AI.Notebooks/IIT/IIT-06-L-Objet-qui-a-Mordu-IIT.ipynb", "series": "MyIA.AI.Notebooks/IIT" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision/4.2d-Detection-AnchorFree-From-Scratch.ipynb", + "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision/4.2e-Detection-FocalLoss-From-Scratch.ipynb", + "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision/4.2h-YOLOv5-Bench-Ultralytics.ipynb", + "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision/4.2i-Detection-Ultralytics-Difficult-Scenes.ipynb", + "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04-Vision" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/04b-Wavelet-Scattering/WS-00a-Ondelettes-1D-from-scratch.ipynb", @@ -805,11 +820,6 @@ "notebook": "MyIA.AI.Notebooks/Probas/DecisionTheory/Actuariat/Actuariat-04-Ruine-Lundberg.ipynb", "series": "MyIA.AI.Notebooks/Probas/DecisionTheory/Actuariat" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Probas/DecisionTheory/Actuariat/Actuariat-05-Valeur-Info-Souscription.ipynb", - "series": "MyIA.AI.Notebooks/Probas/DecisionTheory/Actuariat" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Probas/DecisionTheory/Causal-Bridges/CausalBridges-02-Dowhy-Estimand-Intervention.ipynb", @@ -855,6 +865,21 @@ "notebook": "MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-08b-Lean-Gittins.ipynb", "series": "MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/Probas/Infer/Infer-18-Change-Point.ipynb", + "series": "MyIA.AI.Notebooks/Probas/Infer" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/Probas/Infer/Infer-19-Survival-Analysis.ipynb", + "series": "MyIA.AI.Notebooks/Probas/Infer" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/Probas/Infer/Infer-1b-Premiers-Modeles.ipynb", + "series": "MyIA.AI.Notebooks/Probas/Infer" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Probas/PyMC/PyMC-16-Sparse-Gaussian-Process.ipynb", @@ -1015,6 +1040,96 @@ "notebook": "MyIA.AI.Notebooks/QuantConnect/projects/Research-Executor/research_volatility_regime_ml.ipynb", "series": "MyIA.AI.Notebooks/QuantConnect/projects/Research-Executor" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/intraday_volume_periodicity.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_btc_ml.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_composite_ff_aw.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_composite_mom_regime.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_iv_rank_strike_clusters.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_m11ef_ensemble.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_m12_har_rv_j.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_m12_har_rv_j_minute.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_m12_hf_btc_local.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_m12_hf_dm_test.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_quality_lowvol.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_risk_parity.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_rl_grpo.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_rl_intro.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_rl_multi_asset.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_rl_ppo.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_rl_reward_shaping.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/QuantConnect/research/research_rl_tactical_overlay.ipynb", + "series": "MyIA.AI.Notebooks/QuantConnect/research" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/RL/PostTraining/RLPT-00-Reward-Model-Bradley-Terry-Python.ipynb", @@ -1080,16 +1195,6 @@ "notebook": "MyIA.AI.Notebooks/Search/Applications/CSP/App-11b-Picross-CSharp.ipynb", "series": "MyIA.AI.Notebooks/Search/Applications/CSP" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Applications/CSP/App-19-ProceduralGeneration-WFC-CSharp.ipynb", - "series": "MyIA.AI.Notebooks/Search/Applications/CSP" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Applications/CSP/App-19-ProceduralGeneration-WFC.ipynb", - "series": "MyIA.AI.Notebooks/Search/Applications/CSP" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Search/Applications/CSP/App-1b-NQueens-CSharp.ipynb", @@ -1125,11 +1230,6 @@ "notebook": "MyIA.AI.Notebooks/Search/Applications/CSP/App-8-MiniZinc-CSharp.ipynb", "series": "MyIA.AI.Notebooks/Search/Applications/CSP" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Applications/Hybrid/App-13-TSP-Metaheuristics.ipynb", - "series": "MyIA.AI.Notebooks/Search/Applications/Hybrid" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Search/Applications/Hybrid/App-13b-TSP-Metaheuristics-CSharp.ipynb", @@ -1157,7 +1257,7 @@ }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Applications/Search/App-14-ConnectFour-CSharp.ipynb", + "notebook": "MyIA.AI.Notebooks/Search/Applications/Search/App-14-ConnectFour-Adversarial-CSharp.ipynb", "series": "MyIA.AI.Notebooks/Search/Applications/Search" }, { @@ -1235,11 +1335,6 @@ "notebook": "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb", "series": "MyIA.AI.Notebooks/Search/Part1-Foundations" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb", - "series": "MyIA.AI.Notebooks/Search/Part1-Foundations" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Search/Part1-Foundations/Search-11-Metaheuristics-CSharp.ipynb", @@ -1265,11 +1360,6 @@ "notebook": "MyIA.AI.Notebooks/Search/Part2-CSP/CSP-7-Soft-CSharp.ipynb", "series": "MyIA.AI.Notebooks/Search/Part2-CSP" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Part2-CSP/CSP-8-Temporal-CSharp.ipynb", - "series": "MyIA.AI.Notebooks/Search/Part2-CSP" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Search/Part2-CSP/CSP-9-Distributed-CSharp.ipynb", @@ -1290,11 +1380,6 @@ "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-13-LandscapeDebias.ipynb", "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-16-AlgorithmSelection.ipynb", - "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-17-ParameterControl.ipynb", @@ -1310,11 +1395,6 @@ "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-20-Langage-de-Composition.ipynb", "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-21-Representation-vs-Algorithme.ipynb", - "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-vs-mealpy/MGS-28-BareBonesPSO-vs-Mealpy.ipynb", @@ -1340,16 +1420,6 @@ "notebook": "MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-03-MAPF-Guarantee-Audit-Python.ipynb", "series": "MyIA.AI.Notebooks/Search/Part5-Frontieres" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-08-OrbitalAssembly-Certificate-Audit-Python.ipynb", - "series": "MyIA.AI.Notebooks/Search/Part5-Frontieres" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-09-RCPSP-Max-Feasibility-Bounds-Python.ipynb", - "series": "MyIA.AI.Notebooks/Search/Part5-Frontieres" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-10-NeuralDiving-Coloration-Python.ipynb", @@ -1430,6 +1500,11 @@ "notebook": "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argumentation-07b-Communication-Channels-Python.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis" }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argumentation-07c-Orchestration-Modes-Python.ipynb", + "series": "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis" + }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argumentation-08d-Restitution-3-Actes-Python.ipynb", @@ -1475,16 +1550,6 @@ "notebook": "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argumentation-Onto-03-Vertus-SKOS-Python.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-01-From-Figure-To-Equation.ipynb", - "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-02-From-Equation-To-Proof.ipynb", - "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-07b-Examples-Python.ipynb", @@ -1512,12 +1577,7 @@ }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb", - "series": "MyIA.AI.Notebooks/SymbolicAI/Lean" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16j-Conway-Hashlife-Correctness-Native.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Lean" }, { @@ -1555,21 +1615,6 @@ "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-38-Capstone-Geometry-Lean-Python.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Lean" }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Planners/02-Classical/Planners-5b-Lean-Relaxation.ipynb", - "series": "MyIA.AI.Notebooks/SymbolicAI/Planners/02-Classical" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Planners/02-Classical/Planners-5c-Differentiel-Atteignabilite.ipynb", - "series": "MyIA.AI.Notebooks/SymbolicAI/Planners/02-Classical" - }, - { - "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/03_Sudoku_Modes_Comparison.ipynb", - "series": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3" - }, { "kind": "orphan_entry", "notebook": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/07_Meal_Planner_Data_External.ipynb", @@ -1702,54 +1747,178 @@ }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-04-Aspic-CSharp.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-07a-Extended-Frameworks-CSharp.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Tweety" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-05b-Argumentation-Lean.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-07b-Ranking-Probabilistic-CSharp.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Tweety" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-07a-Extended-Frameworks-CSharp.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-09-Preferences-CSharp.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Tweety" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-07b-Ranking-Probabilistic-CSharp.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-11-Causal-CSharp.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Tweety" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-09-Preferences-CSharp.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-12-Grounded-Via-TweetyProject-Python.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Tweety" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-11-Causal-CSharp.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-04-Aspic-CSharp.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Tweety" }, { "kind": "orphan_entry", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-12-Grounded-Via-TweetyProject-Python.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-05b-Argumentation-Lean.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Tweety" }, { "kind": "unreachable", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12b-Lean-Sensitivity-Theorem.ipynb", - "series": "MyIA.AI.Notebooks/SymbolicAI/Lean" + "notebook": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced/02-5-Multi-Model-TTS-Gateway.ipynb", + "series": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced/02-6-MIDI-Generation.ipynb", + "series": "MyIA.AI.Notebooks/GenAI/Audio/02-Advanced" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire/07-Aspire-SemanticFleet-MultiConnector.ipynb", + "series": "MyIA.AI.Notebooks/GenAI/Integrations-DotNet/Aspire" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/GenAI/PostTraining/PT_03_dpo_direct_preference.ipynb", + "series": "MyIA.AI.Notebooks/GenAI/PostTraining" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Probas/DecisionTheory/Actuariat/Actuariat-05-Valeur-Info-Souscription.ipynb", + "series": "MyIA.AI.Notebooks/Probas/DecisionTheory/Actuariat" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Applications/CSP/App-19-ProceduralGeneration-WFC-CSharp.ipynb", + "series": "MyIA.AI.Notebooks/Search/Applications/CSP" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Applications/CSP/App-19-ProceduralGeneration-WFC.ipynb", + "series": "MyIA.AI.Notebooks/Search/Applications/CSP" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Applications/Hybrid/App-13-TSP-Metaheuristics.ipynb", + "series": "MyIA.AI.Notebooks/Search/Applications/Hybrid" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part2-CSP/CSP-8-Temporal-CSharp.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part2-CSP" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-09-EverestRelief.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-10-CenterBias.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-14-IslandSynergyFound.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-15-LandscapeAnalysis.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-16-AlgorithmSelection.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-18-CecBanc.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-19-MetropolisReinsertion.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics/MGS-21-Representation-vs-Algorithme.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part4-Metaheuristics" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-01-From-Figure-To-Equation.ipynb", + "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-03-Wu-Method-Python.ipynb", + "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-03b-Ritt-Decomposition-Python.ipynb", + "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry" }, { "kind": "unreachable", - "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12c-Tensor-Product-Representations-Lean.ipynb", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-04-DD-AR-Python.ipynb", + "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-23-ERC20-Invariant-Companion.ipynb", "series": "MyIA.AI.Notebooks/SymbolicAI/Lean" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/Planners/02-Classical/Planners-5c-Differentiel-Atteignabilite.ipynb", + "series": "MyIA.AI.Notebooks/SymbolicAI/Planners/02-Classical" + }, + { + "kind": "unreachable", + "notebook": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3/03_Sudoku_Modes_Comparison.ipynb", + "series": "MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-Linq2Z3" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-08-OrbitalAssembly-Certificate-Audit-Python.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part5-Frontieres" + }, + { + "kind": "orphan_entry", + "notebook": "MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-09-RCPSP-Max-Feasibility-Bounds-Python.ipynb", + "series": "MyIA.AI.Notebooks/Search/Part5-Frontieres" } ], "wrapped": [ { "series": "MyIA.AI.Notebooks/Complexity", - "notebooks": 14 + "notebooks": 13 + }, + { + "series": "MyIA.AI.Notebooks/GenAI/00-GenAI-Environment", + "notebooks": 6 }, { "series": "MyIA.AI.Notebooks/GenAI/Audio/01-Foundation", @@ -1759,6 +1928,10 @@ "series": "MyIA.AI.Notebooks/GenAI/Audio/03-Orchestration", "notebooks": 3 }, + { + "series": "MyIA.AI.Notebooks/GenAI/Image/01-Foundation", + "notebooks": 6 + }, { "series": "MyIA.AI.Notebooks/GenAI/Image/03-Orchestration", "notebooks": 4 @@ -1767,6 +1940,10 @@ "series": "MyIA.AI.Notebooks/GenAI/Image/05-History", "notebooks": 3 }, + { + "series": "MyIA.AI.Notebooks/GenAI/Texte", + "notebooks": 36 + }, { "series": "MyIA.AI.Notebooks/GenAI/Vibe-Coding/Claude-Code/notebooks", "notebooks": 5 @@ -1781,11 +1958,11 @@ }, { "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/01-PythonForDataScience/notebooks", - "notebooks": 6 + "notebooks": 2 }, { "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/02-ML-Cours", - "notebooks": 38 + "notebooks": 37 }, { "series": "MyIA.AI.Notebooks/ML/DataScienceWithAgents/Track2-GoogleADK/Day4-Foundations", @@ -1803,18 +1980,6 @@ "series": "MyIA.AI.Notebooks/NLP", "notebooks": 5 }, - { - "series": "MyIA.AI.Notebooks/Probas/Infer", - "notebooks": 21 - }, - { - "series": "MyIA.AI.Notebooks/QuantConnect/research", - "notebooks": 19 - }, - { - "series": "MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS", - "notebooks": 3 - }, { "series": "MyIA.AI.Notebooks/SymbolicAI/Planners/01-Foundation", "notebooks": 6 @@ -1831,10 +1996,6 @@ "series": "MyIA.AI.Notebooks/SymbolicAI/SmartContracts/01-Solidity-Foundation", "notebooks": 4 }, - { - "series": "MyIA.AI.Notebooks/SymbolicAI/SmartContracts/02-Solidity-Advanced", - "notebooks": 8 - }, { "series": "MyIA.AI.Notebooks/SymbolicAI/SmartContracts/03-Foundry-Testing", "notebooks": 3