From 01185e94f705bdfd30df7b9ad1d825c046cb9fb7 Mon Sep 17 00:00:00 2001 From: jsboige Date: Fri, 9 Oct 2026 17:59:07 +0200 Subject: [PATCH] fix(lean,#17357): Lean-16g -- excursion du noyau (y=10) et ancre pulsar_RLE Deux affirmations fausses, mesurees firsthand : F1 -- la cellule c15 annoncait que le noyau excursionne hors boite jusqu'a y = 11 pendant t = 0..29. Reproduit avec le moteur du carnet (step/islands de c02, boite de c04, core de c06) : le noyau culmine a y = 10 (t = 24..27) et revient a y = 8 a t = 28 ; le y = 11 appartient a l'ile hors boite de 5 cellules, c'est-a-dire a la quasi-particule emise. La prose attribuait au noyau l'excursion de l'emission. F2 -- l'enonce de l'exercice 1 citait pulsar_RLE a RLE.lean:247 ; le def est ligne 255, et la 247 est le corps RLE du lwss (b4o$o3bo$4bo$o2bo!). Les autres ancres du carnet (268, 277, 332-343, 213-219, Life.lean:155, Computation.lean:176) sont exactes -- reverifiees au fichier. Diff : 2 cellules markdown, source seule. Aucune cellule de code modifiee, donc aucune re-execution due (C.2) et aucune sortie touchee. See #17357 Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../SymbolicAI/Lean/Lean-16g-Conway-Canons.ipynb | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16g-Conway-Canons.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16g-Conway-Canons.ipynb index a55b3e0bab..ba649beb53 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16g-Conway-Canons.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16g-Conway-Canons.ipynb @@ -736,14 +736,16 @@ " émission par période).\n", "\n", "Ce que le certificat **ne prétend pas** :\n", - "- il ne dit rien des instants *entre* les multiples de 30 (le noyau excursione hors\n", - " boîte pendant le cycle — mesuré : y jusqu'à 11 pendant t = 0..29) ;\n", + "- il ne dit rien des instants *entre* les multiples de 30 : le noyau sort de la boîte\n", + " stricte au milieu du cycle — mesuré sur t = 0..29, il atteint y = 10 à t = 24..27,\n", + " puis revient à y = 8 à t = 28 quand la quasi-particule s'en détache (le y = 11 observé\n", + " à t = 28..29 appartient à cette quasi-particule, déjà une île disjointe du noyau) ;\n", "- il ne prouve pas la périodicité **pour tout** $t$ : cela exigerait une induction sur\n", " les horizons et l'argument que la quasi-particule émise ne réinteragit jamais avec le\n", " noyau — un théorème lake-side, pas une évaluation ;\n", "- `#eval` reste une évaluation. La version `decide` (preuve noyau) du barreau 1 existe\n", " pour le planeur (`Computation.lean:176`) ; son analogue au canon est le prochain\n", - " geste du lake." + " geste du lake.\n" ] }, { @@ -796,11 +798,11 @@ "\n", "### Exercice 1 — Reconnaître un autre objet : le pulsar\n", "\n", - "Le lake encode aussi le pulsar (`pulsar_RLE`, `RLE.lean:247`) : oscillateur de période 3,\n", + "Le lake encode aussi le pulsar (`pulsar_RLE`, `RLE.lean:255`) : oscillateur de période 3,\n", "48 cellules, le grand oscillateur le plus courant dans les soupes (votre recherche en a\n", "d'ailleurs trouvé, période 3 : 28 instances). Appliquez le protocole de l'exemple guidé 1 :\n", "mesurez sa période, puis montrez qu'il échoue **au critère 2** — aucune émission. Un\n", - "oscillateur n'est pas une source : il n'y a d'horloge que pour lui-même." + "oscillateur n'est pas une source : il n'y a d'horloge que pour lui-même.\n" ] }, {