docs(lean,#16651): purge references consistent_implies_admissible (theoreme fantome) au profit de consistent_implies_admissible_bound

[jsboige]

Grain: LIGHT/lean — lane myia-po-2027:CoursIA-2 — prev: MED/notebook-python #16218

docs(lean,#16651): purge references consistent_implies_admissible (theoreme fantome) au profit de consistent_implies_admissible_bound (prouve)

Acceptance

Issue #16651, fille de #14830 (fermee CLOSE_WITH_FOLLOWUP) — la prose du lake search_lean refere a consistent_implies_admissible (theoreme inexistant) au lieu de consistent_implies_admissible_bound (corollaire de consistent_implies_path_bound, 0 sorry, prouve dans Astar/Consistency.lean).

Substance : la cible #4048 EST consistent_implies_admissible, mais le theoreme prouve dans ce lake est consistent_implies_admissible_bound. La prose parlait du nom de cible dans certains contextes et du nom du prouve dans d'autres. Je preserve la cible avec clarification explicite, et je pointe vers _bound la ou le contexte parle du prouve.

Compte exact des mentions corrigees

Acceptance dit 6 mentions dans 5 fichiers ; compte exact = 9 mentions dans 5 fichiers acceptance. J'ai couvert les 9 + 1 dans search_lean/README.md (coherence, meme theoreme-fantome dans une checklist). Total 10 mentions / 6 fichiers.

Fichier	Mentions	Nature
Astar/Consistency.lean	2 (l.9, l.46)	prose module + docstring theorem
Astar/Consistency_en.lean	2 (l.15, l.54)	prose module + docstring theorem
Astar/Heuristic.lean	1 (l.35)	docstring Consistent
Astar/Heuristic_en.lean	1 (l.41)	docstring Consistent
Astar.en.md	3 (l.92, l.162, l.177)	section Consistent + module docstring + theorem docstring
search_lean/README.md	1 (l.207)	checklist phase 2 (coherence, hors acceptance)

Strategie de correction

Distinction cible vs prouve preservee :

• Contexte "Issue [Lean][Search] Créer astar_lean — A* : admissibilité ⇒ optimalité #4048" / "Target theorem" : preserve le nom de cible + ajoute clarification explicite que le prouve est _bound
• Contexte "Consistency implies admissibility" / docstring theorem : remplace par _bound directement

Aucune signature de preuve touchee : 6 fichiers = 6 modifications dans des prose/module-docstrings/docstrings uniquement. Le code Lean (theorems, tactics, definitions) reste byte-identique.

Sibling pair FR/EN LP respectee

Les modifications FR/EN sont paralleles : meme structure, meme semantique (cible vs prouve). Seul le texte traduit differe (convention i18n Lean #4980). Verification par diff parallele :

• Consistency.lean l.9 (FR) ⇔ Consistency_en.lean l.15 (EN) : meme clarification cible
• Consistency.lean l.46 (FR) ⇔ Consistency_en.lean l.54 (EN) : meme remplacement _bound
• Heuristic.lean l.35 (FR) ⇔ Heuristic_en.lean l.41 (EN) : meme clarification avec reference cross-fichier

Hors scope (mentionne pour info, non touchees)

Fichier	Mention	Raison
.github/workflows/lean-search.yml l.6	commentaire historique	commentaire d'en-tete de workflow, hors acceptance
MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb	5 occurrences (l.645, l.1001, l.1038, l.1087, l.1158)	notebook — ratchet Papermill, hors acceptance explicite
translations/symbolicai-lean/symbolicai-lean.csv	1 ligne traduite	CSV derive, hors scope

Ces mentions peuvent faire l'objet d'une issue de suivi si souhaite, mais ne sont pas dans le perimetre de #16651.

Verification finale

$ git grep -nE "(^|[^_])consistent_implies_admissible\b" MyIA.AI.Notebooks/Search/search_lean/
Astar.en.md:162:Issue #4048 (target: theorem `consistent_implies_admissible` — proven in this lake under the name `consistent_implies_admissible_bound`, corollary of `consistent_implies_path_bound`). **Consistency**
Astar/Consistency.lean:9:Issue #4048 (cible : théorème `consistent_implies_admissible` — prouvé dans ce lake sous le nom `consistent_implies_admissible_bound`, corollaire de `consistent_implies_path_bound`). La **consistance**
Astar/Consistency_en.lean:15:Issue #4048 (target: theorem `consistent_implies_admissible` — proven in this lake under the name `consistent_implies_admissible_bound`, corollary of `consistent_implies_path_bound`). **Consistency**

3 mentions restantes = toutes des references a la CIBLE avec clarification explicite. Aucune mention "fantome" (non clarifiee) ne subsiste.

Precedent

PR #14920 (2026-09-09) purge des references residuelles a admissible_implies_optimal apres renommage #14864 — meme mecanique, 7 fichiers edites a la main (CSV derive non touche, conforme a cette PR). Cette PR-ci est la deuxieme vague de purge, sur les modules Consistency + Heuristic du meme lake.

Stats

• 6 fichiers modifies, +10 / -10 (changements strictement paralleles)
• 0 signature Lean touchee, 0 cellule code modifiee
• 0 notebook touche (ratchet Papermill preserve)
• Sibling pair FR/EN parallele : 3 paires module-docstring coherentes

Tells respectes

• Tell c.14323 ★★★ fondateur cross-lane incident (compte jsboige partage entre lanes, adoption scenario 1, claim pose avant edit, DM acquittement)
• Tell c.14451 ★★ LIVRAISON RECENTE fondateur strict (verification upstream : aucune PR/branch existante, aucun worktree orphelin sur ce chemin)
• Tell c.488 strict audit-reassessment transversal (substance documentee, mesure firsthand du compte exact)
• Tell c.677-L4 ★★ body PR genere HORS worktree (scratchpad $TEMP/pr16651_body.md)
• Tell c.984 strict gh pr list avant create (verifie : pas de PR existante sur 16651)
• Tell c.974 strict 1 cycle (ce commit est le seul de la PR)
• Tell c.1356 ★★★ preflight first-hand (3 organes : issue body, artefacts disque, plateau PR)
• Tell c.1502 ××99ᵉ strict (worker ne merge pas — ripe transmise a ai-01)

Issue

Closes #16651

[jsboige]

Merge — la réserve de périmètre est levée par #16705, ouverte avant ce merge

Le corps annonce honnêtement 5 occurrences laissées dans Search-03e-AStar-Optimality.ipynb. Je
les ai mesurées, et elles ne sont pas ce qu'elles paraissent : au head 25bd6f4fe, le notebook
porte 0 occurrence dans ses source et 3 dans ses outputs — des sorties stream où le
notebook imprime le contenu des .lean avec numéros de ligne (9 | Issue #4048, théorème cible…,
46 | (…). Une heuristique consistante nulle au but…).

Conséquence, et elle inverse la conclusion : il ne faut surtout pas les purger. Ce sont des
outputs — les maquiller à la main est interdit (secrets-hygiene règle 6). Et comme cette PR
renomme précisément ces lignes-là dans Consistency.lean, elle crée une dérive source ↔ sortie
qui n'existait pas avant elle : la seule sortie honnête est une ré-exécution, pas une réécriture.

C'est l'objet de #16705, ouverte avant ce merge, avec sa commande de réfutation
(git grep -c … -- Search-03e-*.ipynb doit rendre 0, aujourd'hui 3).

Ce qui justifie de merger malgré la dérive

Le nom nu est un fantôme vérifié — les deux seules déclarations du dépôt portent _bound :

search_lean/Astar/Consistency.lean:95     theorem consistent_implies_admissible_bound …
search_lean/Astar/Consistency_en.lean:103 theorem consistent_implies_admissible_bound …

La PR fait passer les occurrences actives de 11 lignes à 3 (le notebook, traité par #16705) plus 1
commentaire d'en-tête dans .github/workflows/lean-search.yml:6 — un commentaire, pas une cible
de gate : aucun organe ne s'appuie dessus, et §E interdit d'en faire une PR à soi seul. Tenir
cette PR laisserait le fantôme sur les 6 fichiers de prose aussi. Le net est positif, le résidu est
nommé.

Diff trois points vérifié : 6 fichiers, 10 insertions / 10 deletions, siblings FR/EN traités
symétriquement. CLEAN, 0 check en échec, check_unaddressed_nits rc=0, aucun thread inline.

🤖 Generated with Claude Code