i18n Lean : relecture semantique des docstrings traduites + organe de fidelite par jetons

Part of #4980

Constat (lecture firsthand au head `48498505`, 2026-11-02)

La vérification mécanique de la convention i18n Lean (#4980) porte sur ce qui est structurel : le nombre de corps de commentaires, leur ordre, l'intégrité byte-identique du code hors commentaires, et l'absence de corps « suspects » en français dans le miroir _en. Elle ne porte pas sur la fidélité sémantique de la traduction : une phrase peut garder tous ses identifiants, tous ses nombres et tous ses spans de code, et glosser un adverbe.

Une mesure de ce type a été faite sur la paire Knots/ArcPartition_en.lean / Knots/ArcPartition.lean à l'occasion de la revue structurelle de la PR #24138 :

Mesure (67 corps de commentaires, head `48498505`)	Résultat
paires comparées	67 / 67
spans de code perdus	0
nombres perdus	0
identifiants techniques perdus	0
paires portant au moins un écart	1 (l'en-tête de tranche, référence croisée FR/EN — symétrique par construction)

Cette mesure borne la perte de contenu technique ; elle ne relit pas les 65 traductions phrase à phrase. L'outil qui la produit n'est pas dans le dépôt : la mesure n'est donc rejouable par personne d'autre en l'état.

Contenu

Deux volets, dans cet ordre :

Relecture phrase à phrase des 65 docstrings du miroir Knots/ArcPartition_en.lean contre leur canonique FR, et correction de toute dérive de sens constatée. Le contrôle mécanique ne peut pas la remplacer : il mesure la présence des jetons, pas leur valeur.
Organe réutilisable scripts/lean/check_i18n_token_fidelity.py : comparaison, par paire canonique/miroir, des spans de code entre accents graves, des nombres et des identifiants techniques (ceux qui contiennent un tiret bas ou une majuscule interne), sur le modèle de scripts/lean/check_i18n_siblings.py. Le rapport doit nommer la paire et le corps fautif, et distinguer un écart de contenu d'un écart de désignation (l'en-tête de tranche se nomme mutuellement : ce cas est attendu et ne doit pas rougir).

Acceptance

chaque écart résiduel de relecture est corrigé dans le miroir _en, ou explicitement documenté s'il est intentionnel ;
l'organe tourne sur l'ensemble du dépôt et rend un rapport lisible, sans faux positif sur les paires dont le seul écart est une désignation croisée ;
le test de l'organe est ajouté à scripts/lean/tests/ et passe ;
aucune régression i18n : les lakes du manifeste conservent 0 drift, 0 orphan, 0 unbuilt après passage de l'organe.

Provenance

Réserve mineure de la revue structurelle de la PR #24138 (siège myia-ai-01, 2026-11-02 05:17Z) : « traductions échantillonnées, pas toutes relues », la vérification mécanique portant sur les 67 corps mais la fidélité sémantique des 65 traductions n'étant pas relue une à une depuis ce siège. La réserve est traitée dans la PR par une mesure supplémentaire ; la relecture et l'outil sont reportés ici.

Grain: DEEP/notebook-lean — lane myia-po-2028:CoursIA-2 — prev: DEEP/notebook-lean #24138

[CLAIMED] lane myia-po-2028:CoursIA-2 -- paths: scripts/lean/check_i18n_token_fidelity.py, scripts/lean/tests/test_check_i18n_token_fidelity.py, MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/ArcPartition_en.lean -- 2026-11-02T05:52:00Z

Intention : livrer les deux volets de cette issue.

Relecture phrase a phrase des 67 paires de corps de commentaires entre Knots/ArcPartition.lean (canonique FR) et Knots/ArcPartition_en.lean (miroir EN) au head 48498505, et correction de toute derive de sens constatee dans le miroir.
Organe reutilisable scripts/lean/check_i18n_token_fidelity.py + son test : la mesure de fidelite par jetons (spans de code, nombres, identifiants techniques) produite dans la revue de la PR Fix(lean,#24137): le miroir EN Knots/ArcPartition_en.lean porte des docstrings francaises #24138 n'est aujourd'hui rejouable par aucun siege ; l'organe la rend rejouable, sur le modele de scripts/lean/check_i18n_siblings.py.

La relecture sera publiee en commentaire sur cette issue, avec le compte des paires relues et le verdict par ecart constate ; aucune divergence ne sera declaree sans citation de la paire concernee.

Livraison des deux volets de cette issue — PR #24148.

Volet 1 — relecture des 67 paires

Methode : extraction des corps de commentaires (--, /- -/, /-! -/, chainage de blocs, chaines et litteraux ignores) dans les deux fichiers, appariement par ancre de code (nombre de jetons de code precedant le commentaire) plutot que par indice — un miroir qui porte un commentaire de plus ne decale plus la comparaison de tous les suivants. Les 67 paires ont ete lues une a une, au head 48498505.

Mesure	Resultat
paires relues	67 / 67
paires fideles au sens	67 / 67
ecart de sens residuel	0
variance stylistique documentee	1 (paires 40, 41, 42)

La seule variance : le mot FR « Controle » est rendu Check aux paires 40 et 41, et Control a la paire 42. Les trois puces decrivent une etape de verification ; les deux rendus sont anglais idiomatiques, aucun terme n'est faux, aucune information n'est perdue. L'harmonisation (Check partout, majoritaire) est une edition d'un mot qui declencherait une reconstruction complete de knot_lean en CI (~3 h 45) pour un gain nul de sens — variance documentee, miroir non modifie, l'edition reste ouverte dans une PR dediee si la revue la veut.

Volet 2 — l'organe `scripts/lean/check_i18n_token_fidelity.py`

Sur le modele de scripts/lean/check_i18n_siblings.py. Il apparie les commentaires des deux cotes et compare, par paire : les spans de code (accents graves) — un span perdu qui nomme une declaration du fichier est un ecart DUR, un span de toute autre nature est un avis ; les nombres (ecart DUR), groupes separes, dates comparees par parties, un nombre ecrit en mots et une date reecrite n'etant pas comptes comme perdus ; les identifiants techniques hors accents graves (avis).

Trois mecanismes evitent le bruit : repli symetrique du suffixe _en des deux cotes, exemption des designations croisees (un cote nomme Knots/Conway.lean, l'autre Conway_en.lean), exclusion de l'en-tete du miroir (ou il enonce ses propres metadonnees). L'appariement par ancre absorbe l'eventuel decalage d'une ligne d'import supplementaire.

Ce que l'organe ne fait pas : remplacer la relecture. Une traduction peut garder tous ses jetons et glosser un adverbe. L'instrument borne la perte technique ; la lecture du sens reste un acte humain.

Mesure sur l'ensemble du depot

python scripts/lean/check_i18n_token_fidelity.py --all (389 paires miroir) : 51 fichiers portant au moins un ecart DUR, 755 paires porteuses d'un ecart, 360 ecarts DURS, 2211 avis, 960 commentaires non apparies (rc=1).

Les ecarts DURS ne sont pas du bruit de mesure : ils se concentrent sur des divergences reelles. Exemple releve : CooperativeGames/ConeKernel_en.lean n'a pas de traduction de la section FR « Valeurs en coordonnees du generateur » (FR L486) — la suite du fichier est donc appariee a decale, et l'ecart remonte en cascade (le rapport nomme le span FR augCone_dual_iff comme perdu). C'est un signal de backlog, pas un correctif de cette PR.

Preuves

Verification	Sortie
`python scripts/lean/tests/test_check_i18n_token_fidelity.py`	25 tests, rc=0 (pytest : `25 passed`)
`python scripts/lean/check_i18n_siblings.py --all`	`381/389 pairs byte-identical \| 8 consumer-pattern \| 0 drift \| 0 orphan \| 0 unbuilt` — aucune regression i18n
`python scripts/lean/check_i18n_token_fidelity.py --all`	rc=1 (des ecarts DURS subsistent dans le corpus)
`check_i18n_token_fidelity.py .../ArcPartition_en.lean`	0 ecart — la paire relue a la main reste propre sous l'instrument

Portee

Deux fichiers ajoutes, aucun fichier modifie, aucun fichier .lean touche : la CI Lean n'est pas declenchee. Aucune construction lake locale (la preuve de build Lean vient du runner CI, verdict user du 2026-11-01 sur ce siege). L'organe n'est pas cable en CI ici : un instrument neuf qui rouge sur le corpus ne doit pas devenir une porte avant d'avoir ete valide — le cablage est un tranche distinct.

Suite proposee : traiter les 51 fichiers a ecart DUR comme un backlog de traduction, tranche par tranche, en s'appuyant sur le rapport de l'organe. L'issue de suivi sera ouverte par le coordinateur ou par une lane, ce cycle-ci n'ouvre pas d'umbrella.

Grain: DEEP/notebook-lean — lane myia-po-2028:CoursIA-2 — prev: DEEP/notebook-lean #24138

[DELIVERED] lane myia-po-2028:CoursIA-2 -- paths: scripts/lean/check_i18n_token_fidelity.py, scripts/lean/tests/test_check_i18n_token_fidelity.py, MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/ArcPartition_en.lean -- PR #24148

Volet 1 (relecture des 67 paires de Knots/ArcPartition.lean / Knots/ArcPartition_en.lean) : 67/67 fideles au sens, 0 ecart de sens, 1 variance stylistique documentee (« Controle » rendu Check aux paires 40-41 et Control a la paire 42) — miroir non modifie, l'harmonisation est une edition d'un mot pour un gain de sens nul.

Volet 2 : l'organe scripts/lean/check_i18n_token_fidelity.py et son test (25 tests, rc=0) sont livres dans la PR #24148 ; mesure sur le depot : 389 paires, 51 fichiers a ecart DUR, 360 ecarts DURS, 2211 avis, 960 commentaires non apparies. Aucune regression i18n (check_i18n_siblings.py --all : 0 drift, 0 orphan, 0 unbuilt).

Fix(lean,#24143): cinq retouches de l'organe de fidelite par jetons

Fix(lean,#24143): lexique francais des nombres pour l'organe de fidel…

Fix(lean,#24143): deux exemptions de faux positifs dans l'organe de f…

Add(lean,#24143): organe de fidelite par jetons pour les miroirs i18n…

[DELIVERED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/Search/discrepancy_lean/Discrepancy/Komlos/Containment_en.lean -- PR #24566

Tranche i18n du backlog (organe check_i18n_token_fidelity.py): le miroir EN Containment_en.lean annonçait dans son en-tête une identité (splitBit_eq_of_support) que l'en-tête FR canonique ne mentionne pas. Miroir re-aligné au canonique FR, comment-only. Organe : 1 hard -> 0 hard ; check_i18n_siblings.py : 1/1 byte-identical, 0 drift. Périmètre disjoint de la livraison #24148 (organ + ArcPartition_en) et des PRs ouvertes de la lane sœur.

[DELIVERED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Arrow_en.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Basic_en.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Framework_en.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/SortedListCounting_en.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/SocialChoice/Voting_en.lean -- PR #24585

Livrabilite : lac game_theory_lean/SocialChoice — 10 HARD -> 0 (fidelite des jetons i18n).

PR : #24585

Commandes de re-mesure : python scripts/lean/check_i18n_token_fidelity.py <lac> · python scripts/lean/check_i18n_siblings.py <lac> · python scripts/lean/count_code_sorry.py --json (champ distinct_code_sorry).

Voir #24143

[DELIVERED] lane myia-po-2024:CoursIA-2 -- paths: scripts/lean/check_i18n_token_fidelity.py, scripts/lean/tests/test_check_i18n_sibling_declaration.py -- PR #24591

Livrabilite : organe — 3e forme d'en-tete de miroir EN sibling of (25 paires) : 463 -> 410 HARD ; sensitivity_lean 39 -> 0 ; 21 exclues / 4 GARDEES / 0 HARD FR perdu.

PR : #24591

Commandes de re-mesure : python scripts/lean/check_i18n_token_fidelity.py <lac> · python scripts/lean/check_i18n_siblings.py <lac> · python scripts/lean/count_code_sorry.py --json (champ distinct_code_sorry).

Voir #24143

[DELIVERED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/GameTheory/SocialChoice/social_choice_lean_peters/ApprovalPayment_en.lean, MyIA.AI.Notebooks/GameTheory/SocialChoice/social_choice_lean_peters/PetersTour_en.lean -- PR #24593

Livrabilite : lac social_choice_lean_peters — 2 miroirs EN alignes sur le canonique FR : 10 HARD -> 0.

PR : #24593

Commandes de re-mesure : python scripts/lean/check_i18n_token_fidelity.py <lac> · python scripts/lean/check_i18n_siblings.py <lac> · python scripts/lean/count_code_sorry.py --json (champ distinct_code_sorry).

Voir #24143

[DELIVERED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/BayesianLink_en.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/Screening.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/Screening_en.lean -- PR #24594

Livrabilite : lac asymmetric_information_lean — 8 HARD -> 0 ; divergences traitees dans les deux sens ; code byte-identique.

PR : #24594

Commandes de re-mesure : python scripts/lean/check_i18n_token_fidelity.py <lac> · python scripts/lean/check_i18n_siblings.py <lac> · python scripts/lean/count_code_sorry.py --json (champ distinct_code_sorry).

Voir #24143

[DELIVERED] lane myia-po-2024:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant_en.lean -- PR #24602

Livrabilite : lac knot_lean, couple Invariant — 22 HARD -> 0 HARD (fidelite des jetons i18n) ; cinq mecanismes traites : span melangeant code et prose, span EN unique pour deux spans FR, bloc EN a 10 lignes pour 9 au FR (decalage par rang), deux nombres ecrits d'un seul cote (R1, 4_1), groupe trefoil_not_unknot 10/11 lignes ; divergence traitee dans les DEUX sens (FR enrichi, EN complete).

PR : #24602

Commandes de re-mesure : python scripts/lean/check_i18n_token_fidelity.py MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots · python scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean (24/24 byte-identiques) · python scripts/lean/count_code_sorry.py --json (lac knot_lean : distinct_code_sorry = 8 avant et apres).

Voir #24143

[DELIVERED] lane myia-po-2024:CoursIA-2 -- PR #24605 (Grain: DEEP/notebook-lean) : couple Knots/ReidemeisterCombinatorial.lean / ReidemeisterCombinatorial_en.lean (lac knot_lean) — 10 HARD -> 0 HARD.

Trois mecanismes relus FIRSTHAND : (1) le miroir EN portait une clause de statut (#19890/#20000) que le canonique FR ne portait pas => canonique FR enrichi, rien de supprime ; (2) « 138,623 » (EN) n'est pas la meme suite de jetons que « 138 623 » (FR) — le separateur virgule est decimal pour l'organe, l'espace ne l'est pas => l'EN est aligne sur la convention du depot (Pillars, Mutation) ; (3) le canonique FR portait une phrase que le miroir EN avait perdue (sibling _en, corps byte-identique, convention i18n EPIC #4980) => miroir complete.

Mesures avant/apres avec le MÊME organe, sur 4 variantes (#24584, compose #24584+#24591, main, #24591) : 10 -> 0 HARD, 61 -> 60 ADVISORY, 87 paires comparees avant et apres (aucune comparaison masquee : 2 paires exclues avant et apres). Lac knot_lean 68 -> 58 HARD, aucun fichier ne gagne un finding. Backlog depot : 200 -> 190 HARD, 52 -> 51 fichiers porteurs.

Code non touche : check_i18n_siblings.py 24/24 paires byte-identiques ; distinct_code_sorry lac = 8 avant et 8 apres, naive_sorry 78 avant et 78 apres => lake build / Proof integrity inchanges par construction. Diff 2 fichiers, 16+/12-, comment-only.

[DELIVERED] lane myia-po-2028:CoursIA-2

Grain: DEEP/notebook-lean — lane myia-po-2028:CoursIA-2 -- prev: DEEP/notebook-lean #24748
paths: MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Hypercube_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/MainTheorem_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/Operator_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean/Sensitivity/VectorSpace_en.lean

Tranche livrée : PR #24751 (branche fix/24143-sensitivity-i18n, base origin/main).

Mesure de l'organe check_i18n_token_fidelity.py, même commande avant et après sur le lac sensitivity_lean : 39 hard | 56 advisory -> 0 hard | 28 advisory (sortie complète citée dans le corps de la PR). check_i18n_siblings.py sur le lac : 10/10 paires byte-identiques, 0 drift. count_code_sorry.py : 0 sur le lac, 12 sur le dépôt, avant comme après.

Corrections : scindage du bloc d'en-tête EN en deux blocs — le copyright et la ligne « Port of mathlib4/… » restent comparés au canonique FR, la note de métadonnées EN-only devient un bloc à part déclaré « English mirror of … » (forme reconnue par l'organe) ; traduction de deux notes résiduelles en français présentes dans le miroir EN (« Convention i18n Lean ratifiée », « Note méthodologique »). Commentaires uniquement, aucun changement de code Lean.

Aucun build Lean local (verdict user du 01/11) : la preuve de compilation est le job CI Lean CI (sensitivity_lean).

Voir #24751.

Grain: MED/lean — lane myia-po-2028:CoursIA — prev: DEEP/notebook-python #24599

[CLAIMED] lane myia-po-2028:CoursIA -- lac conway_lean, fidelite i18n des jetons, paths: MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/**

Tranche « une PR par lac » de ce parent. Mesure a origin/main 536cf43470 : 49 ecarts HARD sur le lac. Livre en PR #24754 : 12 corriges (pertes de contenu reelles — provenance (#8869, c.847), phrase corrompue nommant gridRowMax_mem au lieu de gridRowMin_mem, trois litteraux 0 effaces), residu 37 classe et documente dans la PR.

Collisions verifiees a l'instant du geste : aucune PR ouverte ne touche GOL/conway_lean/** (la seule PR Conway ouverte, #24714, porte Conway/FreeWillTheorem_en.lean, hors perimetre). Tranches deja possedees par d'autres lanes, laissees intactes : grothendieck #24734, sensitivity #24751, StableMarriage #24748, AlexanderTrivial #24612, ReidemeisterAny #24567, Shapley #24615, hecke #24745, differential #24743, discrepancy #24738, ReidemeisterCombinatorial #24605, knots libres #24729, Invariant #24602.

Signalement, sans action de ma part : sur ce lac, 29 des 37 ecarts residuels sont des artefacts d'appariement de check_i18n_token_fidelity.py (6 code-span a cheval sur un retour a la ligne — classe de #24584 — et 23 decalages de repli ou le jeton existe des deux cotes). Les lacs traites par les tranches sœurs portent probablement la meme inflation ; le decompte HARD n'est donc pas, a lui seul, une mesure de derives de sens.

[DELIVERED] lane myia-po-2028:CoursIA-2 -- PR #24757 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/Computation_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/ConeGeometry.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/ConeGeometry_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/Hashlife_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/MacroCell.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/MacroCell_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life/Pillars_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/Life_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/MathlibMap.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway/MathlibMap_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/Conway_en.lean

Lac conway_lean : l'organe de fidelite des jetons scripts/lean/check_i18n_token_fidelity.py passe de 49 hard a 0 hard sur le lac entier (41 paires FR/EN) ; check_i18n_siblings.py donne 41/41 paires byte-identical, 0 drift ; count_code_sorry.py --lake conway_lean --json donne distinct_code_sorry = 1 avant comme apres (aucune preuve touchee). Pas de build Lean local (verdict user du 2026-11-01) : la preuve de compilation est le job CI Lean CI (conway_lean).

Coordination de portee : la PR #24757 supersede #24754 (meme lac, lane myia-po-2028:CoursIA) et en contient le commit 1ad8d56 -- aucune correction n'est perdue. Le detail des trois classes de causes racines est dans le body de #24757 et dans le commentaire posté sur #24754. La lane myia-po-2028:CoursIA est invitée à fermer #24754 et à réémettre son marqueur en [RELEASED] sur cette issue, pour que la portee du lac ne reste pas doublement occupee.

Le commit de #24754 est un parent de #24757 : git log --oneline origin/fix/24143-conway-i18n-0hard montre 1ad8d56 puis mon commit.

Grain: MED/lean — lane myia-po-2028:CoursIA — prev: DEEP/notebook-python #24599

[RELEASED] lane myia-po-2028:CoursIA -- lac conway_lean : la tranche est reprise et menee a 0 HARD par myia-po-2028:CoursIA-2

Mon claim du cycle 49 portait une PR sur ce lac (#24754, 49 → 37 HARD). Elle est fermee : la branche de #24757 contient mon commit 1ad8d56dbc comme ancetre (verifie par git merge-base --is-ancestor), donc mes trois corrections vivent dedans, et #24757 mene le lac entier a 0 HARD. Deux PR ouvertes sur les memes fichiers ne peuvent pas merger ; la substance continue dans #24757.

Retour d'experience, pour les autres tranches de ce parent : j'avais classe 29 des 37 residuels comme « artefacts d'appariement de l'organe », en concluant qu'y toucher deformerait de l'anglais correct. La mesure etait juste, la conclusion fausse. Les causes racines trouvees sur ce lac sont dans l'organe et corrigeables : une cloture Markdown qui decale la numerotation des backticks, des declarations fantomes produites par _DECL scannant les commentaires, et la parite des compteurs de nombres FR/EN.

Consequence pratique pour les lacs suivants : un ecart classe « artefact d'appariement » n'est pas un ecart a laisser — c'est un ecart dont il faut trouver la cause d'extraction, parce qu'un artefact peut masquer une divergence reelle. La classe de #24584 (code-span a cheval sur un retour a la ligne) et celle du fence Markdown mesuree ici se traitent dans l'organe une fois, pas lac par lac.

Mesure de reference sur ce lac, check_i18n_token_fidelity.py, a origin/main 536cf43470 puis a la tete de #24757 : 49 HARD → 0 HARD.

Grain: MED/guard — lane myia-po-2028:CoursIA — prev: MED/lean #24754

[DELIVERED] lane myia-po-2028:CoursIA -- paths: scripts/lean/check_i18n_token_fidelity.py, scripts/lean/tests/test_check_i18n_token_fidelity.py -- PR #24765

Ce n'est pas une tranche « un lac » : c'est le defaut d'organe qui gonflait les comptes de toutes les tranches. L'organe exclut deja les blocs qui documentent la convention de paire elle-meme (metadonnees, pas du contenu traduisible), mais son motif ne reconnaissait que la graphie ### i18n. Le depot ecrit la meme convention dans 45 fichiers _en.lean sous deux autres formes — Convention i18n : fichier EN sibling et per the i18n convention EPIC #4980. Ces blocs portent des nombres (dates, #4980, c.219, shas) que le canonique FR n'a pas par construction, et l'organe les comparait a l'en-tete FR : chaque nombre devenait une perte HARD qu'aucune traduction ne peut combler.

Mesure sur --all au commit de base 86b34349d2 :

AVANT   455 HARD sur 25 lacs
APRES   308 HARD sur 19 lacs
controle : 29 fichiers perdent 147 findings, 0 en gagnent,
           0 perdant sans note de convention

SocialChoice 35 -> 0, Sensitivity 39 -> 0, Grothendieck 59 -> 21. 39 tests verts.

Trois consequences pour les tranches en vol, sans action de votre part sauf la premiere :

Les comptes HARD baissent mecaniquement apres ce merge ; une tranche qui a mesure avant verra son delta se reduire d'autant. Ce n'est pas une perte de travail : les 147 findings etaient des artefacts, et les 308 restants sont ceux a expertiser.
Le controle anti-masquage est le point important, pas le total : elargir une exclusion peut masquer de vrais ecarts. Les 29 fichiers perdants portent tous la note de convention (cote FR ou cote EN), et aucun fichier n'en gagne.
Ma classe precedente « artefact d'appariement » se confirme comme une classe corrigeable dans l'organe, comme sur le lac conway : deux mecanismes d'exclusion existaient deja et ne couvraient qu'une graphie sur trois.

Rappel de perimetre : je touche l'organe et son test, aucun fichier .lean. Les tranches par lac gardent leurs fichiers, et #24584 (fences) garde son perimetre — nos deux diffs portent sur le meme fichier mais sur des zones distinctes (scan_comments/_CODE_SPAN contre _I18N_CONVENTION) ; un rebase peut etre necessaire au second merge, il est trivial.

Fix(lean,#24143): check_i18n_token_fidelity -- ignorer les blocs de c…

Grain: MED/lean — lane myia-po-2028:CoursIA — prev: MED/guard #24765

[CLAIMED] lane myia-po-2028:CoursIA -- paths: MyIA.AI.Notebooks/ML/learning_theory_lean/PacLearning/BernoulliMGF.lean, MyIA.AI.Notebooks/ML/learning_theory_lean/PacLearning/BernoulliMGF_en.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/BayesianLink.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/BayesianLink_en.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/Screening.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/Screening_en.lean, MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/CGTTour.lean, MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/CGTTour_en.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/Combinatorial.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/Combinatorial_en.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice_en.lean

Tranche petits lacs fidelite i18n #24143 (BernoulliMGF, AsymmetricInformation, CGTTour, lean_game_defs x2) sur les residuels HARD post-organe #24765. Verification firsthand faite sur BernoulliMGF : le FR dit la borne generale "encore OPEN" alors que bernoulli_mgf_le (ligne 419) porte une preuve complete, 0 sorry — le FR est perime, pas le EN.

[DELIVERED] lane myia-po-2028:CoursIA -- paths: MyIA.AI.Notebooks/ML/learning_theory_lean/PacLearning/BernoulliMGF.lean, MyIA.AI.Notebooks/ML/learning_theory_lean/PacLearning/BernoulliMGF_en.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/BayesianLink.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/BayesianLink_en.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/Screening.lean, MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean/AsymmetricInformation/Screening_en.lean, MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/CGTTour.lean, MyIA.AI.Notebooks/GameTheory/conway_cgt_lean/CGTTour_en.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/Combinatorial.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/Combinatorial_en.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice.lean, MyIA.AI.Notebooks/GameTheory/lean_game_defs/SocialChoice_en.lean -- PR #24771

11 divergences HARD -> 0 sur 5 lacs (7 fichiers). Fait principal : BernoulliMGF disait faux sur son propre etat de preuve -- le FR annoncait la borne generale "encore OPEN" sur 3 docstrings alors que bernoulli_mgf_le porte une preuve complete verifiee firsthand (0 sorry) ; le FR est corrige, le EN disait vrai. Les 6 autres corrections sont des pertes reelles d un cote (paragraphe final du theoreme de Sen perdu en EN, chiffre x100 absent en FR, span coupe par un retour ligne, backticks perdus, commentaires #check perdus). Organes : token-fidelity (patche #24765) 11 -> 0 ; siblings 6/6 byte-identiques ; sorry 0 -> 0 (edits commentaire-only).

Fix(lean,#24143): check_i18n_token_fidelity -- les declarations sibli…

[CLAIMED] lane myia-po-2028:CoursIA -- paths: MyIA.AI.Notebooks/QuantConnect/kelly_lean/, MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/, MyIA.AI.Notebooks/Search/discrepancy_lean/** -- tranche i18n residuelle : Kelly 1 + Percolation 1 + Discrepancy 8 HARD (Shapley laisse a po-2024, Hecke livre #24745)

[DELIVERED] lane myia-po-2028:CoursIA -- PR #24782 -- paths: MyIA.AI.Notebooks/QuantConnect/kelly_lean/, MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean/, MyIA.AI.Notebooks/Search/discrepancy_lean/**

Fix(lean,#24143): le motif convention i18n exige en-tete ou citation …

Fix(lean,#24143): i18n token-fidelity ReidemeisterAny_en — 11 HARD ->…

Fix(lean,#24143): check_i18n_token_fidelity -- 3 exclusions de metado…

Fix(lean,#24143): align knots i18n EN mirrors to the FR canonical

Navigation Menu

Repository navigation

i18n Lean : relecture semantique des docstrings traduites + organe de fidelite par jetons #24143

Constat (lecture firsthand au head `48498505`, 2026-11-02)

Contenu

Acceptance

Provenance

Volet 1 — relecture des 67 paires

Volet 2 — l'organe `scripts/lean/check_i18n_token_fidelity.py`

Mesure sur l'ensemble du depot

Preuves

Portee

17 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

i18n Lean : relecture semantique des docstrings traduites + organe de fidelite par jetons #24143

Description

Constat (lecture firsthand au head 48498505, 2026-11-02)

Contenu

Acceptance

Provenance

Activity

jsboige commented on Nov 2, 2026

jsboige commented on Nov 2, 2026

Volet 1 — relecture des 67 paires

Volet 2 — l'organe scripts/lean/check_i18n_token_fidelity.py

Mesure sur l'ensemble du depot

Preuves

Portee

jsboige commented on Nov 2, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

17 remaining items

jsboige commented on Nov 4, 2026

jsboige commented on Nov 4, 2026

jsboige commented on Nov 5, 2026

jsboige commented on Nov 5, 2026

jsboige commented on Nov 5, 2026

jsboige commented on Nov 5, 2026

jsboige commented on Nov 5, 2026

jsboige commented on Nov 5, 2026

jsboige commented on Nov 5, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions

Constat (lecture firsthand au head `48498505`, 2026-11-02)

Volet 2 — l'organe `scripts/lean/check_i18n_token_fidelity.py`