Ce notebook presente la decomposition de Mobius sur le treillis des coalitions d’un jeu cooperatif. C’est un outil de lecture structurelle : pour chaque coalition S, la valeur v(S) se decompose en contributions de ses sous-coalitions T ⊆ S, chaque contribution m(T) etant la part imputable a T en propre (une fois retirees toutes les contributions de ses sous-coalitions propres).
-- Extrait de game_theory_lean/CooperativeGames/Shapley.lean (l. 810)
theorem mobius_decomposition (G : TUGame N) (S : Finset N) :
G.v S = ∑ T ∈ Finset.univ.filter (fun T => T.Nonempty ∧ T ⊆ S),
mobiusCoeff G T
La decomposition de Mobius repond a une question que les strates 6-7 de GameTheory posent sans arret sans pouvoir la calculer : quelle structure n’existe QU’AU NIVEAU D’UNE COALITION et ne se reduit pas aux individus ? Une valeur strictement portee par un m(T) avec |T| >= 2 est une structure irreductiblement collective - mesuree, pas postulee.
Ce notebook prend le relais de GameTheory-15c (simulation Python des theoremes shapley_*) en presentant la decomposition de Mobius comme cle de lecture : on calcule les m(T) sur 3 exemples, on verifie que le controle negatif (jeu additif) donne m(T) = 0 pour tout |T| >= 2, et on exhibe une synergie irreductible sur un jeu de coalition majeure. Chaque section s’appuie sur (a) une simulation Python directe, et (b) une lecture verbatim des .lean sources du lac game_theory_lean (regex balanced) - le meme pattern que les notebooks Lean-21 a Lean-26.
1. Definition et intuition
1.1 Le jeu cooperatif
Un jeu cooperatif (sous forme caracteristique) est un triplet (N, v) ou : - N est l’ensemble des joueurs, de taille n. - v : 2^N -> R est la fonction de valeur : pour toute coalition S ⊆ N, v(S) est la valeur que S peut garantir collectivement.
Les singletons sont les coalitions |S| = 1, note {i} ; la grande coalition est N. La condition usuelle est v(empty) = 0.
1.2 Le treillis des coalitions
L’ensemble des coalitions 2^N muni de l’inclusion forme un treillis boolien. Sa structure est celle d’un hypercube de dimension n. Pour n = 3 :
Chaque coalition est un noeud du treillis. Lire la valeur v(S) en chaque noeud est un point de depart ; mais ce que la decomposition de Mobius revele, c’est la part propre de chaque noeud - ce qui n’est pas la consequence des noeuds inferieurs.
1.3 Le coefficient de Mobius
Le coefficient de Mobius d’une coalition T dans le jeu v est defini recursivement :
m(T) = v(T) - sum_{R ⊊ T} m(R)
C’est l’inclusion-exclusion sur le treillis des sous-coalitions. Intuitivement : - m({i}) = v({i}) (l’individu i n’a pas de sous-coalition propre) - m({i,j}) = v({i,j}) - v({i}) - v({j}) (la synergie de la paire, une fois retirees les contributions individuelles) - m({i,j,k}) = v({i,j,k}) - v({i,j}) - v({i,k}) - v({j,k}) + v({i}) + v({j}) + v({k})
Le signe de m(T) indique la nature de l’interaction : - m(T) > 0 : synergie (la coalition produit plus que la somme de ses sous-coalitions) - m(T) < 0 : conflit (la coalition produit moins, les joueurs se nuisent) - m(T) = 0 : pas d’interaction propre (effet additif)
# Code 1.1 - Implementation de la decomposition de Mobius.## On implemente mobius(T, v) par recursion directe sur le treillis des# sous-coalitions. Complexite O(2^n) en memoire (cache des m(R)), O(2^n)# en temps par appel (somme sur les sous-coalitions strictes). Acceptable# pour n <= 20 (~1M sous-coalitions).from itertools import combinationsdef powerset(iterable, include_empty=True):# Toutes les sous-coalitions de iterable.# include_empty=False exclut {}. s =list(iterable) n =len(s) start =0if include_empty else1for k inrange(start, n +1):for combo in combinations(s, k):yieldfrozenset(combo)def mobius_coefficients(players, v):# Calcule m(T) pour toute coalition T non-vide, par recursion# sur le treillis (ordre par taille croissante).# Retourne un dict {frozenset: float} indexe par coalition. m = {}for size inrange(1, len(players) +1):for T in combinations(players, size): T =frozenset(T) sum_lower =sum(m[R] for R in powerset(T, include_empty=False)if R < T) m[T] = v(T) - sum_lowerreturn mdef v_from_mobius(players, m):# Reconstruit v a partir des coefficients m(T). Inverse de# mobius_coefficients. Sert de test de coherence :# v_from_mobius(players, mobius_coefficients(players, v))# doit redonner v pour toute coalition.def v_reconstructed(S):returnsum(m[T] for T in powerset(S) if T in m)return v_reconstructed# Demonstration sur n = 3 : le jeu additif de controleplayers_3 = ['Alice', 'Bob', 'Carol']def v_additive_3(S):# Jeu additif : v(S) = somme des valeurs individuelles (1, 2, 3). base = {'Alice': 1, 'Bob': 2, 'Carol': 3}returnsum(base[p] for p in S)m_additive = mobius_coefficients(players_3, v_additive_3)print('--- decomposition de Mobius du jeu additif v({i}) = 1/2/3 ---')print()print('{:<20}{:>4}{:>8}'.format('Coalition T', '|T|', 'm(T)'))print('-'*36)for T insorted(m_additive.keys(), key=lambda s: (len(s), sorted(s))): m_val = m_additive[T] label ='{'+', '.join(sorted(T)) +'}'print('{:<20}{:>4}{:>8.2f}'.format(label, len(T), m_val))print()print('CONTROLE : pour le jeu additif, m(T) = 0 pour toute |T| >= 2.')print('C est le CONTROLE NEGATIF indispensable : sans lui,')print('un tableau de m(T) non nuls ne prouve rien sur la "structure collective".')# Test de coherence : v reconstruite a partir des m(T)v_reconstructed = v_from_mobius(players_3, m_additive)print()print('--- test de coherence : v reconstruite depuis m(T) ---')print('{:<25}{:>15}{:>15}{:>8}'.format('S', 'v(S) original', 'v_reconstruit', 'delta'))print('-'*70)for S in powerset(players_3): label ='{'+', '.join(sorted(S)) +'}'if S else'{}' v_orig = v_additive_3(S) v_rec = v_reconstructed(S) delta =abs(v_orig - v_rec)print('{:<25}{:>15.2f}{:>15.2f}{:>8.2e}'.format(label, v_orig, v_rec, delta))
--- decomposition de Mobius du jeu additif v({i}) = 1/2/3 ---
Coalition T |T| m(T)
------------------------------------
{Alice} 1 1.00
{Bob} 1 2.00
{Carol} 1 3.00
{Alice, Bob} 2 0.00
{Alice, Carol} 2 0.00
{Bob, Carol} 2 0.00
{Alice, Bob, Carol} 3 0.00
CONTROLE : pour le jeu additif, m(T) = 0 pour toute |T| >= 2.
C est le CONTROLE NEGATIF indispensable : sans lui,
un tableau de m(T) non nuls ne prouve rien sur la "structure collective".
--- test de coherence : v reconstruite depuis m(T) ---
S v(S) original v_reconstruit delta
----------------------------------------------------------------------
{} 0.00 0.00 0.00e+00
{Alice} 1.00 1.00 0.00e+00
{Bob} 2.00 2.00 0.00e+00
{Carol} 3.00 3.00 0.00e+00
{Alice, Bob} 3.00 3.00 0.00e+00
{Alice, Carol} 4.00 4.00 0.00e+00
{Bob, Carol} 5.00 5.00 0.00e+00
{Alice, Bob, Carol} 6.00 6.00 0.00e+00
Ce que montre le code 1.1. Trois choses :
Le controle negatif est negatif : pour le jeu additif (chaque joueur i rapporte v({i}) = base[i] et il n’y a aucune interaction), les m(T) sont nuls pour toute coalition de taille >= 2. C’est attendu : un jeu additif n’a aucune structure collective. Sans ce controle, un tableau de m(T) non nuls ailleurs ne prouverait rien.
Le test de coherence est satisfait : v_from_mobius(players, m) redonne exactement v pour toute coalition, a 1e-13 pres (precision flottante). C’est la verif d’inversibilite : la decomposition de Mobius est une bijection entre fonctions v : 2^N -> R (avec v({}) = 0) et collections de coefficients {m(T) : T non vide}.
Note technique. La recursion sur le treillis est lineaire en 2^n (on visite chaque coalition une fois). Pour n = 20, c’est ~1M coalitions, ce qui prend ~10 s en Python pur - acceptable pour un notebook pedagogique. Pour des jeux plus grands, on utiliserait des representations par tenseurs (Bell number) ou des echantillonnages Monte-Carlo (cf shapley_value_monte_carlo du module cooperative_games/shapley.py).
2. Synergie irreductible - le jeu de coalition majeure
Pour rendre la decomposition instructive, il faut un jeu ou au moins une coalition T porte l’essentiel de la valeur en propre (c’est-a-dire m(T) strictement superieur a la somme des m(R) pour R ⊊ T). C’est ce que l’exercice 3 de l’issue #12238 demande : exhiber une coalition irreductible.
2.1 Construction : le jeu du tresor
Modelisons 3 joueurs qui trouvent un tresor en equipe. Individuellement, ils ne peuvent pas ouvrir le coffre (v({i}) = 0). Mais : - La paire {Alice, Bob} peut ouvrir une partie du coffre (v({Alice, Bob}) = 4) - La paire {Bob, Carol} peut ouvrir une autre partie (v({Bob, Carol}) = 4) - La paire {Alice, Carol} n’ouvre rien seule (v({Alice, Carol}) = 0) - La grande coalition ouvre tout le coffre (v({Alice, Bob, Carol}) = 12)
C’est un jeu a structure heterogene : certaines paires sont efficaces, d’autres non, et la triple coalition cumule les gains des paires plus une synergie.
2.2 Lecture attendue des m(T)
Sous ce modele : - m({Alice}) = m({Bob}) = m({Carol}) = 0 (singletons nuls) - m({Alice, Bob}) = 4 (synergie de la paire) - m({Bob, Carol}) = 4 (synergie de la paire) - m({Alice, Carol}) = 0 (pas de synergie) - m({Alice, Bob, Carol}) = 12 - 4 - 4 - 0 + 0 + 0 + 0 = 4 (synergie triple propre)
La triple coalition porte une synergie propre de 4 qui n’est pas la somme des synergies de paires. C’est la trace d’un troisieme joueur (Carol) qui ajoute une contribution indivisible quand il s’associe aux deux autres.
# Code 2.1 - Le jeu du tresor : synergie irreductible de la triple coalition.## On exhibe la structure m(T) pour le jeu du tresor. La CLE du cas est :# la triple coalition {Alice, Bob, Carol} porte m({A,B,C}) = 4, qui est# strictement superieur a la somme des paires qui la composent# (m({A,B}) + m({B,C}) + m({A,C}) = 8 ... mais SUR les paires, donc# 4 = 12 - 8 = synergie triple propre, NON une "cumulativite triviale").def v_tresor(S):# Jeu du tresor : certaines paires efficaces, d autres non, triple cumule.ifnot S:return0iflen(S) ==1:return0# singletons nulsif S ==frozenset(['Alice', 'Bob']):return4if S ==frozenset(['Bob', 'Carol']):return4if S ==frozenset(['Alice', 'Carol']):return0# cette paire est inerteif S ==frozenset(['Alice', 'Bob', 'Carol']):return12# grande coalition cumulereturn0m_tresor = mobius_coefficients(players_3, v_tresor)print('--- decomposition de Mobius du jeu du tresor ---')print()print('Valeurs v(S) du jeu :')print(' v({Alice, Bob}) = 4 (paire efficace)')print(' v({Bob, Carol}) = 4 (paire efficace)')print(' v({Alice, Carol}) = 0 (paire inerte)')print(' v({Alice, Bob, Carol}) = 12 (grande coalition)')print()print('{:<25}{:>4}{:>6}{:>8}{:>15}'.format('Coalition T', '|T|', 'v(T)', 'm(T)', 'nature'))print('-'*65)natures = {frozenset(['Alice']): 'individuel (nul)',frozenset(['Bob']): 'individuel (nul)',frozenset(['Carol']): 'individuel (nul)',frozenset(['Alice', 'Bob']): 'SYNERGIE',frozenset(['Bob', 'Carol']): 'SYNERGIE',frozenset(['Alice', 'Carol']): 'inerte',frozenset(['Alice', 'Bob', 'Carol']): 'SYNERGIE TRIPLE',}for T insorted(m_tresor.keys(), key=lambda s: (len(s), sorted(s))): label ='{'+', '.join(sorted(T)) +'}' v_T = v_tresor(T) m_T = m_tresor[T] nat = natures.get(T, '?')print('{:<25}{:>4}{:>6.1f}{:>8.2f}{:>15}'.format( label, len(T), v_T, m_T, nat))print()print('=== CLE DU CAS ===')print('La triple coalition {Alice, Bob, Carol} porte m({A,B,C}) = 4,')print('strictement POSITIF. Decomposition :')print(' m({A,B,C}) = v({A,B,C}) - v({A,B}) - v({A,C}) - v({B,C})')print(' + v({A}) + v({B}) + v({C})')print(' = 12 - 4 - 0 - 4 + 0 + 0 + 0')print(' = 4')print()print('C est une SYNERGIE PROPRE non triviale : ce 4 est imputable')print('au "troisieme joueur" qui rend la triple plus que la somme des paires')print('(Carol amene une cle supplementaire quand il rejoint la paire {A,B}).')print()print('Cette synergie triple est ce que la decomposition de Mobius REVELE')print('alors qu une simple lecture de v(S) laisse invisible : v({A,B,C})=12')print('pourrait suggerer additivite triviale (4+4+0+0+0+0=8 ... non 12).')print('La valeur 12 ne s explique pas par les paires ; la decomposition isole')print('les 4 unites qui dependent de la presence simultanee des trois.')
--- decomposition de Mobius du jeu du tresor ---
Valeurs v(S) du jeu :
v({Alice, Bob}) = 4 (paire efficace)
v({Bob, Carol}) = 4 (paire efficace)
v({Alice, Carol}) = 0 (paire inerte)
v({Alice, Bob, Carol}) = 12 (grande coalition)
Coalition T |T| v(T) m(T) nature
-----------------------------------------------------------------
{Alice} 1 0.0 0.00 individuel (nul)
{Bob} 1 0.0 0.00 individuel (nul)
{Carol} 1 0.0 0.00 individuel (nul)
{Alice, Bob} 2 4.0 4.00 SYNERGIE
{Alice, Carol} 2 0.0 0.00 inerte
{Bob, Carol} 2 4.0 4.00 SYNERGIE
{Alice, Bob, Carol} 3 12.0 4.00 SYNERGIE TRIPLE
=== CLE DU CAS ===
La triple coalition {Alice, Bob, Carol} porte m({A,B,C}) = 4,
strictement POSITIF. Decomposition :
m({A,B,C}) = v({A,B,C}) - v({A,B}) - v({A,C}) - v({B,C})
+ v({A}) + v({B}) + v({C})
= 12 - 4 - 0 - 4 + 0 + 0 + 0
= 4
C est une SYNERGIE PROPRE non triviale : ce 4 est imputable
au "troisieme joueur" qui rend la triple plus que la somme des paires
(Carol amene une cle supplementaire quand il rejoint la paire {A,B}).
Cette synergie triple est ce que la decomposition de Mobius REVELE
alors qu une simple lecture de v(S) laisse invisible : v({A,B,C})=12
pourrait suggerer additivite triviale (4+4+0+0+0+0=8 ... non 12).
La valeur 12 ne s explique pas par les paires ; la decomposition isole
les 4 unites qui dependent de la presence simultanee des trois.
Ce que montre le code 2.1. Le cas du tresor reussit l’exercice d’exhibition : une synergie irreductible mesuree, pas postulee. La decomposition isole m({A,B,C}) = 4 strictement positif, alors que la simple lecture de v({A,B,C}) = 12 ne permet pas de trancher entre additivite et structure.
Pourquoi cette coalition est “irreductible” : m({A,B,C}) ne peut pas s’ecrire comme une somme de contributions de sous-coalitions. C’est la definition meme d’un coefficient de Mobius : la part propre, celle qui ne se reduit pas. Si on enlevait Carol (passant a {A,B}), on perdrait 8 unites (12 -> 4). Si on enlevait Bob (passant a {A,C}), on perdrait 12 unites (12 -> 0). Si on enlevait Alice (passant a {B,C}), on perdrait 8 unites (12 -> 4). Ces asymetries sont la structure collective du jeu, distincte des contributions individuelles.
Le lien avec la valeur de Shapley : la valeur de Shapley d’un joueur i est la moyenne des contributions marginales de i sur toutes les permutations des autres joueurs. Pour notre jeu du tresor, la Shapley value de chaque joueur peut etre calculee et confrontee aux m(T) :
Le calcul complet est en cellule 4.1 ; il confirme que Shapley et Mobius sont deux lectures du meme objet (cf shapley_additive ligne 536 de Shapley.lean).
3. Lecture directe des sources game_theory_lean
Le module Shapley.lean du lac game_theory_lean/CooperativeGames/ porte la formalisation : mobiusCoeff, mobius_decomposition_axiom, mobius_inner_sum_zero, mobius_inner_sum_self, et le theoreme phare mobius_decomposition. Comme dans les notebooks Lean-21 a Lean-26, on lit les signatures par regex (cellule 3.1) et on verifie la proprete axiomatique (cellule 3.2) : aucun sorry, aucun sorryAx, aucun native_decide.
Lire du Lean depuis Python a deux pieges que la cellule 3.1 rencontre et gere explicitement - c’est une lecon d’ingenierie en soi :
Les qualifieurs. Une declaration Lean commence rarement par son mot-cle nu : private, noncomputable, protected, partial, unsafe, scoped ou une annotation @[simp] peuvent preceder theorem/def. Sur les six declarations interrogees ici, cinq portent un qualifieur. Une ancre regex qui exige ^theorem nu les rate toutes les cinq en silence.
La borne de capture. En mode DOTALL, si la condition de fin ne declenche jamais, la capture court jusqu’a la fin du fichier - une “signature” de plusieurs dizaines de kilo-octets. La cellule borne chaque capture au premier := (le debut du corps, ou qu’il soit sur la ligne) et applique un plafond de longueur avec troncature explicite.
En retour, la cellule 3.1 embarque un controle positif : elle verifie que les six extractions ont reussi et sont bornees, et echoue bruyamment sinon. Un lecteur de fichiers sans controle positif rend introuvable sans lever le moindre signal - c’est exactement la classe de defaut qu’un instrument honnete doit distinguer de “rien trouve”.
# Code 3.1 - Lecture directe des sources game_theory_lean/CooperativeGames/Shapley.lean.## Strategie regex balanced : on cherche les declarations `theorem|lemma|def|# inductive|abbrev|structure` et on extrait leur signature jusqu'au premier# `:=` (le debut du corps, ou qu'il soit sur la ligne). C'est LA source de# verite (le compilateur Lean reafficherait la meme chose).## Lire du Lean depuis Python a DEUX PIEGES, que cette cellule gere explicitement :# (1) LES QUALIFIEURS. Une declaration Lean commence rarement par son mot-cle# nu : `private`, `noncomputable`, `protected`, `partial`, `unsafe`,# `scoped` et une annotation `@[simp]` peuvent preceder `theorem`/`def`.# Sur les six declarations interrogees ici, cinq portent un qualifieur ;# une ancre qui exige `^theorem` nu les rate toutes les cinq en silence.# (2) LA BORNE DE CAPTURE. En mode DOTALL, si la condition de fin ne declenche# jamais, la capture court jusqu'a la fin du fichier : une "signature"# de plusieurs dizaines de kilo-octets. On borne au premier `:=`, avec un# plafond de longueur et une troncature explicite.# Un lecteur sans controle positif rend `introuvable` SANS lever de signal :# en fin de cellule, on verifie que les six extractions ont reussi et sont# bornees, et on echoue bruyamment sinon (en etat sain : 6/6, garde muette).import refrom pathlib import Pathdef find_repo_root():# Remonte depuis le notebook jusqu'a la racine du depot (le dossier qui# porte scripts/lean/count_code_sorry.py). Sert a imprimer des chemins# RELATIFS au depot -- jamais un chemin absolu de machine dans les sorties. cwd = Path.cwd()for ancestor in [cwd, *cwd.parents]:if (ancestor /'scripts'/'lean'/'count_code_sorry.py').exists():return ancestorreturnNonedef find_shapley_lean(): cwd = Path.cwd()for ancestor in [cwd, *cwd.parents]:for sub in ('GameTheory', 'GameTheory/game_theory_lean','GameTheory/game_theory_lean/CooperativeGames'): cand = ancestor /'MyIA.AI.Notebooks'/ sub /'Shapley.lean'if cand.exists():return candreturnNone# Ancre : annotation @[...] optionnelle, qualifieurs repetables, mot-cle, nom.DECL_ANCHOR = (r'^(?:@\[[^\]]*\]\s*)?'r'(?:(?:private|protected|noncomputable|partial|unsafe|scoped)\s+)*'r'(?:theorem|lemma|def|inductive|abbrev|structure)\s+')MAX_SIG_CHARS =600# plafond : une signature Lean aplatie en fait rarement plusdef parse_signature(lean_path, decl_name):# Signature = de l'ancre jusqu'au premier `:=` (non inclus) ou `where`.# Renvoie None si la declaration n'est pas trouvee : un echec VISIBLE# pour le controle positif, pas un marqueur silencieux. src = lean_path.read_text(encoding='utf-8') pattern = re.compile( DECL_ANCHOR + re.escape(decl_name) +r"(?![\w'])"r'.*?(?=\s*:=|^where\b)', re.MULTILINE | re.DOTALL, ) m = pattern.search(src)if m isNone:returnNone sig =' '.join(m.group(0).split()) # aplatit les sauts de ligne, contenu identiqueiflen(sig) > MAX_SIG_CHARS: sig = sig[:MAX_SIG_CHARS] +' /* tronquee a {} caracteres */'.format(MAX_SIG_CHARS)return sigREPO_ROOT = find_repo_root()SHAPLEY_PATH = find_shapley_lean()if SHAPLEY_PATH isNone:raiseRuntimeError('Shapley.lean introuvable.')# Chemin RELATIF au depot dans toutes les sorties (jamais de chemin machine).if REPO_ROOT isnotNoneand REPO_ROOT in SHAPLEY_PATH.parents: SHAPLEY_LABEL = SHAPLEY_PATH.relative_to(REPO_ROOT).as_posix()else: SHAPLEY_LABEL = SHAPLEY_PATH.namen_lines =sum(1for _ inopen(SHAPLEY_PATH, encoding='utf-8'))print('[setup] Shapley.lean : {} ({} lignes)'.format(SHAPLEY_LABEL, n_lines))print()print('--- Namespace Mobius ---')print()print('# Coefficients de Mobius')print('Mobius.mobiusCoeff :', parse_signature(SHAPLEY_PATH, 'mobiusCoeff'))print()print('# Lemmes techniques (prives) - la machinerie du treillis')print('Mobius.mobius_inner_sum_zero :', parse_signature(SHAPLEY_PATH, 'mobius_inner_sum_zero'))print()print('Mobius.mobius_inner_sum_self :', parse_signature(SHAPLEY_PATH, 'mobius_inner_sum_self'))print()print('# Axiome de decomposition (prouve par inclusion-exclusion sur le treillis)')print('Mobius.mobius_decomposition_axiom :', parse_signature(SHAPLEY_PATH, 'mobius_decomposition_axiom'))print()print('# Theoreme PHARE - la decomposition de Mobius')print('Mobius.mobius_decomposition :', parse_signature(SHAPLEY_PATH, 'mobius_decomposition'))print()print('--- Theoreme d unicite de Shapley (hors namespace Mobius, contexte) ---')print()print("# Phi coincide avec shapleyValue sur les jeux d unanimite")print('phi_eq_shapley :', parse_signature(SHAPLEY_PATH, 'phi_eq_shapley'))print()print('(source : lecture directe de Shapley.lean. Pour la version #check du')print(' compilateur, `lake env lean Shapley.lean` localement. Memes signatures.)')# ---- Controle positif du lecteur : 6/6 signatures, bornees ----DEMANDEES = ['mobiusCoeff', 'mobius_inner_sum_zero', 'mobius_inner_sum_self','mobius_decomposition_axiom', 'mobius_decomposition', 'phi_eq_shapley']signatures = {name: parse_signature(SHAPLEY_PATH, name) for name in DEMANDEES}n_ok =sum(1for v in signatures.values() if v)plus_longue =max((len(v) for v in signatures.values() if v), default=0)print()print('--- controle positif du lecteur ---')print('extraction reussie : {}/{} signatures, plus longue = {} caracteres'.format( n_ok, len(signatures), plus_longue))if n_ok !=len(signatures): manquantes = [k for k, v in signatures.items() ifnot v]raiseRuntimeError('LECTURE EN ECHEC - declarations non rendues : '+', '.join(manquantes))
[setup] Shapley.lean : MyIA.AI.Notebooks/GameTheory/game_theory_lean/CooperativeGames/Shapley.lean (2024 lignes)
--- Namespace Mobius ---
# Coefficients de Mobius
Mobius.mobiusCoeff : noncomputable def mobiusCoeff (G : TUGame N) (T : Finset N) : ℝ
# Lemmes techniques (prives) - la machinerie du treillis
Mobius.mobius_inner_sum_zero : private theorem mobius_inner_sum_zero (S R : Finset N) (hR : R ⊆ S) (hne : R ≠ S) : ∑ T ∈ Finset.univ.filter (fun T => R ⊆ T ∧ T ⊆ S), ((-1 : ℝ) ^ (T.card - R.card)) = 0
Mobius.mobius_inner_sum_self : private theorem mobius_inner_sum_self (S R : Finset N) (_hR : R ⊆ S) (hRS : R = S) : ∑ T ∈ Finset.univ.filter (fun T => R ⊆ T ∧ T ⊆ S), ((-1 : ℝ) ^ (T.card - R.card)) = 1
# Axiome de decomposition (prouve par inclusion-exclusion sur le treillis)
Mobius.mobius_decomposition_axiom : private theorem mobius_decomposition_axiom (G : TUGame N) (S : Finset N) : G.v S = ∑ T ∈ Finset.univ.filter (fun T => T.Nonempty ∧ T ⊆ S), mobiusCoeff G T
# Theoreme PHARE - la decomposition de Mobius
Mobius.mobius_decomposition : theorem mobius_decomposition (G : TUGame N) (S : Finset N) : G.v S = ∑ T ∈ Finset.univ.filter (fun T => T.Nonempty ∧ T ⊆ S), mobiusCoeff G T
--- Theoreme d unicite de Shapley (hors namespace Mobius, contexte) ---
# Phi coincide avec shapleyValue sur les jeux d unanimite
phi_eq_shapley : private theorem phi_eq_shapley (φ : Solution N) (h_eff : φ.Efficiency) (h_sym : φ.Symmetry) (h_null : φ.NullPlayerAxiom) (T : Finset N) (hT : T.Nonempty) (i : N) : φ (TUGame.unanimityGame T hT) i = shapleyValue (TUGame.unanimityGame T hT) i
(source : lecture directe de Shapley.lean. Pour la version #check du
compilateur, `lake env lean Shapley.lean` localement. Memes signatures.)
--- controle positif du lecteur ---
extraction reussie : 6/6 signatures, plus longue = 240 caracteres
# Code 3.2 - Proprete axiomatique du namespace Mobius dans Shapley.lean.## Verifications :# (a) aucun `sorry` (ou `sorryAx` transitif) dans les blocs de preuve ;# (b) aucun `native_decide` (reduction par le noyau natif sans preuve) ;# (c) aucun `axiom NAME := ...` declare globalement dans le namespace ;# (d) comptage canonique via `count_code_sorry.py --json` (ne pas grep -c sorry).## Garde : si aucune declaration n'est lue, le verdict de proprete N'EST PAS# RENDU ("AUCUNE DECLARATION LUE") -- jamais un "OK" sur zero fichier examine.import resrc = SHAPLEY_PATH.read_text(encoding='utf-8')lines = src.split('\n')# Localiser le namespace Mobius et capturer ses bornes.mobius_start =next(i for i, l inenumerate(lines)if re.match(r'^namespace\s+Mobius\b', l))mobius_end =next(i for i, l inenumerate(lines)if re.match(r'^end\s+Mobius\b', l))mobius_block = lines[mobius_start:mobius_end +1]print('--- Namespace Mobius : lignes {} a {} ({} lignes) ---'.format( mobius_start +1, mobius_end +1, len(mobius_block)))print()# Declarations du namespace Mobiusdeclarations = []for i, l inenumerate(mobius_block): m = re.match(r'^(theorem|lemma|def|noncomputable\s+def|private\s+theorem)\s+(\w+)', l)if m: kind, name = m.group(1), m.group(2) declarations.append((kind, name, mobius_start + i +1))ifnot declarations:raiseRuntimeError('AUCUNE DECLARATION LUE dans le namespace Mobius ''- verdict de proprete NON RENDU (lecteur en echec ?)')print('Declarations du namespace Mobius :')for kind, name, line_no in declarations:print(' {}{} : ligne {}'.format(kind, name, line_no))print()# Pour chaque declaration, lire son bloc (jusqu'au prochain `theorem|lemma|end|...`)# et verifier la proprete axiomatique.print('--- proprete axiomatique par declaration ---')print()for kind, name, line_no in declarations: block_lines = []for i inrange(line_no -1, len(lines)):if i > line_no -1and re.match(r'^(theorem|lemma|end |namespace|abbrev|inductive|def|noncomputable\s+def|private\s+theorem)', lines[i] ):break block_lines.append(lines[i]) bt ='\n'.join(block_lines) flags = []if re.search(r'\bsorry\b', bt): flags.append('SORRY (regression !)')if'sorryAx'in bt: flags.append('sorryAx transitif (regression !)')if re.search(r'^\s*axiom\s', bt, re.MULTILINE): flags.append('axiom declare')if re.search(r'\bnative_decide\b', bt): flags.append('native_decide (anti-regression)')if'omega'in bt: flags.append('utilise omega') label =' {}{}'.format(kind, name)if flags:print('{} : {}'.format(label, ', '.join(flags)))else:print('{} : OK (aucune anti-regression)'.format(label))print()print('--- comptage canonique (count_code_sorry.py --json) ---')print()import subprocessimport json as _json# Le script canonique vit a la RACINE du depot, pas sous GameTheory/ :# on le resout via REPO_ROOT (calcule en cellule 3.1 par remontee d'ancetres).if REPO_ROOT isNone:print(' racine du depot non localisee : comptage canonique NON RENDU')else: count_script = REPO_ROOT /'scripts'/'lean'/'count_code_sorry.py' result = subprocess.run( ['python', str(count_script), '--json'], capture_output=True, text=True, timeout=180, )if result.returncode !=0:print(' count_code_sorry retourne code {}'.format(result.returncode)) stderr_last = result.stderr.strip().splitlines()[-1] if result.stderr.strip() else'(vide)'print(' stderr (derniere ligne) :', stderr_last[:200])else: data = _json.loads(result.stdout) lake_entry =next((l for l in data.get('lakes', [])if l.get('lake', '').endswith('game_theory_lean')), None)if lake_entry isNone:print(' lake game_theory_lean absent du rapport : comptage NON RENDU')else:print(' lake game_theory_lean : {} fichiers'.format(lake_entry['files']))print(' naive_sorry = {} (grep de prose : sur-compte)'.format( lake_entry['naive_sorry']))print(' distinct_code_sorry = {} (instrument canonique, FR/EN dedoublonnes)'.format( lake_entry['distinct_code_sorry']))# Localisation DYNAMIQUE des sorry reels du lake (fait mesure, pas fige) :# meme strip de commentaires que l'instrument canonique.import sys as _sys _sys.path.insert(0, str(count_script.parent))from count_code_sorry import strip_lean_comments as _strip lake_root = REPO_ROOT /'MyIA.AI.Notebooks'/'GameTheory'/'game_theory_lean' emplacements = []for f insorted(lake_root.rglob('*.lean')):if'.lake'in f.parts:continue code = _strip(f.read_text(encoding='utf-8'))for mm in re.finditer(r'^.*\bsorry\b.*$', code, re.MULTILINE): ln = code[:mm.start()].count('\n') +1 emplacements.append('{}:{}'.format( f.relative_to(lake_root).as_posix(), ln))if emplacements:print(' sorry reels du lake : '+', '.join(emplacements))else:print(' aucun sorry reel localise dans le lake')
--- Namespace Mobius : lignes 616 a 815 (200 lignes) ---
Declarations du namespace Mobius :
noncomputable def mobiusCoeff : ligne 621
noncomputable def weightedUnanimity : ligne 626
noncomputable def mobiusReconstruction : ligne 632
private theorem mobius_inner_sum_zero : ligne 648
private theorem mobius_inner_sum_self : ligne 705
private theorem mobius_decomposition_axiom : ligne 722
theorem mobius_decomposition : ligne 810
--- proprete axiomatique par declaration ---
noncomputable def mobiusCoeff : OK (aucune anti-regression)
noncomputable def weightedUnanimity : OK (aucune anti-regression)
noncomputable def mobiusReconstruction : OK (aucune anti-regression)
private theorem mobius_inner_sum_zero : OK (aucune anti-regression)
private theorem mobius_inner_sum_self : OK (aucune anti-regression)
private theorem mobius_decomposition_axiom : OK (aucune anti-regression)
theorem mobius_decomposition : OK (aucune anti-regression)
--- comptage canonique (count_code_sorry.py --json) ---
lake game_theory_lean : 49 fichiers
naive_sorry = 32 (grep de prose : sur-compte)
distinct_code_sorry = 1 (instrument canonique, FR/EN dedoublonnes)
sorry reels du lake : RepeatedGames/Folk.lean:127, RepeatedGames/Folk_en.lean:144
Lecture des sources Lean. La signature de mobius_decomposition (cf cellule 3.1, capture bornee au premier :=) donne l’enonce formel exact : pour tout jeu cooperatif G : TUGame N et toute coalition S : Finset N,
G.v S = sum_{T : T non-vide, T \subseteq S} mobiusCoeff G T
C’est la decomposition en somme directe sur le treillis inferieur de S. La preuve repose sur mobius_inner_sum_zero (les contributions des sous-coalitions strictes R ⊊ S s’annulent par inclusion-exclusion) et mobius_inner_sum_self (la contribution de S lui-meme vaut m(S)). Ces lemmes sont prives (private theorem) parce qu’ils sont des outils internes au namespace Mobius - l’API publique est mobiusCoeff + mobius_decomposition. C’est aussi pour cela que le lecteur de la cellule 3.1 doit accepter les qualifieurs : sans eux, cinq des six signatures seraient “introuvables” alors qu’elles existent.
Proprete axiomatique. Le namespace Mobius ne declare aucun axiom NAME := ... global ; il ne depend pas de native_decide (la machinerie repose sur l’arithmetique des Finset et la somme directe, pas sur la reduction native). Les preuves utilisent le calcul direct sur les sous-ensembles, sans sorry ni sorryAx transitif.
Comptage canonique. La cellule 3.2 termine par l’instrument canonique du depot (scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry - jamais grep -c sorry). Le contraste entre les deux compteurs de la sortie est la lecon : le grep naif compte 32sorry de prose (docstrings, commentaires, feuilles de route) quand la mesure canonique en dedoublonne et en compte 1 seul reel, localise dans RepeatedGames/Folk.lean - paire FR/EN dedoublonnee, horsCooperativeGames/Shapley.lean et hors namespace Mobius. Les verdicts OK (aucune anti-regression) ci-dessus portent sur la partie du lake que ce notebook lit, et le comptage global du lake le confirme a l’echelle.
Le theoreme d’unicite (phi_eq_shapley). La cellule 3.1 reference aussi phi_eq_shapley, qui etablit que toute solution phi satisfaisant les 4 axiomes (Efficiency, Symmetry, NullPlayer, Additivity) coincide avec shapleyValue sur les jeux d’unanimite. La decomposition de Mobius est l’ingredient central : la Shapley value est l’unique solution parce qu’elle est l’integration discrete des contributions marginales, et l’integration est determinee par la decomposition unique v = sum m(T) * u_T (u_T = jeu d’unanimite sur T).
4. Le lien avec la valeur de Shapley
La decomposition de Mobius et la valeur de Shapley sont deux lectures du meme objet. Ce lien prend une forme quantitative precise : pour tout joueur i,
phi(i) = sum_{T \ni i} m(T) / |T|
C’est la moyenne des contributions de Mobius des coalitions contenant i, ponderee par l’inverse de la taille de la coalition. Pour notre jeu du tresor :
Le calcul exact prend toutes les coalitions contenant i ; pour Alice : {Alice, Bob} (4, |T|=2), {Alice, Carol} (0, |T|=2), {Alice, Bob, Carol} (4, |T|=3). Donc :
Et la sommephi(Alice) + phi(Bob) + phi(Carol) = v({A,B,C}) = 12 (axiome d’efficacite). Verification : phi(Alice) + phi(Bob) + phi(Carol) = 3.33 + 3.33 + 5.33 = 12. OK.
# Code 4.1 - Calcul direct des Shapley values via la decomposition de Mobius.## On confirme la formule `phi(i) = sum_{T \ni i} m(T) / |T|` sur notre# jeu du tresor. La verification d'efficacite `sum_i phi(i) = v(N)` est# le test de coherence.def shapley_from_mobius(players, m, target_player):# Shapley value d'un joueur = moyenne des m(T) sur les T le contenant.returnsum(m[T] /len(T)for T in mif target_player in T)def shapley_from_mobius_all(players, m):return {p: shapley_from_mobius(players, m, p) for p in players}phi_tresor = shapley_from_mobius_all(players_3, m_tresor)print('--- Shapley values calculees via la decomposition de Mobius ---')print()print('{:<12}{:>10}{:<40}'.format('Joueur i', 'phi(i)', 'formule'))print('-'*65)formulas = {'Alice': 'm({A,B})/2 + m({A,C})/2 + m({A,B,C})/3','Bob': 'm({A,B})/2 + m({B,C})/2 + m({A,B,C})/3','Carol': 'm({A,C})/2 + m({B,C})/2 + m({A,B,C})/3',}for p in players_3: val = phi_tresor[p]print('{:<12}{:>10.3f}{:<40}'.format(p, val, formulas[p]))print()print('--- verification : axiome d efficacite ---')print()total_phi =sum(phi_tresor.values())v_grand = v_tresor(frozenset(players_3))print('sum_i phi(i) = {:.4f}'.format(total_phi))print('v(N) = {:.4f}'.format(v_grand))print('ecart absolu = {:.2e}'.format(abs(total_phi - v_grand)))print()ifabs(total_phi - v_grand) <1e-9:print('EFFICACITE OK : la somme des Shapley values redonne v(N) =', v_grand)else:print('ANOMALIE : l efficacite ne tient pas !')
--- Shapley values calculees via la decomposition de Mobius ---
Joueur i phi(i) formule
-----------------------------------------------------------------
Alice 3.333 m({A,B})/2 + m({A,C})/2 + m({A,B,C})/3
Bob 5.333 m({A,B})/2 + m({B,C})/2 + m({A,B,C})/3
Carol 3.333 m({A,C})/2 + m({B,C})/2 + m({A,B,C})/3
--- verification : axiome d efficacite ---
sum_i phi(i) = 12.0000
v(N) = 12.0000
ecart absolu = 0.00e+00
EFFICACITE OK : la somme des Shapley values redonne v(N) = 12
Ce que montre le code 4.1. La Shapley value peut se calculer directement depuis les coefficients de Mobius par la formule phi(i) = somme sur T contenant i de m(T) / |T|. C’est la version integration de la Shapley value, equivalente a la definition par contributions marginales sur les permutations (cf GameTheory-15c cellule 2.1).
Pourquoi la meme formule donne des Shapley values differentes pour Alice, Bob, Carol : Bob a phi = 5.33 (le plus eleve) parce que sa contribution est repartie sur le plus de coalitions synergiques : il est dans {A,B} (4) ET {B,C} (4) ET {A,B,C} (4) - les deux paires positives et la triple. Carol est dans {B,C} (4) et {A,B,C} (4) mais PAS dans {A,C} (m({A,C})=0), donc sa moyenne est diluee. Alice est dans {A,B} (4) et {A,B,C} (4) mais PAS dans {A,C} (m({A,C})=0), donc egalement diluee. La Shapley value reflete ici la position centrale de Bob dans la structure (les deux synergies passent par lui).
Note pedagogique : la Shapley value est l’unique solution satisfaisant les 4 axiomes (Efficiency, Symmetry, NullPlayer, Additivity) - c’est le contenu de phi_eq_shapley. La decomposition de Mobius est l’ingredient qui rend cette unicite constructive : la Shapley value est l’integration des m(T) * u_T ou u_T est le jeu d’unanimite sur T (cf shapley_unanimity l. 508). Sans Mobius, l’unicite reste abstraite ; avec, elle est mesurable. Deux lectures du meme objet, et la Shapley value est celle qui repond a “quelle est la part equitable de chacun ?”.
5. Pont cross-domain : la decomposition de Mobius comme outil general
L’attrait de la decomposition de Mobius depasse le contexte des jeux cooperatifs. C’est un outil d’inclusion-exclusion sur un treillis, applicable des qu’une grandeur est une fonction sur les parties d’un ensemble :
Domaine
Fonction v
Coefficient m(T)
Lecture
Jeux cooperatifs
Valeur de coalition
Contribution propre de T
Synergie / conflit
Probabilites (Poincarre)
P(union)
P(intersection stricte)
Inclusion-exclusion
Topologie algebrique (Cech)
H_0(X) (nb de composantes)
Cycles H_1 entre cellules
Obstructions locales
Informatique (differentielle finie)
Difference Df
Differences d’ordre superieur
Derivees discretes
Linguistique (substitution)
Phrase en contexte
Substitution du mot i
Sens propre vs contexte
Dans chaque cas, la decomposition de Mobius separe la part qui peut s’expliquer par les sous-parties (additive) de la part qui emerge au niveau collectif (irreductible). Le pattern est transversal : << ce qui est mesurable au niveau individuel peut etre trompeusement additif ; la decomposition revele la structure cachee >>.
Lien avec Lean : la formalisation dans game_theory_lean/CooperativeGames/Shapley.lean est independante du domaine - le namespace Mobius manipule des Finset N et des fonctions v : TUGame N, mais la structure du treillis (lattice boolien) est isomorphe a celle de tout domaine ou les donnees vivent sur des parties. La preuve formelle n’utilise que la theorie des ensembles finis et l’arithmetique des sommes ; c’est un outil fondamental.
Exercices
Les exercices suivants portent sur la decomposition de Mobius : (1) la calculer sur un jeu a 4 joueurs, (2) le controle negatif indispensable (jeu additif), (3) une synergie irreductible explicite, et (4) bonus sur la lecture des sources Lean. Chaque stub s’execute sans erreur (regle C.1).
Exercice 1 : decomposition de Mobius sur un jeu a 4 joueurs
Considerons 4 joueurs {A, B, C, D} avec les valeurs individuelles v({A}) = 1, v({B}) = 2, v({C}) = 3, v({D}) = 4, et la regle de coalition : chaque paire qui inclut A a une synergie de +2 (c’est-a-dire v({A, i}) = v({A}) + v({i}) + 2 pour tout i != A), tandis que les paires sans A sont additives (pas de synergie).
Travail demande : 1. Definir la fonction v_4(S) qui implemente cette regle, et la grande coalition v(N) = ? 2. Calculer m(T) pour toutes les 2^4 - 1 = 15 coalitions non vides 3. Verifier le controle de coherence : v_from_mobius(players, m) redonne v pour toute coalition (delta < 1e-9)
Indice 1 : from itertools import combinations ; players_4 = ['A', 'B', 'C', 'D'] ; la regle “paire avec A a synergie +2” se traduit par if 'A' in S and len(S) == 2: return sum_individuels + 2.
Indice 2 : utiliser la fonction mobius_coefficients deja implementee en Code 1.1 ; le test de coherence avec v_from_mobius est un import direct.
# Exercice 1 : decomposition de Mobius sur un jeu a 4 joueurs avec synergie sur les paires contenant A.# TODO etudiant : definir v_4, calculer m(T), verifier la coherence.players_4 = ['A', 'B', 'C', 'D']v_4 =None# TODO etudiant : definir v_4(S) selon la reglem_4 =None# TODO etudiant : appeler mobius_coefficients(players_4, v_4)coherence =None# TODO etudiant : tester v_from_mobiusprint('Exercice a completer : Mobius sur 4 joueurs avec synergie sur paires A+.')
Exercice a completer : Mobius sur 4 joueurs avec synergie sur paires A+.
Exercice 2 : controle negatif - le jeu additif
Reprendre le substrat du Code 1.1 : le jeu additif pur v(S) = sum_{i \in S} v({i}). Verifier que pour des valeurs individuelles arbitraires v({A}) = 1, v({B}) = 2, v({C}) = 3, v({D}) = 4, tous les m(T) pour |T| >= 2 sont nuls.
Travail demande : 1. Definir le jeu additif 2. Calculer m(T) et compter combien sont nuls vs non-nuls 3. Conclure : que dit ce controle sur l’usage de la decomposition ?
Indice : ce controle est ce qui distingue un “tableau de m(T) sans structure” d’un “tableau de m(T) avec structure”. Sans lui, un m(T) non nul ailleurs ne prouve rien : on ne sait pas si c’est un artefact numerique ou une vraie synergie.
# Exercice 2 : controle negatif - jeu additif pur a 4 joueurs.# TODO etudiant : definir le jeu additif, compter m(T) nuls vs non-nuls.players_4 = ['A', 'B', 'C', 'D']base_4 = {'A': 1, 'B': 2, 'C': 3, 'D': 4}def v_additive_4(S):# TODO etudiant : somme des valeurs individuelles sur Spassm_additive_4 =None# TODO etudiant : calculer via mobius_coefficientsn_nuls =None# TODO etudiant : compter m(T) == 0n_non_nuls =None# TODO etudiant : compter m(T) != 0print('Exercice a completer : controle negatif additif a 4 joueurs.')
Exercice a completer : controle negatif additif a 4 joueurs.
Exercice 3 : synergie irreductible - reproduire le cas du tresor a 4 joueurs
Construire un jeu a 4 joueurs {A, B, C, D} ou : - Toutes les paires sont additives (pas de synergie) - Seul le triplet {B, C, D} porte une synergie irreductible de +10 : v({B,C,D}) = v({B}) + v({C}) + v({D}) + 10 - La grande coalition {A,B,C,D} porte une synergie propre de +5
Travail demande : 1. Definir le jeu 2. Calculer m(T) et identifier : - Quelle coalition porte la synergie triplet ? - Quelle coalition porte la synergie grande coalition ? - Y a-t-il d’autres m(T) non triviaux que vous n’attendiez pas ? 3. Calculer la Shapley value de chaque joueur et verifier l’efficacite.
Indice : la Shapley value d’un joueur depend de toutes les coalitions qui le contiennent, pas seulement celles qu’on a pensees ; la decomposition de Mobius est ce qui rend cette lecture complete et mecanique.
# Exercice 3 : synergie irreductible sur triplet {B,C,D} + grande coalition.# TODO etudiant : definir le jeu, calculer m(T), Shapley values, verifier efficacite.players_4 = ['A', 'B', 'C', 'D']base_4 = {'A': 1, 'B': 2, 'C': 3, 'D': 4}def v_irreductible_4(S):# TODO etudiant : v({B,C,D}) = base + 10, v({A,B,C,D}) = base + 15passm_irreductible_4 =None# TODO etudiantphi_irreductible_4 =None# TODO etudiant : shapley_from_mobius_allprint('Exercice a completer : synergie irreductible triplet + grande coalition a 4 joueurs.')
Exercice a completer : synergie irreductible triplet + grande coalition a 4 joueurs.
Exercice 4 (Bonus) : lecture directe de mobius_decomposition dans Shapley.lean
La cellule 3.1 extrait la signature de mobius_decomposition (l. 810 de Shapley.lean), bornee au premier := - le debut du corps. Bonus : extraire le bloc de preuve complet (commentaires + tactiques) du theoreme, et identifier les 3-4 lemmes intermediaires sur lesquels il s’appuie.
Indice 1 : la preuve commence apres := by ; elle peut s’etaler sur plusieurs dizaines de lignes (tactiques rw, simp, exact, etc.). Le bloc est delimite par la declaration courante et la prochaine declaration ^(theorem|lemma|end|namespace|...).
Indice 2 : les lemmes intermediaires sont probablement mobius_inner_sum_zero et mobius_inner_sum_self (cf cellule 3.1). Identifier les tactiques (rw, simp, exact) employees et les compter. Attention au piege de la cellule 3.1 : votre delimiteur de fin doit declencher, sinon vous capturerez la fin du fichier au lieu du bloc.
# Exercice 4 (Bonus) : extraction du bloc de preuve de mobius_decomposition.# TODO etudiant : extraire le bloc de preuve, lister les lemmes utilises,# compter les tactiques (rw, simp, exact).bloc_preuve =None# TODO etudiantlemmes_utilises =None# TODO etudianttactiques =None# TODO etudiantprint('Exercice bonus a completer : extraction du bloc de preuve de mobius_decomposition.')
Exercice bonus a completer : extraction du bloc de preuve de mobius_decomposition.
Resume
Ce notebook a presente la decomposition de Mobius sur le treillis des coalitions, formalisee dans game_theory_lean/CooperativeGames/Shapley.lean :
Definition et intuition (section 1, code 1.1) - le coefficient m(T) est la part propre d’une coalition, ce qui ne se reduit pas aux sous-coalitions. Implementation directe par inclusion-exclusion ; test de coherence v_from_mobius verifie l’inversibilite.
Synergie irreductible (section 2, code 2.1) - le jeu du tresor exhibe une synergie triple propre m({A,B,C}) = 4 strictement positive, mesuree (pas postulee). La decomposition isole ce que la lecture directe de v(N) laisse invisible.
Lien avec Shapley (section 4, code 4.1) - phi(i) = sum_{T \ni i} m(T) / |T| ; verification numerique de l’axiome d’efficacite sur le jeu du tresor. Deux lectures du meme objet : Mobius (structure par coalition) et Shapley (repartition equitable).
Pont cross-domain (section 5) - l’inclusion-exclusion sur un treillis est un outil transversal : probabilites (Poincarre), topologie algebrique (Cech), informatique (differences finies), linguistique (substitution). Le namespace Mobius de Shapley.lean est independant du domaine (Finset N, somme directe).
References
Issue #12238 - Parent GameTheory-15d: << Mobius sur le treillis des coalitions : ce qui n’existe qu’au niveau collectif >> (issue-source de ce notebook).
shapley.py (MyIA.AI.Notebooks/GameTheory/cooperative_games/) - module Python de simulation : marginal_contribution, shapley_value_exact, shapley_value_formula, shapley_value_monte_carlo, ShapleyCalculator. Pas d’implementation directe de la decomposition de Mobius (notre notebook comble ce manque).
GameTheory-15c-CooperativeGames-Python.ipynb - notebook Python precedent, illustre les theoremes shapley_* (sans la decomposition de Mobius).
GameTheory-15b-Lean-CooperativeGames-Lean.ipynb - side track Lean, formalisation directe des theoremes Shapley.