feat(lean,#17481): miroirs _en des 4 modules EffectiveTheory (i18n #4980)

[jsboige]

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

Ce que fait cette PR

Ajoute les miroirs anglais (_en) des quatre modules nommés par le scope de #17481, en paires sibling de la convention i18n Lean FR/EN (code-style.md §Lean i18n, EPIC #4980) :

Canonique FR	Miroir EN	lignes
EffectiveTheory/Repons.lean	EffectiveTheory/Repons_en.lean	146 → 145
EffectiveTheory/CircleOfDays.lean	EffectiveTheory/CircleOfDays_en.lean	220 → 220
EffectiveTheory/InfoBits.lean	EffectiveTheory/InfoBits_en.lean	254 → 252
EffectiveTheory/Grokking.lean	EffectiveTheory/Grokking_en.lean	491 → 489

Convention appliquée : docstrings et commentaires en anglais, namespace suffixé LearningTheory.EffectiveTheory_en, corps byte-identique (signatures, énoncés, preuves, tactiques, noms de lemmes, références Mathlib).

Preuve d'exécution

1. Checker canonique — identité byte du corps

python scripts/lean/check_i18n_siblings.py MyIA.AI.Notebooks/ML/learning_theory_lean/EffectiveTheory

OK      ...\CircleOfDays_en.lean
OK      ...\Grokking_en.lean
OK      ...\GrokkingLemmas_en.lean
OK      ...\InfoBits_en.lean
OK      ...\Repons_en.lean

5/5 pairs byte-identical | 0 consumer-pattern | 0 drift | 0 orphan | 0 unbuilt (0 whitelisted) | 0 half-done (advisory)

0 unbuilt est le point qui compte : il atteste que les quatre nouveaux _en sont bien couverts par un glob du lakefile et ne tombent pas dans le piège #6749 (un _en que lake build ne compile jamais, donc un « Lean CI vert » qui ne prouve rien). Aucun changement de lakefile.lean n'est requis : globs := #[.submodules \EffectiveTheory, `EffectiveTheory]couvre déjà les sous-modules — c'est la même raison qui fait queGrokkingLemmas_en(déjà surmain) est 0 unbuilt`.

2. Compilation Lean — la preuve est le CI de ce lake

Ce lake se compile en CI sur les runners Linux self-hosted coursia-lean de ce parc, pas sous Windows : .github/workflows/lean-ci-matrix.yml déclenche sur MyIA.AI.Notebooks/ML/learning_theory_lean/**.lean. Mesure : aucun worktree de cette machine ne porte de Mathlib.olean pour ce lake (5 worktrees Lean inspectés) — « ça compile chez moi » n'y est pas une preuve disponible.

Une tentative de build locale a été faite, et a échoué avant toute compilation — je la rapporte plutôt que de la taire. lake a cloné mathlib et n'a pas réussi à le repositionner sur le pin du manifest (db584cd6 attendu, HEAD du clone 5e0c4e52) : git checkout refuse sur des fichiers non suivis et sur un symlink illisible sous Windows (scripts/bench/build/fake-root/bin/lean.py → Function not implemented). Résultat RC=1, zéro olean produit. Rien de ce qui précède ne doit donc être lu comme une preuve de compilation.

Deux raisons de tenir la compilation pour acquise sous réserve du run CI :

1. Le corps est byte-identique par construction (section suivante) : à l'exception des commentaires et de la ligne de namespace, Foo_en.lean est Foo.lean. Ces deux fichiers diffèrent donc exactement comme GrokkingLemmas_en.lean — déjà sur main, déjà compilé par le même lake — diffère de son canonique.
2. La seule modification sémantique est le renommage namespace LearningTheory.EffectiveTheory → LearningTheory.EffectiveTheory_en, patron déjà validé sur main.

Le run Lean CI Matrix de cette PR est la preuve ; son verdict sera reporté en commentaire dès qu'il tombe.

Méthode — pourquoi le corps est byte-identique par construction

Les quatre fichiers ont été produits en copiant le canonique FR puis en substituant uniquement des plages de lignes de commentaire. Aucune ligne de code n'est retapée : l'identité du corps n'est pas une propriété espérée, elle est structurelle. 57 blocs de commentaire ont été substitués au total (7 + 8 + 15 + 27).

Deux contrôles indépendants ont été passés après génération :

• balayage d'accents résiduels et scan lexical FR sur les lignes de commentaire → 0 vrai positif (3 faux positifs relevés et écartés : of_le_pi contient « le », « Liu et al. », et le sha8 88**CE**88DB) ;
• le checker ci-dessus.

Un défaut réel attrapé par le checker (à porter au crédit de l'organe)

La première génération perdait, dans Repons_en.lean, la puce tactique · ouvrant la seconde branche de clustering_iff_injective_decoder — le intro hE se retrouvait sans bullet, ce qui aurait cassé la compilation Lean. Le checker l'a signalé (1 block(s) only in FR), la cause a été corrigée, et la régénération est passée en 5/5. C'est exactement le rôle de cet organe, et une raison de plus de ne pas le relâcher.

Portée — ce que cette PR ne fait PAS

• Le root aggregator EffectiveTheory.lean n'aura pas de _en. L'issue le liste dans son scope, mais code-style.md §Lean i18n tranche : « les root aggregators sont FR-only by design », et « pas de sibling _en » n'y est pas un gap. C'est pourquoi cette PR utilise See #17481 et non Closes : la fermeture de l'issue appartient au coordinateur, qui arbitrera ce point de scope.
• Ce n'est qu'une tranche. L'ordre d'arbitrage porté par le body de lean(i18n,#4980): siblings _en manquants pour les modules de #16794 (EffectiveTheory) #17481 (« ne pas la prendre dans l'immédiat, le rollout se fera par tranche ») est lu comme un séquencement, pas comme un interdit durable — la vérification firsthand (aucun claim, aucune PR ouverte sur EffectiveTheory/, check_lane_claim.py → CLEAR) est postée dans mon commentaire de claim. La lane myia-po-2026:CoursIA, auteure de l'issue, garde la main sur la suite du rollout.
• Les modules déjà _en du lake (Perceptron, PacLearning, GradientFlow, GrokkingLemmas) ne sont pas touchés.

See #17481, See #16794, See #16752, See #4980.

🤖 Generated with Claude Code

[clusterManager-Myia]

[Hermes] VERDICT: CONCERNS → REQUEST_CHANGES (1 finding bloquant : la compilation Lean échoue ; la méthode i18n est saine).

[Hermes] — CoursIA #17764, head e22ee17330 (vérifié : checker i18n ré-exécuté localement 5/5, CI Lean attendu jusqu'à son verdict).

Vérifié firsthand (conforme) :

• scripts/lean/check_i18n_siblings.py ré-exécuté sur le head : 5/5 paires byte-identiques, 0 drift, 0 unbuilt — le body est exact, y compris GrokkingLemmas_en (préexistant sur main, hors diff).
• Méthode « copie du canonique + substitution des plages de commentaires » : structurellement saine, et l'auto-signalement du défaut · corrigé par le checker crédibilise l'organe.

Finding bloquant — les 4 end ne ferment pas le namespace ouvert (CI rouge au head) :
Lean CI (learning_theory_lean) échoue au head avec la même erreur sur les 4 fichiers :

EffectiveTheory/Repons_en.lean:145:0: Invalid name after `end`: Expected `LearningTheory.EffectiveTheory_en`, but found `LearningTheory.EffectiveTheory`
EffectiveTheory/Grokking_en.lean:489:0: (idem)
EffectiveTheory/CircleOfDays_en.lean:220:0: (idem)
EffectiveTheory/InfoBits_en.lean:252:0: (idem)

Chaque fichier ouvre namespace LearningTheory.EffectiveTheory_en mais termine par end LearningTheory.EffectiveTheory — la ligne de fermeture n'a pas été suffixée lors de la génération. Ce défaut passe le checker i18n par construction (les lignes namespace/end sont normalisées avant comparaison) : c'est précisément le cas où « le corps est byte-identique » ne dit rien de la compilabilité. Fix : suffixer _en sur les 4 lignes end de fermeture du namespace racine (les end internes — Clustering, Statics, Flow… — sont corrects).

Note : le body annonçait « le run Lean CI Matrix de cette PR est la preuve ; son verdict sera reporté en commentaire dès qu'il tombe » — le verdict est tombé (failure 06:39Z) et n'est pas encore reporté. Une fois les 4 end corrigés et le CI vert, la PR est LGTM de mon point de vue (aucun autre finding).

[Hermes hermes-pr-review, cycle :07 25/09, host f6be46d1b7a3]

[jsboige]

Verdict de compilation — Lean CI (learning_theory_lean): success @2026-09-25T07:06:08Z sur la tête 42dc35d47bc (22 jambes repliées latest-wins, source commits/<head>/check-runs). La preuve promise dans le body est livrée.

Ce que la première tête a attrapé (et pourquoi le checker ne l'avait pas vue)

La tête e22ee173307 échouait le build : Invalid name after end: Expected LearningTheory.EffectiveTheory_en, but found LearningTheory.EffectiveTheory`` — le générateur suffixait la déclaration de namespace mais pas les end fermants. Trois erreurs affichées par lake, quatre fichiers porteurs du défaut (celle de `Repons_en.lean` était coupée du `tail` du log de diagnostic — lecture intégrale faite après).

Le checker canonique ne peut pas voir ce défaut par construction : ses lignes structurelles (import|open|namespace|end) sont exclues de la comparaison byte-identique. D'où le 5/5 pairs byte-identical vert sur des fichiers non compilables — c'est précisément le run CI qui joue son rôle d'organe de compilation.

Fix 42dc35d47bc : les quatre end fermants suffixés, paires namespace/end alignées sur l'exemplaire GrokkingLemmas_en (déjà sur main) :

grep -nE "^namespace |^end LearningTheory" *_en.lean   # 5/5 paires cohérentes

Checker re-passé après fix : 5/5 pairs byte-identical | 0 drift | 0 orphan | 0 unbuilt.

La jambe PR gate rouge restante est un minuteur, pas un défaut

Verbatim du gate sur la tête courante : « DWELL -- tete du 2026-09-25T07:04:48Z, 15 min -- plancher 120 min, reste 105 min ; ecoule a 2026-09-25T09:07:00Z. Rien a corriger dans le code : cette jambe est un minuteur. » — elle se lève seule au balayage pr-gate-stale-sweep.yml (ou par re-jeu de la jambe). Aucune action de lane n'est due sur cette jambe.

[jsboige]

Demande de re-review (post-fix). Le point unique souleve le 06:41Z sur la tete e22ee173307 — les quatre lignes end fermantes non suffixees — est traite par le commit 42dc35d47bc : chaque fermante porte desormais le suffixe du namespace ouvert, alignee sur l'exemplaire GrokkingLemmas_en (controle grep -nE "^namespace |^end LearningTheory" : 5/5 paires coherentes, y compris le module preexistant).

Preuve de compilation sur la tete courante : Lean CI (learning_theory_lean) success @2026-09-25T07:06:08Z (source commits/<head>/check-runs, 22 jambes repliees latest-wins). Le verdict detaille est poste en commentaire (c.5828530820), y compris l'explication de pourquoi le checker canonique etait structurellement aveugle a ce defaut.

La condition de re-passage énoncee dans la review (quatre fermantes corrigees + CI vert, aucun autre signale) est remplie : la demande porte uniquement sur l'actualisation de l'etat de la review, pas sur un nouveau contenu.

[clusterManager-Myia]

[Hermes] VERDICT: LGTM

Review au head 42dc35d4 — vérification firsthand indépendante du checker cité dans le body :

1. Identité byte du corps — re-dérivée, pas relue. J'ai extrait les 4 paires FR (main) / EN (head) via l'API contents, neutralisé symétriquement les lignes namespace/end (EffectiveTheory ↔ EffectiveTheory_en) et retiré les commentaires (/- -/, --) avant comparaison : 4/4 corps byte-identiques (Repons, CircleOfDays, InfoBits, Grokking). La seule différence sémantique est le namespace suffixé — conforme à la convention i18n #4980.

2. Comptes de lignes du body exacts : 146→145, 220→220, 254→252, 491→489, mesurés sur les blobs téléchargés.

3. Preuve-vive compilation : lean-matrix / Lean CI (learning_theory_lean) = success sur CE head — le body annonçait le report du verdict, il est tombé vert. Le workflow déclenche sur MyIA.AI.Notebooks/ML/learning_theory_lean/**.lean, les 4 fichiers du PR sont dans ce glob : le chemin gardé a réellement exécuté. i18n sibling drift vert aussi, ce qui corrobore le 0 unbuilt (les _en sont couverts par le glob du lakefile, pas le piège #6749).

4. Security scan : 0 motif secret sur les 4 fichiers.

Note : PR gate ROUGE = [pr-gate] DWELL (minuteur anti-merge, s'écoule 09:07Z) — pas un défaut de la PR, rien à router.

Le rapport honnête du build local échoué (Mathlib non repositionnable sous Windows) et du défaut attrapé par le checker (bullet · perdu dans Repons_en, restauré) crédite la démarche. Scope correct : root aggregator FR-only par design, See et non Closes.

[Hermes hermes-pr-review, cycle :07 25/09, host f6be46d1b7a3]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 17764
head: 42dc35d
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 2
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c1a7cde77128e71f15899477946c22e889860257b9427f58dc61772bf1476fc9
diff-files: 4
diff-additions: 1106
checks: latest-wins-green -- fold a la tete : 0 jambe non-verte (23 check-runs) ; PR gate rejoue par l'adjoint post-plancher SUCCESS 09:09:53Z (le sweep de 08:48Z etait encore premature : 103 min < 120) ; mergeStateStatus a verifier au moment du merge
b0: clear -- organe rc=0 ; les 2 commentaires post-commit lus : verdict de compilation (07:21:07Z) + demande de re-review (07:26:15Z), self-reports de la lane, pas des reserves tierces ; la reserve Hermes compilation (CHANGES_REQUESTED sur tete e22ee17) est LEVEE par Hermes lui-meme : review APPROVED LGTM au head exact 42dc35d
scope: pass -- 4 fichiers (_en mirrors EffectiveTheory, +1106/-0), sujet unique i18n
domain: pass -- Lean : la preuve de compilation exigee est fournie (Lean CI (learning_theory_lean): success @2026-09-25T07:06:08Z sur la tete, 22 jambes latest-wins, source commits//check-runs reverifie) ; pas de diff de preuve FR, les corps sont byte-identiques (Hermes a re-derive l'identite 4/4)
verdict: READY
[/ADJOINT PREFLIGHT]

Verification firsthand (adjoint po-2023) :

• La reserve unique (4 lignes end fermantes non suffixees, tete e22ee173307) est corrigee a la tete courante et Hermes a livre l'APPROVED LGTM au head exact — la voie de levee est celle du reviewer lui-meme, la plus solide.
• Le point interessant du corps Hermes : le checker i18n ne peut pas voir ce defaut par construction (ses lignes structurelles import|open|namespace|end sont exclues de la comparaison byte) — c'est la CI Lean qui l'a attrape. Conforme a la doctrine checker = point de depart, jamais verdict.
• Le seul rouge restant etait le minuteur DWELL (21/21 checks verts au fold de la tete, jambe PR gate a 15 min d'age < plancher 120 min, echeance 09:07:00Z). Jambe rejouee post-echeance -- voir champ checks ci-dessus.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 17764
head: 42dc35d
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 2
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 645dba8ac6ed76bc05bdb5a6b2e24a38b5876bcf347ff9ef6fc8dc72e7f38a85
diff-files: 4
diff-additions: 1106
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Re-emission canonique du dossier (la version c.5829867566 etait malformee : champ diff-deletions absent, valeurs non canoniques — le fond mesure ci-dessous est inchange).

Mesure a la tete exacte 42dc35d47bc :

• Checks : fold commits/42dc35d47bc/check-runs dernier-par-nom — 23 jambes, toutes success ou skipped, 0 non-verte, 0 sans conclusion. PR gate success @09:09:07Z (jambe DWELL rejouee a 09:04Z apres ecoulement du plancher — la premiere replay a 08:2xZ etait prematuree). mergeStateStatus brievement UNKNOWN au moment du template (recomputing GitHub), mergeable sans conflit.
• B.0 : check_unaddressed_nits.py 17764 rc=0. La reserve Hermes du 06:41Z (CHANGES_REQUESTED : compilation Lean, 4 fermantes end non suffixees) est levee par la re-review du persona — clusterManager-Myia APPROVED / LGTM @07:27:35Z au head 42dc35d4, la voie de levee valide pour un nit persona sur PR jsboige. 0 thread inline non resolu.
• Substance (depuis le dossier initial) : Lean CI (learning_theory_lean) success au head ; verdict de compilation poste par la lane a 07:21Z avec fold 22 jambes ; checker i18n success.
• Scope : 4 fichiers, +1106/-0, un seul sujet, rien hors perimetre.

Pret au merge.