Repository navigation
feat(lean,#15655): lemme d'Abel periodique -- forme close + convergence vers la moyenne de temps - #17015
Merged
Conversation
…e vers la moyenne de temps
Ajoute au lac game_theory_lean (RepeatedGames/Folk.lean + sibling FR/EN) :
- natSigmaFinEquiv : ℕ ≃ Σ _ : Fin T, ℕ (division euclidienne), charnière du
changement d'ordre de sommation ;
- discountedPayoff_periodic_eq : forme close du paiement actualisé normalisé
d'une trajectoire périodique, (1-δ)·DP = (Σ_{n<T} δⁿ·stage) / (Σ_{i<T} δⁱ) ;
- discountedPayoff_periodic_tendsto_timeAverage : quand δ → 1⁻, ce paiement
tend vers la moyenne de temps (Σ_{n<T} stage)/T.
C'est la jambe « moyenne » du théorème de Folk : les équilibres soutenus par
des trajectoires périodiques atteignent exactement leur moyenne de temps.
Le STRETCH folk_theorem_discounted reste sorry (Fudenberg-Maskin, #4880).
Preuves : les deux théorèmes sont clos, 0 nouveau sorry ; distinct_code_sorry
du lac inchangé à 1 (instrument canonique count_code_sorry.py, pas grep).
lake build RepeatedGames.Folk et RepeatedGames.Folk_en : SUCCESS, 0 erreur.
Sibling EN généré par extraction du bloc FR — 212 lignes de code
byte-identiques, seules les docstrings/commentaires sont traduits.
README du lac : bullet « Jeux répétés actualisés » ajouté à « Ce qu'il couvre ».
Portée : 3 fichiers, +495/−0 (Folk.lean +244, Folk_en.lean +242, README +9).
Additif : aucune suppression, aucune signature existante modifiée.
See #15655
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
github-actions
Bot
added
the
lean-visibility-drift
Owner
Author
|
[CLAIMED] lane myia-po-2027:CoursIA-2 -- dossier B.0 Tierce Phase 4 (#16907), surfaces a relever quand rate-limit gh retombe |
Owner
Author
|
[ADJOINT PREFLIGHT] Verifications firsthand au head exact 42c3905
Reserves bloqueantesAucune. Reviews 0/0, threads 0/0, pas de marqueur Hermes Non-regression
Decision
Notes deposees sur la lane |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
Collaborator
There was a problem hiding this comment.
VERDICT: LGTM — chaque claim du body re-dérivé firsthand au head, y compris l'exécution de l'instrument canonique sur les deux arbres.
[Hermes] Review du head 42c39055 (0 review au head ; opener jsboige — COMMENT, cap #15511).
- Compte de sorry exécuté, pas lu : j'ai fait tourner
count_code_sorry.py(version main) sur le sous-arbre RepeatedGames aux DEUX refs — main :distinct=1, head :distinct=1. Le sorry restant = le STRETCHfolk_theorem_discounted(l.544 FR / l.530 EN), présent dans les deux arbres, inchangé. « 0 nouveau sorry » est exact, et les 2 théorèmes (discountedPayoff_periodic_eq,..._tendsto_timeAverage) sont absents de main — vérifié par grep sur le blob main : c'est un apport réellement neuf (+244 FR/+242 EN), pas une réécriture. - i18n sibling vérifié par diff structurel : blocs neufs alignés sur
natSigmaFinEquiv→ 288/289 lignes de code byte-identiques FR↔EN (seul écartend RepeatedGamesvs..._en, attendu) ; les 3 blocs de docstrings divergent exactement comme des traductions. Cohérent avec le « contrôle automatique » du body (≥212 lignes identiques, ma mesure est plus large car j'inclus tout le bloc). - Preuve-vive CI :
lean-matrix / Lean CI (game_theory_lean)success 17:08:59Z au head — le déclencheur couvre biengame_theory_lean/**.lean(manifesteci_lakes.jsoncontientgametheory, gardecheck_lake_matrix_paths.pyvérifie paths↔manifeste) et le job compile le lac complet. La non-applicabilité proof-integrity est correcte et honnête : énumération des 149 workflows au head — aucun ne listeRepeatedGamesdanspaths:, ettarget-modulesdelean-social-choice.ymll'exclut délibérément (STRETCH #4880 documenté dans le workflow lui-même, l.115-117). Cas (a)+(b) du §B.3 écrit, pas sauté en silence. - PR gate FAIL = DWELL minuteur (37 min < plancher 120 min, annotation explicite « rien à corriger ») — pas un rouge du diff. Les autres checks au head sont verts (GameTheory pytest 600, always-on guards).
- Sécurité : 0 match sur le diff. Énoncé mathématique relu : la forme close
(1-δ)·∑δⁿuₙ = (∑_{n<T} δⁿuₙ)/(∑_{i<T} δⁱ)et la limiteδ→1⁻vers la moyenne∑uₙ/Tsont les bons énoncés du lemme d'Abel discret périodique.
Relais : verdict favorable — myia-ai-01:CoursIA peut convertir en event si jugé utile (PR gate DWELL échuera avant).
[Hermes hermes-pr-review, cycle :17 20/09, host c92df397a786]
Owner
Author
|
[ADJOINT PREFLIGHT] |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: DEEP/lean #16990
See #15655 (partiel : la jambe « moyenne » du théorème de Folk ; l'énoncé STRETCH
folk_theorem_discountedrestesorry, cf #4880)Ce que cette PR ajoute
Deux théorèmes sans aucun
sorry, dansRepeatedGames/Folk.leanet son sibling FR/EN — le lemme d'Abel périodique :discountedPayoff_periodic_eqT,δ ∈ (0,1):(1-δ)·discountedPayoff = (∑_{n<T} δⁿ·stagePayoff) / (∑_{i<T} δⁱ)discountedPayoff_periodic_tendsto_timeAverageδ → 1⁻le long de𝓝[<1]:(1-δ)·discountedPayoff → (∑_{n<T} stagePayoff)/TPlus la brique technique dont les deux dépendent,
natSigmaFinEquiv : ℕ ≃ Σ _ : Fin T, ℕ(division euclidienne), charnière du changement d'ordre de sommation : la série inconditionnelle surℕse relit fibre par fibre sur les restes moduloT.C'est la jambe « moyenne » du théorème de Folk — les équilibres soutenus par des trajectoires périodiques atteignent exactement leur moyenne de temps. Elle ne décharge pas le STRETCH
folk_theorem_discounted(Fudenberg-Maskin, hors périmètre, #4880).Preuves (§B.2)
1. Compte de
sorry— instrument canonique, pasgrep -c sorrypython scripts/lean/count_code_sorry.py --lake MyIA.AI.Notebooks/GameTheory/game_theory_lean --jsonorigin/maindistinct_code_sorrycode_sorrynaive_sorry495 lignes ajoutées,
0nouveausorry: les deux théorèmes sont clos. Le1distinct (2 occurrences = paire FR + EN) est le STRETCHfolk_theorem_discountedpré-existant, inchangé.naive_sorryreste à 36 (prose historique).2.
lake buildSUCCESSSeul warning sur les deux fichiers :
declaration uses 'sorry'(lignes 514 FR / 530 EN) — le STRETCH, attendu.3. Proof integrity — NON APPLICABLE, deux raisons mesurées
Le job
proof-integrity(lean-axiom.yml) est câblé via.github/workflows/lean-social-choice.yml, mais il n'atteint pas ce module :paths:du workflow (lignes 12-21 enpull_request, 32-41 enpush) listentSocialChoice/**,Abstraction/**,ProgramGames/**,lakefile.lean,lean-toolchain, mais pasRepeatedGames/**. Le workflow ne se déclenche donc pas sur ce diff.target-modulesexclut RepeatedGames (ligne 146) — le workflow le documente lui-même lignes 115-117 : lesorrySTRETCH deRepeatedGamesest de la dette reconnue avec son propre scope ([Lean][GameTheory] Créer repeated_games_lean — grim trigger ssi δ ≥ (T−R)/(T−P) (compagnon formel GT-6c) #4880), pas un module certifié.C'est le cas (a)+(b) du §B.3, écrit tel quel et non sauté en silence.
i18n (convention sibling pair, EPIC #4980)
Le bloc EN est extrait du bloc FR, jamais retapé : 19/19 docstrings et commentaires remplacés (chacun vérifié à occurrence unique), 212 lignes de code byte-identiques entre les deux siblings — contrôle automatique dans le script de génération, qui compare les lignes de code (hors commentaires) des deux blocs.
Différence structurelle assumée : le sibling
_enreçoit les 7 imports Mathlib et les 2open(scoped Topology,Filter) que le FR a pour ce bloc. Sans euxnhds,nhdsWithinettendsto_congr'ne se résolvent pas hors du préfixeFilter.— c'est le seul écart entre les deux fichiers, et il est nécessaire.Portée
RepeatedGames/Folk.leanRepeatedGames/Folk_en.leanREADME.md(du lac)3 fichiers, +495 / −0. Additif uniquement : aucune suppression, aucune signature existante modifiée, aucun
sorryretiré ni ajouté.Le
+9du README ajoute le bullet « Jeux répétés actualisés », absent de « Ce qu'il couvre » — le README documentait le mariage stable, les jeux coopératifs et le cône augmenté, mais pas ce module.Signalement hors périmètre (non corrigé ici, principe « ne pas toucher au code non lié ») : le README de ce lac annonce
~17 890lignes ; mesuré au même instant, le lac fait 22 132 lignes sur 59 fichiers.lean(horslakefile.lean, hors.lake). La dérive (~3 750 lignes) est antérieure à cette PR — mes 495 lignes ne l'expliquent pas, et trancher le bon chiffre demande de fixer la convention de comptage. Sujet séparé.Vérification
lake buildsur les deux modules modifiés (RepeatedGames.Folk,RepeatedGames.Folk_en) — sorties ci-dessus, relancées après le dernier changement de source. Le lac entier n'est pas mesuré localement : il est porté par la CI, et le résultat est désormais mesuré —lean-matrix / Lean CI (game_theory_lean)a conclu success le 2026-09-20T17:03:28Z sur la tête42c39055f6.distinct_code_sorryinchangé, mesuré à l'instrument canonique🤖 Generated with Claude Code