rename(#16231,#17545): descente ANALYSE en dossier — 4 carnets + referents (pilote CL1)

.claude/rules/pr-review-discipline.md

@@ -75,7 +75,7 @@ Single-seed ou single-fold = **CHANGES_REQUESTED** sauf flag explicite `[POC]` d
 
 7. **PRs notebook : lire le check-run ADVISORY `Output-collapse ratchet (base vs PR, advisory)`** (organe `scripts/notebook_tools/check_output_collapse.py`, enregistré `blocking=False` dans `scripts/ci/fast_lane_registry.py`, #15327). Conclusion neutre par design — le signal vit dans le détail du check-run. Un finding `SIGNATURE` (sortie base substantielle remplacée par « `Execution sautee (API non configuree)` » et consœurs) = **re-exécution sans les clés → `CHANGES_REQUESTED`** : les cellules se sont « exécutées avec succès » en dégradation gracieuse (`if api_ok:`), c'est le contournement de C.2 par la porte de secours. Contre-exemple mesuré (fondateur) : #15209, `Lean-7b-Examples.ipynb` `6b327a9bf` → `56d98429a` — 11 → 11 cellules, 0 erreur, `execution_count` réels partout, et **10637 → 2985** caractères de sortie (cellules `2195 → 147`, `2568 → 38`, `2074 → 42`) : tous les organes verts, la perte réelle. Un finding `MAGNITUDE` (perte d'un ordre de grandeur par cellule, non couvert par les exemptions automatiques contenu-déplacé/purge-diagnostic) exige une **justification dans le body** (allègement déclaré, au même titre que les autres ratchets) — sans elle : `CHANGES_REQUESTED`.
 
-8. **PRs notebook : lire le check-run ADVISORY `Source-collapse ratchet (base vs PR, advisory)`** (organe `scripts/notebook_tools/check_source_collapse.py`, enregistré `blocking=False` dans `scripts/ci/fast_lane_registry.py`, #15901). Le point 7 mesure la perte de **sortie**, celui-ci la perte de **source** : les deux sont indépendantes, et c'est tout l'intérêt. Contre-exemple mesuré (fondateur) : #15862, `GameTheory-06e-Open-Source-Game-Theory.ipynb` `244c7c54f032` → `7a355873de32`, cellule `c989_independent_v2` **8425 → 5309** caractères de source (-37.0 %, 3116 perdus) — une table déclarative et un `assert` avaient disparu, aucun organe rouge, parce qu'une table supprimée et un `assert` reduit ne produisent **aucune sortie** : la perte est invisible par construction aux ratchets de sortie. Un finding `MAGNITUDE` exige une **justification dans le body** (allègement déclaré) — sans elle : `CHANGES_REQUESTED`. Les exemptions automatiques (contenu déplacé vers une AUTRE cellule du **même** notebook, purge de texte de diagnostic type `CS####`/`warning`) blanchissent le signal : leur silence n'est **pas** un acquittement, et un `exempt-moved` qui ne déplace que quelques lignes doit être recontrôlé à l'œil. Le **même** check-run porte depuis #16110 le **second mécanisme** de la famille, pris par l'autre bout : la source survit en volume et perd sa **forme**. Un finding `STRUCTURE` signale `emptied` (la cellule avait des instructions, elle n'en a plus) et/ou `orphan-output` (elle porte une sortie qu'aucune instruction ne peut avoir produite) : le code est parti, la preuve d'exécution est restée → **restaurer la source ou retirer la sortie**, sinon `CHANGES_REQUESTED`. Contre-exemple mesuré (fondateur) : #16097, `Lean-18-Sendov-Complex-Analysis.ipynb` cellule `40cb37d5`, **1132 → 1728** caractères (la cellule **grossit** : la même écriture qui a retiré les `\n` a ajouté une note de récupération) et `ast.parse(...).body` **10 → 0** — tout le code replié en un seul commentaire. Le ratchet de volume ne pouvait pas le voir (le gate s'arrête avant tout plancher quand la tête est plus longue) et `notebook-cell-source-parses` non plus (une cellule intégralement commentée se **parse proprement**) : `orphan-output` ne consulte que la cellule, il n'y a aucune exemption qui le blanchisse.
+8. **PRs notebook : lire le check-run ADVISORY `Source-collapse ratchet (base vs PR, advisory)`** (organe `scripts/notebook_tools/check_source_collapse.py`, enregistré `blocking=False` dans `scripts/ci/fast_lane_registry.py`, #15901). Le point 7 mesure la perte de **sortie**, celui-ci la perte de **source** : les deux sont indépendantes, et c'est tout l'intérêt. Contre-exemple mesuré (fondateur) : #15862, `GameTheory-06e-Open-Source-Game-Theory.ipynb` `244c7c54f032` → `7a355873de32`, cellule `c989_independent_v2` **8425 → 5309** caractères de source (-37.0 %, 3116 perdus) — une table déclarative et un `assert` avaient disparu, aucun organe rouge, parce qu'une table supprimée et un `assert` reduit ne produisent **aucune sortie** : la perte est invisible par construction aux ratchets de sortie. Un finding `MAGNITUDE` exige une **justification dans le body** (allègement déclaré) — sans elle : `CHANGES_REQUESTED`. Les exemptions automatiques (contenu déplacé vers une AUTRE cellule du **même** notebook, purge de texte de diagnostic type `CS####`/`warning`) blanchissent le signal : leur silence n'est **pas** un acquittement, et un `exempt-moved` qui ne déplace que quelques lignes doit être recontrôlé à l'œil. Le **même** check-run porte depuis #16110 le **second mécanisme** de la famille, pris par l'autre bout : la source survit en volume et perd sa **forme**. Un finding `STRUCTURE` signale `emptied` (la cellule avait des instructions, elle n'en a plus) et/ou `orphan-output` (elle porte une sortie qu'aucune instruction ne peut avoir produite) : le code est parti, la preuve d'exécution est restée → **restaurer la source ou retirer la sortie**, sinon `CHANGES_REQUESTED`. Contre-exemple mesuré (fondateur) : #16097, `ANALYSE-01-Sendov-Lean-Python.ipynb` cellule `40cb37d5`, **1132 → 1728** caractères (la cellule **grossit** : la même écriture qui a retiré les `\n` a ajouté une note de récupération) et `ast.parse(...).body` **10 → 0** — tout le code replié en un seul commentaire. Le ratchet de volume ne pouvait pas le voir (le gate s'arrête avant tout plancher quand la tête est plus longue) et `notebook-cell-source-parses` non plus (une cellule intégralement commentée se **parse proprement**) : `orphan-output` ne consulte que la cellule, il n'y a aucune exemption qui le blanchisse.
 
 **Advisory `.NET execution_count` ≠ outputs vides autorisés (#5214).** L'advisory autorise à sauter la ré-exécution **CI** (pas de kernel .NET en CI), **pas** à committer des sorties vides : `.NET Interactive` s'exécute **localement** sur chaque worker → une cellule .NET committée **DOIT** porter `execution_count != null`. `validate_pr_notebooks.py` FAIL sur `.NET` + `null`, et ne tolère `null` que là où l'exécution locale est aussi impossible (QC Cloud, Lean). Verdict attendu dans le body : `EXEC_PROVED` vs `STRUCTURAL_ONLY` (refus).
 

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-18-Sendov-Complex-Analysis.ipynb → MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-01-Sendov-Lean-Python.ipynb

@@ -26,7 +26,7 @@
     "\n",
     "| Notebook precedent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [A* Optimalite (Search-03e)](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | [Lean-19 - Analysis-I Tao Workflow](Lean-19-Analysis-I-Tao-Workflow.ipynb) |\n",
+    "| [A* Optimalite (Search-03e)](../../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | [Lean-19 - Analysis-I Tao Workflow](ANALYSE-02-Tao-Lean-Python.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -1360,13 +1360,13 @@
    "end_time": "2026-09-14T09:43:28.570564+00:00",
    "environment_variables": {},
    "exception": null,
-   "input_path": "Lean-18-Sendov-Complex-Analysis.ipynb",
-   "output_path": "Lean-18-Sendov-Complex-Analysis.ipynb",
+   "input_path": "ANALYSE-01-Sendov-Lean-Python.ipynb",
+   "output_path": "ANALYSE-01-Sendov-Lean-Python.ipynb",
    "parameters": {},
    "start_time": "2026-09-14T09:43:09.504617+00:00",
    "version": "2.6.0"
   }
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-19-Analysis-I-Tao-Workflow.ipynb → MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-02-Tao-Lean-Python.ipynb

@@ -25,7 +25,7 @@
     "\n",
     "| Notebook precedent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [Lean-18 - Sendov Complex Analysis](Lean-18-Sendov-Complex-Analysis.ipynb) | [Lean-20 - PFR Entropy Method](Lean-20-PFR-Entropy-Method.ipynb) |\n",
+    "| [Lean-18 - Sendov Complex Analysis](ANALYSE-01-Sendov-Lean-Python.ipynb) | [Lean-20 - PFR Entropy Method](ANALYSE-03-PFR-Lean.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -37,7 +37,7 @@
     "\n",
     "- Notre serie Lean a deja couvert Sendov (Lean-18 : digestion par Tao de la preuve de L. Mazur, analyse complexe, 1 grain = 1 théorème). Pour ce 2e grain — cette fois une oeuvre propre de Tao — on prend du recul : ce n'est plus *un* théorème mais *un manuel entier* (11 chapitres, 109 fichiers, 44 297 LOC, 2079 `sorry` deliberes par l'auteur comme exercices au lecteur).\n",
     "- **Substance nouvelle** : Lean-19 est le premier grain de notre serie qui est *Lean-meta* (recit methodologique) plutot que *Lean-content* (preuve formelle). C'est ce qu'on appelle dans le jargon de la preuve agentique un *process notebook* — un notebook qui decrit un processus de preuve, pas une preuve.\n",
-    "- **Méthode nouvelle** : comparaison directe avec notre cluster — en realite TROIS méthodes : Tao a la main (seul, 2 ans, 5-15 commits/jour), Tao + grosse machinerie (Sendov digere en 2 jours, cf. [Lean-18](Lean-18-Sendov-Complex-Analysis.ipynb)), et notre cluster (4 workers + 1 coordinateur, ~2 PRs/h, petits increments sur des problemes varies). Quels sont les tradeoffs ?\n",
+    "- **Méthode nouvelle** : comparaison directe avec notre cluster — en realite TROIS méthodes : Tao a la main (seul, 2 ans, 5-15 commits/jour), Tao + grosse machinerie (Sendov digere en 2 jours, cf. [Lean-18](ANALYSE-01-Sendov-Lean-Python.ipynb)), et notre cluster (4 workers + 1 coordinateur, ~2 PRs/h, petits increments sur des problemes varies). Quels sont les tradeoffs ?\n",
     "- **Apport a Mathlib** : Tao n'utilise presque pas Mathlib dans les chapitres 2-5 (auto-contenu, axiomes Peano, construction de Cauchy des réels), puis transitionne progressivement vers Mathlib a partir du chapitre 6. C'est une approche pedagogique rare — la plupart des projets partent de Mathlib.\n",
     "\n",
     "**Note methodologique** : conformement a la convention de notre serie (cf. Lean-12 Sensitivity, Lean-17 Knots, Lean-18 Sendov), ce notebook utilise un **kernel Python 3**, pas Lean 4. Les enonces Lean sont presentes sous forme pedagogique (pseudo-Lean), et les preuves sont illustrees en Python. Le **vrai code Lean** est disponible dans le lac source : `git clone https://github.com/teorth/analysis && cd analysis && lake build`."
@@ -535,7 +535,7 @@
     "\n",
     "| | Méthode 1 — Humain a la main, longue haleine | Méthode 2 — Single-agent + grosse machinerie | Méthode 3 — Cluster distribue |\n",
     "|---|---|---|---|\n",
-    "| **Exemple** | Tao, *Analysis I* (ce manuel) | Tao digerant la preuve Sendov de L. Mazur ([Lean-18](Lean-18-Sendov-Complex-Analysis.ipynb)) | CoursIA (ce depot) |\n",
+    "| **Exemple** | Tao, *Analysis I* (ce manuel) | Tao digerant la preuve Sendov de L. Mazur ([Lean-18](ANALYSE-01-Sendov-Lean-Python.ipynb)) | CoursIA (ce depot) |\n",
     "| **Duree** | 2 ans, continuite | 2 jours, sprint intensif | continue, sans terme |\n",
     "| **Machinerie** | Lean 4 + Mathlib, en grande partie a la main | Claude Opus 5 en co-pilote (14,9k LOC en 2 jours) | 4-5 workers + coordinateur + harnais de regles |\n",
     "| **Objet** | UN projet profond tenu longtemps : manuel complet, 11 chapitres | UN théorème SOTA digere en entier | problemes varies ; les 2 travaux presentes ici (Lean-18, Lean-19) sont des petites noix typiques |\n",

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20-PFR-Entropy-Method.ipynb → MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-03-PFR-Lean.ipynb

@@ -29,7 +29,7 @@
     "\n",
     "| Notebook précédent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [Lean-19 - Analysis-I Tao Workflow](Lean-19-Analysis-I-Tao-Workflow.ipynb) | [Lean-21 - MIMO Detection Flips](Lean-21-MIMO-Detection-Flips.ipynb) |\n",
+    "| [Lean-19 - Analysis-I Tao Workflow](ANALYSE-02-Tao-Lean-Python.ipynb) | [Lean-21 - MIMO Detection Flips](../Lean-21-MIMO-Detection-Flips.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -1384,13 +1384,13 @@
    "source": [
     "## 7. Pont vers la série ICT — l'entropie comme monnaie commune\n",
     "\n",
-    "La série [ICT](../../IIT/ICT-Series/) (information et calcul) manipule l'entropie dans des contextes très différents de la combinatoire additive. PFR s'y rattache directement :\n",
+    "La série [ICT](../../../IIT/ICT-Series/) (information et calcul) manipule l'entropie dans des contextes très différents de la combinatoire additive. PFR s'y rattache directement :\n",
     "\n",
     "| Notebook ICT | Rôle de l'entropie | Lien avec PFR |\n",
     "|---|---|---|\n",
-    "| [ICT-16 — MDL](../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) | longueur de code minimale = entropie | `binEntropy` est la longueur du code optimal d'un bit biaisé (section 5) |\n",
-    "| [ICT-17 — Epsilon-machine](../../IIT/ICT-Series/ICT-17-EpsilonMachine.ipynb) | entropie des états causaux, complexité statistique | « structure = compressibilité » : mesurer l'entropie pour révéler la machine cachée |\n",
-    "| [ICT-14 — Free energy](../../IIT/ICT-Series/ICT-14-FreeEnergySurprise.ipynb) | surprise, bornes informationnelles | l'information comme borne sur le comportement d'un système |\n",
+    "| [ICT-16 — MDL](../../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) | longueur de code minimale = entropie | `binEntropy` est la longueur du code optimal d'un bit biaisé (section 5) |\n",
+    "| [ICT-17 — Epsilon-machine](../../../IIT/ICT-Series/ICT-17-EpsilonMachine.ipynb) | entropie des états causaux, complexité statistique | « structure = compressibilité » : mesurer l'entropie pour révéler la machine cachée |\n",
+    "| [ICT-14 — Free energy](../../../IIT/ICT-Series/ICT-14-FreeEnergySurprise.ipynb) | surprise, bornes informationnelles | l'information comme borne sur le comportement d'un système |\n",
     "\n",
     "Le slogan commun : **l'information mesure la structure**. En ICT, une faible complexité statistique révèle une machine à états petite ; en théorie additive, une **petite duplication** (peu d'entropie dans X + X′) force une **structure algébrique** — le sous-espace H de la conjecture de Marton. PFR est un théorème de « compression ⟹ structure », et il est prouvé par la théorie de l'information elle-même."
    ]
@@ -1498,7 +1498,7 @@
     "\n",
     "**Dette 3 -- Generalisation aux structures non-polynomiales.** PFR polynomial dit : si la pluie sur les `n` degres est `1/n^(1+δ)`, alors structure. La generalisation aux structures non-polynomiales (pluie exponentielle, melange Markov, chaines de Markov) reste conjecturale. Le travail de Gowers 2016 sur la *Normalised Fourier Analysis* n'aborde pas la generalisation.\n",
     "\n",
-    "**Dette 4 -- Pont vers la serie ICT non formalise.** La section 7 evoque le pont « entropie comme monnaie commune » avec la serie [ICT](../../IIT/ICT-Series/), mais le pont formel entre `PFR.ForMathlib.Entropy.Basic` et `InformationFlow.lean` (ICT) n'est pas etabli. Une issue de suivi pourrait nommer ce deficit dans l'EPIC #13106 (tranche D, hors cette PR).\n",
+    "**Dette 4 -- Pont vers la serie ICT non formalise.** La section 7 evoque le pont « entropie comme monnaie commune » avec la serie [ICT](../../../IIT/ICT-Series/), mais le pont formel entre `PFR.ForMathlib.Entropy.Basic` et `InformationFlow.lean` (ICT) n'est pas etabli. Une issue de suivi pourrait nommer ce deficit dans l'EPIC #13106 (tranche D, hors cette PR).\n",
     "\n",
     "**Statut au 2026-09** : ces quatre dettes sont *documentees*, pas *resolues*. Elles relevent d'un travail ulterieur, pas d'un fix de fond dans ce notebook. La mention explicite sert deux fins : (a) empecher un lecteur de croire la preuve close sur les points quantitatifs ; (b) ouvrir la voie a un futur grain qui attaquerait l'une des quatre."
    ]
@@ -1517,7 +1517,9 @@
     "tags": []
    },
    "source": [
-    "## 9. Exercices\n\nTrois exercices pour s'approprier les briques. Chaque cellule code est un point de départ **exécutable** : elle charge l'énoncé-cible (`#check`) ou un calcul d'amorce (`#eval`), et laisse le raisonnement en `TODO`. Le kernel persiste d'une cellule à l'autre : les définitions du Code 2.1 (`addBit`, `sumset`) restent disponibles."
+    "## 9. Exercices\n",
+    "\n",
+    "Trois exercices pour s'approprier les briques. Chaque cellule code est un point de départ **exécutable** : elle charge l'énoncé-cible (`#check`) ou un calcul d'amorce (`#eval`), et laisse le raisonnement en `TODO`. Le kernel persiste d'une cellule à l'autre : les définitions du Code 2.1 (`addBit`, `sumset`) restent disponibles."
    ]
   },
   {
@@ -1786,7 +1788,7 @@
     "2. Le cas d'égalité est caractérisé par `binEntropy_eq_log_two` : H₂(p) = log 2 ⟺ p = 1/2.\n",
     "3. Avec `binEntropy_eq_zero` : H₂(p) = 0 ⟺ p ∈ {0, 1} — une pièce parfaitement déterminée n'a aucune incertitude.\n",
     "\n",
-    "**Conclusion attendue** : le bit le plus imprévisible possible est un bit **équilibré** — pont direct vers [ICT-16](../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) : le code le plus court pour un bit est celui d'une pièce honnête."
+    "**Conclusion attendue** : le bit le plus imprévisible possible est un bit **équilibré** — pont direct vers [ICT-16](../../../IIT/ICT-Series/ICT-16-MDLTwoPartCode.ipynb) : le code le plus court pour un bit est celui d'une pièce honnête."
    ]
   },
   {
@@ -1912,7 +1914,7 @@
     "\n",
     "### 10.3 Ce qui reste ouvert\n",
     "\n",
-    "L'exposant continue de baisser (12 → 11,123 → 11 → 9) ; l'extension aux groupes de torsion bornée avance dans le lac ; et la version entropique elle-même (`entropic_PFR_conjecture`) reste un bel objet d'étude — la constante 11 y est-elle optimale ? Autant de grains futurs pour cette série — et côté [ICT](../../IIT/ICT-Series/), l'entropie y reviendra sous toutes ses formes."
+    "L'exposant continue de baisser (12 → 11,123 → 11 → 9) ; l'extension aux groupes de torsion bornée avance dans le lac ; et la version entropique elle-même (`entropic_PFR_conjecture`) reste un bel objet d'étude — la constante 11 y est-elle optimale ? Autant de grains futurs pour cette série — et côté [ICT](../../../IIT/ICT-Series/), l'entropie y reviendra sous toutes ses formes."
    ]
   }
  ],
@@ -1932,4 +1934,4 @@
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-20b-PFR-Primitives-Transportables.ipynb → MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb

@@ -17,15 +17,15 @@
     "# Lean-20b : Trois primitives de PFR, et l'endroit exact où elles cessent de valoir\n",
     "\n",
     "**Série** : SymbolicAI / Lean — Digestions de résultats profonds, companion de Lean-20\n",
-    "**Source** : Lean-20-PFR-Entropy-Method.ipynb (digestion PFR par Gowers-Green-Manners-Tao, 2023)\n",
+    "**Source** : ANALYSE-03-PFR-Lean.ipynb (digestion PFR par Gowers-Green-Manners-Tao, 2023)\n",
     "**Lac source** : https://github.com/teorth/pfr (formalisation collaborative Lean 4)\n",
     "**Kernel** : `lean4-wsl` — le notebook conceptuel Python illustre les primitives, les preuves formelles restent dans Lean-20\n",
     "\n",
     "## Navigation\n",
     "\n",
     "| Notebook précédent | Notebook suivant |\n",
     "|---|---|\n",
-    "| [Lean-20 - PFR Entropy Method](Lean-20-PFR-Entropy-Method.ipynb) | [Lean-21 - MIMO Detection Flips](Lean-21-MIMO-Detection-Flips.ipynb) |\n",
+    "| [Lean-20 - PFR Entropy Method](ANALYSE-03-PFR-Lean.ipynb) | [Lean-21 - MIMO Detection Flips](../Lean-21-MIMO-Detection-Flips.ipynb) |\n",
     "\n",
     "***\n",
     "\n",
@@ -991,19 +991,19 @@
    "end_time": "2026-09-02T21:29:17.311787",
    "environment_variables": {},
    "exception": null,
-   "input_path": "Lean-20b-PFR-Primitives-Transportables.ipynb",
-   "output_path": "Lean-20b-PFR-Primitives-Transportables.ipynb",
+   "input_path": "ANALYSE-04-PFR-Primitives-Python.ipynb",
+   "output_path": "ANALYSE-04-PFR-Primitives-Python.ipynb",
    "parameters": {},
    "start_time": "2026-09-02T21:29:13.778559",
    "version": "2.6.0"
   },
   "references": [
-   "Lean-20-PFR-Entropy-Method.ipynb (companion upstream)",
+   "ANALYSE-03-PFR-Lean.ipynb (companion upstream)",
    "Gowers, Green, Manners, Tao (novembre 2023) — On a conjecture of Marton",
    "https://github.com/teorth/pfr — formalisation collaborative Lean 4"
   ],
   "title": "Lean-20b : Trois primitives de PFR, et l'endroit exact où elles cessent de valoir"
  },
  "nbformat": 4,
  "nbformat_minor": 5
-}
+}