build(mimo,#14773): migrate lake to Lean 4.33

[jsboige]

Grain: MED/lean — lane myia-po-2025:CoursIA — prev: LIGHT/docs #15567

Résumé

• migre mimo_lean de Lean/Mathlib 4.32.1 vers Lean 4.33.0 et Mathlib au commit exact db584cd6d46c92f209a44c0f1c829460d327499d ;
• régénère la fermeture transitive Mathlib 4.33 (Batteries, Qq, Cli, Aesop, ProofWidgets, ImportGraph, LeanSearchClient, Plausible) ;
• conserve SLT sur la base upstream exacte d0f506f0a695018265dccb33bcb05e2f5ca1c876, via le commit de compatibilité Lean 4.33 borné jsboige/lean-stat-learning-theory@0b1020a4771037b89d0b3809913608d177c09a14 (proposé upstream dans YuanheZ/lean-stat-learning-theory#4) ;
• documente la contrainte d'ordre des require : le lake SLT cible encore Mathlib 4.32, donc Mathlib doit être déclaré en dernier pour que Lake 5 sélectionne sa fermeture 4.33 ;
• ne modifie aucune preuve MIMO ni aucun package sous .lake/packages.

Résolution du conflit de dépendances

Le premier manifest ne mettait à jour que le package direct mathlib tout en conservant les transitifs 4.32 hérités de SLT. Le build exact était visible avant les modules MIMO (Batteries.Data.BinaryHeap.Basic, Batteries.Data.ByteArray, Batteries.Recycling.MonadSatisfying.Basic, Batteries.Lean.LawfulMonadLift, Batteries.Tactic.Alias, Qq.Typ).

Après inversion des deux dépendances directes et lake update, ces mêmes modules compilent sous leurs pins 4.33. Le build complet a ensuite atteint SLT.HansonWright à 8685/8753 et révélé une unique dérive de tactique au cas de rayon nul (failed to prove positivity/nonnegativity/nonzeroness). Le commit SLT 0b1020a… remplace ce positivity fragile par les lemmes explicites de non-négativité ; le module corrigé compile en 3189/3189 jobs contre Lean/Mathlib 4.33, sans changer son énoncé.

scripts/lean/compare_lake_manifests.py --root <worktree> place mimo_lean dans le cluster de référence des 13 lakes Lean 4.33 ; sa seule différence est le package supplémentaire slt, attendu.

Validation Lean réelle

lake exe cache get
Aucune complétion observée : processus silencieux et sans croissance de fichiers,
arrêté proprement après plus de 22 minutes. Aucun cache WSL disponible ne
correspondait au pin Mathlib db584cd6 ; aucun cache 4.32 incompatible n'a été réutilisé.

lake build
Build completed successfully (8753 jobs).

Le build complet a été exécuté dans un clone WSL ext4 du lake après l'arrêt
propre du téléchargement de cache bloqué ; il utilise exactement Mathlib
`db584cd6d46c92f209a44c0f1c829460d327499d` et SLT
`0b1020a4771037b89d0b3809913608d177c09a14`.

Dette formelle

{
  "lake": "MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean",
  "files": 13,
  "code_sorry": 0,
  "distinct_code_sorry": 0,
  "vacuous": []
}

Avant : distinct_code_sorry = 0. Après : distinct_code_sorry = 0.

Convention i18n

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

Les six siblings MIMO (Bridge_en, Converse_en, Descent_en, Lmmse_en, NormTails_en, Objective_en) restent valides et sont construits comme cibles du lake.

Audit des axiomes

proof-integrity est câblé sur mimo_lean avec target-modules: "*", include-i18n-siblings: "true" et fail-on-sorry: true : B.3 est applicable.

Audit local #print axioms après build :

'Mimo.descent_target_before_ceiling' depends on axioms: [propext, Quot.sound]
'Mimo.mimo_flip_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mimo.lmmse_error_eq_trace' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mimo.chisq_norm_concentration' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mimo.mimo_flip_cost_via_bridge' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mimo.ml_error_prob_ge_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mimo.norm_concentration' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mimo.mimoObj' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mimo.B_ρ' depends on axioms: [propext, Classical.choice, Quot.sound]

• zéro sorryAx ;
• zéro native_decide.* ;
• Classical.choice est présent sur huit des neuf déclarations auditées ;
• propext et Quot.sound sont présents ;
• ces trois noms appartiennent à la whitelist explicite par défaut de lean-axiom.yml; allow-axioms: "" signifie donc « aucun axiome supplémentaire », et non « whitelist vide ».

Collision bornée

La PR ouverte #15613 renumérote la colonne Lean et touche deux références de notebook dans mimo_lean/README.md (Lean-22b → Lean-21b). Le présent diff touche le même README dans des hunks distincts — version/pins en tête et caveat de résolution des dépendances — sans modifier ces références. Un rebase après #15613 conservera les deux changements.

See #14773.

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15964 (build(mimo,#14773): migrate lake to Lean 4.33) 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.

• faible -- renum(lean,#15612): refermer la colonne canonique (trous 18/25) — deux decalages (19..24 en N-1, 26..32 en N-2), arborescence finale 01..30 #15613 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md