[Lean-22 companion] Retraite des comptes quantitatifs derive dans la prose #16642

Objet

Issue de suivi pour la retraite du compte quantitatif dans la cellule 13 du notebook compagnon Grothendieck_M23 (parent: #16581).

Pourquoi

Le PR #16588 a aligne 34 modules -> 77 leaf + 1 umbrella + 77 _en, mais la remarque user (jsboige) sur #16588 est de fond : MAJ perpetuelle des comptes = anti-pattern. La voie d'avenir est le retrait des references quantitatives dans la prose quand elles sont derivees (le checker mesure, la prose n'en parle plus).

Plan

1. Choisir 1 cellule dans chaque notebook compagnon Lean ou le compte quantitatif derive est lit : passer en reference dynamique via un shortcode ou un include.
2. Le checker (scripts/lean/check_grothendieck_readme.py + soeurs) garde la verite, la prose ne la repete plus.
3. Alternative bas cout : retirer purement la ligne (le linter trivial-diff-15740 flaggait deja +1/-1 papercuts).

Critere de sortie

• Aucun chiffre derive dans la prose des notebooks compagnons Lean.
• Les checkers anti-recidive tournent toujours.
• Les papercuts +1/-1 disparaissent du garde.

Origine

C.1259 — issue ouverte en réponse à la CR de jsboige sur #16588 (papier-a-cigarette anti-pattern).

🤖 Generated with Claude Code