[jsboige]

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

Ce que cette PR corrige

Le lac knot_lean portait 22 findings HARD de l'organe de fidelite des jetons i18n (scripts/lean/check_i18n_token_fidelity.py) sur le couple Invariant.lean / Invariant_en.lean. Les 22 ont ete relus FIRSTHAND : ce sont des divergences de contenu reelles, et non des artefacts d'appariement. Elles se repartissent en cinq mecanismes.

1. Un span de code melangeant code et prose FR

Le FR ecrivait `d₂.edges = d₁.edges ++ (labels de c₁, c₂)` : la prose francaise etait a l'interieur du span de code, si bien que le span EN ((labels of c₁, c₂)) ne pouvait pas etre le miroir. La prose est sortie du span des deux cotes :

• FR : `d₂.edges = d₁.edges` ++ (labels de c₁, c₂)
• EN : `d₂.edges = d₁.edges` ++ (labels of c₁, c₂)

2. Un span EN unique ou le FR en porte deux

Le FR ecrivait, sur deux lignes, `simp only` puis `triColorConditionAt, hcol*` ; le miroir EN les avait fusionnes en un seul span `simp only [triColorConditionAt, hcol*]`. Les deux lignes EN sont re-posees, un span par ligne, comme le FR.

3. Un bloc de commentaire EN comptant 10 lignes pour 9 au FR (le « mur R2 »)

Le bloc du contre-exemple formel R2 comptait 10 lignes en EN pour 9 en FR. L'organe apparie les commentaires par rang dans le groupe d'ancre : le decalage d'une ligne faisait porter r2_append_only_wall et le nombre 2 (de « ≥ 2 couleurs » / "≥ 2 colors") sur des paires qui ne se correspondent pas — 6 des 22 findings HARD n'etaient que cela. Le bloc EN est re-pose en 9 lignes, span par span :

• « the door on the free moves, the master is proven (§2-Ω), and not_tricolorable_invariant_current »
• « becomes false by construction. The wall r2_append_only_wall (below) remains »
• « valid: it speaks of the FREE move, not of the ReidemeisterEquiv closure. »

Aucun contenu n'est perdu : les trois phrases anglaises sont integralement redistribuees.

4. Deux nombres ecrits d'un seul cote

• Le FR ecrivait « Un auto-croisement (kink R1) » sur sa 11ᵉ ligne du groupe ; le miroir EN ecrivait « An R1 » une ligne plus haut ⇒ le 1 etait reporte d'une paire a l'autre. Il est desormais sur la meme ligne que le FR.
• Le FR ecrivait « La figure-eight (4₁) » ; le miroir EN ecrivait « The figure-eight (4_1) » — le 1 ASCII est un nombre pour l'organe, l'indice ₁ ne l'est pas. Le 1 ASCII etait donc un nombre « extra EN ». L'EN ecrit desormais 4₁, comme le FR.

5. Le groupe trefoil_not_unknot — 10 lignes FR pour 11 lignes EN

Le miroir EN nommait les deux pieces (`trefoil_tricolorable`, `unknot_not_tricolorable`) que le FR laissait en prose (« the two pieces are proven ») ; l'inverse valait aussi pour sorry, que le FR mentionne et que l'EN avait perdu en resumant.

La divergence se traite dans les deux sens :

• le FR est enrichi — les deux pieces y sont nommees comme spans de code (rien n'est supprime) ;
• le miroir EN est complete — sorry y est mentionne comme au FR.

Les deux blocs sont re-posees a 11 lignes, span par span.

En passant : l'en-tete du miroir

L'en-tete EN annonçait « (3-colorability, crossing number) » la ou le canonique FR ecrit « (tricolorabilite, nombre de croisements) » : le 3 etait un nombre « extra EN ». Le titre EN dit desormais « tricolorability ».

Mesures

Meme organe avant et apres (mesures « avant » et « apres » faites avec le meme organe) :

organe	avant	apres
#24584 (fence corrigee)	22 HARD / 267 ADVISORY / 517 paires	0 HARD / 240 ADVISORY / 519 paires
compose #24584 + #24591	22 HARD / 267 ADVISORY / 517 paires	0 HARD / 240 ADVISORY / 519 paires
main (avant la correction fence)	152 HARD / 458 ADVISORY	130 HARD / 431 ADVISORY
#24591 seul (avant la correction fence)	152 HARD / 458 ADVISORY	130 HARD / 431 ADVISORY

Les 130 residuels sous l'organe de main sont les artefacts de fence (classe c.828), deja corriges par la PR #24584 : ce ne sont pas des pertes de traduction. Aucune variante d'organe ne gagne un finding, et le lac passe de 68 a 46 HARD (les 22 de ce fichier etant les seuls vises).

Preuves

• python scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean → 24/24 paires byte-identiques | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt — le code n'est pas touche.
• python scripts/lean/count_code_sorry.py --json → lac knot_lean : distinct_code_sorry = 8 avant, 8 apres ; code_sorry = 16 avant et apres. Le compteur naif (naive_sorry, qui compte la prose) passe de 78 a 79 : c'est le mot sorry mentionne dans un commentaire que le miroir EN porte desormais comme le FR — pas un sorry de code.
• lake build SUCCESS / Proof integrity SUCCESS : inchanges par construction (code byte-identique, 24/24 paires). L'environnement Lean local n'a pas de cache Mathlib construit, la construction n'est donc pas rejouee ici.
• Controle de non-regression : aucun fichier du lac ne gagne un finding ; les ADVISORY baissent et les paires de commentaires appariees montent (517 → 519).

Perimetre

• 2 fichiers, 16 insertions / 16 suppressions, commentaires uniquement.
• 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 — autre fichier du meme lac), 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, Fix(lean,#24143): aligner les miroirs EN de asymmetric_information_lean sur le canonique FR (8 HARD -> 0) #24594, Fix(lean,#24143): SymbolCodec_en.lean — docstrings EN fidèles au canonique FR #24596 (SymbolCodec) — aucun ne touche Invariant.lean ni Invariant_en.lean.

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).