diff --git a/.github/workflows/lean-search.yml b/.github/workflows/lean-search.yml index aa7490df3b..b80cb4a115 100644 --- a/.github/workflows/lean-search.yml +++ b/.github/workflows/lean-search.yml @@ -2,7 +2,7 @@ name: Lean CI (search_lean) # CI for search_lean (Search/search_lean) — A* optimality lake at the Search series # root. Formalizes the landmark theorems of A* (Hart, Nilsson & Raphael, 1968): -# phase-1 `admissible_implies_optimal` (PR #4090), phase-2 +# phase-1 `admissible_le_suffix_cost` (anciennement `admissible_implies_optimal`, PR #4090), phase-2 # `consistent_implies_admissible` (téléscopage). See #4048, roadmap #4038, # registry #3801 (prong B « problème non-trivial » — répond au grief BFS-vs-A* # dégénéré sur graphe à coût uniforme). diff --git a/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md b/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md index a78c8a65a1..254b1b67f4 100644 --- a/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md +++ b/MyIA.AI.Notebooks/Search/LEAN_INVENTORY.md @@ -48,14 +48,16 @@ CP-SAT en oracle exact. Pas encore câblé. #### Théorèmes prouvés (0 sorry) -- **`admissible_implies_optimal`** (flagship, phase-2) : A* sous heuristique admissible - renvoie un chemin de coût optimal. +- **`admissible_le_suffix_cost`** (flagship, phase-1, anciennement `admissible_implies_optimal`) : + borne en `f` — sous heuristique admissible, `h(nœud)` ne dépasse jamais le coût du + suffixe restant du chemin allant au but (le cœur de l'argument d'optimalité de A*, + pas la garantie « chemin optimal renvoyé », cf #14824). - **`consistent_implies_path_bound`** / **`consistent_implies_admissible_bound`** (phase-2) : consistance ⟹ admissibilité par téléscopage. - **`consistent_implies_f_monotone`** (phase-3) : consistance ⟹ la fonction d'évaluation `f = g + h` est non-décroissante (pas de re-expansion de nœuds). -- `admissible_implies_optimal_start` (cas de base), `admissible_head_bound` (borne sur le - nœud de tête), lemmes de support sur `head?`/`getLast?`. +- `admissible_head_bound` (borne en `f` au départ), `suffix_pathFrom` (un suffixe + d'un chemin allant au but va encore au but), lemmes de support sur `head?`/`getLast?`. #### Honnêteté du périmètre (G.3/G.9) diff --git a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb index 9d0dddd6b6..f78caef317 100644 --- a/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb +++ b/MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb @@ -5,10 +5,10 @@ "id": "153addc9", "metadata": { "papermill": { - "duration": 0.008001, - "end_time": "2026-07-03T08:50:40.387667", + "duration": 0.002598, + "end_time": "2026-09-09T01:16:28.362776", "exception": false, - "start_time": "2026-07-03T08:50:40.379666", + "start_time": "2026-09-09T01:16:28.360178", "status": "completed" }, "tags": [] @@ -39,10 +39,10 @@ "id": "54d2b874", "metadata": { "papermill": { - "duration": 0.006001, - "end_time": "2026-07-03T08:50:40.398914", + "duration": 0.001959, + "end_time": "2026-09-09T01:16:28.367238", "exception": false, - "start_time": "2026-07-03T08:50:40.392913", + "start_time": "2026-09-09T01:16:28.365279", "status": "completed" }, "tags": [] @@ -82,16 +82,16 @@ "id": "06366578", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:09:39.099212Z", - "iopub.status.busy": "2026-07-08T19:09:39.099212Z", - "iopub.status.idle": "2026-07-08T19:09:39.116843Z", - "shell.execute_reply": "2026-07-08T19:09:39.116843Z" + "iopub.execute_input": "2026-09-09T01:16:28.372944Z", + "iopub.status.busy": "2026-09-09T01:16:28.372375Z", + "iopub.status.idle": "2026-09-09T01:16:28.399700Z", + "shell.execute_reply": "2026-09-09T01:16:28.399300Z" }, "papermill": { - "duration": 0.038195, - "end_time": "2026-07-03T08:50:40.443109", + "duration": 0.031121, + "end_time": "2026-09-09T01:16:28.400460", "exception": false, - "start_time": "2026-07-03T08:50:40.404914", + "start_time": "2026-09-09T01:16:28.369339", "status": "completed" }, "tags": [] @@ -227,7 +227,11 @@ " print(f'--- fin ({total} lignes) ---')\n", "\n", "def run_lake_build(targets='Astar', timeout=1500):\n", - " \"\"\"Construit le lake search_lean.\"\"\"\n", + " \"\"\"Construit le lake search_lean (invocation reelle, natif ou WSL).\n", + " Aucun court-circuit local : la fonction tente toujours le backend\n", + " disponible -- un build qui doit etre evite se decide a l'appelant\n", + " (arret explicite), pas par une heuristique de repertoire.\n", + " \"\"\"\n", " if USE_NATIVE_LEAN:\n", " try:\n", " r = subprocess.run(['lake', 'build', targets], cwd=WIN_LEAN_PROJECT,\n", @@ -278,16 +282,16 @@ "id": "c8f96298", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:09:39.118853Z", - "iopub.status.busy": "2026-07-08T19:09:39.117854Z", - "iopub.status.idle": "2026-07-08T19:09:39.123111Z", - "shell.execute_reply": "2026-07-08T19:09:39.123111Z" + "iopub.execute_input": "2026-09-09T01:16:28.405320Z", + "iopub.status.busy": "2026-09-09T01:16:28.405151Z", + "iopub.status.idle": "2026-09-09T01:16:28.432926Z", + "shell.execute_reply": "2026-09-09T01:16:28.432361Z" }, "papermill": { - "duration": 0.014581, - "end_time": "2026-07-03T08:50:40.463691", + "duration": 0.031258, + "end_time": "2026-09-09T01:16:28.433930", "exception": false, - "start_time": "2026-07-03T08:50:40.449110", + "start_time": "2026-09-09T01:16:28.402672", "status": "completed" }, "tags": [] @@ -328,16 +332,16 @@ "id": "4d0b1a42", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:09:39.124126Z", - "iopub.status.busy": "2026-07-08T19:09:39.124126Z", - "iopub.status.idle": "2026-07-08T19:13:38.831433Z", - "shell.execute_reply": "2026-07-08T19:13:38.831433Z" + "iopub.execute_input": "2026-09-09T01:16:28.439452Z", + "iopub.status.busy": "2026-09-09T01:16:28.439249Z", + "iopub.status.idle": "2026-09-09T01:16:28.443022Z", + "shell.execute_reply": "2026-09-09T01:16:28.442653Z" }, "papermill": { - "duration": 411.977126, - "end_time": "2026-07-03T08:57:32.446817", + "duration": 0.007522, + "end_time": "2026-09-09T01:16:28.443725", "exception": false, - "start_time": "2026-07-03T08:50:40.469691", + "start_time": "2026-09-09T01:16:28.436203", "status": "completed" }, "tags": [] @@ -347,33 +351,49 @@ "name": "stdout", "output_type": "stream", "text": [ - "lake build Astar -> exit=0 : SUCCESS, preuves compilees, 0 sorry verifie par build.\n", - "dev/CoursIA/MyIA.AI.Notebooks/Search/search_lean/.lake/packages/aesop' has local changes\n", - "warning: Qq: repository '/mnt/c/dev/CoursIA/MyIA.AI.Notebooks/Search/search_lean/.lake/packages/Qq' has local changes\n", - "warning: batteries: repository '/mnt/c/dev/CoursIA/MyIA.AI.Notebooks/Search/search_lean/.lake/packages/batteries' has local changes\n", - "warning: Cli: repository '/mnt/c/dev/CoursIA/MyIA.AI.Notebooks/Search/search_lean/.lake/packages/Cli' has local changes\n", - "Build completed successfully (8501 jobs).\n" + "lake build Astar : NON EXECUTE sur cette machine -- arret user 2026-08-30\n", + "(plus aucun build lake/lean ni commande WSL sur po-2023 jusqu'a re-autorisation explicite).\n", + "\n", + "La verification statique ci-dessus (regex sur les sources) confirme deja 0 sorry.\n", + "Pour valider par compilation, re-executer ce notebook sur une machine autorisee\n", + "avec LEAN_BUILD_ALLOWED_HERE = True, ou lancer l'equivalent :\n", + " wsl -d Ubuntu -- bash -lc \"cd && lake build Astar\"\n" ] } ], "source": [ "# Build du lake (confirme que les preuves compilent reellement).\n", "# run_lake_build capture le VRAI exit code de lake (pas celui de `tail`, qui\n", - "# masquerait un echec). Astuce : le build complet d'Astar importe Mathlib et\n", - "# requiert les oleans Mathlib ; s'ils manquent, on le signale honnetement et on\n", - "# imprime la commande manuelle (convention Lean-15).\n", - "rc, out, err = run_lake_build('Astar', timeout=600)\n", - "if rc == 0:\n", - " print(f\"lake build Astar -> exit={rc} : SUCCESS, preuves compilees, 0 sorry verifie par build.\")\n", - " if out.strip():\n", - " print(out.strip()[-500:])\n", - "else:\n", - " print(f\"lake build Astar -> exit={rc} : build non complete sur cette machine\")\n", - " print(\"(oles Mathlib manquants : `lake exe cache get` ne repond pas ici).\")\n", + "# masquerait un echec) : invocation reelle du backend natif ou WSL, sans\n", + "# court-circuit.\n", + "#\n", + "# Arret humain explicite sur la lane qui produit ces sorties (user, 2026-08-30) :\n", + "# plus AUCUN process lean ni commande WSL sur po-2023 jusqu'a re-autorisation\n", + "# (la VM WSL partagee a crash plusieurs fois en emportant Docker et les sessions).\n", + "# Le blocage est conservé et affiché tel quel -- il n'est PAS contourné : la\n", + "# compilation attend une machine autorisee (re-executer avec le drapeau a True).\n", + "LEAN_BUILD_ALLOWED_HERE = False\n", + "\n", + "if not LEAN_BUILD_ALLOWED_HERE:\n", + " print(\"lake build Astar : NON EXECUTE sur cette machine -- arret user 2026-08-30\")\n", + " print(\"(plus aucun build lake/lean ni commande WSL sur po-2023 jusqu'a re-autorisation explicite).\")\n", " print()\n", " print(\"La verification statique ci-dessus (regex sur les sources) confirme deja 0 sorry.\")\n", - " print(\"Pour valider par compilation, lancer sur une machine avec l'env Lean/WSL complet :\")\n", - " print(f' wsl -d Ubuntu -- bash -lc \"cd && lake exe cache get && lake build Astar\"')\n" + " print(\"Pour valider par compilation, re-executer ce notebook sur une machine autorisee\")\n", + " print(\"avec LEAN_BUILD_ALLOWED_HERE = True, ou lancer l'equivalent :\")\n", + " print(' wsl -d Ubuntu -- bash -lc \"cd && lake build Astar\"')\n", + "else:\n", + " rc, out, err = run_lake_build('Astar', timeout=600)\n", + " if rc == 0:\n", + " print(f\"lake build Astar -> exit={rc} : SUCCESS, preuves compilees, 0 sorry verifie par build.\")\n", + " if out.strip():\n", + " print(out.strip()[-500:])\n", + " else:\n", + " print(f\"lake build Astar -> exit={rc} : ECHEC -- sortie ci-dessous.\")\n", + " if out.strip():\n", + " print(out.strip()[-500:])\n", + " if err.strip():\n", + " print(err.strip()[-300:])\n" ] }, { @@ -381,10 +401,10 @@ "id": "ad0e26ad", "metadata": { "papermill": { - "duration": 0.005, - "end_time": "2026-07-03T08:57:32.456816", + "duration": 0.002216, + "end_time": "2026-09-09T01:16:28.448184", "exception": false, - "start_time": "2026-07-03T08:57:32.451816", + "start_time": "2026-09-09T01:16:28.445968", "status": "completed" }, "tags": [] @@ -409,16 +429,16 @@ "id": "a1b07c38", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.831433Z", - "iopub.status.busy": "2026-07-08T19:13:38.831433Z", - "iopub.status.idle": "2026-07-08T19:13:38.837694Z", - "shell.execute_reply": "2026-07-08T19:13:38.837694Z" + "iopub.execute_input": "2026-09-09T01:16:28.454230Z", + "iopub.status.busy": "2026-09-09T01:16:28.454021Z", + "iopub.status.idle": "2026-09-09T01:16:28.457971Z", + "shell.execute_reply": "2026-09-09T01:16:28.457521Z" }, "papermill": { - "duration": 0.015872, - "end_time": "2026-07-03T08:57:32.477695", + "duration": 0.008088, + "end_time": "2026-09-09T01:16:28.458764", "exception": false, - "start_time": "2026-07-03T08:57:32.461823", + "start_time": "2026-09-09T01:16:28.450676", "status": "completed" }, "tags": [] @@ -496,10 +516,10 @@ "id": "d1a30e36", "metadata": { "papermill": { - "duration": 0.005999, - "end_time": "2026-07-03T08:57:32.489700", + "duration": 0.002244, + "end_time": "2026-09-09T01:16:28.463340", "exception": false, - "start_time": "2026-07-03T08:57:32.483701", + "start_time": "2026-09-09T01:16:28.461096", "status": "completed" }, "tags": [] @@ -531,10 +551,10 @@ "id": "726d522b", "metadata": { "papermill": { - "duration": 0.005001, - "end_time": "2026-07-03T08:57:32.499704", + "duration": 0.002216, + "end_time": "2026-09-09T01:16:28.467857", "exception": false, - "start_time": "2026-07-03T08:57:32.494703", + "start_time": "2026-09-09T01:16:28.465641", "status": "completed" }, "tags": [] @@ -568,16 +588,16 @@ "id": "0f97f3e5", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.837694Z", - "iopub.status.busy": "2026-07-08T19:13:38.837694Z", - "iopub.status.idle": "2026-07-08T19:13:38.842822Z", - "shell.execute_reply": "2026-07-08T19:13:38.842822Z" + "iopub.execute_input": "2026-09-09T01:16:28.473456Z", + "iopub.status.busy": "2026-09-09T01:16:28.473239Z", + "iopub.status.idle": "2026-09-09T01:16:28.477405Z", + "shell.execute_reply": "2026-09-09T01:16:28.477051Z" }, "papermill": { - "duration": 0.013672, - "end_time": "2026-07-03T08:57:32.516374", + "duration": 0.007737, + "end_time": "2026-09-09T01:16:28.478144", "exception": false, - "start_time": "2026-07-03T08:57:32.502702", + "start_time": "2026-09-09T01:16:28.470407", "status": "completed" }, "tags": [] @@ -681,10 +701,10 @@ "id": "85e7c5cf", "metadata": { "papermill": { - "duration": 0.005487, - "end_time": "2026-07-03T08:57:32.526861", + "duration": 0.004696, + "end_time": "2026-09-09T01:16:28.485260", "exception": false, - "start_time": "2026-07-03T08:57:32.521374", + "start_time": "2026-09-09T01:16:28.480564", "status": "completed" }, "tags": [] @@ -715,10 +735,10 @@ "id": "c942eb65", "metadata": { "papermill": { - "duration": 0.005007, - "end_time": "2026-07-03T08:57:32.536875", + "duration": 0.002216, + "end_time": "2026-09-09T01:16:28.489927", "exception": false, - "start_time": "2026-07-03T08:57:32.531868", + "start_time": "2026-09-09T01:16:28.487711", "status": "completed" }, "tags": [] @@ -729,7 +749,8 @@ "C'est le cœur mathématique de l'optimalité de A\\*. On garde `hStar` abstrait — un\n", "« vrai coût optimal restant » satisfaisant la propriété de **borne inférieure**\n", "`IsTrueRemainingCost` (pour un graphe fini, `hStar` = minimum des coûts des chemins\n", - "simples vers le but). Le théorème phare `admissible_implies_optimal` énonce la\n", + "simples vers le but). Le théorème phare `admissible_le_suffix_cost` (anciennement\n", + "`admissible_implies_optimal`, renommé car il borne un coût de suffixe) énonce la\n", "**borne en `f`** : sous heuristique admissible, pour tout nœud d'un chemin allant au\n", "but, `h(nœud)` ne dépasse jamais le coût du suffixe restant. Combinée à\n", "`f = g + h` et au fait que `g + suffixCost = pathCost`, cette borne donne\n", @@ -739,7 +760,7 @@ "\n", "***\n", "\n", - "**Le pont** : la structure induction sur les listes + lemme auxiliaire est la même qu'en Lean-6 / `Mathlib.Data.List`. Lean-12b utilise la même structure pour la sensibilité booléenne. Search-03e l'instancie pour A*. Search-03-Informed illustre cette optimalité empiriquement sur des graphes concrets.\n" + "**Le pont** : la structure induction sur les listes + lemme auxiliaire est la même qu'en Lean-6 / `Mathlib.Data.List`. Lean-12b utilise la même structure pour la sensibilité booléenne. Search-03e l'instancie pour A*. Search-03-Informed illustre cette optimalité empiriquement sur des graphes concrets." ] }, { @@ -748,16 +769,16 @@ "id": "291a2a3b", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.842822Z", - "iopub.status.busy": "2026-07-08T19:13:38.842822Z", - "iopub.status.idle": "2026-07-08T19:13:38.847408Z", - "shell.execute_reply": "2026-07-08T19:13:38.847408Z" + "iopub.execute_input": "2026-09-09T01:16:28.495299Z", + "iopub.status.busy": "2026-09-09T01:16:28.495096Z", + "iopub.status.idle": "2026-09-09T01:16:28.500453Z", + "shell.execute_reply": "2026-09-09T01:16:28.500017Z" }, "papermill": { - "duration": 0.014001, - "end_time": "2026-07-03T08:57:32.557166", + "duration": 0.009023, + "end_time": "2026-09-09T01:16:28.501162", "exception": false, - "start_time": "2026-07-03T08:57:32.543165", + "start_time": "2026-09-09T01:16:28.492139", "status": "completed" }, "tags": [] @@ -773,98 +794,95 @@ " 3 | import Astar.Heuristic\n", " 4 | \n", " 5 | /-!\n", - " 6 | # Astar.Optimality — admissible ⇒ optimal (lemme abstrait d'optimalité)\n", + " 6 | # Astar.Optimality — borne en `f` (lemme abstrait : borne de suffixe)\n", " 7 | \n", - " 8 | Théorème phare de la série (issue #4048, registre #3801 — prong B « problème\n", - " 9 | non-trivial »). On prouve la **borne en `f`** qui est le mécanisme exact d'optimalité\n", - " 10 | de A* : sous une heuristique admissible, `h(start)` ne dépasse jamais le coût d'un\n", - " 11 | chemin réalisé jusqu'au but. Appliquée à chaque suffixe du chemin optimal, cette borne\n", - " 12 | donne `f(nœud) = g(nœud) + h(nœud) ≤ coût optimal` en tout point du chemin optimal —\n", - " 13 | donc A* (qui déploie le nœud de `f` minimal) ne dépasse jamais la frontière du coût\n", - " 14 | optimal et renvoie un chemin de coût optimal (Hart, Nilsson & Raphael, 1968).\n", - " 15 | \n", - " 16 | On prouve la **forme abstraite** (sans modéliser la file de priorité complète), comme\n", - " 17 | suggéré par #4048 : `hStar` est un « vrai coût optimal restant » satisfaisant la\n", - " 18 | propriété de borne inférieure `IsTrueRemainingCost`.\n", - " 19 | -/\n", - " 20 | \n", - " 21 | namespace Astar\n", - " 22 | \n", - " 23 | variable {V : Type*} (G : WeightedGraph V)\n", - " 24 | \n", - " 25 | /-! ## Le « vrai coût optimal restant » `hStar` -/\n", - " 26 | \n", - " 27 | /-- `hStar` est une **borne inférieure** sur le coût de tout chemin allant de son\n", - " 28 | premier sommet au but. C'est la propriété caractéristique du vrai coût optimal\n", - " 29 | restant : pour un graphe fini, `hStar n = min { pathCost p | p va de n au but }`,\n", - " 30 | minimum atteint (chemins simples en nombre fini) et qui minore donc tout chemin\n", - " 31 | réalisé. On garde ici la forme abstraite (hypothèse), plus propre pédagogiquement\n", - " 32 | (cf #4048). -/\n", - " >>> 33 | def IsTrueRemainingCost (hStar : V → NNReal) (goal : V) : Prop :=\n", - " 34 | ∀ (start : V) (p : Path V), PathFrom start goal p → hStar start ≤ pathCost G p\n", - " 35 | \n", - " 36 | /-! ## Lemme auxiliaire : un suffixe d'un chemin allant au but va encore au but -/\n", - " 37 | \n", - " 38 | /-- Si `p` va de `start` à `goal`, alors pour tout indice `i`, le suffixe\n", - " 39 | `p.drop i` va de `p.get i` à `goal`. -/\n", - " 40 | lemma suffix_pathFrom (p : Path V) (i : Fin p.length) (start goal : V)\n", - " 41 | (hp : PathFrom start goal p) : PathFrom (p.get i) goal (p.drop i.val) := by\n", - " 42 | obtain ⟨hnil, hhead, hlast⟩ := hp\n", - " 43 | have hi : i.val < p.length := i.isLt\n", - " 44 | refine ⟨?_, ?_, ?_⟩\n", - " 45 | · -- (p.drop i.val) ≠ []\n", - " 46 | rw [Ne, List.drop_eq_nil_iff]\n", - " 47 | omega\n", - " 48 | · -- head? (p.drop i.val) = some (p.get i)\n", - " 49 | rw [List.head?_drop, List.getElem?_eq_getElem hi]\n", - " 50 | rfl\n", - " 51 | · -- getLast? (p.drop i.val) = some goal\n", - " 52 | have hne : ¬(p.length ≤ i.val) := by omega\n", - " 53 | rw [List.getLast?_drop, if_neg hne]\n", - " 54 | exact hlast\n", - " 55 | \n", - " 56 | /-! ## Théorème phare : borne en `f` et optimalité -/\n", - " 57 | \n", - " 58 | /-- **Borne en `f` au départ.** Heuristique admissible + `hStar` borne inférieure ⇒\n", - " 59 | `h(start) ≤ pathCost(p)` pour tout chemin `p` allant au but depuis `start`.\n", - " 60 | C'est la borne en `f` (`f = g + h`) au point de départ. -/\n", - " >>> 61 | theorem admissible_head_bound (h hStar : V → NNReal) (hAdm : Admissible h hStar)\n", - " 62 | (goal start : V) (p : Path V) (hStar_lb : IsTrueRemainingCost G hStar goal)\n", - " 63 | (hp : PathFrom start goal p) : h start ≤ pathCost G p :=\n", - " 64 | le_trans (hAdm start) (hStar_lb start p hp)\n", - " 65 | \n", - " 66 | /-- **A* admissible ⇒ optimal (lemme abstrait).** Théorème phare (issue #4048,\n", - " 67 | registre #3801).\n", + " 8 | Brique de la série (issue #4048, registre #3801 — prong B « problème non-trivial »).\n", + " 9 | On prouve la **borne en `f`** : sous une heuristique admissible, pour tout nœud\n", + " 10 | `p.get i` d'un chemin `p` allant au but, `h(p.get i)` ne dépasse jamais le coût du\n", + " 11 | suffixe restant `pathCost (p.drop i)`. C'est le cœur mathématique de l'argument\n", + " 12 | d'optimalité de A* (Hart, Nilsson & Raphael, 1968) — mais **seulement ce cœur**,\n", + " 13 | sous forme abstraite.\n", + " 14 | \n", + " 15 | Le lake ne modélise **pas** l'algorithme A* (ni file de priorité, ni ensemble fermé,\n", + " 16 | ni chemin retourné) : il n'y a donc **aucun théorème d'optimalité d'A*** ici. La\n", + " 17 | garantie « heuristique admissible ⇒ A* renvoie un chemin de coût optimal » — **fausse**\n", + " 18 | pour la variante Graph-Search sans ré-ouverture (cf #14824) — n'est pas prouvée.\n", + " 19 | \n", + " 20 | `hStar` est un « vrai coût optimal restant » : propriété de borne inférieure\n", + " 21 | `IsTrueRemainingCost` (la forme abstraite, cf #4048).\n", + " 22 | -/\n", + " 23 | \n", + " 24 | namespace Astar\n", + " 25 | \n", + " 26 | variable {V : Type*} (G : WeightedGraph V)\n", + " 27 | \n", + " 28 | /-! ## Le « vrai coût optimal restant » `hStar` -/\n", + " 29 | \n", + " 30 | /-- `hStar` est une **borne inférieure** sur le coût de tout chemin allant de son\n", + " 31 | premier sommet au but. C'est la propriété caractéristique du vrai coût optimal\n", + " 32 | restant : pour un graphe fini, `hStar n = min { pathCost p | p va de n au but }`,\n", + " 33 | minimum atteint (chemins simples en nombre fini) et qui minore donc tout chemin\n", + " 34 | réalisé. On garde ici la forme abstraite (hypothèse), plus propre pédagogiquement\n", + " 35 | (cf #4048). -/\n", + " >>> 36 | def IsTrueRemainingCost (hStar : V → NNReal) (goal : V) : Prop :=\n", + " 37 | ∀ (start : V) (p : Path V), PathFrom start goal p → hStar start ≤ pathCost G p\n", + " 38 | \n", + " 39 | /-! ## Lemme auxiliaire : un suffixe d'un chemin allant au but va encore au but -/\n", + " 40 | \n", + " 41 | /-- Si `p` va de `start` à `goal`, alors pour tout indice `i`, le suffixe\n", + " 42 | `p.drop i` va de `p.get i` à `goal`. -/\n", + " 43 | lemma suffix_pathFrom (p : Path V) (i : Fin p.length) (start goal : V)\n", + " 44 | (hp : PathFrom start goal p) : PathFrom (p.get i) goal (p.drop i.val) := by\n", + " 45 | obtain ⟨hnil, hhead, hlast⟩ := hp\n", + " 46 | have hi : i.val < p.length := i.isLt\n", + " 47 | refine ⟨?_, ?_, ?_⟩\n", + " 48 | · -- (p.drop i.val) ≠ []\n", + " 49 | rw [Ne, List.drop_eq_nil_iff]\n", + " 50 | omega\n", + " 51 | · -- head? (p.drop i.val) = some (p.get i)\n", + " 52 | rw [List.head?_drop, List.getElem?_eq_getElem hi]\n", + " 53 | rfl\n", + " 54 | · -- getLast? (p.drop i.val) = some goal\n", + " 55 | have hne : ¬(p.length ≤ i.val) := by omega\n", + " 56 | rw [List.getLast?_drop, if_neg hne]\n", + " 57 | exact hlast\n", + " 58 | \n", + " 59 | /-! ## Théorème phare : borne en `f` (borne de suffixe) -/\n", + " 60 | \n", + " 61 | /-- **Borne en `f` au départ.** Heuristique admissible + `hStar` borne inférieure ⇒\n", + " 62 | `h(start) ≤ pathCost(p)` pour tout chemin `p` allant au but depuis `start`.\n", + " 63 | C'est la borne en `f` (`f = g + h`) au point de départ. -/\n", + " >>> 64 | theorem admissible_head_bound (h hStar : V → NNReal) (hAdm : Admissible h hStar)\n", + " 65 | (goal start : V) (p : Path V) (hStar_lb : IsTrueRemainingCost G hStar goal)\n", + " 66 | (hp : PathFrom start goal p) : h start ≤ pathCost G p :=\n", + " 67 | le_trans (hAdm start) (hStar_lb start p hp)\n", " 68 | \n", - " 69 | Sous une heuristique **admissible**, pour tout nœud `p.get i` d'un chemin `p`\n", - " 70 | allant au but, l'heuristique ne dépasse jamais le coût du suffixe restant\n", - " 71 | `pathCost (p.drop i)`. C'est la **borne en `f`** en chaque nœud : combinée à\n", - " 72 | `f(nœud) = g(nœud) + h(nœud)` et au fait que `g + suffixCost = pathCost`, elle\n", - " 73 | donne `f(nœud) ≤ pathCost(optimal)` le long du chemin optimal — le mécanisme\n", - " 74 | exact d'optimalité de A* (déploiement du `f` minimal ⇒ la frontière du coût\n", - " 75 | optimal n'est jamais dépassée). Voir Hart, Nilsson & Raphael (1968). -/\n", - " >>> 76 | theorem admissible_implies_optimal (h hStar : V → NNReal) (hAdm : Admissible h hStar)\n", - " 77 | (goal start : V) (p : Path V) (hStar_lb : IsTrueRemainingCost G hStar goal)\n", - " 78 | (hp : PathFrom start goal p) (i : Fin p.length) :\n", - " 79 | h (p.get i) ≤ pathCost G (p.drop i.val) := by\n", - " 80 | apply le_trans (hAdm (p.get i))\n", - " 81 | exact hStar_lb (p.get i) (p.drop i.val) (suffix_pathFrom p i start goal hp)\n", - " 82 | \n", - " 83 | /-- **Corollaire : borne globale au départ.** Cas particulier `i = 0`\n", - " 84 | (le nœud de départ) : `h(start) ≤ pathCost(p)`. -/\n", - " >>> 85 | theorem admissible_implies_optimal_start (h hStar : V → NNReal) (hAdm : Admissible h hStar)\n", - " 86 | (goal start : V) (p : Path V) (hStar_lb : IsTrueRemainingCost G hStar goal)\n", - " 87 | (hp : PathFrom start goal p) : h start ≤ pathCost G p :=\n", - " 88 | admissible_head_bound G h hStar hAdm goal start p hStar_lb hp\n", - " 89 | \n", - " 90 | end Astar\n", - "--- fin (90 lignes) ---\n" + " 69 | /-- **Borne en `f` sur un suffixe (heuristique admissible).** Pour tout nœud\n", + " 70 | `p.get i` d'un chemin `p` allant au but, `h(p.get i) ≤ pathCost(p.drop i)` :\n", + " 71 | la valeur de l'heuristique admissible ne dépasse jamais le coût du suffixe\n", + " 72 | restant. C'est la borne en `f` (`f = g + h`) en chaque nœud — le cœur abstrait\n", + " 73 | de l'argument d'optimalité de A* (Hart, Nilsson & Raphael, 1968).\n", + " 74 | \n", + " 75 | **Portée — ce que ce théorème ne dit pas.** Il borne l'heuristique par le coût\n", + " 76 | du suffixe ; il ne prouve **pas** qu'A* renvoie un chemin de coût optimal. Le\n", + " 77 | lake ne modélise ni file de priorité, ni ensemble fermé, ni chemin retourné :\n", + " 78 | la garantie « heuristique admissible ⇒ A* optimal » (fausse pour la variante\n", + " 79 | Graph-Search sans ré-ouverture, cf #14824) n'est pas un théorème de ce lake. -/\n", + " >>> 80 | theorem admissible_le_suffix_cost (h hStar : V → NNReal) (hAdm : Admissible h hStar)\n", + " 81 | (goal start : V) (p : Path V) (hStar_lb : IsTrueRemainingCost G hStar goal)\n", + " 82 | (hp : PathFrom start goal p) (i : Fin p.length) :\n", + " 83 | h (p.get i) ≤ pathCost G (p.drop i.val) := by\n", + " 84 | apply le_trans (hAdm (p.get i))\n", + " 85 | exact hStar_lb (p.get i) (p.drop i.val) (suffix_pathFrom p i start goal hp)\n", + " 86 | \n", + " 87 | end Astar\n", + "--- fin (87 lignes) ---\n" ] } ], "source": [ - "# Source : IsTrueRemainingCost + theoreme phare admissible_implies_optimal\n", - "display_lean_module('Optimality', highlight=[33, 61, 76, 85])\n" + "# Source : IsTrueRemainingCost + theoreme phare admissible_le_suffix_cost\n", + "display_lean_module('Optimality', highlight=[36, 64, 80])" ] }, { @@ -872,10 +890,10 @@ "id": "a19783f4", "metadata": { "papermill": { - "duration": 0.006, - "end_time": "2026-07-03T08:57:32.568165", + "duration": 0.002163, + "end_time": "2026-09-09T01:16:28.505735", "exception": false, - "start_time": "2026-07-03T08:57:32.562165", + "start_time": "2026-09-09T01:16:28.503572", "status": "completed" }, "tags": [] @@ -883,7 +901,7 @@ "source": [ "### Lecture : le mécanisme exact d'optimalité\n", "\n", - "Le théorème `admissible_implies_optimal` (Optimality.lean, mis en évidence ci-dessus)\n", + "Le théorème `admissible_le_suffix_cost` (Optimality.lean, mis en évidence ci-dessus)\n", "se prouve en **deux pas** :\n", "\n", "1. **`suffix_pathFrom`** (lemme auxiliaire) : un suffixe d'un chemin allant au but\n", @@ -905,7 +923,7 @@ "\n", "***\n", "\n", - "**Le pont** : l'induction sur les listes est `List.recOn` en Lean-6 / `Mathlib`. Le lemme auxiliaire `suffix_pathFrom` est un `List.drop` + induction. Search-03e ne réinvente rien — il utilise les primitives de Lean-6 sur le type `PathFrom`. Lean-12b (Sensitivity) utilise exactement la même structure pour ses preuves spectrales.\n" + "**Le pont** : l'induction sur les listes est `List.recOn` en Lean-6 / `Mathlib`. Le lemme auxiliaire `suffix_pathFrom` est un `List.drop` + induction. Search-03e ne réinvente rien — il utilise les primitives de Lean-6 sur le type `PathFrom`. Lean-12b (Sensitivity) utilise exactement la même structure pour ses preuves spectrales." ] }, { @@ -913,10 +931,10 @@ "id": "928ccb5c", "metadata": { "papermill": { - "duration": 0.004999, - "end_time": "2026-07-03T08:57:32.578387", + "duration": 0.002284, + "end_time": "2026-09-09T01:16:28.510308", "exception": false, - "start_time": "2026-07-03T08:57:32.573388", + "start_time": "2026-09-09T01:16:28.508024", "status": "completed" }, "tags": [] @@ -952,16 +970,16 @@ "id": "223eaff2", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.847408Z", - "iopub.status.busy": "2026-07-08T19:13:38.847408Z", - "iopub.status.idle": "2026-07-08T19:13:38.854290Z", - "shell.execute_reply": "2026-07-08T19:13:38.854290Z" + "iopub.execute_input": "2026-09-09T01:16:28.516738Z", + "iopub.status.busy": "2026-09-09T01:16:28.516336Z", + "iopub.status.idle": "2026-09-09T01:16:28.520721Z", + "shell.execute_reply": "2026-09-09T01:16:28.520189Z" }, "papermill": { - "duration": 0.013964, - "end_time": "2026-07-03T08:57:32.598352", + "duration": 0.008199, + "end_time": "2026-09-09T01:16:28.521465", "exception": false, - "start_time": "2026-07-03T08:57:32.584388", + "start_time": "2026-09-09T01:16:28.513266", "status": "completed" }, "tags": [] @@ -1117,10 +1135,10 @@ "id": "05bb11e7", "metadata": { "papermill": { - "duration": 0.0, - "end_time": "2026-07-03T08:57:32.604353", + "duration": 0.00233, + "end_time": "2026-09-09T01:16:28.526253", "exception": false, - "start_time": "2026-07-03T08:57:32.604353", + "start_time": "2026-09-09T01:16:28.523923", "status": "completed" }, "tags": [] @@ -1156,10 +1174,10 @@ "id": "b454a17d", "metadata": { "papermill": { - "duration": 0.01667, - "end_time": "2026-07-03T08:57:32.621023", + "duration": 0.002321, + "end_time": "2026-09-09T01:16:28.530783", "exception": false, - "start_time": "2026-07-03T08:57:32.604353", + "start_time": "2026-09-09T01:16:28.528462", "status": "completed" }, "tags": [] @@ -1184,14 +1202,15 @@ " └─▶ Dijkstra (recherche à coût uniforme)\n", "```\n", "\n", - "Tout cela est **formellement prouvé à 0 `sorry`** dans `search_lean` — la garantie\n", - "que l'optimalité de A\\* n'est pas un argument de manuel mais un théorème vérifié\n", - "mécaniquement.\n", + "Les bornes et la monotonie ci-dessus sont **formellement prouvées à 0 `sorry`**\n", + "dans `search_lean`. Seul le dernier saut — « donc A\\* renvoie un chemin optimal » —\n", + "relèverait de modéliser l'algorithme lui-même (file de priorité), ce que le lake\n", + "ne fait pas (cf #14824).\n", "\n", "\n", "***\n", "\n", - "**Le pont** : Search-03e et Lean-12b sont **structurellement jumeaux** : 4 modules, preuve par induction sur les listes, théorème final issu d'une accumulation locale → globale. C'est le **template** de la série Lean : un grand théorème décomposé en 4 modules factorisés pour réutilisation.\n" + "**Le pont** : Search-03e et Lean-12b sont **structurellement jumeaux** : 4 modules, preuve par induction sur les listes, théorème final issu d'une accumulation locale → globale. C'est le **template** de la série Lean : un grand théorème décomposé en 4 modules factorisés pour réutilisation." ] }, { @@ -1199,10 +1218,10 @@ "id": "10e00a65", "metadata": { "papermill": { - "duration": 0.0, - "end_time": "2026-07-03T08:57:32.621023", + "duration": 0.002303, + "end_time": "2026-09-09T01:16:28.535654", "exception": false, - "start_time": "2026-07-03T08:57:32.621023", + "start_time": "2026-09-09T01:16:28.533351", "status": "completed" }, "tags": [] @@ -1231,16 +1250,16 @@ "id": "45115592", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.854290Z", - "iopub.status.busy": "2026-07-08T19:13:38.854290Z", - "iopub.status.idle": "2026-07-08T19:13:38.863025Z", - "shell.execute_reply": "2026-07-08T19:13:38.863025Z" + "iopub.execute_input": "2026-09-09T01:16:28.541725Z", + "iopub.status.busy": "2026-09-09T01:16:28.541372Z", + "iopub.status.idle": "2026-09-09T01:16:28.548503Z", + "shell.execute_reply": "2026-09-09T01:16:28.548023Z" }, "papermill": { - "duration": 0.033927, - "end_time": "2026-07-03T08:57:32.654950", + "duration": 0.011167, + "end_time": "2026-09-09T01:16:28.549219", "exception": false, - "start_time": "2026-07-03T08:57:32.621023", + "start_time": "2026-09-09T01:16:28.538052", "status": "completed" }, "tags": [] @@ -1261,8 +1280,8 @@ " theorem zero_admissible (hStar : V → NNReal) : Admissible (fun _ => (0 : NNReal)) hStar :=\n", " Astar/Optimality.lean :: IsTrueRemainingCost\n", " def IsTrueRemainingCost (hStar : V → NNReal) (goal : V) : Prop :=\n", - " Astar/Optimality.lean :: admissible_implies_optimal\n", - " theorem admissible_implies_optimal (h hStar : V → NNReal) (hAdm : Admissible h hStar)\n", + " Astar/Optimality.lean :: admissible_le_suffix_cost\n", + " theorem admissible_le_suffix_cost (h hStar : V → NNReal) (hAdm : Admissible h hStar)\n", " Astar/Consistency.lean :: consistent_implies_path_bound\n", " theorem consistent_implies_path_bound (h : V → NNReal) (goal : V)\n", " Astar/Consistency.lean :: consistent_implies_f_monotone\n", @@ -1293,14 +1312,14 @@ "for mod, names in [\n", " ('Graph', ['WeightedGraph', 'pathCost']),\n", " ('Heuristic', ['Admissible', 'zero_admissible']),\n", - " ('Optimality', ['IsTrueRemainingCost', 'admissible_implies_optimal']),\n", + " ('Optimality', ['IsTrueRemainingCost', 'admissible_le_suffix_cost']),\n", " ('Consistency', ['consistent_implies_path_bound', 'consistent_implies_f_monotone']),\n", "]:\n", " sigs = extract_signatures(mod, names)\n", " for nm in names:\n", " print(f\" Astar/{mod}.lean :: {nm}\")\n", " print(f\" {sigs.get(nm, '(non trouve -- verifier le nom)')}\")\n", - "print(\"--- fin ---\")\n" + "print(\"--- fin ---\")" ] }, { @@ -1309,16 +1328,16 @@ "id": "e98124bf", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.863025Z", - "iopub.status.busy": "2026-07-08T19:13:38.863025Z", - "iopub.status.idle": "2026-07-08T19:13:38.867158Z", - "shell.execute_reply": "2026-07-08T19:13:38.867158Z" + "iopub.execute_input": "2026-09-09T01:16:28.555234Z", + "iopub.status.busy": "2026-09-09T01:16:28.555057Z", + "iopub.status.idle": "2026-09-09T01:16:28.558547Z", + "shell.execute_reply": "2026-09-09T01:16:28.558107Z" }, "papermill": { - "duration": 0.020741, - "end_time": "2026-07-03T08:57:32.675691", + "duration": 0.007375, + "end_time": "2026-09-09T01:16:28.559262", "exception": false, - "start_time": "2026-07-03T08:57:32.654950", + "start_time": "2026-09-09T01:16:28.551887", "status": "completed" }, "tags": [] @@ -1384,16 +1403,16 @@ "id": "3dbe2a83", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.867158Z", - "iopub.status.busy": "2026-07-08T19:13:38.867158Z", - "iopub.status.idle": "2026-07-08T19:13:38.871087Z", - "shell.execute_reply": "2026-07-08T19:13:38.871087Z" + "iopub.execute_input": "2026-09-09T01:16:28.565344Z", + "iopub.status.busy": "2026-09-09T01:16:28.565009Z", + "iopub.status.idle": "2026-09-09T01:16:28.568099Z", + "shell.execute_reply": "2026-09-09T01:16:28.567747Z" }, "papermill": { - "duration": 0.010405, - "end_time": "2026-07-03T08:57:32.693706", + "duration": 0.006978, + "end_time": "2026-09-09T01:16:28.568814", "exception": false, - "start_time": "2026-07-03T08:57:32.683301", + "start_time": "2026-09-09T01:16:28.561836", "status": "completed" }, "tags": [] @@ -1452,16 +1471,16 @@ "id": "efa74d77", "metadata": { "execution": { - "iopub.execute_input": "2026-07-08T19:13:38.871087Z", - "iopub.status.busy": "2026-07-08T19:13:38.871087Z", - "iopub.status.idle": "2026-07-08T19:13:38.875031Z", - "shell.execute_reply": "2026-07-08T19:13:38.875031Z" + "iopub.execute_input": "2026-09-09T01:16:28.574863Z", + "iopub.status.busy": "2026-09-09T01:16:28.574635Z", + "iopub.status.idle": "2026-09-09T01:16:28.577898Z", + "shell.execute_reply": "2026-09-09T01:16:28.577470Z" }, "papermill": { - "duration": 0.012362, - "end_time": "2026-07-03T08:57:32.710766", + "duration": 0.007379, + "end_time": "2026-09-09T01:16:28.578809", "exception": false, - "start_time": "2026-07-03T08:57:32.698404", + "start_time": "2026-09-09T01:16:28.571430", "status": "completed" }, "tags": [] @@ -1528,10 +1547,10 @@ "id": "1259861b", "metadata": { "papermill": { - "duration": 0.0, - "end_time": "2026-07-03T08:57:32.714065", + "duration": 0.002577, + "end_time": "2026-09-09T01:16:28.584331", "exception": false, - "start_time": "2026-07-03T08:57:32.714065", + "start_time": "2026-09-09T01:16:28.581754", "status": "completed" }, "tags": [] @@ -1540,15 +1559,18 @@ "## Conclusion\n", "\n", "Ce notebook a visité le lake **`search_lean`** (0 `sorry`), qui prouve\n", - "**formellement** l'optimalité de A\\* sous heuristique admissible.\n", + "**formellement** la borne en `f` — le cœur mathématique de l'optimalité de A\\*\n", + "sous heuristique admissible.\n", "\n", "### Ce qui est prouvé\n", "\n", "- **Modèle** (`Graph`) : graphe pondéré `ℝ≥0`, coût additif `pathCost` d'un chemin.\n", "- **Prédicats** (`Heuristic`) : `Admissible` (globale) et `Consistent` (locale),\n", " avec leurs propriétés de base — dont la **connexion à Dijkstra** (`h ≡ 0`).\n", - "- **Optimalité** (`Optimality`) : le théorème phare `admissible_implies_optimal`\n", - " — la borne en `f` qui garantit qu'A\\* renvoie un chemin de coût optimal.\n", + "- **Optimalité** (`Optimality`) : le théorème phare `admissible_le_suffix_cost`\n", + " — la borne en `f` en chaque nœud d'un chemin allant au but. C'est le mécanisme\n", + " exact de l'optimalité de A\\* ; la garantie « A\\* renvoie un chemin optimal »\n", + " elle-même n'est pas un théorème du lake (file de priorité non modélisée, cf #14824).\n", "- **Téléscopage** (`Consistency`) : la consistance implique l'admissibilité (par\n", " récurrence le long du chemin) ET la monotonie de `f` (non-ré-expansion).\n", "\n", @@ -1573,28 +1595,28 @@ "\n", "***\n", "\n", - "**Le pont** : Search-03e ↔ Lean-12b (cérémonie commune) ↔ Lean-6 (Mathlib / primitives `List`, `NNReal`, `linarith`) ↔ Search-03-Informed (vue empirique Python du même sujet). Search-03e ferme la boucle : on a maintenant la version *formelle* et la version *empirique* de l'optimalité A*, comparables et complémentaires. Lean-13 (Kochen-Specker) et Lean-14 (Finiteness) poursuivent la série Lean avec d'autres théorèmes.\n" + "**Le pont** : Search-03e ↔ Lean-12b (cérémonie commune) ↔ Lean-6 (Mathlib / primitives `List`, `NNReal`, `linarith`) ↔ Search-03-Informed (vue empirique Python du même sujet). Search-03e ferme la boucle : on a maintenant la version *formelle* et la version *empirique* de l'optimalité A*, comparables et complémentaires. Lean-13 (Kochen-Specker) et Lean-14 (Finiteness) poursuivent la série Lean avec d'autres théorèmes." ] } ], "metadata": { "cost": { - "api_usd_est": 0.0, "api_provider": "none", - "qcc_tokens_est": 0, + "api_usd_est": 0, + "cpu_min": 2, + "external_account": false, + "free_alternative": "self", "gpu_min": 0, "gpu_required": false, - "vram_gb": 0, - "vram_tier": "none", + "metadata_written": "2026-08-03", "network": true, - "external_account": false, - "free_alternative": "self", + "notes": "A* search optimality theorem: Lean formal proof via lake build + Python A* demo. Deterministic. No LLM, no GPU. Network=toolchain fetch.", + "qcc_tokens_est": 0, "reduced_pedagogical": false, "reproducibility": "HIGH", - "metadata_written": "2026-08-03", "validator": "check_cost_metadata.py", - "cpu_min": 2, - "notes": "A* search optimality theorem: Lean formal proof via lake build + Python A* demo. Deterministic. No LLM, no GPU. Network=toolchain fetch." + "vram_gb": 0, + "vram_tier": "none" }, "kernelspec": { "display_name": "Python 3", @@ -1611,18 +1633,18 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.11.9" + "version": "3.13.3" }, "papermill": { "default_parameters": {}, - "duration": 414.083194, - "end_time": "2026-07-03T08:57:32.976590", + "duration": 2.161269, + "end_time": "2026-09-09T01:16:28.722244", "environment_variables": {}, "exception": null, - "input_path": "Search-03e-AStar-Optimality.ipynb", - "output_path": "Search-03e-AStar-Optimality.ipynb", + "input_path": "D:\\Dev\\CoursIA-14893-rename\\MyIA.AI.Notebooks\\Search\\Part1-Foundations\\Search-03e-AStar-Optimality.ipynb", + "output_path": "D:\\Dev\\CoursIA-14893-rename\\MyIA.AI.Notebooks\\Search\\Part1-Foundations\\Search-03e-AStar-Optimality_output.ipynb", "parameters": {}, - "start_time": "2026-07-03T08:50:38.893396", + "start_time": "2026-09-09T01:16:26.560975", "version": "2.6.0" } }, diff --git a/MyIA.AI.Notebooks/Search/search_lean/Astar.en.md b/MyIA.AI.Notebooks/Search/search_lean/Astar.en.md index 61cd6a0b62..1a5b506e6c 100644 --- a/MyIA.AI.Notebooks/Search/search_lean/Astar.en.md +++ b/MyIA.AI.Notebooks/Search/search_lean/Astar.en.md @@ -117,13 +117,15 @@ Founding companion lemmas (issue #4048): elementary properties of the two centra --- -## `Astar/Optimality.lean` — admissible ⇒ optimal (abstract optimality lemma) +## `Astar/Optimality.lean` — the f-bound (abstract lemma: suffix-cost bound) **Module docstring (translated).** -Flagship theorem of the series (issue #4048, register #3801 — prong B "non-trivial problem"). We prove the **f-bound** that is the exact optimality mechanism of A*: under an admissible heuristic, `h(start)` never exceeds the cost of a realized path to the goal. Applied to each suffix of the optimal path, this bound gives `f(node) = g(node) + h(node) ≤ optimal cost` at every point of the optimal path — hence A* (which deploys the node of minimal `f`) never crosses the optimal-cost frontier and returns a path of optimal cost (Hart, Nilsson & Raphael, 1968). +Building block of the series (issue #4048, register #3801 — prong B "non-trivial problem"). We prove the **f-bound**: under an admissible heuristic, for every node `p.get i` of a path `p` going to the goal, `h(p.get i)` never exceeds the cost of the remaining suffix `pathCost (p.drop i)`. This is the mathematical core of the A* optimality argument (Hart, Nilsson & Raphael, 1968) — but **only this core**, in abstract form. -We prove the **abstract form** (without modeling the full priority queue), as suggested by #4048: `hStar` is a "true optimal remaining cost" satisfying the lower-bound property `IsTrueRemainingCost`. +The lake does **not** model the A* algorithm (no priority queue, no closed set, no returned path): there is therefore **no A* optimality theorem** here. The guarantee "admissible heuristic ⇒ A* returns a path of optimal cost" — **false** for the Graph-Search variant without re-opening (cf #14824) — is not proved. + +`hStar` is a "true optimal remaining cost": lower-bound property `IsTrueRemainingCost` (the abstract form, cf #4048). ### The "true optimal remaining cost" `hStar` @@ -143,15 +145,13 @@ If `p` goes from `start` to `goal`, then for any index `i`, the suffix `p.drop i **f-bound at the start.** Admissible heuristic + `hStar` lower bound ⇒ `h(start) ≤ pathCost(p)` for every path `p` going to the goal from `start`. This is the f-bound (`f = g + h`) at the starting point. -#### `admissible_implies_optimal` — theorem - -**A* admissible ⇒ optimal (abstract lemma).** Flagship theorem (issue #4048, register #3801). +#### `admissible_le_suffix_cost` — theorem -Under an **admissible** heuristic, for every node `p.get i` of a path `p` going to the goal, the heuristic never exceeds the cost of the remaining suffix `pathCost (p.drop i)`. This is the **f-bound** at each node: combined with `f(node) = g(node) + h(node)` and the fact that `g + suffixCost = pathCost`, it gives `f(node) ≤ pathCost(optimal)` along the optimal path — the exact optimality mechanism of A* (deployment of the minimal `f` ⇒ the optimal-cost frontier is never crossed). See Hart, Nilsson & Raphael (1968). +**f-bound on a suffix (admissible heuristic).** Flagship theorem (issue #4048, register #3801), formerly `admissible_implies_optimal` (renamed by #14864: the statement bounds a suffix cost, it does not prove optimality). -#### `admissible_implies_optimal_start` — theorem +Under an **admissible** heuristic, for every node `p.get i` of a path `p` going to the goal, `h(p.get i) ≤ pathCost(p.drop i)`: an admissible heuristic never exceeds the cost of the remaining suffix. This is the **f-bound** (`f = g + h`) at each node — the abstract core of the A* optimality argument (Hart, Nilsson & Raphael, 1968). -**Corollary: global bound at the start.** Special case `i = 0` (the starting node): `h(start) ≤ pathCost(p)`. +**Scope — what this theorem does not say.** It bounds the heuristic by the suffix cost; it does **not** prove that A* returns a path of optimal cost. The lake models neither priority queue, nor closed set, nor returned path: the guarantee "admissible heuristic ⇒ optimal A*" (false for the Graph-Search variant without re-opening, cf #14824) is not a theorem of this lake. --- diff --git a/MyIA.AI.Notebooks/Search/search_lean/README.md b/MyIA.AI.Notebooks/Search/search_lean/README.md index 1d70069711..219c270d03 100644 --- a/MyIA.AI.Notebooks/Search/search_lean/README.md +++ b/MyIA.AI.Notebooks/Search/search_lean/README.md @@ -1,8 +1,8 @@ # `search_lean` — Optimalité de A* en Lean 4 Mini-projet Lean 4 (avec [Mathlib](https://github.com/leanprover-community/mathlib4)) -formalisant le **théorème phare d'optimalité de A*** : une heuristique *admissible* -garantit que l'algorithme A* renvoie un chemin de coût optimal +formalisant le **cœur mathématique de l'optimalité de A*** : la borne en `f` sous +heuristique *admissible* — le mécanisme exact de l'argument d'optimalité ([Hart, Nilsson & Raphael, 1968](https://doi.org/10.1109/TSSC.1968.300136)). > **Issue** : [#4048](https://github.com/jsboige/CoursIA/issues/4048) — @@ -58,13 +58,13 @@ cf #4048) : la **borne en `f`** qui est le mécanisme exact d'optimalité de A*. - [`Astar/Graph.lean`](Astar/Graph.lean) — `WeightedGraph`, `pathCost`, `PathFrom`. - [`Astar/Heuristic.lean`](Astar/Heuristic.lean) — `Admissible`, `Consistent`. -- [`Astar/Optimality.lean`](Astar/Optimality.lean) — théorème phare (`admissible_implies_optimal`). +- [`Astar/Optimality.lean`](Astar/Optimality.lean) — théorème phare (`admissible_le_suffix_cost`, anciennement `admissible_implies_optimal`). - [`Astar/Consistency.lean`](Astar/Consistency.lean) — `consistent_implies_path_bound` (consistance ⟹ admissibilité, téléscopage). ## Théorème phare ```lean -theorem admissible_implies_optimal +theorem admissible_le_suffix_cost (h hStar : V → NNReal) (hAdm : Admissible h hStar) (goal start : V) (p : Path V) (hStar_lb : IsTrueRemainingCost G hStar goal) (hp : PathFrom start goal p) (i : Fin p.length) : @@ -87,7 +87,7 @@ flowchart TD WG["Graphe pondéré WeightedGraph V
arêtes edge : V → V → ℝ≥0 (non-négatives)"] PATH["Chemin start → goal
PathFrom start goal p · coût pathCost p"] HADM["Heuristique admissible
Admissible h hStar : ∀ n, h n ≤ hStar n"] - BOUND["Borne en f en chaque nœud
h(p.get i) ≤ pathCost(p.drop i)
admissible_implies_optimal (phase 1)"] + BOUND["Borne en f en chaque nœud
h(p.get i) ≤ pathCost(p.drop i)
admissible_le_suffix_cost (phase 1)"] STAR["A* déploie le nœud de f = g + h minimal"] OPT["Chemin optimal renvoyé
jamais au-delà de la frontière du coût optimal"] @@ -175,7 +175,7 @@ flowchart TD CONS["Heuristique consistante
Consistent G h : h n ≤ edge n n' + h n'
locale par arc (relaxation de Bellman)"] TELE["consistent_implies_path_bound
téléscopage le long du chemin
h(start) ≤ pathCost(p)"] ADM["Heuristique admissible
Admissible h hStar : h n ≤ hStar n
globale"] - OPT["admissible_implies_optimal
phase 1 — borne en f
chemin optimal garanti"] + OPT["admissible_le_suffix_cost
phase 1 — borne en f
mécanisme exact d'optimalité"] MONO["consistent_implies_f_monotone
phase 3 — f = g + h croissante"] EFF["Efficacité
aucun nœud jamais ré-expansé"] @@ -203,7 +203,7 @@ Ce livrable couvre les phases 1-3 (#4048) : - [x] Scaffolding du lake (lakefile, toolchain, `.gitignore`) - [x] Modèle (`WeightedGraph`, `pathCost`, `PathFrom`) - [x] Définitions (`Admissible`, `Consistent`, `IsTrueRemainingCost`) -- [x] **Théorème phare `admissible_implies_optimal` — 0 `sorry`** (phase 1, PR #4090) +- [x] **Théorème phare `admissible_le_suffix_cost` (anciennement `admissible_implies_optimal`) — 0 `sorry`** (phase 1, PR #4090) - [x] **`consistent_implies_admissible` — 0 `sorry`** (phase 2, téléscopage de la consistance le long du chemin) - [x] **`consistent_implies_f_monotone` — 0 `sorry`** (phase 3, `f = g + h` croissante ⇒ pas de ré-expansion) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md index e05cbdfac6..55f61b1e07 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/README.md @@ -132,7 +132,7 @@ Tous les notebooks incluent une **barre de navigation** en haut et en bas permet | # | Notebook | Contenu | Durée | |---|----------|---------|-------| -| 18 | [Search-03e-AStar-Optimality](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Optimalité de A* sous heuristique admissible : graphe pondéré ℝ≥0 et coût additif `pathCost`, prédicats `Admissible`/`Consistent`, théorème phare `admissible_implies_optimal` (borne en f), téléscopage `consistent_implies_path_bound` + monotonie de f - companion `search_lean` (lake `Search/`, 0 sorry, registre #3801 prong B) | 35 min | +| 18 | [Search-03e-AStar-Optimality](../../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Optimalité de A* sous heuristique admissible : graphe pondéré ℝ≥0 et coût additif `pathCost`, prédicats `Admissible`/`Consistent`, théorème phare `admissible_le_suffix_cost` (borne en f), téléscopage `consistent_implies_path_bound` + monotonie de f - companion `search_lean` (lake `Search/`, 0 sorry, registre #3801 prong B) | 35 min | ### Partie 7 : Digestions de résultats profonds et companions (Sendov, Tao, PFR, MIMO, Galois, ERC-20, calibration, décision, Hopf S⁶) diff --git a/MyIA.AI.Notebooks/SymbolicAI/README.md b/MyIA.AI.Notebooks/SymbolicAI/README.md index 324d52a856..882d6da8a1 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/README.md @@ -237,7 +237,7 @@ Série de **49 notebooks** sur **Lean 4**, proof assistant basé sur la théorie | 17 | [Lean-17a-Knots-Conway-Proofs](Lean/Lean-17a-Knots-Conway-Proofs.ipynb) | Python WSL | Noeuds de Conway : introduction, énoncés, premier port formel adossé à `conway_knots_lean/` | 3 | | 17b | [Lean-17b-Knots-Invariants-Companion](Lean/Lean-17b-Knots-Invariants-Companion.ipynb) | Python WSL | Companion natif : invariants de noeuds, snippets WSL, sources `conway_knots_lean/` | 3 | | 17c | [Lean-17c-Knots-Companion-Formel](Lean/Lean-17c-Knots-Companion-Formel.ipynb) | Python | Le lake `knot_lean` par ses déclarations (compagnon formel) | 3 | -| 18 | [Search-03e-AStar-Optimality](../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Python 3 | Optimalité de A* sous heuristique admissible/consistante : graphe pondéré ℝ≥0, `pathCost` additif, prédicats `Admissible`/`Consistent`, théorèmes phares `admissible_implies_optimal` + `consistent_implies_path_bound` - companion `search_lean` (lake `Search/`, 0 sorry, registre #3801 prong B) | 3 | +| 18 | [Search-03e-AStar-Optimality](../Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb) | Python 3 | Optimalité de A* sous heuristique admissible/consistante : graphe pondéré ℝ≥0, `pathCost` additif, prédicats `Admissible`/`Consistent`, théorèmes phares `admissible_le_suffix_cost` + `consistent_implies_path_bound` - companion `search_lean` (lake `Search/`, 0 sorry, registre #3801 prong B) | 3 | | **Théorèmes phares 2026** | | | | | | 19 | [Lean-19-Sendov-Complex-Analysis](Lean/Lean-19-Sendov-Complex-Analysis.ipynb) | Python WSL | Conjecture de Sendov (preuve L. Mazur 2026, digestion et formalisation T. Tao) : pour un polynôme dont tous les zéros sont dans le disque unité, chaque zéro a un point critique à distance ≤ 1 — énoncé, illustrations numériques, contexte de la preuve | 4 | | 20 | [Lean-20-Analysis-I-Tao-Workflow](Lean/Lean-20-Analysis-I-Tao-Workflow.ipynb) | Python WSL | Manuel *Analysis I* de T. Tao en lac Lean 4 (`teorth/analysis`) : architecture du lac, philosophie d'auto-contenance vs Mathlib, cinq lemmes emblématiques parmi 44k LOC, méta-récit single-agent vs cluster distribué | 4 |