From ea1e46aca0c31b6a062f35282a4c4dad8ca198c7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 24 Oct 2026 17:01:03 +0200 Subject: [PATCH 1/2] Fix(docs,#22291): H1 des carnets Search-09d/09e et KNOTS-01..04 alignes sur l'ordinal du fichier Tranche 3 du sweep H1 (#22291) : le libelle de la page de parcours generee doit designer le carnet qu'elle lie. Search-09d/09e portaient le label de sous-serie Discrepancy-01/02, KNOTS-01..04 le label legacy Lean 17a-d. Markdown-only (cellule 0, ligne 1), format et corps preserves verbatim ; aucune cellule code, output ou execution_count touche -> pas de re-exec due. Rider bloque par le pre-commit knots-extracts (#21007) : KNOTS-01 cellule 3 citait KNOTS/knot_lean/Knots/FigureEight.lean, forme relative qui ne resout pas depuis le dossier du carnet -> knot_lean/Knots/FigureEight.lean (le renvoi ligne 17 est verifie exact dans le module). Markdown-only aussi. Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../Search-09d-BeckFiala-Lean-Python.ipynb | 6 +++--- .../Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb | 4 ++-- .../Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb | 6 +++--- .../SymbolicAI/Lean/KNOTS/KNOTS-02-Invariants-Python.ipynb | 6 +++--- .../Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb | 2 +- .../Lean/KNOTS/KNOTS-04-Geometrie-Hyperbolique-Python.ipynb | 6 +++--- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-BeckFiala-Lean-Python.ipynb b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-BeckFiala-Lean-Python.ipynb index e45c90a105c..58bea20dc92 100644 --- a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-BeckFiala-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09d-BeckFiala-Lean-Python.ipynb @@ -14,13 +14,13 @@ "tags": [] }, "source": [ - "# Discrepancy-01 - Beck-Fiala (la noix `disc <= 2k-1`) et le pont vers le lake `discrepancy_lean`\n", + "# Search-09d - Beck-Fiala (la noix `disc <= 2k-1`) et le pont vers le lake `discrepancy_lean`\n", "\n", "> **Premier carnet de la sous-série `Discrepancy/`.** Il expose en Python les énoncés du lake `discrepancy_lean` (Mathlib4 pinné `db584cd6`, toolchain `leanprover/lean4:v4.33.0` dans `discrepancy_lean/lean-toolchain`) et rend palpable la frontière entre ce qui est **certifié** sur `main` et ce qui ne l'est pas : une conjecture n'est jamais présentée comme un résultat. Ce notebook n'est pas une preuve formelle : il implémente un **squelette** de l'algorithme de Beck-Fiala (rounding itératif, départ `0`, phases sur les lignes dangereuses), expose les définitions Lean verbatim comme citations, et compare la discrépance obtenue à la borne `2k - 1` du théorème `beck_fiala_classic`.\n", "\n", "> **Précondition du théorème.** La borne `2*k - 1` de `beck_fiala_classic` n'engage que sous la précondition `maxDegree(F) ≤ k`, où `k` borne le **degré** maximal d'un sommet, et non la cardinalité des parties. Sur les instances aléatoires de la cellule 4 (`n=10, m=15, k_max=2`), cette précondition est violée pour les 40 instances (degré maximal mesuré entre 4 et 9) : la borne n'est donc pas applicable, et les cellules 3 et 5 en tirent les conséquences.\n", "\n", - "**Navigation** : [Search README](..) ; [LEAN_INVENTORY](../LEAN_INVENTORY.md) ; [FORMAL_STATUS](../discrepancy_lean/FORMAL_STATUS.md) ; module source [BeckFiala.lean](../discrepancy_lean/Discrepancy/BeckFiala.lean). Issue de suivi : #17816.\n" + "**Navigation** : [Search README](..) ; [LEAN_INVENTORY](../LEAN_INVENTORY.md) ; [FORMAL_STATUS](../discrepancy_lean/FORMAL_STATUS.md) ; module source [BeckFiala.lean](../discrepancy_lean/Discrepancy/BeckFiala.lean). Issue de suivi : #17816." ] }, { @@ -961,4 +961,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +} diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb index 6479a35f942..e54daf06646 100644 --- a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb +++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-09e-Komlos-Lean.ipynb @@ -14,7 +14,7 @@ "tags": [] }, "source": [ - "# Discrepancy-02 — Discrépance combinatoire : la couche formelle (Komlós, Bansal–Jiang 2025)\n", + "# Search-09e — Discrépance combinatoire : la couche formelle (Komlós, Bansal–Jiang 2025)\n", "\n", "> **Deuxième marche de la sous-série `Discrepancy/`** (issue #17816, arbitrage Search #17802) — compagnon formel de [Search-09c](../Part1-Foundations/Search-09c-CombinatorialDiscrepancy.ipynb)\n", "\n", @@ -4480,4 +4480,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb index be65b9e5a7b..179ef981bd3 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb @@ -14,7 +14,7 @@ "tags": [] }, "source": [ - "# Lean 17a — Conway, les Nœuds et la Preuve de Piccirillo\n", + "# KNOTS-01 — Conway, les Nœuds et la Preuve de Piccirillo\n", "\n", "**Série** : SymbolicAI / Lean — Knots Theory (**17a**)\n", "\n", @@ -37,7 +37,7 @@ "La section **6** recense, elle, ce qui manque encore à Mathlib — et la section\n", "**5** décrit l'arborescence du projet.\n", "\n", - "**Notebook compagnon** : `KNOTS-02-Invariants-Python.ipynb` — calcul effectif des invariants via SnapPy/SageMath.\n" + "**Notebook compagnon** : `KNOTS-02-Invariants-Python.ipynb` — calcul effectif des invariants via SnapPy/SageMath." ] }, { @@ -179,7 +179,7 @@ "carré parfait (condition **nécessaire** de Fox–Milnor :\n", "$|\\Delta(-1)| = 1, 4, 9, 16, \\ldots$).\n", "Or $\\det(4_1) = |\\Delta(-1)| = 5$ — la condition de Fox–Milnor échoue\n", - "(valeur documentée par `KNOTS/knot_lean/Knots/FigureEight.lean` ligne 17 :\n", + "(valeur documentée par `knot_lean/Knots/FigureEight.lean` ligne 17 :\n", "`det(4_1) = |Δ(-1)| = 5`).\n", "Attention : le déterminant non-carré n'est qu'**une** obstruction parmi\n", "d'autres, pas un critère autonome de non-sliceness. Une seconde voie, plus\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-02-Invariants-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-02-Invariants-Python.ipynb index 8e6f7286ca4..5ac0c095c02 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-02-Invariants-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-02-Invariants-Python.ipynb @@ -14,7 +14,7 @@ "tags": [] }, "source": [ - "# Lean 17b — Invariants de Nœuds : Calcul et Vérification\n", + "# KNOTS-02 — Invariants de Nœuds : Calcul et Vérification\n", "\n", "**Série** : SymbolicAI / Lean — Knots Theory (17b = compagnon de 17a)\n", "\n", @@ -33,7 +33,7 @@ "- Python 3.10+ avec `snappy`, `matplotlib`, `numpy`\n", "- `pip install snappy matplotlib numpy`\n", "\n", - "## Durée estimée : 45 min\n" + "## Durée estimée : 45 min" ] }, { @@ -2319,4 +2319,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +} diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb index 9b5f02bc705..bd33e6bf06c 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-03-Companion-Formel-Lean-Python.ipynb @@ -14,7 +14,7 @@ "tags": [] }, "source": [ - "# Lean 17c — Le lake `knot_lean` par ses déclarations (compagnon formel)\n", + "# KNOTS-03 — Le lake `knot_lean` par ses déclarations (compagnon formel)\n", "\n", "Compagnon du **Lean-17** (« Conway, les Nœuds et la Preuve de Piccirillo »). Là où Lean-17 raconte l'histoire mathématique (Fox 3-colorabilité, mutants, Piccirillo 2020, Lidman 2026) et interroge `Conway.lean` et `Lidman.lean`, ce notebook interroge les modules que Lean-17 ne cite pas — **`Basic.lean`** (les structures fondamentales), **`Invariant.lean`** (la chaîne 3-colorabilité), **`Reidemeister.lean`** (les moves R1/R2/R3 et leurs murs) et **`MathlibPrerequisites.lean`** (la feuille de route des prérequis Mathlib) — et mesure l'état de la formalisation : déclarations par module, sorries réels vs prose, axiomes admis.\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-04-Geometrie-Hyperbolique-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-04-Geometrie-Hyperbolique-Python.ipynb index b247bcc9f1a..ccb87d6ab84 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-04-Geometrie-Hyperbolique-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-04-Geometrie-Hyperbolique-Python.ipynb @@ -15,7 +15,7 @@ "tags": [] }, "source": [ - "# Lean 17d — Géométrie hyperbolique : tétraèdres idéaux, chirurgie de Dehn, rigidité de Mostow\n", + "# KNOTS-04 — Géométrie hyperbolique : tétraèdres idéaux, chirurgie de Dehn, rigidité de Mostow\n", "\n", "**Série** : SymbolicAI / Lean — Knots Theory (17d = compagnon de 17a/17b/17c)\n", "\n", @@ -39,7 +39,7 @@ "## Prerequis\n", "\n", "- `pip install snappy>=3.2 mpmath>=1.3`\n", - "- lecture recommandée de KNOTS-02 (volume hyperbolique) avant ce carnet-ci : la vérification croisée présuppose de voir où le volume sort.\n" + "- lecture recommandée de KNOTS-02 (volume hyperbolique) avant ce carnet-ci : la vérification croisée présuppose de voir où le volume sort." ] }, { @@ -1088,4 +1088,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +} From 3b04f6262f3d2f63433627991a44f47698e888de Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 24 Oct 2026 22:46:19 +0200 Subject: [PATCH 2/2] Fix(notebook-lean,#22291): le renvoi FigureEight.lean pointe la ligne 16 La cellule citait 'ligne 17' : dans Knots/FigureEight.lean, det(4_1) = |Delta(-1)| = 5 est en ligne 16, la 17 etant sa continuation. Markdown-only, aucune re-execution due. Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb index 179ef981bd3..d39cb235bde 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/KNOTS-01-Conway-Proofs-Lean-Python.ipynb @@ -179,7 +179,7 @@ "carré parfait (condition **nécessaire** de Fox–Milnor :\n", "$|\\Delta(-1)| = 1, 4, 9, 16, \\ldots$).\n", "Or $\\det(4_1) = |\\Delta(-1)| = 5$ — la condition de Fox–Milnor échoue\n", - "(valeur documentée par `knot_lean/Knots/FigureEight.lean` ligne 17 :\n", + "(valeur documentée par `knot_lean/Knots/FigureEight.lean` ligne 16 :\n", "`det(4_1) = |Δ(-1)| = 5`).\n", "Attention : le déterminant non-carré n'est qu'**une** obstruction parmi\n", "d'autres, pas un critère autonome de non-sliceness. Une seconde voie, plus\n",