[jsboige]

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

Ce que cette PR corrige

Le lac asymmetric_information_lean portait 8 findings HARD de l'organe de fidelite des jetons i18n (scripts/lean/check_i18n_token_fidelity.py). Les 8 ont ete relus FIRSTHAND : ce sont des divergences de contenu reelles, et non des artefacts d'appariement. Elles se repartissent dans les deux sens — un miroir EN plus riche que son canonique, et un miroir EN plus pauvre.

1. Le canonique FR ne portait pas l'index des modules du lac

Le miroir EN AsymmetricInformation_en.lean portait une section « Modules: » listant les 5 modules du lac avec une description chacun ; le canonique FR ne l'avait pas. L'ecart se lisait comme 4 nombres « extras EN » (1970, 1973, 1976, 4).

Alignement choisi : l'index est ajoute au canonique FR, traduit, et le miroir EN le conserve tel quel. Rien n'est supprime — les deux cotes portent desormais le meme contenu. C'est le seul endroit ou cette PR touche un fichier FR canonique, et la raison en est la : supprimer la section du miroir aurait detruit un contenu utile sans contrepartie.

2. Screening_en.lean — un paragraphe du canonique FR avait disparu

Le docstring FR de globalExpectedProfit explique que la somme (sur les 2 types) reste dans le domaine lineaire de omega, et qu'une variante moyennee (division Int par 2) en sortrait. Le miroir EN n'en gardait qu'une phrase : « sum (not average) ». Le docstring EN est desormais la traduction fidele du docstring FR.

3. Screening_en.lean — deux lignes de commentaire FR fusionnees en une

Le commentaire FR sur la contradiction de Nash compte 6 lignes ; le miroir EN en comptait 5, la troisieme ayant fusionne « contradiction 0 < ... ≤ ... ≤ -1. » et « The simpa [...] using ... ».

Deux consequences, toutes deux mesurees :

• l'apparimage par rang decale d'un cran tous les commentaires suivants ;
• le span `simpa [globalExpectedProfit, expectedProfit] using` se retrouve coupe en fin de ligne par le retour a la ligne, ce qui produit des spans parasites (and, transformation unfolds both sides of, hPosOff).

Les 6 lignes EN reproduisent desormais les 6 lignes FR une a une, span intact.

4. Screening_en.lean — un commentaire de 2 lignes avait ete supprime

Le canonique FR porte, avant have hle := hNash c hMemC c' hNotMem, un commentaire de 2 lignes sur la borne superieure de Nash sur la deviation profitable. Le miroir EN ne l'avait pas : il etait signale comme commentaire FR non apparie. Il est desormais restitue, traduit.

Apres ce geste, la lake ne porte plus aucun commentaire non apparie (2 -> 0).

5. BayesianLink_en.lean — un nombre ecrit en mots d'un cote

Le canonique FR ecrit « simplification 1ere tranche » ; le miroir EN ecrivait « first-tranche ». Le miroir porte desormais « simplification of the 1st tranche ».

6. Screening.lean (canonique FR) — le facteur d'encodage n'etait precise que dans le miroir

Le miroir EN ecrivait « premium in cents (x100) to stay integer » ; le canonique FR ecrivait seulement « prime en centimes ». Le canonique porte desormais « prime en centimes (x100) » — la precision que le code porte (c.premium * 100).

Mesures

Sur le lac (check_i18n_token_fidelity.py, 6 paires) :

etat	HARD	ADVISORY	paires de commentaires
avant	8	71	125
apres	0	50	128

Le verdict est independant de l'organe : les quatre variantes donnent le meme chiffre apres (0 HARD / 50 ADVISORY) — l'organe de main, celui de #24584, celui de #24591, et le compose #24584 + #24591. Les mesures « avant » sont faites avec le meme organe que les mesures « apres » (les deux lignes « avant » : 8 / 71, quel que soit l'organe).

Preuves

• python scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/GameTheory/asymmetric_information_lean → 6/6 paires byte-identiques | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt — le code n'est pas touche : la construction et le resultat de build sont ceux de main par construction.
• python scripts/lean/count_code_sorry.py --json → lake asymmetric_information_lean : distinct_code_sorry = 0 avant, 0 apres ; depot : 12.
• lake build SUCCESS / Proof integrity SUCCESS : inchanges par construction (code byte-identique, 6/6 paires) ; les runs CI de cette PR en sont la preuve.
• Controle de non-regression : aucun fichier de la lake ne gagne un finding ; les ADVISORY baissent (71 -> 50) et les paires de commentaires commentaires apparies montent (125 -> 128).

Perimetre

• 4 fichiers, 32 insertions / 10 suppressions, commentaires uniquement (Screening.lean et AsymmetricInformation.lean sont les deux fichiers FR canoniques touches, pour les points 1 et 6 ci-dessus).
• Aucune collision avec les PRs en vol : Fix(lean,#24143): SymbolCodec_en.lean -- en-tete EN fidele au canonique FR (labelAll/labelAll_cons) #24517 (Compression_lean), Fix(lean,#24143): Folk_en.lean -- commentaire EN re-cadre aux zeros du canonique FR #24526 (RepeatedGames), Fix(lean,#24143): Containment_en.lean -- en-tete EN fidele au canonique FR #24566 (Komlos), Fix(lean,#24143): i18n token-fidelity ReidemeisterAny_en — 11 HARD -> 0 #24567 (KNOTS/ReidemeisterAny), Fix(lean,#24143): check_i18n_token_fidelity - les blocs fence cassaient l appariement des backticks #24584, Fix(lean,#24143): les miroirs EN de la famille SocialChoice sont fideles au canonique FR (35 HARD -> 0) #24585, Fix(lean,#24143): reconnaitre la declaration de jumeau « EN sibling of X » (check_i18n_token_fidelity) #24591, Fix(lean,#24143): les miroirs EN de social_choice_lean_peters sont fideles au canonique FR (10 HARD -> 0) #24593 — ce lac n'est pas touché.

See #24143

🤖 Generated with Claude Code

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #24594 (Fix(lean,#24143): aligner les miroirs EN de asymmetric_information_lean sur le canonique FR (8 HARD -> 0)) 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.

• fort -- Fix(lean,#24143): fidelite i18n petits lacs -- 11 divergences HARD, BernoulliMGF FR perime #24771 partage : 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 (issues communes : i18n Lean : relecture semantique des docstrings traduites + organe de fidelite par jetons #24143)