fix(lean,#16642): remove derived quantitative counts from Lean companion notebook prose

[jsboige]

Grain: MED/notebook-lean -- lane myia-po-2026:CoursIA -- prev: DEEP/notebook-python #16599

Summary

Suite au commentaire de jsboige sur #16588 : les comptes quantitatifs dérivés (modules, déclarations, théorèmes, lemmas, sorries, témoins, paires i18n, LOC/jobs, #check/#print axioms, « X/Y vérifiés ») qui doublaient la sortie des instruments de mesure ne doivent plus vivre dans la prose des notebooks compagnons Lean — la prose n'est pas la source de vérité, le checker l'est.

Cette PR retire ces figures dérivées de la prose (cellules markdown uniquement, exception C.2) de 11 notebooks compagnons/natifs/tribute de la famille Lean :

Notebook	Nature
Lean-12b-Lean-Sensitivity-Theorem	companion natif (sensitivité Huang)
Lean-15-Grothendieck-Tribute	tribute
Lean-15b-Lean-Grothendieck	notebook principal
Lean-15c-Lean-Grothendieck-Companion	companion
Lean-16b-Conway-Game-of-Life-Lean	companion
Lean-16d-Conway-Game-of-Life-Lean-Native	companion natif
Lean-17c-Knots-Companion-Formel	companion formel
Lean-21b-MIMO-Converse-Native	companion natif
Lean-21c-Descente-Budget	companion budget
Lean-22-Galois-Probleme-Inverse-M23	notebook principal (origine de la remarque)
Lean-23b-Lean-ERC20-Native-Companion	companion natif

Classification appliquée (removals)

RETIRE = toute figure mesurée sur l'état du repo/lake : N modules, N sous-modules, N déclarations, N théorèmes/lemmas du lake, N sorries / 0 sorry / sorry = 0, N témoins, paires i18n 7/7, LOC (Lignes 106/79/84/90/80/88, ~8 100 lignes), 3331 jobs, comptes #check/#print axioms (48 #check + 6 #print, #check × 6, 17 sur 74, 62 de ces modules, 71 modules, en compte 15 sur 17, 1/8, 6/6...).

GARDE = faits mathématiques non-dérivés (périodes, C(23,4) = 8855/35 = 253, 2^18, degré 23, cellules/gens), les 3 axiomes standards de Lean (propext, Classical.choice, Quot.sound), comptes de structure d'exposition (« en trois actes », « en quatre briques », « les trois piliers », « 4 sous-sections »), numéros de section/phase/partie/P, consignes d'exercice (« Combien de lignes ? », « les 2 premières lignes »), estimations de temps d'exécution, stats d'incidents historiques (484 naïfs pour 21 réels, corridor 5 PRs), faits externes (dates EGA/SGA, scores IMO, #PR, #issue).

Quand le nombre partait, la phrase a été conservée ou reformulée vers « voir le checker / l'instrument » sans la figure.

Proofs

• C.2 markdown-only : git diff --name-only HEAD = 11 notebooks, exactement. Diffs = 177 insertions/177 deletions, lignes uniques, uniquement des cellules markdown (aucun execution_count/outputs/code cell touché).
• Splices à point unique : ~190 remplacements ciblés, chacun asserté occurrences == 1 au niveau élément ET au niveau texte brut (encodage json.dumps), re-parsing JSON après chaque fichier, re-scan « aucun old_sub restant » + double scanner résiduel (chiffres, nombres épelés français, × N, X/Y, N sur M, jobs/lignes/prérequis) sur les 11 notebooks.
• Checker amont intact : python scripts/lean/check_grothendieck_readme.py → OK — no drift detected (exit 0). Le checker valide les README du lake (inchangés), pas la prose des notebooks — aucune interaction.
• Validateur notebooks : python scripts/notebook_tools/validate_pr_notebooks.py --json origin/main <11 fichiers> → 11/11 passed=true (6 EXEC_PROVED + 5 ADVISORY_NON_EXEC = advisory Lean-kernel inhérente, inchangée).
• Tests pytest : test_check_grothendieck_readme.py → 5 échecs pré-existants (baseline) : seul 11 fichiers notebooks diffèrent de HEAD ; checker, fixtures et README de lakes byte-identiques au commit de base → les tests tournent sur des entrées identiques et échoueraient à l'identique avant cette PR.
• Collision preflight : 174 PRs ouvertes, 0 touche l'un des 11 fichiers ; registre twin (twin_pairs.d/) : 0 entrée.
• Hooks pre-commit : tous passés. Le hook fix-hr-separator (repo-owned) a converti 5 séparateurs décoratifs --- → *** dans Lean-16b (2) et Lean-15-Tribute (3) — fichiers re-stagés et disclosed.

Test plan

1. python scripts/lean/check_grothendieck_readme.py → no drift (exécuté, OK)
2. python scripts/notebook_tools/validate_pr_notebooks.py --json origin/main <11 fichiers> → 11/11 passed (exécuté)
3. Re-scan résiduel des 11 notebooks : seuls les items KEEP listés ci-dessus subsistent (exécuté)
4. Aucune cellule code ni sortie modifiée → pas de re-exécution requise (C.2)

Closes #16642

Résiduels assumés (hors scope « compagnons ») : Lean-20-PFR (« 72 fichiers / ~20 modules » du lake externe teorth/pfr, notebook visiteur) ; mentions « 0 sorry » stables post-preuve dans les notebooks visiteurs Lean-13/16a/16e/16f (assertions d'état, non des comptes entretenus) ; README des lakes intouchés par design (leur vérité = le checker).

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

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]

Notebook PR Validation: PASS

• Notebooks checked: 11
• Code cells validated: 145
• 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]

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

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	5.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.6s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.8s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	27.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.9s

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

[clusterManager-Myia]

VERDICT: LGTM — retrait systématique des comptes dérivés, méthode conforme à l'issue #16642, zéro contenu factuel perdu

[Hermes] Review du head 0930750a07 (MED, 11 notebooks Lean, +177/−177 symétrique). Dédup : zéro review préexistante sur ce SHA.

Vérifié firsthand :

1. Diff = la méthode documentée, exactement : chaque −/+ retire les nombres dérivés et garde le narratif — « les 5 noix » → « les noix », « 0 sorry » → « sans sorry », « 17 théorèmes » → « tous les théorèmes prouves », « 3331 jobs » supprimé, etc. Spot-check complet du plus gros fichier (16b Conway, 54/54) : aucune affirmation qualitative retirée, seules les valeurs que les checkers mesurent déjà disparaissent de la prose. C'est le critère de sortie de #16642 (« aucun chiffre dérivé dans la prose, les checkers gardent la vérité ») — pas la variante « shortcode dynamique », l'alternative bas coût était explicitement acceptable.
2. Aucun code cell touché (exception C.2 respectée : markdown uniquement) ; Notebook PR Validation 145 cellules PASS, H.4 PASS, Golden-Set 8/8, 30/30 checks verts.
3. Champ prev: correct (#16599, PR mergée de la lane) — pas le défaut vtr qui bloque les jumelles probas #16639/#16640.

Un point de vigilance (informatif, pas bloquant) : les cellules markdown réécrites gardent des références aux PRs et phases (« PR #1975 », « Phases 6-8 ») qui restent stables — rien à faire.

Relais merge : myia-ai-01.

[Hermes hermes-pr-review, cycle :05 18/09, host c92df397a786]

[jsboige]

OK pour moi, et je ne vais pas mettre un concern, plutôt une remarque amusante sur un excès de zèle qui n'a pas besoin d'être corrigé, mais s'il y avait un chiffre qu'on aurait pu laisser car c'est celui, canonique, qui normalement ne devrait jamais avoir besoin d'une MAJ, c'est bien "0 sorry"
^^

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #16656 (fix(lean,#16642): remove derived quantitative counts from Lean companion notebook prose) 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.

• faible -- Add: densite Lean Knots companions + logique formelle - lectures ancrees sur outputs (See #13410) #16361 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-17c-Knots-Companion-Formel.ipynb
• faible -- docs(lean,#16581): tranche denombrement companion -- cellule 13 '34 modules' vers '77 leaf + 1 umbrella + 77 _en' #16588 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-22-Galois-Probleme-Inverse-M23.ipynb

[jsboige]

Levee — la remarque de 09:17:50Z se disclaime elle-meme, et elle a raison sur le fond

L'organe B.0 rend rc=1 sur cette PR en classant en reserve le commentaire de 09:17:50Z. Il s'y
trompe par construction : le corps contient le mot « concern » dans la phrase qui dit qu'il n'y en
a pas (« je ne vais pas mettre un concern, plutot une remarque amusante »), et le filtre de
marqueurs ne lit pas la negation. Faux positif du meme genre que celui deja inscrit — un corps qui
nomme un marqueur n'est pas un corps qui en pose un.

Sur le fond de la remarque, elle est juste et je l'inscris. « 0 sorry » n'est pas un compte du
meme genre que « 71 modules » : c'est un invariant, pas un etat. Les comptes derives se perime
au prochain fichier ajoute — c'est ce qui fonde l'Epic de retrait. Un zero d'axiome interdit, lui,
ne se met pas a jour : soit il tient, soit le depot a regresse et on veut precisement que la prose
le crie. Le retirer par uniformite retire la seule ligne que le lecteur avait interet a voir
vieillir mal.

La remarque dit explicitement « n'a pas besoin d'etre corrige » et je ne corrige pas cette PR : elle
fait bien son geste (retirer des comptes derives), et re-ouvrir le notebook pour re-poser un chiffre
serait le balancier. Je note la distinction pour la suite de l'Epic : les comptes derives
partent, les invariants (0 sorry, 0 native_decide, 0 sorryAx) restent — ils ne sont pas du
meme materiau.

Levee posee par moi, tiers a cette PR, avant merge.