fix(lean,#14773): bump kelly_lean 4.32.1 -> v4.33.0 (rollout 4.33)

[jsboige]

Grain: MED/lean — lane myia-po-2026:CoursIA-2 — prev: DEEP/notebook-python #16249

Summary

Migration du lake kelly_lean de la toolchain v4.32.1 vers v4.33.0 (rollout Mathlib 4.33 de l'EPIC #14773, même rev que les précédents mergés #15233/#15237/#15238 — Mathlib db584cd6d46c, résolu par le tag v4.33.0 via lake update).

• lean-toolchain : leanprover/lean4:v4.32.1 → v4.33.0
• lakefile.lean : require mathlib ... @ "v4.32.1" → @ "v4.33.0"
• lake-manifest.json : régénéré par lake update (Mathlib db584cd6d46c, dépendances resynchronisées)
• README.md : mention toolchain corrigée au passage (v4.31.0-rc1 périmée → v4.33.0 ; la mention datait d'avant le bump 4.32)

Aucune source .lean modifiée : le lake compile sans aucune adaptation de preuve à 4.33.0 (vérifié lake build post-bump, 8 712 jobs, log ci-dessous). FR/EN siblings non touchés (byte-identité préservée, aucune dérive i18n possible).

Comptage sorry (instrument canonique)

• Avant (main f76b037fa2) et après (commit b0f249f711) : python scripts/lean/count_code_sorry.py --json → kelly_lean distinct_code_sorry = 0 (naive_sorry = 1, prose uniquement — l'écart naïf/code est le point de l'instrument). La migration n'introduit aucun sorry : les sources .lean sont inchangées.

Preuves de build

• lake update → manifest régénéré, Mathlib db584cd6d46c (tag v4.33.0), dépendances resynchronisées (batteries 4488d40d, Qq 92c15be1, aesop 3448c0bc, plausible b7eb3304, importGraph 16f02aa7, proofwidgets 4be2e3d, Cli v4.33.0, LeanSearchClient 5f4d51b8)
• lake exe cache get → oleans Mathlib 4.33 (8 689 fichiers, cache local, aucun téléchargement résiduel)
• lake build : Build completed successfully (8712 jobs) — Kelly.Kelly, Kelly.Kelly_en, Kelly.Growth, Kelly.Growth_en, Kelly.Bet, Kelly.Bet_en tous bâtis (WSL, toolchain v4.33.0, commit b0f249f711)
• CI lean-kelly.yml re-déclenchée par le path lean-toolchain (déclencheur lignes 23/31)

Proof integrity (B.3)

Non applicable — cas (a) : le job lean-axiom n'est pas câblé sur le lake de cette PR (lean-kelly.yml n'appelle pas lean-axiom.yml ; câblage existant : 12 autres lakes — conway, knot, percolation, planning, sensitivity, social-choice, etc.). Aucun sorry/native_decide introduit (cf comptage ci-dessus), sources inchangées.

Chiffres

• Additions/suppressions (gh api repos/jsboige/CoursIA/pulls/16328) : +14 / −14, 4 fichiers — même profil que fix(lean,#14773): bump erc20_lean 4.32.1 -> v4.33.0 (rollout 4.33, Mathlib db584cd6) #15238 (erc20 : +14/−14).

Références

See #14773 (rollout 4.33 — sous-grain kelly_lean). Claim : issuecomment-5685687799 (paths MyIA.AI.Notebooks/QuantConnect/kelly_lean/**).

---

🤖 Generated with Claude Code

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-15) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=4 cap=3)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=0 genre=4 cap=3)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.