Repository navigation
lean(folk): normaliser le paiement actualisé et réfuter l'énoncé non normalisé #15655
Description
Activity
Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/research-code #15647
[CLAIMED] lane myia-po-2025:CoursIA — corriger la normalisation du Folk theorem et prouver le contre-exemple non normalisé
paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean[RELEASED] lane myia-po-2025:CoursIA — paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean
Aucun artefact ni commit n'a été produit par cette lane depuis son claim. La PR #15876 de myia-po-2026:CoursIA livre désormais la substance sur ces deux chemins ; le préflight B.0 exact-head �146c8a803 confirme que notre claim est l'unique cause du rouge lane_claim. Ce RELEASED lève ce verrou administratif sans préjuger de la review ni du merge, qui restent au coordinateur.
- added a commit that references this issue
on Sep 13, 2026 Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/lean #16990
[CLAIMED] lane myia-po-2025:CoursIA -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean, MyIA.AI.Notebooks/GameTheory/game_theory_lean/README.md — incrément vers le STRETCH folk_theorem_discounted : lemme d'Abel périodique (limite d→1⁻ du paiement actualisé normalisé d'une trajectoire périodique = moyenne temporelle), brique « δ → 1 » de l'énoncé verbal FM. Dossier TRACKING (issue close, registre de claim). Le sorry STRETCH n'est PAS visé ce cycle.
- added a commit that references this issue
on Sep 21, 2026
Part of #13105. See #4880.
Constat
RepeatedGames.folk_theorem_discountedformalise actuellement la réalisation d'un paiement faisable fixe par la somme actualisée non normaliséepour tout
δassez proche de1. Cet énoncé est faux, même dans l'intervalle convergent0 ≤ δ < 1ajouté par #11093.Contre-exemple : pour
g = ⟨3,2,1,0⟩etu = (2,2), les hypothèses de faisabilité et de rationalité individuelle stricte sont satisfaites. À chaque profil d'action, la somme des paiements ligne+colonne vaut au moins2. Toute trajectoire vérifie doncqui est strictement supérieur à
4 = u_row + u_coldèsδ > 1/2. Aucune trajectoire ne peut satisfaire la conclusion actuelle pour toutδproche de1.Sous-grain atomique
folk_theorem_discountedavec la normalisation canonique(1 - δ) * discountedPayoff ... = u.sorrySTRETCH sur l'existence Fudenberg–Maskin normalisée : ce grain corrige la fausseté de l'énoncé et la prouve par contre-exemple, il ne prétend pas fermer la direction difficile.Acceptation
folk_theorem_discounted_unnormalized_refuted(ou nom équivalent) compile sanssorryet établit le témoin(3,2,1,0),(2,2)pour tout seuilδ_star < 1.folk_theorem_discountedporte(1 - d)sur les deux équations de paiement.distinct_code_sorrydu lake reste1 → 1; aucun nouveausorryAx.lake build RepeatedGames.Folk RepeatedGames.Folk_enréussit sous le toolchain épinglé.Périmètre
MyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk.leanMyIA.AI.Notebooks/GameTheory/game_theory_lean/RepeatedGames/Folk_en.lean