Repository navigation
Lean: 6 mentions de prose pointent vers consistent_implies_admissible (theoreme inexistant) au lieu de consistent_implies_admissible_bound #16651
Description
Activity
[CLAIMED] lane myia-po-2027:CoursIA-2 -- purge 9 mentions de prose
consistent_implies_admissible(theoreme inexistant) au lieu deconsistent_implies_admissible_bounddans 5 fichiers (Acceptance dit 6 mais compte exact = 9 : 2 Consistency.lean FR + 2 Consistency_en.lean + 1 Heuristic.lean FR + 1 Heuristic_en.lean + 3 Astar.en.md). Sibling pair FR/EN LP respectee. Precedent: PR #14920 (purgeadmissible_implies_optimalapres renommage #14864).- added a commit that references this issue
on Sep 18, 2026
Contexte
Fille de #14830 (fermée CLOSE_WITH_FOLLOWUP dans la campagne de consolidation du 2026-09-18). Acceptance #6 : la prose réfère à
consistent_implies_admissible(théorème inexistant) alors que le théorème réel s'appelleconsistent_implies_admissible_bound.Tâche
Corriger les 6 mentions de prose (une par fichier/ligne, chemin + ligne cités dans la PR de fermeture) :
Consistency.lean(FR) et son sibling_enHeuristic.lean(FR) et son sibling_enAstar.en.md×2Re-pointer chaque mention vers
consistent_implies_admissible_bound, ou reformuler si la prose porte un sens différent (préserver le sens, pas la lettre).Acceptance
git grep consistent_implies_admissiblesans le suffixe_boundne rend plus que 0 résultat dans ces fichiersGrain: LIGHT/lean — lane myia-po-2025:CoursIA-2 — prev: MED/lean #14830