Skip to content
Merged
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@
"3. Primitive 3 — La fonctionnelle τ : patron de descente, **test de limite**.\n",
"4. Conclusion — lien vers ANALYSE-03 et le lac `pfr`.\n",
"\n",
"**Suite de la sous-série** : [ANALYSE-06 — Sensibilité 2026 (notre lac face aux familles d'openai/math)](ANALYSE-06-Sensibilite-2026-Lean.ipynb)\n",
"**Suite de la sous-série** : [ANALYSE-06 — Sensibilité 2026 (notre lac face aux familles d'openai/math)](ANALYSE-06b-Sensibilite-2026-Lean.ipynb)\n",
"**Suite de la sous-série** : [ANALYSE-07 — Percolation critique (notre lac face aux familles 2026 213/236)](ANALYSE-07-Percolation-Critique.ipynb)"
]
},
Expand Down Expand Up @@ -1647,8 +1647,8 @@
"end_time": "2026-10-23T22:00:28.041614+00:00",
"environment_variables": {},
"exception": null,
"input_path": "D:\\Dev\\CoursIA-2-22206-analyse\\MyIA.AI.Notebooks\\SymbolicAI\\Lean\\ANALYSE\\ANALYSE-04-PFR-Primitives-Python.ipynb",
"output_path": "D:/Dev/CoursIA-2-22206-analyse/MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-04-PFR-Primitives-Python.ipynb",
"input_path": "ANALYSE-04-PFR-Primitives-Python.ipynb",
"output_path": "ANALYSE-04-PFR-Primitives-Python.ipynb",
"parameters": {},
"start_time": "2026-10-23T22:00:21.892909+00:00",
"version": "2.6.0"
Expand All @@ -1662,4 +1662,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
"\n",
"| Notebook précédent | Notebook suivant |\n",
"|---|---|\n",
"| [ANALYSE-04 — Trois primitives de PFR](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — version anglaise](ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) |"
"| [ANALYSE-04 — Trois primitives de PFR](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — version anglaise](ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb) |"
]
},
{
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
"\n",
"**ANALYSE** sub-series (#17545 grading) — Fold 2 of the **Origami** digestion (#19898): the Boolean-combinatorics results published by `openai/math` in 2026, read from **our** `Sensitivity` lake — the port of Huang's theorem (2019).\n",
"\n",
"This notebook is a **native** companion: Lean 4 kernel under WSL, every `#check` queries the actually-compiled lake, every `#eval` really computes. Numerical computation is done **natively in Lean** — no Python fallback; the file-name suffix follows the series naming convention. This is the English twin of the French notebook `ANALYSE-06-Sensibilite-2026-Lean.ipynb`; it renders the **same** computation in English: the code cells are byte-identical to the French side (the repository's twin-parity invariant), while the lake's English siblings (`*_en`, i18n convention #4980) carry the English docstrings.\n",
"This notebook is a **native** companion: Lean 4 kernel under WSL, every `#check` queries the actually-compiled lake, every `#eval` really computes. Numerical computation is done **natively in Lean** — no Python fallback; the file-name suffix follows the series naming convention. This is the English twin of the French notebook `ANALYSE-06b-Sensibilite-2026-Lean.ipynb`; it renders the **same** computation in English: the code cells are byte-identical to the French side (the repository's twin-parity invariant), while the lake's English siblings (`*_en`, i18n convention #4980) carry the English docstrings.\n",
"\n",
"**Prerequisites**: the main series tutorial (notebooks 1 to 6). Reading [Lean-12b — Huang's Sensitivity Theorem](../Lean-12b-Lean-Sensitivity-Theorem.ipynb) makes section 1 more comfortable, but is not required: we recall what we need.\n",
"\n",
Expand All @@ -28,7 +28,7 @@
"\n",
"| Previous notebook | French version | Next notebook |\n",
"|---|---|---|\n",
"| [ANALYSE-04 — Three PFR primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — French version](ANALYSE-06-Sensibilite-2026-Lean.ipynb) | [Lean-12b — Huang's Sensitivity Theorem](../Lean-12b-Lean-Sensitivity-Theorem.ipynb) |"
"| [ANALYSE-04 — Three PFR primitives](ANALYSE-04-PFR-Primitives-Python.ipynb) | [ANALYSE-06 — French version](ANALYSE-06b-Sensibilite-2026-Lean.ipynb) | [Lean-12b — Huang's Sensitivity Theorem](../Lean-12b-Lean-Sensitivity-Theorem.ipynb) |"
]
},
{
Expand Down
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ La série principale garde son tutoriel (numéros 1 à 14) ; le présent dossier
| [ANALYSE-04-PFR-Primitives-Python](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-KLS-Lean-Python](ANALYSE-05-KLS-Lean-Python.ipynb) | La conjecture KLS démontrée (Bizeul–Klartag–Lehec, arXiv:2610.05474) : énoncé (Théorème 1.1), chaîne de la preuve en cinq maillons (thin-shell, germe quadratique, localisation stochastique, suspension, critère de Song–Zhang), lac local `kls_lean` — audit Mathlib au pin, six définitions, deux théorèmes prouvés (0 sorry, `#print axioms` propre) — thin-shell en Monte-Carlo avec saturation exacte à 8n par l'exponentielle produit, banc 1-lipschitzien minorant `poincareConstant` | 45 min |
| [ANALYSE-05b-KLS-Song-Zhang-O1](ANALYSE-05b-KLS-Song-Zhang-O1.ipynb) | Le KLS constant est-il O(1) ? (Zhao Song, Xinzhi Zhang, arXiv:2610.01447v2) : les quatre expériences du passage `log*` → constante — `log* n` mesuré (3 puis 4, et 4 encore à `10^1000`) et plafonnement géométrique des coûts ; le centrage d'Appell du Théorème 4.1, où la variance gaussienne vaut `d!` contre une borne `1024^d (d!)^4` (rapport `7.9e37` à `d = 8`), Hermite retrouvé et contrôlé contre une référence externe ; le germe quadratique, avec l'identité `Var = 2‖B‖²_HS` et un ancrage exact à `8` ; enfin l'inégalité de Cheeger en dimension 1, où `λ ≥ ψ²/4` est vérifiée et **saturée**, et la seconde borne du Lemme 2.2 (`ψ² ≤ πC_P`) **reconstituée par triangulation** — le symbole de comparaison n'a pas survécu à l'extraction du PDF, les lectures naïves sont réfutées une par une et la lecture restante (`C_P = 1/λ`) vérifiée sur six familles isotropes : une reconstruction nôtre, jamais attribuée au papier | 45 min |
| [ANALYSE-06-Sensibilite-2026-Lean](ANALYSE-06-Sensibilite-2026-Lean.ipynb) | La combinatoire booléenne 2026 d'openai/math (familles 127/132/186/192) lue depuis notre lac `Sensitivity` : Huang prouvé chez nous (`#check`/`#print axioms`), énoncés 2026 cités avec leur statut épistémique, et nos séparations sensibilité/sensibilité de bloc du module `Sensitivity.Separations`, prouvées et calculées (`#eval` natif, Pli 2 d'Origami #19898) ; jumeau anglais à code byte-identique : [ANALYSE-06-...-_en](ANALYSE-06-Sensibilite-2026-Lean_en.ipynb) | 35 min |
| [ANALYSE-06b-Sensibilite-2026-Lean](ANALYSE-06b-Sensibilite-2026-Lean.ipynb) | La combinatoire booléenne 2026 d'openai/math (familles 127/132/186/192) lue depuis notre lac `Sensitivity` : Huang prouvé chez nous (`#check`/`#print axioms`), énoncés 2026 cités avec leur statut épistémique, et nos séparations sensibilité/sensibilité de bloc du module `Sensitivity.Separations`, prouvées et calculées (`#eval` natif, Pli 2 d'Origami #19898) ; jumeau anglais à code byte-identique : [ANALYSE-06b-...-_en](ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb) | 35 min |
| [ANALYSE-07-Percolation-Critique](ANALYSE-07-Percolation-Critique.ipynb) | Percolation critique et Ising sur l'arbre d-régulier — pli 3 de la digestion Origami (#19898) : les inégalités de Harris–Kleitman `#check`ées dans notre lac `percolation_lean`, les familles 2026 **213** (criticité Benjamini–Schramm) et **236** (seuil factor-of-IID de l'Ising sur l'arbre) citées avec leur statut, et deux calculs nôtres **exacts** — la probabilité critique p_c = 1/(d-1) par Galton–Watson (point fixe non trivial 4/9, vérifiable à la main) et l'écart entre seuil de reconstruction et seuil d'aimantation ; jumeau anglais à code byte-identique : [ANALYSE-07-...-_en](ANALYSE-07-Percolation-Critique_en.ipynb) | 40 min |
| [ANALYSE-08-Ramsey-VdW](ANALYSE-08-Ramsey-VdW.ipynb) | Ramsey et van der Waerden par épuisement : R(3,3)=6 et W(2,3)=9 prouvés par énumération exhaustive (survivantes 18→12→0 côté graphes, 6→0 côté progressions), le mur 2^153 où le geste meurt, et le pont probabiliste d'Erdős (#19960, pli 4 Origami #19898) | 30 min |
| [ANALYSE-09-Tuilage-Aperiodique](ANALYSE-09-Tuilage-Aperiodique.ipynb) | Famille 155 du corpus `openai/math` : un carreau de ℤ³ qui pave sans périodicité totale (contre-exemple de dimension trois). Le carnet ramène le pavage par translations à la couverture exacte que le dépôt formalise déjà (`sudoku_lean`, `ExactCover.IsExactCover`), puis mesure quatre expériences avec deux organes déterministes — backtracking borné `place_tiles` et rang de période `period_rank` (élimination de Gauss exacte sur ℚ) — la leçon transverse étant que la demi-fenêtre cache toute période plus longue qu'elle ; jumeau anglais à code byte-identique : [ANALYSE-09-...-_en](ANALYSE-09-Tuilage-Aperiodique_en.ipynb) | 30 min |
Expand Down
4 changes: 2 additions & 2 deletions scripts/notebook_tools/pedagogy_density_baseline.json
Original file line number Diff line number Diff line change
Expand Up @@ -1127,8 +1127,8 @@
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-05-KLS-Lean-Python.ipynb": 2115.667,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python.ipynb": 2157.6,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb": 2110.8,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb": 2414.5,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb": 2401.625,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb": 2414.5,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb": 2401.625,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique.ipynb": 1996.625,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-07-Percolation-Critique_en.ipynb": 2016.0,
"MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-08-Ramsey-VdW.ipynb": 865.273,
Expand Down
4 changes: 2 additions & 2 deletions translations/translation_golden_set.json
Original file line number Diff line number Diff line change
Expand Up @@ -1808,8 +1808,8 @@
},
{
"kind": "notebook",
"fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean.ipynb",
"en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06-Sensibilite-2026-Lean_en.ipynb",
"fr": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean.ipynb",
"en": "MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-06b-Sensibilite-2026-Lean_en.ipynb",
"sha1_fr": "eaf45cfea264a611cbdb5c523da69353249b3477",
"sha1_en": "aa7ff661aae1abef4d08ba674296ca350a741fb6",
"sources_sha1_fr": "1063a3296c8ff96e92b6c335b36d5fa920aa50cc",
Expand Down
Loading