[GameTheory] FairBot et Abstraction : re-mesure des consommateurs — 06k importe FairBot, la racine Abstraction.lean reste sans consommateur (suivi #20316) #21774

Part of #20316 (étude de numérotation GameTheory — sous-grain demandé par ai-01, c.6109879992 : « FairBot (0 importeur) et Abstraction/Basic (orphelin). Ces points sortent des déplacements : une issue de suivi, ouverte par la lane, tranche entre l'import manquant et la marche manquante »).

Mesure sur origin/main (2026-10-21, git grep sur les fichiers suivis)

Précisions de mesure :

• git grep -ln "import.*FairBot" origin/main -- "MyIA.AI.Notebooks/GameTheory/**/*.lean" → vide. git grep -ln "FairBot" origin/main -- "*.ipynb" → 5 carnets, dont GameTheory-06k-FairBot-Loeb-Lean.ipynb qui l'importe explicitement (les autres le citent en prose ou consomment un autre module — Lean-34b importe FormalLogic.FairBotLoeb, un lake distinct).
• Abstraction.lean déclare dans sa docstring formaliser « la dette d'abstraction mesurée par GameTheory-19-Abstraction-a-Dette-Python.ipynb » ; or GT-19 est un carnet Python (imports itertools/random), il ne peut pas consommer un module Lean. Le lien annoncé est documentaire, pas un import.
• Le lakefile.lean déclare bien les deux cibles (lean_lib Abstraction avec globs := #[Abstraction.*]`, bloc ProgramGames incluant FairBot) : le build ne les omet pas.

Ce que ce constat n'est pas

• FairBot : pas un import manquant — son usage réel est le carnet 06k, exécuté par kernel Lean. Rien à réparer.
• Abstraction/Basic : pas un orphelin — il est importé par sa racine. La formulation « Abstraction/Basic (orphelin) » du commentaire c.6109879992 désigne en réalité la racine Abstraction.lean.

Question à trancher

Abstraction.lean (racine) n'a aucun consommateur Lean ni carnet Lean. Deux lectures possibles :

1. Marche manquante — GT-19 est Python ; si l'on veut que la formalisation soit exécutée par un carnet, il manque un carnet Lean (ou des cellules Lean dans GT-19) important Abstraction. Le module serait alors le seul lake GameTheory dont la preuve miroir n'est jamais chargée par un kernel.
2. Artefact de formalisation autonome — la preuve existe comme statut formel vérifié par lake build, sans consommateur pédagogique. Acceptable si c'est un choix assumé (comme une preuve de référence), mais il faut alors le dire dans le README de la série, sinon un relecteur le prendra pour un oubli.

Recommandation

Trancher (1) ou (2) — la décision est pédagogique, elle appartient au mainteneur ou au coordinateur. Dans les deux cas, aucun renommage ni déplacement n'est requis par ce constat : la table de la carte cible (#20316, phase 1) n'est pas affectée.

Aucun geste de cette lane au-delà de l'ouverture de cette issue : les chemins Dynamics/**, README.md et le lakefile sont sous claim myia-po-2023:CoursIA-2 (T3, #20374 CLOSED non mergée).

🤖 Generated with Claude Code