search_lean : le theoreme nomme admissible_implies_optimal prouve une borne de suffixe, et son nom est enonce que #14824 refute #14830

Constat

Le lake search_lean porte un théorème nommé admissible_implies_optimal. C'est, mot pour mot, la proposition que #14824 mesure fausse sur l'A* que la même série enseigne.

Le lake ne prouve pas cette proposition. Il prouve autre chose — quelque chose de vrai, d'utile, et de beaucoup plus faible.

Ce que l'énoncé dit réellement

MyIA.AI.Notebooks/Search/search_lean/Astar/Optimality.lean:76-81 :

theorem admissible_implies_optimal (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) :
    h (p.get i) ≤ pathCost G (p.drop i.val) := by
  apply le_trans (hAdm (p.get i))
  exact hStar_lb (p.get i) (p.drop i.val) (suffix_pathFrom p i start goal hp)

La conclusion est une borne sur un suffixe : l'heuristique en un nœud ne dépasse pas le coût du reste du chemin. La preuve est une transitivité entre deux hypothèses qui la donnent presque immédiatement :

• hAdm : h n ≤ hStar n — par définition d'Admissible ;
• hStar_lb : IsTrueRemainingCost (l.33-34) pose déjà ∀ start p, PathFrom start goal p → hStar start ≤ pathCost G p.

Autrement dit h ≤ hStar et hStar ≤ pathCost(chemin vers le but), donc h ≤ pathCost(suffixe). C'est le_trans, appliqué au suffixe via le lemme de listes suffix_pathFrom. Le notebook le décrit d'ailleurs exactement ainsi (c13 : « donc h(nœud) ≤ pathCost(suffixe) par le_trans »).

Il n'y a pas d'algorithme dans le lake

C'est le point décisif, et il se mesure :

$ grep -rniE "consist|reopen|re-open|closed|frontier|priorityqueue|visited" \
      MyIA.AI.Notebooks/Search/search_lean/ --include=*.lean

Les seuls résultats sont dans les docstrings de Consistency.lean (prose sur la non-ré-expansion). Aucune définition de file de priorité, d'ensemble fermé, de relation d'expansion, de terminaison, ni du chemin qu'A* retourne. Les modules du lake sont Graph / Heuristic / Optimality / Consistency plus l'agrégateur ; ils définissent un graphe, un coût de chemin, deux prédicats sur h, et des bornes.

Un théorème d'optimalité d'A* est un énoncé sur ce que l'algorithme renvoie. Il n'existe ici aucun objet dont « optimal » pourrait être une propriété. Le nom admissible_implies_optimal ne désigne donc pas un résultat sous-modélisé : il désigne un résultat d'une autre nature que ce que son nom annonce.

Même remarque, plus bénigne, sur admissible_implies_optimal_start (l.85-88) : c'est le cas i = 0, et son corps est littéralement admissible_head_bound — un doublon sous un second nom qui, lui aussi, dit « optimal ».

Ce que le notebook en dit

Search-03e-AStar-Optimality.ipynb (24 cellules) :

La dernière ligne est la plus nette : elle affirme une garantie sur la valeur de retour de l'algorithme, précisément l'objet dont le lake ne parle pas.

La section d'honnêteté existe — et ne rétracte rien

Il faut le porter au crédit du notebook : c23 contient une sous-section « La chaîne, honnêtement » :

search_lean prouve la forme abstraite de l'optimalité (per #4048) : hStar est une borne inférieure, le modèle isole le cœur mathématique (coût additif + borne en f) sans modéliser la file de priorité complète. C'est délibéré — plus propre pédagogiquement, et le mécanisme exact d'optimalité est bien là.

Trois raisons pour lesquelles cette réserve ne suffit pas :

1. « sans modéliser la file de priorité complète » suggère un modèle partiel. Il n'y en a aucun — ni partiel, ni simplifié. L'écart annoncé est un écart de degré ; l'écart réel est de nature.
2. « le mécanisme exact d'optimalité est bien là » réaffirme la revendication à l'intérieur même de la réserve.
3. La réserve est au-dessous des deux affirmations non qualifiées de la même cellule, qu'elle ne reprend ni ne corrige. Un lecteur qui s'arrête à « Ce qui est prouvé » a lu une garantie sur la valeur de retour d'A*.

Pourquoi ce n'est pas une pinaillerie de portée — le lien avec #14824

Le « Pont » de c23 conclut :

on a maintenant la version formelle et la version empirique de l'optimalité A*, comparables et complémentaires.

La version empirique est Search-3-Informed.ipynb. #14824 y mesure, avec les classes et l'a_star_search du notebook, une heuristique admissible sur les quatre nœuds sous laquelle cet A* retourne un chemin de coût 4 là où l'optimum vaut 3,5 — parce que son Graph-Search ferme les états sans jamais les rouvrir.

Les deux versions ne sont donc pas complémentaires : l'empirique réfute la lecture donnée à la formelle. Et le nom du théorème formel — admissible_implies_optimal — est exactement l'énoncé que l'empirique met en défaut. Un étudiant qui cherche la garantie dans le lake y trouve son nom, « 0 sorry », et rien qui la porte.

À noter que le lake prouve la bonne chose du bon côté : consistent_implies_f_monotone (Consistency.lean:123) est précisément l'ingrédient qui rend la variante sans ré-ouverture correcte. C'est la branche admissibilité qui est mal nommée et sur-lue, pas la branche consistance.

Résidu de nommage

consistent_implies_admissible est annoncé comme « théorème cible » dans 6 endroits (Consistency.lean:9,46, Consistency_en.lean:15,54, Heuristic.lean:35, Astar.en.md:92,162). Il n'est livré nulle part : ce qui existe est consistent_implies_admissible_bound (l.95), un énoncé différent — une borne de chemin, sans hypothèse sur hStar. Le corriger relève du même geste que ci-dessus : faire coïncider les noms avec les énoncés.

Ce que ce constat n'est pas

Ce n'est pas un reproche de sorry : count_code_sorry.py --json rend 0 pour ce lake, et c'est exact. Ce n'est pas non plus un reproche d'abstraction : garder hStar abstrait est un choix légitime et bien expliqué. Le défaut est le nom d'un théorème et les phrases qui le lisent, pas la preuve, qui est correcte pour ce qu'elle énonce.

Acceptance

1. admissible_implies_optimal est renommé d'après ce qu'il prouve (admissible_le_suffix_cost, ou équivalent), ou bien son énoncé est étendu jusqu'à une véritable conclusion d'optimalité — ce qui exige de modéliser expansion, ensemble fermé et terminaison. Le renommage est la voie honnête et peu coûteuse ; l'extension est un chantier à part, à ouvrir comme tel s'il est voulu. Même traitement pour admissible_implies_optimal_start (et son doublon avec admissible_head_bound).
2. Les siblings _en suivent dans le même mouvement (convention i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 : un fix se porte sur les deux).
3. Dans Search-03e, les quatre formulations du tableau ci-dessus sont mises d'accord avec ce que le lake prouve. En particulier « garantit qu'A* renvoie un chemin de coût optimal » ne survit pas en l'état.
4. La réserve de c23 précède les affirmations qu'elle borne, au lieu de les suivre — et « sans modéliser la file de priorité complète » devient « sans modéliser l'algorithme », qui est la mesure.
5. Le « Pont » cesse d'annoncer deux versions complémentaires du même résultat, et renvoie explicitement au contre-exemple de Search-3 : le « théorème » admissible ⇒ optimal (c38/c39) est réfuté par l'implémentation du notebook lui-même — sa cellule 15 énonce pourtant la bonne condition #14824 : c'est le rapprochement le plus instructif que ces deux notebooks permettent — la borne formelle est vraie, la garantie qu'on lui prête est fausse, et l'écart entre les deux est la leçon.
6. consistent_implies_admissible : soit livré, soit les 6 mentions pointent le nom réellement présent.
7. C.2 : notebook re-exécuté, sorties committées ; lake build vert sur search_lean après renommage.

Vérifié firsthand sur origin/main (fichiers Lean lus intégralement, grep d'absence exécuté sur tout le lake, 24 cellules du notebook parcourues, c23 lue en entier) — pas depuis le rapport d'origine, dont je confirme par ailleurs la concession sur la section d'honnêteté.

See #14824 · See #4048