docs(lean,#14893): purge des references residuelles a admissible_implies_optimal apres renommage #14864

.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).

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)