[Lean][infra] Carte du materiel Lean et regle d'accretion d'un lac (suite de #4365) #23097

Part of #4362

D'où vient cette issue

Concern de jsboigeEPF sur la PR #23030, verbatim :

Quid de https://github.com/jsboige/CoursIA/blob/main/MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Arrow.lean ? Il faut un vrai audit et une consolidation du matériel Lean du dépôt […] trop où sont les choses en l'état. On avait fait un effort pour commencer à rassembler ce qui pouvait l'être. L'effort n'a pas été suivi et l'entropie a repris le dessus. Prévoir une issue spécifique.

Cette issue est cette issue spécifique. Le Concern porte deux affirmations : l'effort n'a pas été suivi, et l'entropie a repris le dessus. La mesure départage les deux, et le résultat n'est pas celui qu'on attendait.

Première mesure — l'état, rejouable

Six plus gros lacs, en modules propres : grothendieck_lean 196, conway_lean 91, learning_theory_lean 62, game_theory_lean 62, discrepancy_lean 54, knot_lean 47.

Deuxième mesure — l'effort a bien été suivi, et il a été fermé sur mesure

#4365 — « Regrouper les lakes cohésifs (GameTheory 6→2) » — est CLOSED depuis le 2026-08-14, et sa fermeture n'est pas un label : ai-01 y a repris les trois critères d'acceptance un par un contre main. Verdict mesuré, verbatim de la clôture :

Donc l'effort a été suivi, mesuré, et clos avec son résidu nommé.

Troisième mesure — ce qui a repris, c'est l'accrétion, pas la dispersion

Dates d'ajout du lakefile de chaque lac GameTheory (git log -1 --diff-filter=A), contre la date de clôture de #4365 (2026-08-14) :

Deux lacs sont nés dans les deux semaines qui ont suivi la clôture de la consolidation, et game_theory_lean est passé de 47 à 62 modules. Ce n'est pas la consolidation qui a échoué : c'est la série qui a ré-accrété après elle. #4365 ne pouvait pas couvrir des lacs qui n'existaient pas encore, et il n'existe aujourd'hui aucune règle qui dise si un nouveau lac de série est légitime ou s'il doit être un module de plus dans le lac de la série.

C'est le vrai sujet de cette issue, et il est structurel, pas historique.

Ce que la mesure écarte aussi

Aucune duplication de preuves entre lacs. Les seuls noms de modules qui se répètent sont des conventions : lakefile.lean (36), Basic.lean (19), Basic_en.lean (16), Examples.lean (3). Aucun théorème n'est prouvé deux fois sous le même nom de module dans deux lacs. Consolider ne veut donc pas dire « fusionner des doublons » — il n'y en a pas.

Et le gate d'axiomes le dit lui-même, verbatim :

Cette couverture est une MESURE, pas un verdict de sûreté : un lake sans gate d'axiomes n'est pas illicite, il doit seulement être CONNU comme tel (#17097 critère 3).

Donc cette issue ne demande pas de câbler treize gates. Elle demande que les treize soient connus, et qu'une règle d'accrétion existe.

Tranches, dans l'ordre

T1 — La carte datée, et l'organe qui la régénère

Une page docs/reference/lean-material-map.md : par lac — chemin, modules propres, miroirs _en, présence au ci_lakes.json, verdict du gate d'axiomes, dette distinct_code_sorry, et date de naissance du lac. Plus l'organe qui la produit (scripts/lean/lean_material_map.py --json --check), parce qu'une table recopiée à la main dérive à chaque merge — c'est la maladie que l'issue soigne, et la colonne « date de naissance » est ce qui rend l'accrétion visible sans recherche git.

Sortie : la page, et --check qui échoue quand page et arbre divergent.

T2 — La règle d'accrétion d'un lac (la tranche qui décide)

Un lac nouveau dans une série existante : quand est-ce légitime ? Trois cas à trancher, chacun avec sa mesure :

1. Toolchain divergente → légitime (social_choice_lean_peters, INTRINSIC docs(gt,#4365): document INTRINSIC verdict for social_choice_lean_peters #7081). Rien à changer.
2. Théorie distincte → légitime (minimax, conway_cgt), déjà tranché par la clause anti-god-lake de [Lean][infra] Regrouper les lakes cohesifs post-convergence (GameTheory 6->2, modele multi-module) #4365.
3. Même théorie, même toolchain → c'est le cas non couvert. assignment_lean et asymmetric_information_lean sont-ils 1 et 3 ? La question se tranche en lisant SocialChoice/ et les imports, pas par principe.

Sortie : une phrase de règle, écrite là où un contributeur la lira (README de la série + docs/reference/lean-material-map.md), et pour les deux lacs récents, soit un statut documenté, soit un grain de fusion ouvert séparément.

T3 — lean_game_defs et lean_game_defs_ext : un lac ou deux ?

Douze et vingt-huit modules, le second nommé comme l'extension du premier. Lire les deux lakefile et les imports croisés, puis dire si _ext est une extension réelle (le nom doit alors le dire et le lakefile le refléter) ou un lac indépendant (le nom est alors trompeur). Le geste par défaut est documenter ; la fusion n'est retenue que si elle ne casse aucun import de notebook.

T4 — Les treize sans gate, déclarés connus

Publier dans docs/reference/lean-axiom-coverage.md la liste des treize lacs avec, pour chacun, la raison (lac externe, build trop lourd, jamais câblé). La liste est déjà produite par l'organe ; il s'agit de la publier au lieu de la laisser dans une sortie de commande. Critère 3 de #17097, coût CI nul.

Acceptance

• T1 : la page existe, lean_material_map.py --check rend 0 sur main, et régénérer la page depuis l'arbre redonne le même fichier
• T2 : la règle d'accrétion est écrite en une phrase, et assignment_lean / asymmetric_information_lean reçoivent chacun un verdict explicite (légitime-documenté, ou grain de fusion ouvert et nommé)
• T3 : la décision est écrite avec sa mesure (imports croisés, contenu des deux lakefile), et le lakefile ou le nom reflète la décision
• T4 : les treize lacs sont énumérés dans lean-axiom-coverage.md avec leur raison
• Aucun sorry ajouté : count_code_sorry.py --json distinct_code_sorry mesuré avant/après chaque tranche, non augmenté

Ce que cette issue n'est pas

• Ce n'est pas une réouverture de [Lean][infra] Regrouper les lakes cohesifs post-convergence (GameTheory 6->2, modele multi-module) #4365 : celui-ci a livré ce qu'il annonçait, mesuré pièce par pièce, et sa clôture est fondée. L'objet ici est l'après, qui n'avait pas été couvert.
• Ce n'est pas un mandat de câbler treize gates d'axiomes : l'organe de couverture dit lui-même que la couverture n'est pas un verdict de sûreté.
• Ce n'est pas une fusion décidée d'avance : T2 et T3 se tranchent par la mesure, et le défaut de repli est de documenter, pas de déplacer.
• Ce n'est pas une revue de traduction : les 384 miroirs _en sont une dimension de la carte (T1), pas un chantier ici.

🤖 Generated with Claude Code