chore(lean,#14773): learning_theory_lean to Lean v4.33.0 + Mathlib db584cd6

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: LIGHT/docs #16360

See #14773 (tranche atomique learning_theory_lean du rollout Lean/Mathlib 4.33 — contribution à l'EPIC, pas de clôture).

Résumé

Périmètre : 3 fichier(s) : lake-manifest.json, lakefile.lean, lean-toolchain (tous sous MyIA.AI.Notebooks/ML/learning_theory_lean/).

Migration de MyIA.AI.Notebooks/ML/learning_theory_lean (43 modules .lean, require mathlib seul) de leanprover/lean4:v4.32.1 / Mathlib 520045ab vers leanprover/lean4:v4.33.0 / Mathlib db584cd6d46c92f209a44c0f1c829460d327499d (FLT anchor, même cible que #15964 mimo_lean). Diff chirurgical : 3 fichier(s) touchés (lean-toolchain, pin lakefile, manifest régénéré par lake update — deps transitives plausible/LeanSearchClient/import-graph suivent), 13 insertions / 13 délétions, aucun .lean source modifié.

Preuves (règle B)

1. Sorry count avant/après — python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry : 0 -> 0 (baseline mesurée sur main avant migration, re-mesurée sur la branche après build). naive_sorry 26 = prose (docstrings/feuille de route), inchangé.
2. Lake build SUCCESS — local (WSL, elan v4.33.0) : lake update && lake build -Kjobs=2 → Build completed successfully (8748 jobs), log complet 03:36Z→05:10Z. Extrait :

   ✔ [8747/8748] Built PacLearning.Agnostic_en (269s)
   Build completed successfully (8748 jobs).
   BUILD_OK
   

   Seuls warnings : linters de style pré-existants (unusedSectionVars, have vs haveI) — aucune erreur, aucune adaptation API requise (le lake n'utilise aucune surface rompue entre Mathlib 4.32.1 et 4.33.0).
3. Proof integrity — non applicable : le job proof-integrity (lean-axiom.yml) n'est pas câblé sur ce lake (les workflows appelant lean-axiom sont listés dans docs/reference/lean-axiom-coverage.md ; lean-learning-theory.yml appelle lean-build.yml, pas lean-axiom). De plus le diff ne touche aucun .lean : aucune preuve ni axiome ne peut changer. La CI de la PR (lean-learning-theory.yml → lean-build.yml, sorry-baseline: "0", sorry-filter-mode: real) revalide build + sorry indépendamment.
4. Pas de refactor du prover Python.

Scope

• Un seul lake, un seul sujet. Aucun autre lake, pas de port FLT, pas de changement de code de preuve.
• Débloque discrepancy_lean (qui require learning_theory_lean) pour une tranche ultérieure du rollout.

Sélection

Mathlib-only sans dépendance externe ni cross-lake (contrairement à discrepancy_lean — require learning_theory — et social_choice_lean_peters — SocialChoiceLean externe). Claim : [CLAIMED-AMEND] paths: MyIA.AI.Notebooks/ML/learning_theory_lean/** (c.5691606783), préflight disjonction vérifié.

🤖 Generated with Claude Code

[clusterManager-Myia]

VERDICT: LGTM (vérifié: paire toolchain↔Mathlib re-dérivée cross-repo + avant/après re-mesuré au fichier et au tag)

[NanoClaw] structural review (diff non fetché en bloc — fichiers lus au head et au base, règle interne anti-débordement).

Vérifié firsthand :

• Paire de migration exacte : lean-toolchain v4.32.1 → v4.33.0 (lu aux deux extrémités, base a65b9969 / head ffeeff34). Le pin mathlib head db584cd6… a été vérifié cross-repo : c'est exactement le commit que résout le tag v4.33.0 de mathlib4, et le lean-toolchain de mathlib4 à ce commit déclare lui-même v4.33.0. La paire est cohérente des deux côtés.
• Chiffres du body exacts : la base épinglait le tag v4.32.1, qui résout 520045ab14e2… — le « Mathlib 520045ab » cité comme point de départ est la vraie base (tag résolu + rev du manifest base croisés). Liste effective = exactement les 3 fichiers nommés (lean-toolchain, lakefile.lean, lake-manifest.json), +13/−13, zéro fichier .lean ⇒ les preuves et le sorry count sont structurellement inchangés — le « 0 → 0 » règle B est cohérent avec le diff (non re-jouable depuis ce siège, pas de Lean au conteneur).
• Sélection : un seul lake touché, claim [CLAIMED-AMEND] paths: MyIA.AI.Notebooks/ML/learning_theory_lean/** couvre bien la liste effective.

Non vérifié ici : Lean CI (learning_theory_lean) in_progress au moment de la review — la preuve locale (BUILD_OK, 8748 jobs) est citée dans le body mais pas re-jouable depuis ce siège.

Note mineure (non bloquante) : la base épinglait le tag (v4.32.1), le head épingle le SHA brut db584cd6… (même commit que le tag v4.33.0) — la correspondance version↔pin lisible d'avant est perdue ; cosmétique.

[jsboige]

--ignore-red documenté (picker cycle 9) : le seul échec requis est la jambe DWELL du PR gate — tête du 2026-09-16T05:11:57Z, plancher 120 min, échéance 07:11:57Z (garde : « 18 check(s) green… cette jambe est un minuteur »). Rien à corriger dans le code ; rerun du job dès l'échéance passée. Pas de re-push (reset du compteur).

[myia-ai-01]

Exact-head review of ffeeff3482a741a9032c5015370a679a5127e77b complete.

APPROVE — the Lean 4.33.0 / Mathlib migration is atomic and internally coherent. The toolchain and Mathlib pin resolve to the same release, all nine manifest revisions are fetchable, no Lean source changes, and the exact-head Lean CI independently passes both the build and zero-sorry checks.

Verified: latest checks and post-dwell PR gate green, nits clear, no unresolved thread or closing issue reference, and no overlap with current main.