From 55d392d41ce03b90c058c89f0438238498ce2cbd Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 28 Sep 2026 15:45:14 +0200 Subject: [PATCH] fix(lean,#17357): sweep pin v4.32.1 Famille B -- mention duale provenance/pin courant (3 carnets) Co-Authored-By: Claude Sonnet 5 --- .../SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb | 3 +-- .../SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb | 2 +- .../SymbolicAI/Lean/Lean-16h-Conway-PatternTour-Native.ipynb | 3 +-- 3 files changed, 3 insertions(+), 5 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb index 932da45153..a6d3f484b7 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13b-CHSH-Tsirelson-Native.ipynb @@ -1636,8 +1636,7 @@ "## 9. Provenance, raccords et conclusion\n", "\n", "**Ce qui a été exécuté.** Les huit cellules de code ci-dessus ont été exécutées par le kernel\n", - "Lean 4 (`lean4-wsl-conway`, `--cd ~/conway-build`) sur le lake `conway_lean` au pin\n", - "`leanprover/lean4:v4.32.1`. Les sorties sont celles du noyau : `#check`, `#print axioms` et\n", + "Lean 4 (`lean4-wsl-conway`, `--cd ~/conway-build`) sur le lake `conway_lean`, au pin `leanprover/lean4:v4.32.1` à\nl'exécution de ces sorties (le lake au HEAD pinne `v4.33.0` depuis la migration\n#16341). Les sorties sont celles du noyau : `#check`, `#print axioms` et\n", "`#eval` sont rendus par le REPL, aucune sortie n'a été écrite à la main.\n", "\n", "**Chaîne de dépendance, telle qu'elle se lit dans les sorties.** `tsirelson_bound` n'est pas une\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb index d2af053aa1..c251927cf4 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-13c-CHSH-Landau-Saturation.ipynb @@ -1658,7 +1658,7 @@ "## 11. Provenance, raccords et conclusion\n", "\n", "**Ce qui a été exécuté.** Les onze cellules de code ci-dessus (huit de démonstration et trois exercices) ont été exécutées par le kernel\n", - "Lean 4 (`lean4-wsl`) sur le lake `conway_lean` au pin `leanprover/lean4:v4.32.1`. Les sorties\n", + "Lean 4 (`lean4-wsl`) sur le lake `conway_lean`, au pin `leanprover/lean4:v4.32.1` à l'exécution\nde ces sorties (le lake au HEAD pinne `v4.33.0` depuis la migration #16341). Les sorties\n", "sont celles du noyau : `#check`, `#print axioms` et `#eval` sont rendus par le REPL, aucune\n", "sortie n'a été écrite à la main.\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16h-Conway-PatternTour-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16h-Conway-PatternTour-Native.ipynb index f7e33fbf03..ad2ee77bc7 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16h-Conway-PatternTour-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16h-Conway-PatternTour-Native.ipynb @@ -658,8 +658,7 @@ "source": [ "**Lecture du contraste.** `beacon_is_oscillator` : *does not depend on any axioms*. Une ligne\n", "plus bas, `pulsar_is_oscillator` : `depends on axioms:\n", - "[pulsar_is_oscillator._native.native_decide.ax_1_1]` — l'auxiliaire nommé par théorème que la\n", - "v4.32.1 génère pour chaque `native_decide`.\n", + "[pulsar_is_oscillator._native.native_decide.ax_1_1]` — l'auxiliaire nommé par théorème que la toolchain\ngénère pour chaque `native_decide` (v4.32.1 à l'exécution de ces sorties ; le lake\nau HEAD pinne `v4.33.0` depuis la migration #16341).\n", "La bascule `decide` → `native_decide` est exactement le diagnostic documenté dans le module (cycle\n", "c.736, `decidable_instance_propagation.md`) : sur les prédicats d'état du Jeu de la Vie, `decide`\n", "tient jusqu'à une profondeur de récursion modérée, puis cède. La tournée ne cache pas la bascule —\n",