Lean-22 companion : compte de modules grothendieck_lean triple (prose 34 / run 150 / README 75+1) — reconciliation requise #16581

Source : reserves 1 et 2 de la review [Hermes] COMMENT_WITH_CONCERNS sur #16256 (2026-09-17T18:03Z), confirmees par la re-mesure NanoClaw 19:37Z au head dbfdddf — non bloquantes pour #16256 (phrase preexistante, absente du diff), tracees ici pour ne pas se perdre.

Constat

Trois nombres coexistent pour le meme lake sous les yeux du lecteur du companion Lean-22 (MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb) :

1. Prose markdown (preexistante sur main) : « grothendieck_lean (34 modules, 0 sorry) » — cellule au-dessus de la cellule 5.
2. Sortie re-executee (committee via feat(lean,#11703): annexe du companion Lean-22 — complétion adique et ramification inférieure #16256) : « grothendieck_lean : 150 modules .lean sous Grothendieck/ » (base : 96).
3. README du lake : « 75 modules leaf + 1 umbrella » (151 sources, 152 fichiers .lean sur disque).

Cause

La migration Mathlib 4.33 (#14773) et les livraisons successives de modules galois ont fait croitre le compte de 34 a 150 ; la prose n a pas suivi. Par ailleurs le libele « modules » compte des fichiers, dont les siblings _en, ce qui double mecaniquement le nombre affiche (75 reels vs 150 fichiers).

Acceptance

• Reconcilier les trois surfaces (prose du companion, sortie de la cellule 5, README du lake) sur un compte et un libele coherents (modules reels vs fichiers, _en exclus ou libelle explicite).
• Verifier les autres companions citant des comptes de modules galois (grep « modules » sur les notebooks Lean-* du meme lake).
• Grain MED/docs ou readme, pas de re-execution requise si prose seule (exception C.2 markdown-only) ; sinon re-executer.

Ne pas merger #16256 en attendant : les deux reserves sont traitees (grain separe ici + argument dans l approbation).