fix(lean,#16952): REPAIR-3 morphologique map REACCENT (0 donne + 1 prouve fautifs)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2024:CoursIA-2 — prev: MED/notebook-lean #16994-REPAIR-3-merge

Résumé

REPAIR-3 morphologique de la PR #16952 Lean-7 LLM Integration : map REACCENT sub-grain #16638 a transformé donne (verbe) en donné (participe) et prouve (verbe) en prouvé (participe) en prose markdown. 0 donne + 1 prouve corrections cellules [27].

Diagnostic Tell c.1319-L1 ★★★★ fondateur NEW

Batch REPAIR-3 final sur les 8 PRs sub-grain #16638 restantes non REPAIRed c.1315-c.1318. Total : 1 corrections c.1319 + 35 corrections c.1318 + 82 c.1315-c.1316 + 33 c.1317 = 151 corrections totales REPAIR morphologique sub-grain #16638.

Voie canonique Tell c.1315-L4 ★★★ fondateur NEW (étendue c.1317)

Script repair_morpho_c1318.py avec heuristiques complètes (Tell c.1318-L2 ★★★★).

Intégrité C.2

Vérif	Résultat
Cells totales	inchangées
Cells code	inchangées (REPAIR ne touche que markdown)
Corrections réelles	1 (0 donne + 1 prouve)

🤖 Generated with Claude Code

[github-actions]

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feature/16638-deaccent-lean7. 1 PR ouverte(s) de feature/16638-deaccent-lean7 vers main existe(nt) a cet instant -- c'est un stack legitime, le contenu est en vol. Verifier au moment du merge que la base est effectivement reliee a main.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA
pr: 17003
head: 61e7782
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 1bb4395555ce9deeec5754c2a1b0f972c5c99beff3decdf160d01977866e657a
diff-files: 1
diff-additions: 1
diff-deletions: 61
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Dossier READY — la PR est propre sur la classe morphologique qui bloque ses sœurs de vague (cf #16991/#16992/#16993/#16994/#16997/#16998/#17001/#17002).

Vérifié firsthand au head exact 61e7782 (19:1xZ) :

• Checks : 7 success / 3 skipped / 0 fail au head (best-of-per-name). Diff : 1 fichier (Lean-7-LLM-Integration.ipynb), +1/−61 — les 60 lignes nettes négatives = ré-sérialisation JSON mono-ligne d'une cellule (§6.4 Prompt Engineering), rendu identique ; 0 output / 0 execution_count modifié ; Grain tag ligne 1 lu ; 0 review, 0 thread, commentaire bot BASE-NOT-MAIN lu (stack feature/16638-deaccent-lean7).

Le seul changement textuel de la classe est CORRECT : « Maintenant prouvé → prouve : » — l'occurrence est à l'intérieur d'un bloc de code clôturé (```) qui expose un prompt few-shot destiné au LLM, en troisième position après « Exemple 1: theorem ... := by exact ... » et « Exemple 2: theorem ... := by exact ... ». La forme est l'impératif adressé au modèle (« Maintenant prouve :\ntheorem add_mul_comm (a b c : Nat) : (a + b) * c = a * c + b * c ») — « prouve » sans accent est l'impératif correct de « prouver » ; l'ancien « prouvé » (participe) était la faute. Aucun accent correct détruit, contrairement à #17001 où « non prouvé » adjectival a été cassé dans un contexte comparable : ici la fonction grammaticale est impérative, pas adjectivale.

Contrôles croisés : motif de dépistage souple (est|sont|a|été|ont)[...]{0,28}\b(prouve|donne)\b appliqué au texte ajouté = 0 occurrence (aucun passif, même non adjacent) ; « donné » au sens « données » conservé intact ; « théorème cible », « a prouver » (infinitif) conservés sans changement ; 0 sorry.

Aucune réserve. B.0 clear.

— adjoint preflight, lane myia-po-2026:CoursIA (tierce)