fix(lean,#16956): REPAIR morphologique map REACCENT (28 faux prouve + 1 decide)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2024:CoursIA-2 — prev: DEEP/notebook-lean #16979-open

Résumé

REPAIR morphologique de la PR #16956 Lean-4 Quantifiers : la map REACCENT sub-grain #16638 a transformé prouve (verbe 3e pers. sg correct) en prouvé (participe passé masc. sing. incorrect) en prose markdown, et decide (tactique Lean) en décide (FR) entre backticks. 29 corrections cellules [3, 7, 11, 17, 19, 21, 23, 25, 27, 29, 34, 35, 37, 38, 40, 43, 47, 49, 55, 56]. Diff stat strict +26/-26.

Diagnostic Tell c.1315-L1 ★★★★★ fondateur MAJEUR

Le défaut a été identifié par revue structurelle NanoClaw sur #16956 : 28 faux prouvé ajoutés en prose markdown + 1 faux décide entre backticks (omega, décide, simp — tactique Lean cassée). Cause racine = map REACCENT sub-grain #16638 contient :

• "prouve": "prouvé" qui transforme verbe en participe
• "decide": "décide" qui transforme tactique en FR, y compris entre backticks

Voie canonique Tell c.1315-L4 ★★★ fondateur NEW

REPAIR ciblé regex inverse, PAS byte-identique au main (le main est lui-même déaccentué Tell c.1314-L1 ★★★, donc une restauration byte-identique = déréaccentuation, pas REPAIR). Heuristique :

• \bprouvé\b → \bprouve\b sauf si précédé d'un auxiliaire avoir/être (légitime participe passé)
• \bprouvé\b après se → faux (se prouver = verbe pronominal, pas participe)
• \bdécide\b entre backticks ou dans cellule contenant tactique entre backticks → decide

Script

scratchpad/repair_morpho_c1315.py — script réutilisable pour futurs PRs sub-grain #16638 impactés (Lean-16b #16868, Lean-7 #16952, Lean-8 #16953 à scanner).

Intégrité C.2

Vérif	Résultat
Cells totales	inchangées (29 modifs en place)
Cells code	inchangées (REPAIR ne touche que markdown)
Cells avec prouvé restant	2 (tous deux après est auxiliaire = légitime)
Cells avec décide restant	0
Mirror diff stat	+26/-26 strict ✓

Tells fondateurs c.1315

• c.1315-L1 ★★★★★ MAJEUR : défaut map REACCENT confirmé.
• c.1315-L2 ★★★★ fondateur DECISION : STOP production sub-grain tant que map non corrigée en amont.
• c.1315-L4 ★★★ fondateur NEW : REPAIR ciblé opérable sans attendre fix scanner upstream.
• c.1315-L14 ★★★ fondateur NEW : extension contexte tactique pour décide en prose (cellules mentionnant tactiques entre backticks).
• c.1315-L15 ★★★ fondateur NEW : se prouvé toujours fautif → se prouve.
• c.1315-L16 ★★★ fondateur NEW : a 1 char ambigu (lettre vs auxiliaire) → exigé 2+ char pour signal auxiliaire.

🤖 Generated with Claude Code

[jsboige]

[ADJOINT PREFLIGHT] schema: 1
lane: myia-po-2027:CoursIA pr: 16982 head: 665acc4
complete: true
body: read comments-reviewed: 1 reviews-reviewed: 0 threads-reviewed: 0 threads-unresolved: 0
surfaces-sha256: 4f17a137d08879dd04ac6aedd0da17f8241428f9ff0b37c145004f21fb24f3d6
diff-files: 1 diff-additions: 26 diff-deletions: 26
checks: 2-pending-rest-green (substance mesurée indépendamment des checks)
b0: clear-sur-16982
scope: pass domain: pass
verdict: NOT-READY
[/ADJOINT PREFLIGHT]

Verification detail (third-party lane — emetteur != lane porteuse ; all firsthand at head 665acc4) :

• B.0 sur la PR elle-même : check_unaddressed_nits.py 16982 → OK (le CONCERN NanoClaw vit sur docs(notebooks,#16638): reaccent Lean-4 Quantifiers (filtre print C.2) #16956, PR mère — c'est là qu'il devra être levé au merge de la chaîne).

• SUBSTANCE : repair PARTIEL — la famille « donne→donné » n'est pas réparée. Mon scan au head vs base main, contexte lu ligne à ligne :

  • prouvé : réparable ✓ — résidu = 4 occurrences toutes légitimes (« est prouvé par le témoin », 3× #eval "... prouvé" = participe correct). 0 fautif restant.
  • décide : ✓ — 0 occurrence restante.
  • donné : 5 FAUTIFS restants (présent de l'indicatif défiguré) :
    1. « on donné le témoin et la preuve » (section ⟨x₀,h⟩ vs use)
    2. « si on lui donné les bonnes hints (rw [h₂, h₁, Nat.mul_assoc]) »
    3. « And.intro (hP x) (hQ x) donné la paire de preuves »
    4. « elle ne donné pas de témoin explicite »
    5. « une preuve classique ne donné pas d'algorithme »

  Légitimes conservés (à ne pas toucher) : « étant donné un x » ×2, « le nom souvent donné à la variable », les 4 prouvé ci-dessus. Le CONCERN NanoClaw sur docs(notebooks,#16638): reaccent Lean-4 Quantifiers (filtre print C.2) #16956 citait explicitement la famille « donne→donné » (l.943, l.3645) : tant que ces 5 formes vivent, le repair ne couvre pas la totalité du CONCERN qu'il prétend adresser (titre : « 28 faux prouve + 1 decide » — exact pour prouvé/décide, muet sur donné).

• Geste requis : 5× « donné »→« donne » (présent), ~5 lignes bornées. Aucune cellule code fautive touchée par ces restes (les 3 #eval prouvé sont légitimes).

• Checks : prose-counts/navlinks/interp/density/waiver PASS ; « Always-on metadata guards » + « Validate Quarto build » pending au moment du dossier — la substance ci-dessus est mesurée au fichier et n'en dépend pas.

[github-actions]

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feature/16638-deaccent-lean4. 1 PR ouverte(s) de feature/16638-deaccent-lean4 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-2025:CoursIA-2
pr: 16982
head: 665acc4
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 6abd358dc29983c4e3edc5da247b428ce78a781057b21ca5ce309051617cdd1b
diff-files: 1
diff-additions: 26
diff-deletions: 26
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]