fix(search,#16705): Search-03e ré-exécuté post-#16677 — théorème fantôme éradiqué

[jsboige]

Grain: LIGHT/notebook-rerun -- lane myia-po-2026:CoursIA -- prev: LIGHT/deaccent #16659

Closes #16705

Ce que fait cette PR

1. Ré-exécution de Search-03e-AStar-Optimality.ipynb (kernel python3, outil dédié notebook_tools.py execute, SUCCESS 4,8 s) : les sorties réaffichent le contenu réel des fichiers .lean post-renommage docs(lean,#16651): purge references consistent_implies_admissible (theoreme fantome) au profit de consistent_implies_admissible_bound #16677. Jamais d'édition manuelle des outputs (règle 6 secrets-hygiene) — la cause était en amont.
2. Résiduel traité à la source : le commentaire d'en-tête Consistency.lean:9 (et siblings Consistency_en.lean:15, Astar.en.md:162) menait par le nom cible historique consistent_implies_admissible avec parenthèse « prouvé sous le nom …_bound ». Reformulé pour mener par le nom réel consistent_implies_admissible_bound (référence [Lean][Search] Créer astar_lean — A* : admissibilité ⇒ optimalité #4048 et filiation consistent_implies_path_bound conservées).

Preuves

• Death-check de l'issue : git grep -cE 'consistent_implies_admissible([^_]|$)' sur le notebook → 0 (était 3).
• Étendu à tout MyIA.AI.Notebooks/Search/ → 0 hit (notebook + 2 .lean + .en.md).
• 11 cellules code : execution_count + outputs cohérents (C.2), 0 erreur, _bound présent dans les sorties.
• lake build : NON EXÉCUTÉ dans le notebook par design (LEAN_BUILD_ALLOWED_HERE = False, arrêt user 2026-08-30 po-2023 inchangé).
• Diff +128/−128 sur 4 fichiers, aucune réécriture structurelle ; normalisation metadata.papermill au basename (autorisation explicite secrets-hygiene).

🤖 Generated with Claude Code

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-18) :

• GENRE-UNKNOWN : le genre canonise `rerun` est hors enumeration close -- trou d'adjacence G-VAR-3, requalifier le genre dans le body (Un genre hors énumération passe silencieusement : canonicalize_genre le rend tel quel, aucun signal, adjacence G-VAR-3 inatteignable #12158)

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	2.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.2s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	3.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.7s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.1s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.0s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	15.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.6s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 11
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16707 (fix(search,#16705): Search-03e ré-exécuté post-#16677 — théorème fantôme éradiqué) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• terminal -- docs(lean,#16651): purge references consistent_implies_admissible (theoreme fantome) au profit de consistent_implies_admissible_bound #16677 partage : MyIA.AI.Notebooks/Search/search_lean/Astar.en.md, MyIA.AI.Notebooks/Search/search_lean/Astar/Consistency.lean, MyIA.AI.Notebooks/Search/search_lean/Astar/Consistency_en.lean, recouvrement de chemins 50% -- docs(lean,#16651): purge references consistent_implies_admissible (theoreme fantome) au profit de consistent_implies_admissible_bound #16677 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.