diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb
index 4a11f3e0b2..2b87b2ecdb 100644
--- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb
@@ -4,19 +4,12 @@
    "cell_type": "markdown",
    "id": "intro-title",
    "metadata": {
-    "papermill": {
-     "duration": 0.012089,
-     "end_time": "2026-10-07T02:16:17.021588",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:17.009499",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
     "# Lean-16b : Hommage a John Conway — Game of Life as Computation\n",
     "\n",
-    "**Navigation** : [<< Lean-15 Grothendieck](Lean-15-Grothendieck-Tribute.ipynb) | [Index](README.md) | [Lean-16c Compagnon Golly >>](Lean-16c-Conway-Game-of-Life-Golly.ipynb)\n",
+    "**Navigation** : [<< Lean-16a Conway, l'homme et l'oeuvre](Lean-16a-Conway-Man-and-Work.ipynb) | [Index](README.md) | [Lean-16c Compagnon Golly >>](Lean-16c-Conway-Game-of-Life-Golly.ipynb)\n",
     "\n",
     "**Kernel** : `python3-lean` — CPython 3.13 canonique serie Lean (#17476) + Lean 4 via WSL (source de verite formelle, sections 6-7 et annexes D-G)\n",
     "\n",
@@ -64,13 +57,6 @@
    "cell_type": "markdown",
    "id": "section-2-rule",
    "metadata": {
-    "papermill": {
-     "duration": 0.007412,
-     "end_time": "2026-10-07T02:16:17.040760",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:17.033348",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -93,19 +79,6 @@
    "execution_count": 1,
    "id": "gol-python-impl",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:17.054171Z",
-     "iopub.status.busy": "2026-10-07T02:16:17.053869Z",
-     "iopub.status.idle": "2026-10-07T02:16:24.649093Z",
-     "shell.execute_reply": "2026-10-07T02:16:24.647583Z"
-    },
-    "papermill": {
-     "duration": 7.604039,
-     "end_time": "2026-10-07T02:16:24.650336",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:17.046297",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -168,13 +141,6 @@
    "cell_type": "markdown",
    "id": "section-2b-interp",
    "metadata": {
-    "papermill": {
-     "duration": 0.00896,
-     "end_time": "2026-10-07T02:16:24.666561",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:24.657601",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -197,13 +163,6 @@
    "cell_type": "markdown",
    "id": "8998c242",
    "metadata": {
-    "papermill": {
-     "duration": 0.006581,
-     "end_time": "2026-10-07T02:16:24.684156",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:24.677575",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -219,19 +178,6 @@
    "execution_count": 2,
    "id": "70f39299",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:24.707009Z",
-     "iopub.status.busy": "2026-10-07T02:16:24.706331Z",
-     "iopub.status.idle": "2026-10-07T02:16:24.713579Z",
-     "shell.execute_reply": "2026-10-07T02:16:24.712484Z"
-    },
-    "papermill": {
-     "duration": 0.020264,
-     "end_time": "2026-10-07T02:16:24.714887",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:24.694623",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -274,13 +220,6 @@
    "cell_type": "markdown",
    "id": "section-3-patterns",
    "metadata": {
-    "papermill": {
-     "duration": 0.006359,
-     "end_time": "2026-10-07T02:16:24.730106",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:24.723747",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -304,19 +243,6 @@
    "execution_count": 3,
    "id": "patterns-viz",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:24.740489Z",
-     "iopub.status.busy": "2026-10-07T02:16:24.740226Z",
-     "iopub.status.idle": "2026-10-07T02:16:25.155870Z",
-     "shell.execute_reply": "2026-10-07T02:16:25.154677Z"
-    },
-    "papermill": {
-     "duration": 0.422145,
-     "end_time": "2026-10-07T02:16:25.156993",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:24.734848",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -415,13 +341,6 @@
    "cell_type": "markdown",
    "id": "section-3b-interp",
    "metadata": {
-    "papermill": {
-     "duration": 0.010128,
-     "end_time": "2026-10-07T02:16:25.175364",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:25.165236",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -444,13 +363,6 @@
    "cell_type": "markdown",
    "id": "ea418142",
    "metadata": {
-    "papermill": {
-     "duration": 0.009256,
-     "end_time": "2026-10-07T02:16:25.194357",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:25.185101",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -466,19 +378,6 @@
    "execution_count": 4,
    "id": "4deed899",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:25.212097Z",
-     "iopub.status.busy": "2026-10-07T02:16:25.211751Z",
-     "iopub.status.idle": "2026-10-07T02:16:25.219393Z",
-     "shell.execute_reply": "2026-10-07T02:16:25.218127Z"
-    },
-    "papermill": {
-     "duration": 0.017997,
-     "end_time": "2026-10-07T02:16:25.220945",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:25.202948",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -521,13 +420,6 @@
    "cell_type": "markdown",
    "id": "section-6-pillars",
    "metadata": {
-    "papermill": {
-     "duration": 0.008582,
-     "end_time": "2026-10-07T02:16:25.239609",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:25.231027",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -557,19 +449,6 @@
    "execution_count": 5,
    "id": "pillars-toolbox",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:25.259405Z",
-     "iopub.status.busy": "2026-10-07T02:16:25.259144Z",
-     "iopub.status.idle": "2026-10-07T02:16:25.276939Z",
-     "shell.execute_reply": "2026-10-07T02:16:25.275642Z"
-    },
-    "papermill": {
-     "duration": 0.028581,
-     "end_time": "2026-10-07T02:16:25.277929",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:25.249348",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -703,13 +582,6 @@
    "cell_type": "markdown",
    "id": "acte1-otca",
    "metadata": {
-    "papermill": {
-     "duration": 0.009689,
-     "end_time": "2026-10-07T02:16:25.294931",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:25.285242",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -748,19 +620,6 @@
    "execution_count": 6,
    "id": "render-otca",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:25.309178Z",
-     "iopub.status.busy": "2026-10-07T02:16:25.308733Z",
-     "iopub.status.idle": "2026-10-07T02:16:26.006298Z",
-     "shell.execute_reply": "2026-10-07T02:16:26.004597Z"
-    },
-    "papermill": {
-     "duration": 0.706871,
-     "end_time": "2026-10-07T02:16:26.007756",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:25.300885",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -809,13 +668,6 @@
    "cell_type": "markdown",
    "id": "acte2-cpu",
    "metadata": {
-    "papermill": {
-     "duration": 0.011243,
-     "end_time": "2026-10-07T02:16:26.030183",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:26.018940",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -852,19 +704,6 @@
    "execution_count": 7,
    "id": "render-cpu",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:26.052424Z",
-     "iopub.status.busy": "2026-10-07T02:16:26.051834Z",
-     "iopub.status.idle": "2026-10-07T02:16:26.536060Z",
-     "shell.execute_reply": "2026-10-07T02:16:26.534517Z"
-    },
-    "papermill": {
-     "duration": 0.497413,
-     "end_time": "2026-10-07T02:16:26.537684",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:26.040271",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -906,13 +745,6 @@
    "cell_type": "markdown",
    "id": "acte3-gemini",
    "metadata": {
-    "papermill": {
-     "duration": 0.006882,
-     "end_time": "2026-10-07T02:16:26.553821",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:26.546939",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -951,19 +783,6 @@
    "execution_count": 8,
    "id": "render-gemini",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:26.568045Z",
-     "iopub.status.busy": "2026-10-07T02:16:26.567645Z",
-     "iopub.status.idle": "2026-10-07T02:16:27.685841Z",
-     "shell.execute_reply": "2026-10-07T02:16:27.684725Z"
-    },
-    "papermill": {
-     "duration": 1.125382,
-     "end_time": "2026-10-07T02:16:27.686542",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:26.561160",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1017,13 +836,6 @@
    "cell_type": "markdown",
    "id": "synthese-piliers",
    "metadata": {
-    "papermill": {
-     "duration": 0.005392,
-     "end_time": "2026-10-07T02:16:27.697281",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:27.691889",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1050,26 +862,19 @@
     "| `otca_self_emulates` | `otca_metapixel_witness` | prouve (vide) - Phase 7 réel |\n",
     "| `spartan_adder_correct` | `cpu_witness` (Beluchenko/Stearns) | prouve (vide) - Phase 8 réel |\n",
     "| `gemini_replicates` | `gemini_witness` | prouve (vide) - Phase 6 réel |\n",
-    "| — | `unitcell_witness` (Beluchenko 2011) | prouve (vide) - Phase 8 réel |\n",
+    "| — | `unitcell_initial_population` + `unitcell_initial_nonempty` (Bell, p5760) | **prouvé (grille réelle)** — tranche 2 de #19989 |\n",
     "\n",
-    "> **Statut compile = prouve contre grilles vides.** Les temoins compilent **sans `sorry`** : `otcaInitial` / `otcaTarget` etc. sont des grilles vides (`([] : Grid)`), donc `evolveHashlifeFastMemo N [] = []` est prouvé trivialement par le lemme `evolveHashlifeFastMemo_empty`. Aucun axiome n'est admis. La **preuve réelle** - le pattern RLE charge (OTCA 70 KB, Gemini plusieurs MB) pousse dans `native_decide` - reste l'objectif des Phases 6-8 une fois la memoization Hashlife en place.\n",
+    "> **Statut compile = prouvé contre grilles vides — sauf l'UnitCell.** Les témoins OTCA / Gemini / CPU compilent **sans `sorry`** : leurs grilles `Initial`/`Target` sont vides (`([] : Grid)`), donc `evolveHashlifeFastMemo N [] = []` est prouvé trivialement par le lemme `evolveHashlifeFastMemo_empty`. Aucun axiome n'est admis. L'UnitCell, lui, n'est **plus** vide depuis la tranche 2 de #19989 : `unitcellInitial` charge le RLE réel (`include_str` + `RLE.parseRLE!`), et ses théorèmes d'état sont prouvés par `native_decide` sur cette vraie grille — fermant précisément la route `evolveHashlifeFastMemo_empty` pour ce témoin.\n",
     "\n",
-    "Le temoin (`unitcell_witness`, UnitCell de Beluchenko, 4096 generations) n'apparait pas dans le recit des trois actes : c'est un metapixel plus petit que l'OTCA, plus accessible comme première cible `native_decide`. Il est integrallement défini dans `Pillars.lean` et constitue un jalon intermediaire naturel avant l'OTCA complète.\n",
+    "Le quatrième témoin (l'UnitCell, metapixel compact) n'apparait pas dans le récit des trois actes. Le motif présent dans l'archive est le **p5760 de David Bell** (`p5760unitlifecell.rle`, période 5 760 générations) — le chiffre 4 096 qui circulait décrit l'UnitCell de Beluchenko, un **autre motif**, absent de l'archive. Son témoin de période n'est **pas exprimable** dans ce moteur : sur grille sans bord le motif émet des planeurs (aucune répétition mesurée sur 8 000 générations) ; la période 5 760 est confirmée **sans bord** (tore 500 × 500, génération 11324 = génération 5564). Ce qui est prouvé sur la vraie grille : `unitcell_initial_population` (population 4 761) et `unitcell_initial_nonempty` (grille non vide).\n",
     "\n",
-    "Chaque preuve réelle est prevue comme un seul `by native_decide` une fois la memoization Hashlife en place.\n"
+    "Chaque preuve réelle restante (OTCA, Gemini, CPU) est prevue comme un seul `by native_decide` une fois la memoization Hashlife en place.\n"
    ]
   },
   {
    "cell_type": "markdown",
    "id": "exercice-3-md",
    "metadata": {
-    "papermill": {
-     "duration": 0.005311,
-     "end_time": "2026-10-07T02:16:27.708224",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:27.702913",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1093,19 +898,6 @@
    "execution_count": 9,
    "id": "exercice-3",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:27.724574Z",
-     "iopub.status.busy": "2026-10-07T02:16:27.723914Z",
-     "iopub.status.idle": "2026-10-07T02:16:27.729217Z",
-     "shell.execute_reply": "2026-10-07T02:16:27.728090Z"
-    },
-    "papermill": {
-     "duration": 0.014735,
-     "end_time": "2026-10-07T02:16:27.730163",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:27.715428",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1135,13 +927,6 @@
    "cell_type": "markdown",
    "id": "section-8-demo",
    "metadata": {
-    "papermill": {
-     "duration": 0.011584,
-     "end_time": "2026-10-07T02:16:27.748089",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:27.736505",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1155,19 +940,6 @@
    "execution_count": 10,
    "id": "demo-blinker-glider",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:27.763869Z",
-     "iopub.status.busy": "2026-10-07T02:16:27.763450Z",
-     "iopub.status.idle": "2026-10-07T02:16:28.210351Z",
-     "shell.execute_reply": "2026-10-07T02:16:28.209354Z"
-    },
-    "papermill": {
-     "duration": 0.454776,
-     "end_time": "2026-10-07T02:16:28.211166",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:27.756390",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1231,13 +1003,6 @@
    "cell_type": "markdown",
    "id": "section-8b-interp",
    "metadata": {
-    "papermill": {
-     "duration": 0.005519,
-     "end_time": "2026-10-07T02:16:28.223195",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.217676",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1254,13 +1019,6 @@
    "cell_type": "markdown",
    "id": "section-7-turing",
    "metadata": {
-    "papermill": {
-     "duration": 0.006221,
-     "end_time": "2026-10-07T02:16:28.235507",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.229286",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1307,13 +1065,6 @@
    "cell_type": "markdown",
    "id": "section-6-lean",
    "metadata": {
-    "papermill": {
-     "duration": 0.006797,
-     "end_time": "2026-10-07T02:16:28.250086",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.243289",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1329,19 +1080,6 @@
    "execution_count": 11,
    "id": "subprocess-setup",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:28.266956Z",
-     "iopub.status.busy": "2026-10-07T02:16:28.266246Z",
-     "iopub.status.idle": "2026-10-07T02:16:28.282020Z",
-     "shell.execute_reply": "2026-10-07T02:16:28.280950Z"
-    },
-    "papermill": {
-     "duration": 0.027209,
-     "end_time": "2026-10-07T02:16:28.283309",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.256100",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1404,19 +1142,6 @@
    "execution_count": 12,
    "id": "life-lean-stats",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:28.297034Z",
-     "iopub.status.busy": "2026-10-07T02:16:28.296776Z",
-     "iopub.status.idle": "2026-10-07T02:16:28.333959Z",
-     "shell.execute_reply": "2026-10-07T02:16:28.332521Z"
-    },
-    "papermill": {
-     "duration": 0.045273,
-     "end_time": "2026-10-07T02:16:28.335088",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.289815",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1478,13 +1203,6 @@
    "cell_type": "markdown",
    "id": "section-9b-interp",
    "metadata": {
-    "papermill": {
-     "duration": 0.007319,
-     "end_time": "2026-10-07T02:16:28.348699",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.341380",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1507,13 +1225,6 @@
    "cell_type": "markdown",
    "id": "section-9-7-eval-md",
    "metadata": {
-    "papermill": {
-     "duration": 0.014228,
-     "end_time": "2026-10-07T02:16:28.371513",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.357285",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1537,19 +1248,6 @@
    "execution_count": 13,
    "id": "13a8ea0a",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:16:28.392958Z",
-     "iopub.status.busy": "2026-10-07T02:16:28.392743Z",
-     "iopub.status.idle": "2026-10-07T02:23:16.875425Z",
-     "shell.execute_reply": "2026-10-07T02:23:16.874256Z"
-    },
-    "papermill": {
-     "duration": 408.503126,
-     "end_time": "2026-10-07T02:23:16.881887",
-     "exception": false,
-     "start_time": "2026-10-07T02:16:28.378761",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1649,13 +1347,6 @@
    "cell_type": "markdown",
    "id": "exercice-4-md",
    "metadata": {
-    "papermill": {
-     "duration": 0.007361,
-     "end_time": "2026-10-07T02:23:16.897241",
-     "exception": false,
-     "start_time": "2026-10-07T02:23:16.889880",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1671,19 +1362,6 @@
    "execution_count": 14,
    "id": "exercice-4",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:23:16.917478Z",
-     "iopub.status.busy": "2026-10-07T02:23:16.917020Z",
-     "iopub.status.idle": "2026-10-07T02:23:16.924249Z",
-     "shell.execute_reply": "2026-10-07T02:23:16.923025Z"
-    },
-    "papermill": {
-     "duration": 0.020019,
-     "end_time": "2026-10-07T02:23:16.925819",
-     "exception": false,
-     "start_time": "2026-10-07T02:23:16.905800",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1726,13 +1404,6 @@
    "cell_type": "markdown",
    "id": "section-9-8-rle-eval-md",
    "metadata": {
-    "papermill": {
-     "duration": 0.012808,
-     "end_time": "2026-10-07T02:23:16.950448",
-     "exception": false,
-     "start_time": "2026-10-07T02:23:16.937640",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1754,19 +1425,6 @@
    "execution_count": 15,
    "id": "rle-parse-eval",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:23:16.975321Z",
-     "iopub.status.busy": "2026-10-07T02:23:16.975035Z",
-     "iopub.status.idle": "2026-10-07T02:27:22.367292Z",
-     "shell.execute_reply": "2026-10-07T02:27:22.366198Z"
-    },
-    "papermill": {
-     "duration": 245.413429,
-     "end_time": "2026-10-07T02:27:22.376412",
-     "exception": false,
-     "start_time": "2026-10-07T02:23:16.962983",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1861,13 +1519,6 @@
    "cell_type": "markdown",
    "id": "section-10-build",
    "metadata": {
-    "papermill": {
-     "duration": 0.007132,
-     "end_time": "2026-10-07T02:27:22.390531",
-     "exception": false,
-     "start_time": "2026-10-07T02:27:22.383399",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -1885,19 +1536,6 @@
    "execution_count": 16,
    "id": "lake-build-life",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:27:22.403990Z",
-     "iopub.status.busy": "2026-10-07T02:27:22.403767Z",
-     "iopub.status.idle": "2026-10-07T02:29:30.745811Z",
-     "shell.execute_reply": "2026-10-07T02:29:30.744463Z"
-    },
-    "papermill": {
-     "duration": 128.356514,
-     "end_time": "2026-10-07T02:29:30.752677",
-     "exception": false,
-     "start_time": "2026-10-07T02:27:22.396163",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -1977,19 +1615,6 @@
    "execution_count": 17,
    "id": "grep-sorry-life",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:29:30.771108Z",
-     "iopub.status.busy": "2026-10-07T02:29:30.770668Z",
-     "iopub.status.idle": "2026-10-07T02:29:31.201604Z",
-     "shell.execute_reply": "2026-10-07T02:29:31.200262Z"
-    },
-    "papermill": {
-     "duration": 0.443169,
-     "end_time": "2026-10-07T02:29:31.202789",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:30.759620",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -2064,13 +1689,6 @@
    "cell_type": "markdown",
    "id": "section-12-conclusion",
    "metadata": {
-    "papermill": {
-     "duration": 0.009929,
-     "end_time": "2026-10-07T02:29:31.224336",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:31.214407",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2122,13 +1740,6 @@
    "cell_type": "markdown",
    "id": "annexes-header",
    "metadata": {
-    "papermill": {
-     "duration": 0.008608,
-     "end_time": "2026-10-07T02:29:31.241638",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:31.233030",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2141,13 +1752,6 @@
    "cell_type": "markdown",
    "id": "section-1-phase1-recap",
    "metadata": {
-    "papermill": {
-     "duration": 0.01315,
-     "end_time": "2026-10-07T02:29:31.267185",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:31.254035",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2171,19 +1775,6 @@
    "execution_count": 18,
    "id": "phase1-files-list",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:29:31.295146Z",
-     "iopub.status.busy": "2026-10-07T02:29:31.294087Z",
-     "iopub.status.idle": "2026-10-07T02:29:31.966460Z",
-     "shell.execute_reply": "2026-10-07T02:29:31.964844Z"
-    },
-    "papermill": {
-     "duration": 0.688354,
-     "end_time": "2026-10-07T02:29:31.967843",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:31.279489",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -2332,13 +1923,6 @@
    "cell_type": "markdown",
    "id": "section-1b-interp",
    "metadata": {
-    "papermill": {
-     "duration": 0.009828,
-     "end_time": "2026-10-07T02:29:31.986769",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:31.976941",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2353,13 +1937,6 @@
    "cell_type": "markdown",
    "id": "section-4-spartan",
    "metadata": {
-    "papermill": {
-     "duration": 0.012552,
-     "end_time": "2026-10-07T02:29:32.013695",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:32.001143",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2386,13 +1963,6 @@
    "cell_type": "markdown",
    "id": "section-5-hashlife",
    "metadata": {
-    "papermill": {
-     "duration": 0.008853,
-     "end_time": "2026-10-07T02:29:32.034826",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:32.025973",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2433,13 +2003,6 @@
    "cell_type": "markdown",
    "id": "section-9-lean",
    "metadata": {
-    "papermill": {
-     "duration": 0.012602,
-     "end_time": "2026-10-07T02:29:32.058317",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:32.045715",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2542,21 +2105,14 @@
    "cell_type": "markdown",
    "id": "de0111f4",
    "metadata": {
-    "papermill": {
-     "duration": 0.007626,
-     "end_time": "2026-10-07T02:29:32.078058",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:32.070432",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
     "### Annexe E — Pourquoi les piliers ne sont pas dans Lean : la limite des string literals\n",
     "\n",
-    "Le parseur RLE Lean (`parseRLE`) est entierement prouvé et fonctionne parfaitement sur les patterns de taille moderee (glider : population 5, pulsar : population 48, canon de Gosper : population 36). Mais les RLE des **piliers communautaires** sont d'un tout autre ordre de grandeur : l'OTCA Metapixel pese ~70 KB, Gemini plusieurs megaoctets.\n",
+    "Le parseur RLE Lean (`parseRLE`) est entierement prouvé et fonctionne parfaitement sur les patterns de taille moderee (glider : population 5, pulsar : population 48, canon de Gosper : population 36). Mais les RLE des **piliers communautaires** sont d'un tout autre ordre de grandeur : l'OTCA Metapixel pese ~165 Ko, Gemini plusieurs megaoctets.\n",
     "\n",
-    "Un **string literal Lean 4** est pratique pour les patterns jusqu'a ~65 KB environ. Au-dela, le compilateur devient extremement lent ou echoue. C'est pourquoi `Pillars.lean` utilise des placeholders vides (`([] : Grid)`) pour les `Initial` et `Target` des temoins, accompagnes d'un sorry roadmap documentant le plan de chargement futur (fichier externe ou generation de code).\n",
+    "Un **string literal Lean 4** est pratique pour les patterns jusqu'à ~65 KB environ. Au-delà, le compilateur devient extrêmement lent ou échoue. C'est pourquoi `Pillars.lean` a longtemps utilisé des placeholders vides (`([] : Grid)`) pour les `Initial` et `Target` des témoins. Depuis la tranche 2 de #19989, ce mur est franchi pour l'UnitCell : le fichier RLE est embarqué par `include_str` (Lean 4.33) puis parsé par `RLE.parseRLE!` — la grille est réelle (population mesurée : 4 761). OTCA (RLE de ~165 Ko) et Gemini (plusieurs Mo) restent en placeholders en attendant leurs tranches de chargement.\n",
     "\n",
     "La cellule ci-dessous telecharge les 3 RLE et mesure leur taille pour confirmer empiriquement cette limitation. Le parseur Python `parse_rle` (section 3) les traite sans problème et fournit les populations et bounding boxes, servant de **visualisation complementaire** en attendant que le pipeline Lean puisse les accueillir."
    ]
@@ -2566,19 +2122,6 @@
    "execution_count": 19,
    "id": "d8678121",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:29:32.099686Z",
-     "iopub.status.busy": "2026-10-07T02:29:32.099261Z",
-     "iopub.status.idle": "2026-10-07T02:29:33.280088Z",
-     "shell.execute_reply": "2026-10-07T02:29:33.278624Z"
-    },
-    "papermill": {
-     "duration": 1.192497,
-     "end_time": "2026-10-07T02:29:33.281211",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:32.088714",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
@@ -2702,13 +2245,6 @@
    "cell_type": "markdown",
    "id": "annexe-f-header",
    "metadata": {
-    "papermill": {
-     "duration": 0.006217,
-     "end_time": "2026-10-07T02:29:33.294608",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:33.288391",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2722,98 +2258,45 @@
    "execution_count": 20,
    "id": "50dcfe8c",
    "metadata": {
-    "execution": {
-     "iopub.execute_input": "2026-10-07T02:29:33.309749Z",
-     "iopub.status.busy": "2026-10-07T02:29:33.309316Z",
-     "iopub.status.idle": "2026-10-07T02:29:33.324207Z",
-     "shell.execute_reply": "2026-10-07T02:29:33.323030Z"
-    },
-    "papermill": {
-     "duration": 0.023768,
-     "end_time": "2026-10-07T02:29:33.325028",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:33.301260",
-     "status": "completed"
-    },
     "tags": []
    },
    "outputs": [
     {
-     "name": "stdout",
      "output_type": "stream",
-     "text": [
-      "Fichier : Conway/Life/Pillars.lean (246 lignes)\n",
-      "\n",
-      "Import Conway.Life.RLE active : True\n",
-      "\n",
-      "--- Declarations des 4 temoins + temoin RLE prouve ---\n",
-      "  L 87: | `otcametapixel.rle`    | 2058 × 2058  | 165         | `otca_metapixel_witness` |\n",
-      "  L 88: | `p5760unitlifecell.rle`| 499 × 499    | 15          | `unitcell_witness`     |\n",
-      "  L 90: | `gemini.rle`           | énorme       | 5 300       | `gemini_witness`       |\n",
-      "  L116: def otcaInitial : Grid := ([] : Grid)\n",
-      "  L123: def otcaGens : Nat := 35328\n",
-      "  L126: def unitcellInitial : Grid := ([] : Grid)\n",
-      "  L132: def unitcellGens : Nat := 4096\n",
-      "  L135: def geminiInitial : Grid := ([] : Grid)\n",
-      "  L141: def geminiGens : Nat := 33699586\n",
-      "  L144: def cpuInitial : Grid := ([] : Grid)\n",
-      "  L150: def cpuGens : Nat := 1048576\n",
-      "  L164: def pulsarGrid : Grid := RLE.pulsar_parsed\n",
-      "  L168: theorem pulsar_period3 :\n",
-      "  L169:     evolveHashlifeFast 3 pulsarGrid = pulsarGrid := by\n",
-      "  L192: theorem otca_metapixel_witness :\n",
-      "  L193:     evolveHashlifeFastMemo otcaGens otcaInitial = otcaTarget :=\n",
-      "  L194:   evolveHashlifeFastMemo_empty otcaGens\n",
-      "  L207: theorem unitcell_witness :\n",
-      "  L208:     evolveHashlifeFastMemo unitcellGens unitcellInitial = unitcellTarget :=\n",
-      "  L209:   evolveHashlifeFastMemo_empty unitcellGens\n",
-      "  L225: theorem gemini_witness :\n",
-      "  L226:     evolveHashlifeFastMemo geminiGens geminiInitial = geminiTarget :=\n",
-      "  L227:   evolveHashlifeFastMemo_empty geminiGens\n",
-      "  L240: theorem cpu_witness :\n",
-      "  L241:     evolveHashlifeFastMemo cpuGens cpuInitial = cpuTarget :=\n",
-      "  L242:   evolveHashlifeFastMemo_empty cpuGens\n",
-      "\n",
-      "Sorry reels dans Pillars.lean : 0 (les 4 temoins sont prouves trivialement contre grilles vides)\n",
-      "\n",
-      "Temoin RLE prouve (pulsar_period3, via native_decide) : True\n",
-      "  L168: theorem pulsar_period3 :\n",
-      "  L169:     evolveHashlifeFast 3 pulsarGrid = pulsarGrid := by\n",
-      "  L170:   native_decide\n",
-      "\n",
-      "Sorry reels dans HashlifeMemo.lean : 0 (bridge theoremes prouves)\n",
-      "Sorry reels dans HashlifeCorrectness.lean : 2 (P5 = hashlife_correct)\n",
-      "\n",
-      "Total sorry Phase 3 (Pillars + Memo + Correctness) : 2\n",
-      "Les 4 piliers (OTCA/CPU/Gemini/UnitCell) sont PROUVES contre grilles vides ;\n",
-      "leur preuve reelle (pattern RLE charge) attend la memoization Hashlife.\n",
-      "Le seul sorry restant est P5 dans HashlifeCorrectness.lean (theoreme principal).\n",
-      "Le temoin pulsar_period3, prouve par native_decide sur RLE.pulsar_parsed\n",
-      "demontre que le pipeline RLE -> Grid -> evolve fonctionne deja.\n"
-     ]
+     "name": "stdout",
+     "text": "Fichier : Conway/Life/Pillars.lean (316 lignes)\n\nImport Conway.Life.RLE active : True\n\n--- Declarations des temoins + theoremes d'etat UnitCell ---\n  L 49:   de l'archive. Le `unitcellGens := 5760` ci-dessous décrit donc le motif\n  L 60:   `evolveHashlifeFastMemo N unitcellInitial = unitcellInitial` n'a aucune\n  L 67: - **Témoins négatifs appariés** (critère 2 de #19989) : `pulsar_period1_negative`\n  L 68:   et `pulsar_period2_negative` accompagnent `pulsar_period3` — la période vaut\n  L117: | `otcametapixel.rle`    | 2058 × 2058  | 165         | `otca_metapixel_witness` |\n  L118: | `p5760unitlifecell.rle`| 499 × 499    | 15          | `unitcell_initial_population` |\n  L120: | `gemini.rle`           | énorme       | 5 300       | `gemini_witness`       |\n  L147: def otcaInitial : Grid := ([] : Grid)\n  L154: def otcaGens : Nat := 35328\n  L164: def unitcellInitial : Grid := RLE.parseRLE! unitcellRLE\n  L170: def unitcellGens : Nat := 5760\n  L173: def geminiInitial : Grid := ([] : Grid)\n  L179: def geminiGens : Nat := 33699586\n  L182: def cpuInitial : Grid := ([] : Grid)\n  L188: def cpuGens : Nat := 1048576\n  L201: def pulsarGrid : Grid := RLE.pulsar_parsed\n  L205: theorem pulsar_period3 :\n  L206:     evolveHashlifeFast 3 pulsarGrid = pulsarGrid := by\n  L209: /-- **Témoin négatif apparié** de `pulsar_period3` : la période n'est pas 1 —\n  L210:     le Pulsar n'est pas un still life. Sans ce contrôle, `pulsar_period3` seul\n  L212: theorem pulsar_period1_negative :\n  L213:     evolveHashlifeFast 1 pulsarGrid ≠ pulsarGrid := by\n  L218: theorem pulsar_period2_negative :\n  L219:     evolveHashlifeFast 2 pulsarGrid ≠ pulsarGrid := by\n  L242: theorem otca_metapixel_witness :\n  L243:     evolveHashlifeFastMemo otcaGens otcaInitial = otcaTarget :=\n  L244:   evolveHashlifeFastMemo_empty otcaGens\n  L259:     — donc `evolveHashlifeFastMemo N unitcellInitial = unitcellInitial` n'a\n  L270: theorem unitcell_initial_population : unitcellInitial.length = 4761 := by\n  L278: theorem unitcell_initial_nonempty : unitcellInitial ≠ ([] : Grid) := by\n  L295: theorem gemini_witness :\n  L296:     evolveHashlifeFastMemo geminiGens geminiInitial = geminiTarget :=\n  L297:   evolveHashlifeFastMemo_empty geminiGens\n  L310: theorem cpu_witness :\n  L311:     evolveHashlifeFastMemo cpuGens cpuInitial = cpuTarget :=\n  L312:   evolveHashlifeFastMemo_empty cpuGens\n\nSorry reels dans Pillars.lean : 0 (temoins vacuous OU prouves par native_decide : aucun sorry)\n\nTemoin RLE pulsar_period3 : True (L205)\nTemoin RLE pulsar_period1_negative : True (L212)\nTemoin RLE pulsar_period2_negative : True (L218)\n  L205: theorem pulsar_period3 :\n  L206:     evolveHashlifeFast 3 pulsarGrid = pulsarGrid := by\n  L207:   native_decide\n\nEtat UnitCell reel (grille chargee par include_str + RLE.parseRLE!) :\n  unitcell_initial_population : True (unitcellInitial.length = 4761)\n  unitcell_initial_nonempty   : True (la grille n'est pas vide)\n  -> la route evolveHashlifeFastMemo_empty est FERMEE pour ce temoin.\n\nSorry reels dans HashlifeMemo.lean : 0 (bridge theoremes prouves)\nSorry reels dans HashlifeCorrectness.lean : 2 (P5 = hashlife_correct)\n\nTotal sorry Phase 3 (Pillars + Memo + Correctness) : 2\nTemoins encore vacuous (grilles vides) : OTCA, Gemini, CPU.\nL'UnitCell p5760 (David Bell) est charge et son etat initial prouve ;\nson temoin de PERIODE n'est pas exprimable dans ce moteur (systeme ouvert :\nplaneurs emis sur grille sans bord, aucune repetition sur 8 000 generations ;\nperiode 5 760 confirmee SANS bord, tore 500 x 500 : gen 11324 == gen 5564).\nLe seul sorry restant est P5 dans HashlifeCorrectness.lean (theoreme principal).\nLe trio pulsar (periode 3 + negatifs apparies) demontre que le pipeline\nRLE -> Grid -> evolve fonctionne de bout en bout.\n"
     }
    ],
    "source": [
-    "# La source de verite des 3 piliers : Pillars.lean en direct.\n",
+    "# La source de verite des piliers : Pillars.lean en direct.\n",
     "# L'Epic #1647 ne se contente pas de raconter l'histoire des piliers : il les encode\n",
-    "# dans le module Conway.Life.Pillars.lean, avec 4 temoins declares comme théorèmes\n",
-    "# (otca_metapixel_witness, unitcell_witness, gemini_witness, cpu_witness).\n",
-    "# Chaque temoin est PROUVÉ (sans sorry) contre des grilles vides placeholders :\n",
-    "# evolveHashlifeFastMemo N [] = [] est resolu par le lemme evolveHashlifeFastMemo_empty.\n",
-    "# La preuve RÉELLE (pattern RLE charge, native_decide) attend la memoization Hashlife.\n",
-    "# L'import RLE.lean est actif, permettant de charger des patterns RLE directement dans\n",
-    "# les defs. Verifions le fichier et ses declarations cles.\n",
+    "# dans le module Conway.Life.Pillars.lean. Depuis la tranche 2 de #19989, le scaffold\n",
+    "# n'est plus uniforme :\n",
+    "#  - OTCA / Gemini / CPU : temoins vacuous, prouves contre grilles vides par le lemme\n",
+    "#    evolveHashlifeFastMemo_empty (leur chargement RLE attend les tranches suivantes) ;\n",
+    "#  - UnitCell (p5760 de David Bell) : grille REELLE chargee par include_str +\n",
+    "#    RLE.parseRLE! (population mesuree 4 761), theoremes d'etat\n",
+    "#    (unitcell_initial_population, unitcell_initial_nonempty) prouves par native_decide\n",
+    "#    -- la route evolveHashlifeFastMemo_empty est fermee pour ce temoin ;\n",
+    "#  - le pulsar garde pulsar_period3, flanque de ses negatifs apparies\n",
+    "#    pulsar_period1_negative / pulsar_period2_negative (la periode vaut exactement 3).\n",
+    "# Verifions le fichier et ses declarations cles.\n",
     "import re\n",
+    "import sys\n",
+    "from pathlib import Path\n",
+    "\n",
+    "sys.path.insert(0, str(Path.cwd()))\n",
+    "from lean_notebook_utils import find_lean_project  # meme resolution que la cellule setup\n",
     "\n",
     "_SORRY_RE = re.compile(r'^\\s*sorry\\b')  # baseline anti-regression (cf lean-ci-sorry-filter)\n",
     "\n",
     "def real_sorry(path):\n",
-    "    \"\"\"Compte les sorry RÉELS (axiomes implicites), exclut commentaires et prose.\"\"\"\n",
+    "    \"\"\"Compte les sorry REELS (axiomes implicites), exclut commentaires et prose.\"\"\"\n",
     "    if not path.exists():\n",
     "        return -1\n",
     "    return sum(1 for l in path.read_text(encoding='utf-8').splitlines() if _SORRY_RE.match(l))\n",
     "\n",
-    "pillars_path = WIN_LEAN_PROJECT / 'Conway' / 'Life' / 'Pillars.lean'\n",
+    "pillars_path = find_lean_project('conway_lean') / 'Conway' / 'Life' / 'Pillars.lean'\n",
     "assert pillars_path.exists(), f'Pillars.lean non trouve : {pillars_path}'\n",
     "content = pillars_path.read_text(encoding='utf-8')\n",
     "lines = content.splitlines()\n",
@@ -2821,78 +2304,88 @@
     "print(f'Fichier : Conway/Life/Pillars.lean ({len(lines)} lignes)')\n",
     "print()\n",
     "\n",
-    "# Vérifier l'import RLE\n",
+    "# Verifier l'import RLE\n",
     "has_rle_import = any('import Conway.Life.RLE' in l for l in lines)\n",
     "print(f'Import Conway.Life.RLE active : {has_rle_import}')\n",
     "print()\n",
     "\n",
-    "# Extraire les lignes cles : witness defs + gen counts + RLE section\n",
-    "print('--- Declarations des 4 temoins + temoin RLE prouve ---')\n",
+    "# Extraire les lignes cles : defs des grilles + gen counts + theoremes\n",
+    "print(\"--- Declarations des temoins + theoremes d'etat UnitCell ---\")\n",
     "for i, line in enumerate(lines, 1):\n",
     "    stripped = line.strip()\n",
     "    if any(kw in stripped for kw in ['otcaGens', 'unitcellGens', 'geminiGens', 'cpuGens',\n",
     "                                       'otcaInitial', 'unitcellInitial', 'geminiInitial', 'cpuInitial',\n",
-    "                                       'otca_metapixel_witness', 'unitcell_witness',\n",
+    "                                       'otca_metapixel_witness',\n",
     "                                       'gemini_witness', 'cpu_witness',\n",
-    "                                       'pulsarGrid', 'pulsar_period3']):\n",
+    "                                       'unitcell_initial_population', 'unitcell_initial_nonempty',\n",
+    "                                       'pulsarGrid', 'pulsar_period3',\n",
+    "                                       'pulsar_period1_negative', 'pulsar_period2_negative']):\n",
     "        print(f'  L{i:>3d}: {line.rstrip()[:100]}')\n",
     "\n",
     "print()\n",
-    "# Compter les sorry RÉELS dans Pillars.lean (regex baseline, exclut commentaires/prose)\n",
+    "# Compter les sorry REELS dans Pillars.lean (regex baseline, exclut commentaires/prose)\n",
     "n_pillars_sorry = real_sorry(pillars_path)\n",
     "print(f'Sorry reels dans Pillars.lean : {n_pillars_sorry} '\n",
-    "      f'(les 4 temoins sont prouves trivialement contre grilles vides)')\n",
+    "      f'(temoins vacuous OU prouves par native_decide : aucun sorry)')\n",
     "print()\n",
     "\n",
-    "# Vérifier la theorem RLE prouvée\n",
-    "has_pulsar = 'pulsar_period3' in content\n",
-    "print(f'Temoin RLE prouve (pulsar_period3, via native_decide) : {has_pulsar}')\n",
-    "if has_pulsar:\n",
+    "# Verifier le trio pulsar (periode exacte 3 + negatifs apparies)\n",
+    "for name in ('pulsar_period3', 'pulsar_period1_negative', 'pulsar_period2_negative'):\n",
+    "    hit = next((i for i, l in enumerate(lines, 1)\n",
+    "                if l.strip().startswith('theorem') and name in l), None)\n",
+    "    print(f'Temoin RLE {name} : {hit is not None}' + (f' (L{hit})' if hit else ''))\n",
+    "if 'pulsar_period3' in content:\n",
     "    for i, line in enumerate(lines, 1):\n",
-    "        if 'pulsar_period3' in line:\n",
+    "        if line.strip().startswith('theorem') and 'pulsar_period3' in line:\n",
     "            print(f'  L{i:>3d}: {line.rstrip()[:100]}')\n",
     "            if i < len(lines):\n",
     "                print(f'  L{i+1:>3d}: {lines[i].rstrip()[:100]}')\n",
-    "                if i+1 < len(lines):\n",
+    "                if i + 1 < len(lines):\n",
     "                    print(f'  L{i+2:>3d}: {lines[i+1].rstrip()[:100]}')\n",
+    "            break\n",
     "\n",
     "print()\n",
-    "# Compter les sorry réels dans les modules Phase 3b/3c (source de verite live)\n",
-    "memo_path = WIN_LEAN_PROJECT / 'Conway' / 'Life' / 'HashlifeMemo.lean'\n",
+    "# L'etat UnitCell : grille REELLE chargee (tranche 2 de #19989)\n",
+    "uc_pop = 'unitcell_initial_population' in content\n",
+    "uc_ne = 'unitcell_initial_nonempty' in content\n",
+    "print('Etat UnitCell reel (grille chargee par include_str + RLE.parseRLE!) :')\n",
+    "print(f'  unitcell_initial_population : {uc_pop} (unitcellInitial.length = 4761)')\n",
+    "print(f\"  unitcell_initial_nonempty   : {uc_ne} (la grille n'est pas vide)\")\n",
+    "print('  -> la route evolveHashlifeFastMemo_empty est FERMEE pour ce temoin.')\n",
+    "print()\n",
+    "\n",
+    "# Compter les sorry reels dans les modules Phase 3b/3c (source de verite live)\n",
+    "memo_path = pillars_path.parent / 'HashlifeMemo.lean'\n",
     "n_memo_sorry = real_sorry(memo_path)\n",
     "print(f'Sorry reels dans HashlifeMemo.lean : {n_memo_sorry} (bridge theoremes prouves)')\n",
     "\n",
-    "corr_path = WIN_LEAN_PROJECT / 'Conway' / 'Life' / 'HashlifeCorrectness.lean'\n",
+    "corr_path = pillars_path.parent / 'HashlifeCorrectness.lean'\n",
     "n_corr_sorry = real_sorry(corr_path)\n",
     "print(f'Sorry reels dans HashlifeCorrectness.lean : {n_corr_sorry} (P5 = hashlife_correct)')\n",
     "\n",
     "total_phase3 = n_pillars_sorry + n_memo_sorry + n_corr_sorry\n",
     "print()\n",
     "print(f'Total sorry Phase 3 (Pillars + Memo + Correctness) : {total_phase3}')\n",
-    "print('Les 4 piliers (OTCA/CPU/Gemini/UnitCell) sont PROUVES contre grilles vides ;')\n",
-    "print('leur preuve reelle (pattern RLE charge) attend la memoization Hashlife.')\n",
+    "print('Temoins encore vacuous (grilles vides) : OTCA, Gemini, CPU.')\n",
+    "print(\"L'UnitCell p5760 (David Bell) est charge et son etat initial prouve ;\")\n",
+    "print(\"son temoin de PERIODE n'est pas exprimable dans ce moteur (systeme ouvert :\")\n",
+    "print('planeurs emis sur grille sans bord, aucune repetition sur 8 000 generations ;')\n",
+    "print('periode 5 760 confirmee SANS bord, tore 500 x 500 : gen 11324 == gen 5564).')\n",
     "print('Le seul sorry restant est P5 dans HashlifeCorrectness.lean (theoreme principal).')\n",
-    "print('Le temoin pulsar_period3, prouve par native_decide sur RLE.pulsar_parsed')\n",
-    "print('demontre que le pipeline RLE -> Grid -> evolve fonctionne deja.')\n"
+    "print('Le trio pulsar (periode 3 + negatifs apparies) demontre que le pipeline')\n",
+    "print('RLE -> Grid -> evolve fonctionne de bout en bout.')\n"
    ]
   },
   {
    "cell_type": "markdown",
    "id": "de4e4b3a",
    "metadata": {
-    "papermill": {
-     "duration": 0.008924,
-     "end_time": "2026-10-07T02:29:33.340936",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:33.332012",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
     "### Interpretation : le scaffold Lean des piliers (sans sorry)\n",
     "\n",
-    "Le fichier `Pillars.lean` encode les temoins communautaires comme des **théorèmes prouves** (sans sorry). L'import `Conway.Life.RLE` est actif, et un **temoin prouve non trivial** (`pulsar_period3`) démontre que le pipeline RLE -> Grid -> evolve fonctionne de bout en bout sur un vrai pattern.\n",
+    "Le fichier `Pillars.lean` encode les témoins communautaires comme des **théorèmes prouvés** (sans sorry). L'import `Conway.Life.RLE` est actif, et des **témoins prouvés non triviaux** (`pulsar_period3` et ses négatifs appariés, puis l'état initial réel de l'UnitCell depuis la tranche 2 de #19989) démontrent que le pipeline RLE -> Grid -> evolve fonctionne de bout en bout sur de vrais patterns.\n",
     "\n",
     "Structure de chaque temoin :\n",
     "\n",
@@ -2906,20 +2399,20 @@
     "  evolveHashlifeFastMemo_empty otcaGens    -- prouve : evolveHashlifeFastMemo N [] = []\n",
     "```\n",
     "\n",
-    "Les `Initial` et `Target` sont des grilles vides (`[]`) : comme `otcaInitial = otcaTarget = []`, le théorème se reduit a `evolveHashlifeFastMemo N [] = []`, resolu par le lemme `evolveHashlifeFastMemo_empty`. **Aucun `sorry`, aucun axiome admis** - le module compile sans sorry. Les RLE réels (OTCA = 70 KB, Gemini = plusieurs MB) depassent la taille maximale d'un string literal Lean ; leur chargement via un mécanisme de fichier externe est l'étape qui transformera cette preuve triviale en preuve réelle.\n",
+    "Les `Initial` et `Target` **d'OTCA, Gemini et CPU** sont des grilles vides (`[]`) : comme `otcaInitial = otcaTarget = []`, le théorème se réduit à `evolveHashlifeFastMemo N [] = []`, résolu par le lemme `evolveHashlifeFastMemo_empty`. **Aucun `sorry`, aucun axiome admis** - le module compile sans sorry. L'UnitCell suit désormais l'autre chemin : `unitcellInitial := RLE.parseRLE! unitcellRLE` (grille réelle), théorèmes d'état prouvés par `native_decide` sur cette grille. Les RLE géants (OTCA ~165 Ko, Gemini plusieurs Mo) dépassent la taille maximale d'un string literal Lean ; leur chargement est l'étape qui transformera les preuves triviales restantes en preuves réelles.\n",
     "\n",
-    "#### Les temoins : prouves contre grilles vides\n",
+    "#### Les témoins : trois vacuous, un réel\n",
     "\n",
     "| Temoin | Generations | Niveau quadtree (estimé) | Roadmap Phase | Ce que la preuve réelle etablira |\n",
     "|--------|-------------|--------------------------|---------------|-----------------------------------|\n",
     "| `otca_metapixel_witness` | 35 328 | ~9 | Phase 7 | Life emule Life (1 OTCA-tick = 1 generation macro) |\n",
-    "| `unitcell_witness` | 4 096 | ~7 | Phase 8 | Metapixel compact (Beluchenko 2011) |\n",
+    "| `unitcell_initial_population` / `unitcell_initial_nonempty` | 5 760 | ~7 | Phase 8 | Période p5760 (Bell) — état initial **déjà prouvé** sur grille réelle (tranche 2 #19989) |\n",
     "| `gemini_witness` | 33 699 586 | ~14 | Phase 6 | Auto-replication oblique (knightship) |\n",
     "| `cpu_witness` | 1 048 576 | ~12 | Phase 8 | CPU digital programmable (Beluchenko/Stearns 2016) |\n",
     "\n",
-    "> **Statut compile vs statut mathematique.** Les théorèmes sont *syntaxiquement prouves* (sans sorry, pas d'axiome) parce qu'ils portent sur des grilles vides. La **preuve substantielle** - le pattern RLE réel charge puis pousse dans `native_decide` - reste l'objectif des Phases 6-8. Le notebook distingue donc soigneusement « compile sans sorry » de « preuve du pattern réel ».\n",
+    "> **Statut compile vs statut mathématique.** Les théorèmes OTCA / Gemini / CPU sont *syntaxiquement prouvés* (sans sorry, pas d'axiome) parce qu'ils portent sur des grilles vides. La **preuve substantielle** — le pattern RLE réel chargé puis poussé dans `native_decide` — reste l'objectif des Phases 6-8 pour eux. L'UnitCell a franchi ce pas pour son **état initial** (grille réelle chargée, population prouvée) ; son témoin de **période** n'est pas exprimable dans ce moteur (système ouvert : le motif émet des planeurs sur grille sans bord). Le notebook distingue donc soigneusement « compile sans sorry » de « preuve du pattern réel ».\n",
     "\n",
-    "#### Le temoin prouve non trivial : `pulsar_period3`\n",
+    "#### Les témoins prouvés non triviaux : `pulsar_period3` et l'état UnitCell\n",
     "\n",
     "Le pipeline est déjà valide sur un pattern réel de taille moderee :\n",
     "\n",
@@ -2929,31 +2422,24 @@
     "  native_decide\n",
     "```\n",
     "\n",
-    "Ce théorème utilise `RLE.pulsar_parsed` (pattern réel, non vide) et prouve la periodicite du pulsar par `native_decide`. Contrairement aux 4 piliers (grilles vides), `pulsar_period3` porte sur un **vrai pattern** : il constitue la **preuve de concept** que le pipeline RLE -> Grid -> evolveHashlifeFast fonctionne de bout en bout sur données réelles.\n",
+    "Ce théorème utilise `RLE.pulsar_parsed` (pattern réel, non vide) et prouve la périodicité du pulsar par `native_decide`, flanqué depuis la tranche 2 de #19989 de ses négatifs appariés `pulsar_period1_negative` / `pulsar_period2_negative` (la période vaut exactement 3, pas un diviseur). Les théorèmes `unitcell_initial_population` / `unitcell_initial_nonempty` portent eux aussi sur un **vrai pattern** (population 4 761) : contrairement aux trois piliers restés sur grilles vides, ils établissent un fait sur donnée réelle.\n",
     "\n",
     "#### Roadmap : des preuves triviales aux preuves réelles\n",
     "\n",
     "| Étape | Module | Description | Statut |\n",
     "|-------|--------|-------------|--------|\n",
     "| 1 | `HashlifeMemo.lean` | Memoization operationnelle (`hashlifeResultMemo`) | API posee, sans sorry (bridge théorèmes prouves) |\n",
-    "| 2 | `Pillars.lean` | Chargement RLE réels dans `Initial`/`Target` | sans sorry (placeholders vides) ; RLE réels en attente (fichiers trop grands pour string literal) |\n",
+    "| 2 | `Pillars.lean` | Chargement RLE réels dans `Initial`/`Target` | **UnitCell chargé** (`include_str`, tranche 2 #19989) ; OTCA (~165 Ko) en attente ; Gemini/CPU fichiers absents de l'archive |\n",
     "| 3 | `HashlifeCorrectness.lean` | Théorème central P4 (`hashlifeResultAux_correct`) | P4 PROUVE ; P5 (`hashlife_correct`) reste en sorry |\n",
     "| 4 | Chaque temoin | `by native_decide` sur le pattern réel | En attente des étapes 1-3 |\n",
     "\n",
-    "Le chemin vers les preuves réelles est donc : **HashlifeMemo operationnel -> chargement RLE -> native_decide -> temoin prouve sur pattern réel**. Le temoin pulsar confirme que l'infrastructure RLE -> Grid est prete ; il reste a rendre la memoization tractable pour les patterns geants.\n"
+    "Le chemin vers les preuves réelles est donc : **HashlifeMemo opérationnel -> chargement RLE -> native_decide -> témoin prouvé sur pattern réel**. Le témoin pulsar et l'état UnitCell confirment que l'infrastructure RLE -> Grid est prête ; il reste à rendre la mémoization tractable pour les patterns géants.\n"
    ]
   },
   {
    "cell_type": "markdown",
    "id": "section-11-roadmap",
    "metadata": {
-    "papermill": {
-     "duration": 0.011257,
-     "end_time": "2026-10-07T02:29:33.362245",
-     "exception": false,
-     "start_time": "2026-10-07T02:29:33.350988",
-     "status": "completed"
-    },
     "tags": []
    },
    "source": [
@@ -2969,11 +2455,11 @@
     "| **Phase 2** | `Life/RLE.lean` | Parser RLE + chargement de patterns communautaires | **FAIT** |\n",
     "| **Phase 3a** | `Life/MacroCell.lean` | Encodage quadtree arborescent | **FAIT** |\n",
     "| **Phase 3b** | `Life/Hashlife.lean` + `Life/HashlifeCorrectness.lean` | Step récursif + correction light-cone | **sorry restant** (P5 `hashlife_correct`). P1 ferme par PR #2173, P2/P3 par PRs #2097/#2107, **P4 PROUVE** |\n",
-    "| **Phase 3c** | `Life/HashlifeMemo.lean` + `Life/Pillars.lean` | Memoization + temoins communautaires | **SCAFFOLD POSE - sans sorry** (temoins prouves contre grilles vides) |\n",
+    "| **Phase 3c** | `Life/HashlifeMemo.lean` + `Life/Pillars.lean` | Memoization + témoins communautaires | **SCAFFOLD POSE - sans sorry** (OTCA/Gemini/CPU vacuous ; **UnitCell réel**, tranche 2 #19989) |\n",
     "| Phase 4 | `Life/Omniperiodic.lean` | $\\forall n \\le 64, \\exists P, \\text{period}(P) = n$ | A venir |\n",
     "| Phase 6 | (théorème `gemini_witness` dans Pillars) | Gemini self-replication (33M gen) | Phase 3c dépendance |\n",
     "| Phase 7 | (théorème `otca_metapixel_witness` dans Pillars) | OTCA self-emulation (35K gen) | Phase 3c dépendance |\n",
-    "| Phase 8 | (théorème `unitcell_witness` + `cpu_witness` dans Pillars) | UnitCell 4096 gen + Digital CPU 1M gen | Phase 3c dépendance |\n",
+    "| Phase 8 | (théorèmes `unitcell_initial_*` + `cpu_witness` dans Pillars) | UnitCell p5760 (état initial prouvé, période non exprimable) + Digital CPU 1M gen | Phase 3c dépendance |\n",
     "| Phase 9 | `Life/LogicGates.lean` | NAND gate + axiome Turing-completude | A venir |\n",
     "\n",
     "#### Phase 3b - le sorry restant (P5, théorème principal)\n",
@@ -2995,15 +2481,15 @@
     "1. **`MacroCellId` + `MemoCache`** : identifiant content-addresse + `Std.HashMap MacroCellId MacroCell` pour le cache de hash-consing.\n",
     "2. **`hashlifeResultMemo : MacroCell -> StateM MemoCache MacroCell`** : version memoisee de `hashlifeResultAux`. Théorème bridge `hashlifeResultMemo_correct` **prouve** (extraction d'un lemme auxiliaire valide `cacheOK_empty`, sans sorry).\n",
     "3. **`evolveHashlifeFastMemo`** : entrée top-level pour le chemin rapide memoise. Théorème `evolveHashlifeFastMemo_eq_evolveHashlifeFast` **prouve** (même mécanisme, sans sorry).\n",
-    "4. **Des théorèmes-temoins** dans `Pillars.lean` - tous **prouves** via le lemme `evolveHashlifeFastMemo_empty` contre grilles vides :\n",
+    "4. **Des théorèmes-témoins** dans `Pillars.lean` — OTCA/Gemini/CPU **prouvés** via le lemme `evolveHashlifeFastMemo_empty` contre grilles vides ; l'UnitCell **prouvé sur grille réelle** (tranche 2 de #19989) :\n",
     "   - `otca_metapixel_witness` (35 328 gen)\n",
-    "   - `unitcell_witness` (4 096 gen)\n",
+    "   - `unitcell_initial_population` / `unitcell_initial_nonempty` (5 760 gen, grille réelle p5760 — *native_decide*, pas `evolveHashlifeFastMemo_empty`)\n",
     "   - `gemini_witness` (33 699 586 gen)\n",
     "   - `cpu_witness` (1 048 576 gen)\n",
     "\n",
-    "   Chaque preuve est *trivialement vraie* (grilles vides : `evolveHashlifeFastMemo N [] = []`). La preuve **réelle** - pattern RLE charge, `by native_decide` - est l'objectif des Phases 6-8 une fois la memoization operationnelle.\n",
+    "   Chaque preuve OTCA/Gemini/CPU est *trivialement vraie* (grilles vides : `evolveHashlifeFastMemo N [] = []`). La preuve **réelle** — pattern RLE chargé, `by native_decide` — est l'objectif des Phases 6-8 ; l'UnitCell l'a déjà franchie pour son état initial.\n",
     "\n",
-    "> **Preuve triviale mais sans sorry.** Les temoins compilent sans sorry parce qu'ils portent sur des grilles vides. Aucun axiome n'est admis (le module est coherent), mais la preuve substantielle du pattern réel reste a faire. A contraster avec `pulsar_period3` (section 6.2), seul temoin prouve sur un **vrai** pattern.\n",
+    "> **Preuve triviale mais sans sorry.** Les témoins OTCA/Gemini/CPU compilent sans sorry parce qu'ils portent sur des grilles vides. Aucun axiome n'est admis (le module est cohérent), mais la preuve substantielle du pattern réel reste à faire. A contraster avec `pulsar_period3` et les théorèmes d'état de l'UnitCell (tranche 2 de #19989), témoins prouvés sur un **vrai** pattern.\n",
     "\n",
     "**Total des sorries Lean Life** : P5 (`hashlife_correct` dans `HashlifeCorrectness`) reste en sorry sur les modules `Conway.Life.*`. Les modules fondamentaux (Life + Spaceships + Oscillators) et tout le scaffold Phase 3c (HashlifeMemo + Pillars) sont **sans sorry**.\n",
     "\n",
@@ -3039,18 +2525,6 @@
    "nbconvert_exporter": "python",
    "pygments_lexer": "ipython3",
    "version": "3.13.13"
-  },
-  "papermill": {
-   "default_parameters": {},
-   "duration": 798.691312,
-   "end_time": "2026-10-07T02:29:33.829564",
-   "environment_variables": {},
-   "exception": null,
-   "input_path": "MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16b-Conway-Game-of-Life-Lean.ipynb",
-   "output_path": "Lean-16b-Conway-Game-of-Life-Lean.ipynb",
-   "parameters": {},
-   "start_time": "2026-10-07T02:16:15.138252",
-   "version": "2.6.0"
   }
  },
  "nbformat": 4,