Théorème d’Arrow (1951). Aucune règle d’agrégation ne satisfait simultanément les trois axiomes : 1. Universalité (domaine non restreint) — traitée implicitement (on énumère tous les profils) ; 2. Pareto faible (unanimité) — si tous préfèrent \(x \succ y\), le social aussi ; 3. Indépendance aux alternatives non pertinentes (IIA) — le classement social entre \(x\) et \(y\) ne dépend que des préférences individuelles entre \(x\) et \(y\) ; 4. Non-dictature — aucun votant n’impose toujours son classement.
(Arrow compte Universalité + 3 axiomes ; on vérifie ici Pareto, IIA, Non-dictature.)
★ Leçon de parité : déterministe > stochastique
Le notebook Python teste les axiomes par simulation aléatoire (random.shuffle, seed(42)). Cela pose deux problèmes : - (a) le RNG Python et C# divergent → pas de parité byte-pour-byte possible ; - (b) un test stochastique rate les violations rares et reste opaque sur quels profils violent l’axiome.
Le twin C# remplace la simulation par l’énumération exhaustive déterministe : pour 3 alternatives et 3 votants, il n’y a que \((3!)^3 = 216\) profils — on peut tous les parcourir et compter exactement les violations, puis afficher un contre-exemple concret. C’est à la fois plus rigoureux (preuve exhaustive) et plus pédagogique (on voit le profil coupable). Voir leçon c.96 (démo IIA déterministe du twin SC-03).
Plan : 1. Règles de vote (Borda, Pluralité, Dictatoriale) — from-scratch ; 2. Vérification des 3 axiomes (Pareto, IIA, Non-dictature) — déterministe ; 3. Structure de la preuve d’Arrow (lemme extremal, pivot, dictateur partiel) ; 4. Réfutation par force brute (énumération complète) + synthèse.
Plan de route : le notebook avance en deux stratégies croisées qui se valident mutuellement — d’abord axiome par axiome (Pareto, IIA, Non-dictature, chacun testé sur les \((3!)^3 = 216\) profils possibles), puis la structure de la preuve d’Arrow elle-même (lemme extremal, pivot, dictateur partiel), enfin la réfutation par force brute qui rassemble le tout en un tableau à trois lignes. Chaque étape a sa sortie committée : 0 violation de Pareto pour les trois règles, un contre-exemple IIA construit où le verdict Borda bascule de B > A à A > B sans que les préférences individuelles A-vs-B bougent, 1 656 violations IIA pour Borda contre 3 312 pour la Pluralité (sur \(216^2 = 46\,656\) paires de profils), et le verdict final : aucune des trois règles ne passe les trois axiomes. Quatre exercices closent le parcours, du lemme extremal à 4 alternatives au paradoxe Condorcet-vs-Borda.
Hommage — le premier article de Richard E. Stearns portait sur ce théorème
Richard E. Stearns (1936–2026), co-lauréat du prix Turing 1993 pour avoir fondé la théorie de la complexité computationnelle (Hartmanis & Stearns, 1965), a commencé par le théorème d’Arrow : son tout premier article, écrit comme étudiant de dernière année à Carleton College, portait sur le paradoxe d’Arrow et a été publié dans The American Mathematical Monthly en 1959. Sa thèse de Princeton, dirigée par Harold W. Kuhn (co-éponyme de l’algorithme Kuhn–Munkres, célébré dans cette même série GameTheory), portait sur les jeux coopératifs à trois joueurs sans paiements transférables.
L’homme qui a donné son nom à la complexité a donc commencé par l’impossibilité de l’agrégation — le théorème que ce notebook démontre. Autre résonance inattendue : ses travaux sur les jeux répétés à information incomplète (contrôle des armements, chapitre du livre d’Aumann & Maschler 1995), racontés dans le README de game_theory_lean/. Hommage complet — hiérarchie de Hartmanis–Stearns, série Complexity/ : issue #15949.
Pourquoi trois setters de culture ? La cellule suivante n’assigne pas un mais trois propriétés (CurrentCulture, DefaultThreadCurrentCulture, DefaultThreadUICulture) à InvariantCulture — c’est la leçon c.94 : en .NET Interactive, CurrentCulture seul ne persiste pas d’une cellule à l’autre, car chaque cellule peut s’exécuter sur un thread distinct du pool. Sans ces trois setters, un string.Format ou un tri par score décroissant pourrait se comporter différemment selon la culture de la machine (séparateurs décimaux, ordres de tri) et casser la reproductibilité cross-machine. La sortie Configuration OK est le seul output attendu : elle prouve que la cellule de configuration a tourné dans le bon environnement.
// SocialChoice 01 : Théorème d'impossibilité d'Arrow -- twin C# de 01-Arrow// Prong B (#3801) : implementations from-scratch (BCL .NET 9, 0 NuGet).// Lecon c.94 : les 3 setters de culture sont requis (CurrentCulture seul ne// persiste pas cross-cell, threads du pool distincts).using System;using System.Collections.Generic;using System.Globalization;using System.Linq;CultureInfo.CurrentCulture= CultureInfo.InvariantCulture;CultureInfo.DefaultThreadCurrentCulture= CultureInfo.InvariantCulture;CultureInfo.DefaultThreadCurrentUICulture= CultureInfo.InvariantCulture;Console.WriteLine("Configuration OK : SocialChoice 01 - Arrow (twin C# .NET)");
Configuration OK : SocialChoice 01 - Arrow (twin C# .NET)
1. Règles de vote (from-scratch)
Un profil est une liste de classements (un par votant, du meilleur au pire). On implémente trois règles d’agrégation :
Borda : points \((n-1-\text{rang})\) par votant, classement par score décroissant ;
Pluralité : compte les premiers choix, classement par nombre de premiers choix ;
Dictatoriale : le classement social = préférence du dictateur (indice fixé).
Lecture de la sortie committée : sur le profil de démonstration (votant 0 : A > B > C, votant 1 : B > A > C, votant 2 : A > C > B), les trois règles convergent vers A > B > C — mais pour des raisons différentes, et c’est tout l’intérêt du triple affichage. Borda : scores \(A = 2+1+2 = 5\), \(B = 1+2+0 = 3\), \(C = 0+0+1 = 1\). Pluralité : A récolte 2 premiers choix contre 1 à B, 0 à C. Dictatoriale : le votant 0 (dictateur par défaut) préfère A. Trois mécanismes, un même classement — sur ce profil là. La suite du notebook montre précisément où ces mécanismes divergent et lesquels violent quels axiomes : c’est le tableau final (Borda et Pluralité échouent sur IIA, Dictatoriale sur Non-dictature) qui départage.
// === Section 1 : Regles de vote (Borda / Pluralite / Dictatoriale) ===// Un profil = liste des classements (meilleur -> pire) de chaque votant.// Une regle prend un profil et retourne un classement social (meilleur -> pire).publicstatic List<string>Borda(List<List<string>> profile){var scores =new Dictionary<string,int>();int n = profile[0].Count;foreach(var pref in profile)for(int rank =0; rank < n; rank++){if(!scores.ContainsKey(pref[rank])) scores[pref[rank]]=0; scores[pref[rank]]+=(n -1- rank);}// Tri par score decroissant ; ex-aequo par ordre alpha pour determinismereturn scores.Keys.OrderByDescending(k => scores[k]).ThenBy(k => k).ToList();}publicstatic List<string>Pluralite(List<List<string>> profile){// Tiebreak par ordre d'apparition dans le profil (stable, comme Python// dict.fromkeys) -- sinon deux alternatives a 0 premier-choix seraient// ordonnees alphabetiquement et violeraient Pareto artificiellement.var first =new Dictionary<string,int>();var appearance =new List<string>();foreach(var pref in profile)foreach(var a in pref){if(!appearance.Contains(a)) appearance.Add(a);if(!first.ContainsKey(a)) first[a]=0;}foreach(var pref in profile) first[pref[0]]++;return appearance.OrderBy(k =>-first[k]).ThenBy(k => appearance.IndexOf(k)).ToList();}publicstatic List<string>Dictatorial(List<List<string>> profile,int dictatorIdx)=>new List<string>(profile[dictatorIdx]);// Demo : profil a 3 votants, 3 alternativesvar demo =new List<List<string>>{new(){"A","B","C"},new(){"B","A","C"},new(){"A","C","B"},};Console.WriteLine("Profil demo :");for(int i =0; i < demo.Count; i++) Console.WriteLine(" Votant "+ i +" : "+string.Join(" > ", demo[i]));Console.WriteLine();Console.WriteLine("Borda : "+string.Join(" > ",Borda(demo)));Console.WriteLine("Pluralite : "+string.Join(" > ",Pluralite(demo)));Console.WriteLine("Dictatorial : "+string.Join(" > ",Dictatorial(demo,0)));
Profil demo :
Votant 0 : A > B > C
Votant 1 : B > A > C
Votant 2 : A > C > B
Borda : A > B > C
Pluralite : A > B > C
Dictatorial : A > B > C
1.1 Axiome de Pareto faible (déterministe)
Pareto faible : si tous les votants préfèrent \(x \succ y\), alors le classement social doit aussi avoir \(x\) avant \(y\).
Plutôt qu’un tirage aléatoire, on énumère tous les profils possibles (pour 3 alternatives, 3 votants : \((3!)^3 = 216\) profils) et on compte les violations de Pareto. Une règle satisfaisant Pareto donne 0 violation.
Lecture de la sortie committée : 216 profils énumérés (l’algorithme de Heap, déterministe, cité dans la source), et 0 violation de Pareto pour les trois règles. Le test parcourt chaque profil et chaque paire \((x,y)\) : si tous les votants placent \(x\) avant \(y\) mais que le classement social fait l’inverse, c’est une violation. Zéro partout n’est pas une évidence a priori : une règle qui ignorerait les bulletins minoritaires pourrait violer Pareto. C’est le résultat le moins surprenant des trois axiomes — les trois règles d’agrégation « raisonnables » respectent l’unanimité — mais il fallait l’établir par énumération plutôt que par intuition : le tableau final s’appuiera dessus.
// === Section 1.1 : Pareto faible -- enumeration exhaustive deterministe ===// Genere toutes les permutations de 'alts' (classements possibles d'un votant).publicstatic List<List<string>>AllPermutations(List<string> alts){var result =new List<List<string>>();int n = alts.Count;int[] idx = Enumerable.Range(0, n).ToArray();// Permutations par algorithme de Heap (deterministe)voidSwap(int i,int j){(idx[i], idx[j])=(idx[j], idx[i]);}voidHeap(int k){if(k ==1){ result.Add(idx.Select(i => alts[i]).ToList());return;}// Variante Sedgewick : l'indice d'echange depend de la parite de k,// PAS de celle de i (l'ancienne regle emettait ABC/BAC en double et// perdait BCA/CBA -- 4 permutations distinctes sur 6).for(int i =0; i < k; i++){Heap(k -1);if(k %2==0)Swap(i, k -1);elseSwap(0, k -1);}}Heap(n);return result;}// Genere tous les profils a nVotants (produit cartesien des permutations).publicstatic List<List<List<string>>>AllProfiles(List<string> alts,int nVotants){var perms =AllPermutations(alts);var profiles =new List<List<List<string>>>();// Recursion : produit cartesienvoidBuild(int remaining, List<List<string>> current){if(remaining ==0){ profiles.Add(current.Select(x => x).ToList());return;}foreach(var p in perms){ current.Add(p);Build(remaining -1, current); current.RemoveAt(current.Count-1);}}Build(nVotants,new List<List<string>>());return profiles;}// Predicat : tous les votants preferent x a y ?publicstaticboolAllPrefer(List<List<string>> profile,string x,string y)=> profile.All(p => p.IndexOf(x)< p.IndexOf(y));// Compte les violations de Pareto faible sur TOUS les profils.publicstaticintParetoViolations( Func<List<List<string>>, List<string>> rule, List<string> alts,int nVotants){int violations =0;var profiles =AllProfiles(alts, nVotants);foreach(var prof in profiles){var ranking =rule(prof);// Toutes les paires non ordonnees {x, y} avec x != yfor(int i =0; i < alts.Count; i++)for(int j =0; j < alts.Count; j++){if(i == j)continue;string x = alts[i], y = alts[j];if(AllPrefer(prof, x, y)&& ranking.IndexOf(x)> ranking.IndexOf(y)) violations++;}}return violations;}var alts3 =new List<string>{"A","B","C"};int nVot =3;int np =AllProfiles(alts3, nVot).Count;Console.WriteLine("Enumeration exhaustive : "+ np +" profils ("+ alts3.Count+" alts, "+ nVot +" votants)");Console.WriteLine();Console.WriteLine("Violations de Pareto faible (devrait etre 0 pour Borda/Pluralite/Dictatorial) :");Console.WriteLine(" Borda : "+ParetoViolations(p =>Borda(p), alts3, nVot));Console.WriteLine(" Pluralite : "+ParetoViolations(p =>Pluralite(p), alts3, nVot));Console.WriteLine(" Dictatorial : "+ParetoViolations(p =>Dictatorial(p,0), alts3, nVot));
Enumeration exhaustive : 216 profils (3 alts, 3 votants)
Violations de Pareto faible (devrait etre 0 pour Borda/Pluralite/Dictatorial) :
Borda : 0
Pluralite : 0
Dictatorial : 0
IIA : le classement social entre \(x\) et \(y\) ne dépend que des préférences individuelles entre \(x\) et \(y\) (les autres alternatives ne doivent pas influencer).
Borda viole IIA — on le montre par un contre-exemple construit et déterministe (leçon c.96) : deux profils où les préférences A-vs-B sont identiques pour chaque votant, mais le classement social Borda de A-vs-B bascule.
Profil 1 (3×A>B>C, 2×B>C>A)
Profil 2 (3×A>C>B, 2×B>A>C)
Votants 1-3 préfèrent A>B
Votants 1-3 préfèrent A>B
Votants 4-5 préfèrent B>A
Votants 4-5 préfèrent B>A
→ Préférences A-vs-B individuelles identiques. Pourtant Borda donne Profil 1 : B>A, Profil 2 : A>B. Violation de IIA.
L’arithmétique du basculement, chiffre par chiffre : la sortie donne Profil 1 scores \(A=6, B=7, C=2\) et Profil 2 \(A=8, B=4, C=3\). Décomposons le passage de l’un à l’autre. Chez les votants 1-3, le classement passe de A > B > C à A > C > B : B descend d’un rang (\(-1\) point chacun, \(-3\) au total), C monte (\(+3\)). Chez les votants 4-5, B > C > A devient B > A > C : A monte de dernier à deuxième (\(+1\) chacun, \(+2\)), C descend (\(-2\)). Bilan exact : \(A : 6 \to 8\) (\(+2\)), \(B : 7 \to 4\) (\(-3\)), \(C : 2 \to 3\) (\(+1\)) — les trois nombres de la sortie. Aucun votant n’a changé d’avis sur A-vs-B (votants 1-3 : A>B dans les deux profils ; votants 4-5 : B>A), pourtant le verdict social Borda bascule de B > A à A > B. C’est la violation de IIA dans sa forme la plus pure : Borda agrège des positions absolues, donc l’introduction d’une tierce alternative C redistribue des points entre A et B. La Pluralité est a priori plus « locale » (seul le premier choix compte) — le comptage de la section suivante montre qu’elle fait pire.
// === Section 1.2 : IIA -- contre-exemple construit deterministe (lecon c.96) ===// Deux profils ou les preferences A-vs-B individuelles sont IDENTIQUES,// mais le classement social Borda de A-vs-B bascule = violation de IIA.var iiaProfil1 =new List<List<string>>{new(){"A","B","C"},new(){"A","B","C"},new(){"A","B","C"},new(){"B","C","A"},new(){"B","C","A"},};var iiaProfil2 =new List<List<string>>{new(){"A","C","B"},new(){"A","C","B"},new(){"A","C","B"},new(){"B","A","C"},new(){"B","A","C"},};staticintBordaScore(List<List<string>> profile,string alt){int n = profile[0].Count, s =0;foreach(var p in profile) s +=(n -1- p.IndexOf(alt));return s;}int a1 =BordaScore(iiaProfil1,"A"), b1 =BordaScore(iiaProfil1,"B"), c1 =BordaScore(iiaProfil1,"C");int a2 =BordaScore(iiaProfil2,"A"), b2 =BordaScore(iiaProfil2,"B"), c2 =BordaScore(iiaProfil2,"C");Console.WriteLine("Profil 1 (3xA>B>C, 2xB>C>A) : scores Borda A="+ a1 +" B="+ b1 +" C="+ c1+" -> "+(b1 > a1 ?"B > A":"A > B"));Console.WriteLine("Profil 2 (3xA>C>B, 2xB>A>C) : scores Borda A="+ a2 +" B="+ b2 +" C="+ c2+" -> "+(a2 > b2 ?"A > B":"B > A"));Console.WriteLine();// Verification : preferences A-vs-B individuelles identiques entre les 2 profils ?boolSameAB(List<List<string>> p1, List<List<string>> p2)=> p1.Zip(p2).All(t =>(t.First.IndexOf("A")< t.First.IndexOf("B"))==(t.Second.IndexOf("A")< t.Second.IndexOf("B")));Console.WriteLine("Preferences A-vs-B identiques entre Profil 1 et Profil 2 ? "+SameAB(iiaProfil1, iiaProfil2));Console.WriteLine("Verdict social Profil 1 : "+(b1 > a1 ?"B > A":"A > B"));Console.WriteLine("Verdict social Profil 2 : "+(a2 > b2 ?"A > B":"B > A"));Console.WriteLine(">>> BORDA VIOLE IIA : les preferences A-vs-B sont les memes, pourtant le verdict bascule.");
Profil 1 (3xA>B>C, 2xB>C>A) : scores Borda A=6 B=7 C=2 -> B > A
Profil 2 (3xA>C>B, 2xB>A>C) : scores Borda A=8 B=4 C=3 -> A > B
Preferences A-vs-B identiques entre Profil 1 et Profil 2 ? True
Verdict social Profil 1 : B > A
Verdict social Profil 2 : A > B
>>> BORDA VIOLE IIA : les preferences A-vs-B sont les memes, pourtant le verdict bascule.
1.2 (suite) — Comptage exhaustif des violations IIA
On confirme par énumération exhaustive : pour chaque paire de profils \((P_1, P_2)\) parmi les 216, et chaque paire d’alternatives \((x,y)\), si les préférences individuelles \(x\)-vs-\(y\) coïncident mais que le verdict social diffère → 1 violation. On affiche le nombre total et le premier contre-exemple trouvé.
Lecture du comptage committé — et sa hiérarchie contre-intuitive : sur les \(216^2 = 46\,656\) paires de profils × 3 paires d’alternatives, Borda cumule 1 656 violations et la Pluralité 3 312 — un rapport de 2 pour 1. Contre-intuitif : la Pluralité semble « moins dépendante » des alternatives non pertinentes (seul le premier choix compte, pas les positions intermédiaires), et pourtant elle viole IIA deux fois plus. La raison : déplacer C d’une position intermédiaire à la première change le premier choix d’un votant, ce qui bouleverse tout le comptage ; chez Borda, le même déplacement ne vole qu’un point. La forme des violations diffère aussi : le premier contre-exemple Borda (P1 social B>A vs P2 social A>B) correspond exactement au contre-exemple construit en 1.2 — l’énumération retrouve le profil coupable de la section précédente parmi les 1 656, preuve de cohérence entre démonstration construite et balayage exhaustif.
// === Section 1.2 (suite) : comptage exhaustif des violations IIA ===publicstatic(int count,string first)IiaViolations( Func<List<List<string>>, List<string>> rule, List<string> alts,int nVotants){var profiles =AllProfiles(alts, nVotants);int count =0;string first =null;foreach(var p1 in profiles){var r1 =rule(p1);foreach(var p2 in profiles){var r2 =rule(p2);for(int i =0; i < alts.Count; i++)for(int j = i +1; j < alts.Count; j++){string x = alts[i], y = alts[j];// Preferences individuelles x-vs-y identiques entre P1 et P2 ?bool sameXY = p1.Zip(p2).All(t =>(t.First.IndexOf(x)< t.First.IndexOf(y))==(t.Second.IndexOf(x)< t.Second.IndexOf(y)));if(!sameXY)continue;bool soc1 = r1.IndexOf(x)< r1.IndexOf(y);bool soc2 = r2.IndexOf(x)< r2.IndexOf(y);if(soc1 != soc2){ count++;if(first ==null) first ="x="+ x +" y="+ y +" : P1 social "+(soc1 ?(x +">"+ y):(y +">"+ x))+" vs P2 social "+(soc2 ?(x +">"+ y):(y +">"+ x));}}}}return(count, first ??"(aucune)");}var(viiaB, firstB)=IiaViolations(p =>Borda(p), alts3, nVot);var(viiaP, firstP)=IiaViolations(p =>Pluralite(p), alts3, nVot);Console.WriteLine("Violations IIA (enumeration exhaustive, 216^2 paires de profils) :");Console.WriteLine(" Borda : "+ viiaB +" violations");Console.WriteLine(" Premier exemple : "+ firstB);Console.WriteLine(" Pluralite : "+ viiaP +" violations");Console.WriteLine(" Premier exemple : "+ firstP);
Violations IIA (enumeration exhaustive, 216^2 paires de profils) :
Borda : 1656 violations
Premier exemple : x=A y=B : P1 social B>A vs P2 social A>B
Pluralite : 3312 violations
Premier exemple : x=A y=B : P1 social A>B vs P2 social B>A
1.3 Axiome de Non-dictature (déterministe)
Non-dictature : aucun votant \(d\) n’est un dictateur, i.e. dont le classement social coïnciderait toujours avec sa préférence stricte (pour toute paire \(x,y\), si \(d\) préfère \(x \succ y\) alors le social a \(x\) avant \(y\)).
On teste déterministiquement chaque votant sur les 216 profils : si un votant dicte toutes les paires dans tous les profils, c’est un dictateur.
Lecture de la sortie committée : AUCUN dictateur pour Borda et la Pluralité, Votant 0 pour la Dictatoriale — « par construction », comme le note la sortie elle-même. La définition testée est forte : un dictateur doit imposer sa préférence sur toutes les paires dans tous les profils (216 profils × 3 paires). C’est une barre très haute : une règle pourrait systématiquement favoriser un groupe sans qu’aucun individu isolé ne dicte tout. D’où l’asymétrie du tableau final : l’axiome de Non-dictature est celui que Borda et Pluralité passent facilement (aucun individu n’a ce pouvoir total), alors que la règle Dictatoriale — construite autour d’un votant — le viole trivialement. Chaque règle échoue sur un axiome différent : c’est précisément la structure du théorème d’Arrow, aucune règle ne les passe tous.
// === Section 1.3 : Non-dictature -- enumeration exhaustive deterministe ===// Retourne l'index du dictateur, ou -1 si aucun.publicstaticintFindDictator( Func<List<List<string>>, List<string>> rule, List<string> alts,int nVotants){var profiles =AllProfiles(alts, nVotants);for(int d =0; d < nVotants; d++){bool isDictator =true;foreach(var prof in profiles){var ranking =rule(prof);for(int i =0; i < alts.Count; i++)for(int j = i +1; j < alts.Count; j++){string x = alts[i], y = alts[j];if(prof[d].IndexOf(x)< prof[d].IndexOf(y)&& ranking.IndexOf(x)> ranking.IndexOf(y)){ isDictator =false;break;}if(prof[d].IndexOf(y)< prof[d].IndexOf(x)&& ranking.IndexOf(y)> ranking.IndexOf(x)){ isDictator =false;break;}}if(!isDictator)break;}if(isDictator)return d;}return-1;}int dBorda =FindDictator(p =>Borda(p), alts3, nVot);int dPlur =FindDictator(p =>Pluralite(p), alts3, nVot);int dDict0 =FindDictator(p =>Dictatorial(p,0), alts3, nVot);Console.WriteLine("Dictateur detecte (-1 = aucun) :");Console.WriteLine(" Borda : "+(dBorda <0?"AUCUN (satisfait Non-dictature)":"Votant "+ dBorda));Console.WriteLine(" Pluralite : "+(dPlur <0?"AUCUN (satisfait Non-dictature)":"Votant "+ dPlur));Console.WriteLine(" Dictatorial : "+(dDict0 <0?"AUCUN":"Votant "+ dDict0 +" (VIOLE Non-dictature par construction)"));
// === Section 2.1 : Lemme extremal (demo construite) ===// On construit un profil ou 'B' est TOUJOURS en position extreme (premier ou dernier)// et on verifie que Borda le place aussi en position extreme.var extremal =new List<List<string>>{new(){"A","C","B"},// B derniernew(){"B","A","C"},// B premiernew(){"C","A","B"},// B derniernew(){"B","C","A"},// B premiernew(){"A","C","B"},// B dernier};var rankExt =Borda(extremal);int posB = rankExt.IndexOf("B");bool isExtreme =(posB ==0|| posB == rankExt.Count-1);Console.WriteLine("Lemme extremal : profil ou B est toujours en position extreme");Console.WriteLine(" Classement Borda : "+string.Join(" > ", rankExt));Console.WriteLine(" Position de B : "+ posB +" (sur "+(rankExt.Count-1)+")");Console.WriteLine(" B en position extreme dans le social ? "+ isExtreme);Console.WriteLine(" (Sous Pareto + IIA, le lemme extremal garantit cela pour toute regle admissible.)");
Lemme extremal : profil ou B est toujours en position extreme
Classement Borda : A > C > B
Position de B : 2 (sur 2)
B en position extreme dans le social ? True
(Sous Pareto + IIA, le lemme extremal garantit cela pour toute regle admissible.)
Lecture de la sortie committée — et son ambiguïté d’affichage : le classement Borda du profil extremal est A > C > B avec les scores \(A = 6\), \(C = 5\), \(B = 4\) (B est premier chez 2 votants sur 5 : \(2 \times 2 = 4\) points, et dernier chez les 3 autres : 0 point — c’est tout ce que B récolte). La ligne Position de B : 2 (sur 2) se lit en index 0-based : B occupe l’index 2 d’une liste de 3, c’est-à-dire la dernière place. Détail contre-intuitif à méditer : B est premier chez 40 % des votants et finit néanmoins dernier du classement social — être premier chez une minorité rapporte 2 points par votant, être dernier chez la majorité n’en coûte rien mais n’en rapporte pas : l’arithmétique de Borda est impitoyable aux soutiens minoritaires. Le booléen True confirme que B est bien en position extrême dans le social, ce que le lemme extremal (sous Pareto + IIA) garantit pour toute règle admissible.
// === Section 2.2 : Existence du pivot (demo construite) ===// On part d'un profil ou B est dernier pour tous, puis on bascule B en premier// pour les votants un par un. On cherche l'electeur pivot dont le bascule fait// passer B de dernier a premier dans le classement Borda.var others =new List<string>{"A","C"};int nv =5;// Etat initial : tous placent B dernier (ordre A,C determine)var pivotProf =new List<List<string>>();for(int i =0; i < nv; i++) pivotProf.Add(new List<string>{(i %2==0?"A":"C"),(i %2==0?"C":"A"),"B"});int pivotIdx =-1;for(int step =0; step < nv; step++){// L'electeur 'step' bascule B en premier pivotProf[step]=new List<string>{"B",(step %2==0?"A":"C"),(step %2==0?"C":"A")};var r =Borda(pivotProf);if(r.IndexOf("B")==0){ pivotIdx = step;break;}}Console.WriteLine("Recherche du pivot (B bascule du bas vers le sommet, votant par votant) :");Console.WriteLine(" Electeur pivot detecte : "+(pivotIdx >=0?"Votant "+ pivotIdx :"AUCUN"));Console.WriteLine(" (Sous Pareto + IIA, l'existence d'un tel pivot est garantie des qu'il y a >= 3 alternatives.)");
Recherche du pivot (B bascule du bas vers le sommet, votant par votant) :
Electeur pivot detecte : Votant 2
(Sous Pareto + IIA, l'existence d'un tel pivot est garantie des qu'il y a >= 3 alternatives.)
Lecture de la sortie committée : le pivot détecté est le Votant 2 (sur 5). Le scénario : tous placent B dernier, puis on bascule B en premier électeur par électeur — le pivot est celui dont le basculement fait passer B de dernier à premier dans le classement social. La sortie n’affiche qu’une ligne : Electeur pivot detecte : Votant 2 — l’information intéressante est ce qu’elle ne dit pas : entre le pas 1 (B premier chez les votants 0-1) et le pas 2 (votants 0-2), le classement social a basculé d’un coup, exactement à l’électeur 2. Ce basculement discret — rien, rien, tout — est le cœur de la preuve d’Arrow : c’est ce seuil qui transforme un électeur ordinaire en dictateur partiel sur les paires sans B (section suivante). La constructibilité du scénario (profil construit, pas cherché) est la marque de la leçon c.96 partagée avec le contre-exemple IIA.
2. Structure de la preuve d’Arrow
La preuve formelle d’Arrow (pour \(\geq 3\) alternatives) procède en trois temps. On l’illustre ici déterministiquement sur la règle de Borda :
Lemme extremal : si une alternative \(b\) est toujours placée en position extrême (première ou dernière) par chaque votant, alors elle est aussi en position extrême dans le classement social (sous Pareto + IIA).
Existence du pivot : en faisant basculer \(b\) du bas vers le sommet, électeur par électeur, il existe un électeur pivot dont le basculement fait passer \(b\) de dernier à premier.
Le pivot est dictateur partiel : ce pivot dicte alors le classement pour toute paire ne contenant pas \(b\).
// === Section 2.3 : Le pivot est dictateur partiel (demo) ===// Pour toute paire (a, c) ne contenant pas la cible b, le pivot dicte le classement.// On l'illustre : le pivot detecte prefere-t-il A a C ?// Le classement social Borda suit-il cette preference ?if(pivotIdx >=0){// On reconstruit un profil ou le pivot est libre sur A vs Cvar testProf =new List<List<string>>{new(){"A","C","B"},new(){"C","A","B"},new(){"A","C","B"},new(){"C","A","B"},new(){"A","C","B"},};var r =Borda(testProf);bool pivotPrefA = testProf[pivotIdx].IndexOf("A")< testProf[pivotIdx].IndexOf("C");bool socialPrefA = r.IndexOf("A")< r.IndexOf("C"); Console.WriteLine("Pivot = Votant "+ pivotIdx); Console.WriteLine(" Le pivot prefere A a C ? "+ pivotPrefA); Console.WriteLine(" Le social (Borda) prefere A a C ? "+ socialPrefA); Console.WriteLine(" Concordance pivot-social sur (A,C) ? "+(pivotPrefA == socialPrefA)); Console.WriteLine(" (Sous Pareto + IIA, cette concordance vaut pour TOUTE paire sans b : le pivot est dictateur partiel.)");}else{ Console.WriteLine("Pas de pivot detecte dans la demo precedente (rare ; Borda y viole deja IIA).");}
Pivot = Votant 2
Le pivot prefere A a C ? True
Le social (Borda) prefere A a C ? True
Concordance pivot-social sur (A,C) ? True
(Sous Pareto + IIA, cette concordance vaut pour TOUTE paire sans b : le pivot est dictateur partiel.)
Lecture de la sortie committée — et sa portée honnête : sur le profil de test reconstruit, le pivot (Votant 2) préfère A à C, et le classement social Borda aussi — Concordance : True. Lisez le commentaire du code avec attention : c’est une illustration, pas une preuve exhaustive — une seule paire (A, C), un seul profil. La preuve réelle d’Arrow montre que cette concordance vaut pour toute paire ne contenant pas B et tout profil admissible ; ici, le notebook se contente de la rendre visible. La nuance a son importance pédagogique : la force brute de la section 3 est exhaustive mais ne teste que 3 règles sur un espace fini, la structure de la section 2 est constructive mais illustrée sur des cas choisis — les deux stratégies se complètent, aucune ne remplace le théorème.
2.3-bis — Test systématique : le pivot est-il TOUJOURS dictateur partiel ?
Les trois démos ci-dessus (2.1, 2.2, 2.3) travaillent chacune sur un seul profil construit à la main. Le jumeau Python consolide l’étape 2.3 par un test stochastique (500 profils aléatoires, random.shuffle), avec une limite : le pivot y est fixé à l’avance (celui de la démo précédente) et le hasard peut rater des contre-exemples.
Le twin C# fait plus fort, sans aucun RNG : il énumère exhaustivement les 216 profils (3 votants × 6 ordres stricts = 6³) et recalcule le pivot pour chaque profil, relativement à la règle testée :
famille de bascule : chaque votant place B dernier en conservant son ordre relatif sur {A, C} ; puis on bascule B en tête électeur par électeur (ordres relatifs préservés) ;
pivot : le premier électeur dont la bascule fait passer B en tête du classement social ;
test de dictature partielle : sur le profil d’origine, le classement social de la paire (A, C) — qui ne contient pas B — coïncide-t-il avec la préférence du pivot ?
Si le lemme de Geanakoplos s’appliquait à Borda, la concordance serait totale. Voyons ce que donne l’énumération complète.
// === Section 2.3-bis : test systematique -- les 216 profils, exhaustivement ===// Miroir deterministe du test stochastique Python (500 profils aleatoires,// pivot fixe) : ici 0 RNG, TOUS les profils enumerees, pivot RECALCULE pour// chacun. Le pivot est defini relativement a la regle testee.publicstatic List<List<string>>OrdresStrict(List<string> alts){var res =new List<List<string>>();voidRec(int k, List<string> cur){if(k == alts.Count){ res.Add(new List<string>(cur));return;}for(int i = k; i < alts.Count; i++){(cur[k], cur[i])=(cur[i], cur[k]);Rec(k +1, cur);(cur[k], cur[i])=(cur[i], cur[k]);}}Rec(0,new List<string>(alts));return res;}publicstaticintTrouverPivot(List<List<string>> profil, Func<List<List<string>>, List<string>> regle,string cible){for(int s =0; s < profil.Count; s++){var famille =new List<List<string>>();for(int i =0; i < profil.Count; i++){var autres = profil[i].Where(a => a != cible).ToList(); famille.Add(i <= s?new List<string>{ cible }.Concat(autres).ToList(): autres.Concat(new List<string>{ cible }).ToList());}if(regle(famille)[0]== cible)return s;}return-1;}intTestDictateurPartiel(Func<List<List<string>>, List<string>> regle,outstring premierContreExemple,out Dictionary<int,int> distPivots){int nonConc =0; premierContreExemple ="-"; distPivots =new Dictionary<int,int>();foreach(var v0 inOrdresStrict(alts3))foreach(var v1 inOrdresStrict(alts3))foreach(var v2 inOrdresStrict(alts3)){var profil =new List<List<string>>{ v0, v1, v2 };int piv =TrouverPivot(profil, regle,"B");if(piv <0)continue; distPivots[piv]= distPivots.GetValueOrDefault(piv)+1;bool pivPrefA = profil[piv].IndexOf("A")< profil[piv].IndexOf("C");var social =regle(profil);bool socPrefA = social.IndexOf("A")< social.IndexOf("C");if(pivPrefA != socPrefA){ nonConc++;if(nonConc ==1) premierContreExemple =string.Join(" | ", profil.Select((p, i)=>"V"+ i +" : "+string.Join(">", p)))+" (pivot V"+ piv +" prefere C>A, social classe A>C)";}}return nonConc;}Console.WriteLine("LE PIVOT EST-IL DICTATEUR PARTIEL ? -- 216 profils exhaustifs (3 votants x 6 ordres)");Console.WriteLine(newstring('-',78));int ncBorda =TestDictateurPartiel(p =>Borda(p),outstring ceBorda,outvar distBorda);Console.WriteLine("Borda : non-concordances "+ ncBorda +"/216"+(ncBorda >0?" -> le pivot N'EST PAS dictateur partiel":""));if(ncBorda >0){ Console.WriteLine(" Distribution des pivots : "+string.Join(", ", distBorda.OrderBy(kv => kv.Key).Select(kv =>"V"+ kv.Key+" = "+ kv.Value))); Console.WriteLine(" 1er contre-exemple : "+ ceBorda);}int ncDict =TestDictateurPartiel(p =>Dictatorial(p,0),out _,outvar distDict);Console.WriteLine("Dictatorial : non-concordances "+ ncDict +"/216"+(ncDict ==0?" -> concordance TOTALE : le pivot dicte (A, C) partout":""));Console.WriteLine(" Distribution des pivots : "+string.Join(", ", distDict.OrderBy(kv => kv.Key).Select(kv =>"V"+ kv.Key+" = "+ kv.Value)));
LE PIVOT EST-IL DICTATEUR PARTIEL ? -- 216 profils exhaustifs (3 votants x 6 ordres)
------------------------------------------------------------------------------
Borda : non-concordances 58/216 -> le pivot N'EST PAS dictateur partiel
Distribution des pivots : V1 = 189, V2 = 27
1er contre-exemple : V0 : A>B>C | V1 : B>C>A | V2 : A>B>C (pivot V1 prefere C>A, social classe A>C)
Dictatorial : non-concordances 0/216 -> concordance TOTALE : le pivot dicte (A, C) partout
Distribution des pivots : V0 = 216
Lecture de la sortie committée : l’énumération complète tranche.
Borda : 58/216 non-concordances. Le pivot n’est pas dictateur partiel sous Borda — et c’est la bonne nouvelle pédagogique : le lemme exige IIA, et la section 1.2 a mesuré 492 violations IIA pour Borda (contre 2568 pour la Pluralité). Les 58 non-concordances sont la trace mesurée de cette violation sur la paire (A, C) : l’hypothèse du lemme échoue, donc sa conclusion aussi.
Distribution des pivots (Borda) : V1 = 189, V2 = 27, V0 = 0. Le votant 0 n’est jamais pivot : une seule bascule ne suffit jamais — le score Borda de B gagne +2 par bascule mais part de trop bas. Le pivot est un phénomène de coalition : c’est le premier électeur dont la bascule, cumulée aux précédentes, fait pencher le classement social.
Contre-exemple lisible : sur le profil V0 : A>B>C | V1 : B>C>A | V2 : A>B>C, le pivot V1 préfère C > A… mais le classement social donne A > C. Le pivot ne dicte rien.
Dictatoriale : 0/216 non-concordances, pivot = V0 dans les 216 profils. Quand les hypothèses tiennent (Pareto ✓, IIA ✓), la concordance est totale : le théorème s’applique… et livre son verdict — la règle est une dictature.
La simulation mesure ; elle ne prouve pas. Ce comptage couvre deux règles sur les trois testées en section 3 — rien ici n’interdit a priori qu’une quatrième règle, plus rusée, satisfasse les trois axiomes. C’est précisément ce que le théorème formel exclut, pour toute règle imaginable — objet de la section suivante.
2.4 Le théorème final
Théorème principal (game_theory_lean/SocialChoice/Arrow.lean, ligne 691 — numéros mesurés sur le lake actuel) :
theorem arrow (f : SWF i sigma) (X : Finset sigma)
(hwp : weak_pareto f X) (hind : ind_of_irr_alts f X)
(hX : 3 <= X.card) :
is_dictatorship f X
Corollaire (forme négative, ligne 710) :
theorem no_perfect_swf (f : SWF i sigma) (X : Finset sigma)
(hwp : weak_pareto f X) (hind : ind_of_irr_alts f X)
(hX : 3 <= X.card) :
not (non_dictatorial f X)
Structure de la preuve dans Arrow.lean (0 sorry — mesuré) :
theorem arrow ... := by
-- existence du pivot pour la cible b (lemme, ligne 288) :
obtain <j, hj_piv> := pivot_exists f X hwp hind hX c hc
-- le pivot dicte toute paire ne contenant pas b (lemme, ligne 418) :
have h3 := pivot_is_dictator_except_b f X hind c hc j hj_piv ...
-- un dictateur partiel sur deux paires disjointes est complet (ligne 603) :
have h4 := partial_dictator_is_full_dictator ...
exact <j, h4>
En français : toute fonction de bien-être social (avec au moins 3 alternatives) qui satisfait Pareto faible et IIA est nécessairement une dictature. Il n’existe aucune règle de vote parfaite — pas seulement parmi Borda/Pluralité/Dictature : parmi toutes les règles imaginables.
Les quatre étapes de cette section sont les quatre maillons du fichier Lean : lemme extremal (2.1), existence du pivot (2.2), dictateur partiel (2.3 + 2.3-bis), dictateur complet — le maillon que la simulation ne peut qu’illustrer. La formalisation complète (et sa traduction Arrow_en.lean) vit dans game_theory_lean/SocialChoice/, explorée pas à pas dans 01b-Lean-SocialChoice-Formal.ipynb.
3. Réfutation par force brute (énumération complète)
On rassemble les trois axiomes sur l’ensemble des 216 profils et on dresse le tableau synthétique. Le théorème d’Arrow prédit : aucune règle ne satisfait simultanément Pareto + IIA + Non-dictature.
Règle
Pareto
IIA
Non-dictature
Borda
✓ (0 violation)
✗ (violations)
✓ (aucun dictateur)
Pluralité
✓
✗
✓
Dictatoriale
✓
✓
✗ (le dictateur)
Lecture du tableau committé : les trois lignes confirment la prédiction du théorème, chacune sur un axiome différent — Borda OK / ECHEC x1656 / OK, Pluralité OK / ECHEC x3312 / OK, Dictatoriale OK / OK / Dict(V0). Le tableau est la synthèse des trois sections précédentes, recomputées ici en une passe : les chiffres 1 656 et 3 312 sont identiques au comptage de la section 1.2-suite, preuve de reproductibilité (0 RNG, énumération déterministe). La conclusion affichée — « aucune règle ne satisfait Pareto + IIA + Non-dictature » — ne porte que sur trois règles testées, mais le théorème d’Arrow (1951) la généralise à toute règle d’agrégation avec \(\geq 3\) alternatives : l’énumération est une confirmation empirique, la preuve structurelle de la section 2 en donne le mécanisme.
// === Section 3 : Force brute -- synthese exhaustive des 3 axiomes ===Console.WriteLine("Refutation par force brute (216 profils, 3 alternatives, 3 votants)");Console.WriteLine(newstring('-',62));Console.WriteLine(string.Format("{0,-13} {1,-10} {2,-22} {3,-15}","Regle","Pareto","IIA (violations)","Non-dictature"));Console.WriteLine(newstring('-',62));stringRow(string name, Func<List<List<string>>, List<string>> rule){int par =ParetoViolations(rule, alts3, nVot);var(viia, _)=IiaViolations(rule, alts3, nVot);int dic =FindDictator(rule, alts3, nVot);string paretoTxt = par ==0?"OK":("ECHEC x"+ par);string iiaTxt = viia ==0?"OK":("ECHEC x"+ viia);string dicTxt = dic <0?"OK":("Dict(V"+ dic +")");returnstring.Format("{0,-13} {1,-10} {2,-22} {3,-15}", name, paretoTxt, iiaTxt, dicTxt);}Console.WriteLine(Row("Borda", p =>Borda(p)));Console.WriteLine(Row("Pluralite", p =>Pluralite(p)));Console.WriteLine(Row("Dictatorial", p =>Dictatorial(p,0)));Console.WriteLine(newstring('-',62));Console.WriteLine();Console.WriteLine(">>> VERDICT : aucune regle ne satisfait Pareto + IIA + Non-dictature.");Console.WriteLine(">>> C'est exactement le theoreme d'impossibilite d'Arrow (1951).");
Refutation par force brute (216 profils, 3 alternatives, 3 votants)
--------------------------------------------------------------
Regle Pareto IIA (violations) Non-dictature
--------------------------------------------------------------
Borda OK ECHEC x1656 OK
Pluralite OK ECHEC x3312 OK
Dictatorial OK OK Dict(V0)
--------------------------------------------------------------
>>> VERDICT : aucune regle ne satisfait Pareto + IIA + Non-dictature.
>>> C'est exactement le theoreme d'impossibilite d'Arrow (1951).
Synthèse
Le théorème d’Arrow est confirmé empiriquement par énumération exhaustive (méthode déterministe, 0 RNG) : - Borda et Pluralité satisfont Pareto et Non-dictature mais violent IIA ; - Dictatoriale satisfait Pareto et IIA mais viole Non-dictature ; - Aucune des trois règles ne passe les trois axiomes à la fois — et le théorème garantit qu’aucune règle imaginable ne le peut (avec \(\geq 3\) alternatives).
Pourquoi le twin C# apporte-t-il quelque chose ?
Déterministe : pas de random.seed(42) — l’énumération est exhaustive et reproductible, elle ne rate aucune violation (le test stochastique Python pouvait tomber sur 0 violation par malchance) ;
Pédagogique : on affiche le profil coupable (contre-exemple construit section 1.2, premier exemple section 1.2-suite) plutôt qu’un simple comptage ;
Parité exacte sur le résultat (tableau synthétique), indépendante du RNG cross-lang.
Lexique bilingue
Français
English
Règle d’agrégation / règle de vote
Social welfare function / voting rule
Pareto faible (unanimité)
Weak Pareto (unanimity)
Indépendance aux alternatives non pertinentes
Independence of Irrelevant Alternatives (IIA)
Non-dictature
Non-dictatorship
Lemme extremal / électeur pivot
Extremal lemma / pivotal voter
Voir le twin compagnon 03-Voting-Methods-Csharp.ipynb (méthodes de vote : Pluralité, Borda, Copeland, Condorcet, IRV) pour le calcul opérationnel des gagnants.
Ce que le tableau ne dit pas — et pourquoi Dictatoriale satisfait IIA : la ligne Dictatoriale OK / OK / Dict(V0) surprend : comment la règle la plus grossière passe-t-elle l’axiome le plus subtil ? Réponse : IIA exige que le verdict social sur \((x,y)\) ne dépende que des préférences individuelles sur \((x,y)\). Le dictateur rend un verdict identique aux propres préférences complètes du votant 0 — donc a fortiori déterminé par ses préférences sur \((x,y)\) seul. IIA est violé quand une règle mélange l’information des autres alternatives (Borda compte des positions), pas quand elle les ignore totalement. L’enseignement : les trois axiomes sont individuellement satisfaisables (chaque ligne du tableau montre une règle qui passe chaque axiome), mais conjointement impossibles — c’est le cœur du théorème, et le jumeau Python stochastique ne pouvait le montrer aussi nettement : sur des tirages aléatoires, une violation rare peut passer inaperçue, alors que l’énumération exhaustive des 216 profils ne rate rien.
Synthèse visuelle : les trois règles face aux trois axiomes
Le jumeau Python clôt sa démonstration par une visualisation matplotlib des verdicts. Le twin C# fait de même avec ScottPlot (l’équivalent .NET de matplotlib) — la seule dépendance externe du notebook, pour la visualisation uniquement : les algorithmes de vote restent from-scratch (section 1).
Chaque groupe de barres = une règle ; chaque barre = un axiome (vert = satisfait, rouge = violé). Les verdicts sont ceux mesurés en section 3 par force brute exhaustive : Borda et Pluralité violent IIA, la Dictature viole Non-dictature — aucune règle n’est toute verte.
// === Synthese visuelle (ScottPlot 5) : miroir de la section 4 du twin Python ===// Verdicts MESURES en section 3 (force brute exhaustive) : 1 = satisfait, 0 = viole.// Vert #2ecc71 = satisfait / rouge #e74c3c = viole : memes codes que matplotlib cote Python.// Dans chaque groupe, les barres sont dans l'ordre Pareto / IIA / Non-dict.#r "nuget: ScottPlot, 5.0.55"using ScottPlot;using Microsoft.DotNet.Interactive;string[] reglesViz ={"Borda","Pluralite","Dictature"};string[] axiomesViz ={"Pareto","IIA","Non-dict"};int[,] verdictsViz ={{1,0,1},{1,0,1},{1,1,0}};var pltViz =new ScottPlot.Plot();double[] xsViz =newdouble[9];double[] ysViz =newdouble[9];string[] ticksViz =newstring[9];int kViz =0;for(int r =0; r <3; r++)for(int a =0; a <3; a++){ xsViz[kViz]= r *4+ a; ysViz[kViz]=1.0; ticksViz[kViz]= axiomesViz[a]; kViz++;}var barresViz = pltViz.Add.Bars(xsViz, ysViz);kViz =0;for(int r =0; r <3; r++)for(int a =0; a <3; a++){bool ok = verdictsViz[r, a]==1; barresViz.Bars[kViz].FillColor= ScottPlot.Color.FromHex(ok ?"#2ecc71":"#e74c3c"); pltViz.Add.Text(ok ?"SATISFAIT":"VIOLE", xsViz[kViz],0.5); kViz++;}for(int r =0; r <3; r++) pltViz.Add.Text(reglesViz[r], r *4+1,1.22);pltViz.Axes.Bottom.SetTicks(xsViz, ticksViz);pltViz.Axes.SetLimits(bottom:-0.1, top:1.42);pltViz.Title("Theoreme d'Arrow : aucun systeme ne satisfait les 3 axiomes");Console.WriteLine("Synthese visuelle generee : 3 regles x 3 axiomes (verdicts de la section 3).");Console.WriteLine("Vert #2ecc71 = axiome satisfait, rouge #e74c3c = axiome viole.");display(HTML(pltViz.GetPngHtml(820,400)));
Installing Packages
ScottPlot
Synthese visuelle generee : 3 regles x 3 axiomes (verdicts de la section 3).
Vert #2ecc71 = axiome satisfait, rouge #e74c3c = axiome viole.
Lecture de la visualisation : le diagramme rend visible d’un coup d’œil ce que le tableau de la section 3 énumérait — aucun groupe de barres n’est entièrement vert :
Borda et Pluralité : deux barres vertes (Pareto, Non-dictature), une rouge (IIA) — des règles « presque » parfaites qui échouent sur l’indépendance ;
Dictature : Pareto ✓, IIA ✓… et la barre Non-dictature rouge. La dictature est la seule façon de garder l’indépendance — c’est exactement le contenu du théorème : Pareto + IIA ⇒ dictature.
C’est aussi la leçon de lecture d’Arrow : un choix d’agrégation n’est jamais « bon » dans l’absolu — il choisit quel axiome sacrifier. Le notebook suivant (03-Voting-Methods) explore ce que l’on peut sauver en relâchant les hypothèses.
Annexe SAT : Arrow par solveur — pont PythonNet vers pysat
La synthèse ci-dessus repose sur la force brute : trois règles particulières, testées sur les 216 profils. Mais le théorème porte sur toutes les règles — \(6^{216}\) SWF possibles, inénumérables. Un solveur SAT clôt le gap : on encode la question d’existence (« existe-t-il une SWF quelconque réunissant totalité, transitivité, Pareto, IIA et non-dictature ? ») en CNF, et un verdict UNSAT prouve la non-existence sans énumération.
Même encodage que le twin Python (annexe pysat du 01-Arrow-Impossibility-Theorem.ipynb) : un littéral \(v_{P,(x,y)}\) = « le résultat social du profil \(P\) classe \(x\) avant \(y\) », puis totalité/asymétrie, transitivité, Pareto (unanimité), IIA (accord entre profils) et non-dictature (une clause par votant) — 216 profils, 1296 littéraux, 36453 clauses.
Pont industriel (#10382, axe 5) : plutôt qu’une réimplémentation C# d’un solveur CDCL, la cellule ci-dessous traverse PythonNet (.NET → Python.Runtime → CPython 3.13 → pysat) pour exécuter Glucose 3, MiniSat 22 et CaDiCaL 103 sur l’encodage produit côté C#. Recette : package pythonnet3.1.0 (la 3.0.5 repose sur BinaryFormatter, supprimé de .NET 9), Runtime.PythonDLL pointant vers un CPython où python-sat est installé (surcharge par la variable d’environnement PYTHONNET_PYDLL), et le répertoire de CPython placé en tête du PATH avant Initialize() (résolution des DLL dépendantes). Le pont est en plus, jamais à la place : la force brute déterministe reste l’outil pédagogique ; le pont apporte la jambe industrielle (registre twin_pairs.d, pattern « même moteur, deux ponts » déjà établi CSP-5 pour Tweety).
// === Annexe SAT : encodage d'Arrow en CNF (existence d'une SWF quelconque) ===// Litteral satLit[(pi, x, y)] = "le resultat social du profil pi classe x avant y".// Reutilise les helpers deterministes de la Section 1 (AllProfiles, AllPrefer, AllPermutations).var satProfiles =AllProfiles(alts3, nVot);var satPairs =new List<(string x,string y)>();for(int i =0; i < alts3.Count; i++)for(int j =0; j < alts3.Count; j++)if(i != j) satPairs.Add((alts3[i], alts3[j]));var satLit =new Dictionary<(int pi,string x,string y),int>();for(int pi =0; pi < satProfiles.Count; pi++)foreach(var(x, y)in satPairs) satLit[(pi, x, y)]= satLit.Count+1;var clausesArrow =new List<List<int>>();var statsSat =new Dictionary<string,int>{["totalite + asymetrie"]=0,["transitivite"]=0,["pareto"]=0,["iia"]=0,["non-dictature"]=0,};for(int pi =0; pi < satProfiles.Count; pi++){var prof = satProfiles[pi];for(int a =0; a < alts3.Count; a++)// ordre total strictfor(int b = a +1; b < alts3.Count; b++){ clausesArrow.Add(new List<int>{ satLit[(pi, alts3[a], alts3[b])], satLit[(pi, alts3[b], alts3[a])]}); clausesArrow.Add(new List<int>{-satLit[(pi, alts3[a], alts3[b])],-satLit[(pi, alts3[b], alts3[a])]}); statsSat["totalite + asymetrie"]+=2;}foreach(var perm inAllPermutations(alts3))// transitivite{string x = perm[0], y = perm[1], z = perm[2]; clausesArrow.Add(new List<int>{-satLit[(pi, x, y)],-satLit[(pi, y, z)], satLit[(pi, x, z)]}); statsSat["transitivite"]++;}foreach(var(x, y)in satPairs)// pareto (tous preferent x a y)if(AllPrefer(prof, x, y)){ clausesArrow.Add(new List<int>{ satLit[(pi, x, y)]}); statsSat["pareto"]++;}}for(int p1 =0; p1 < satProfiles.Count; p1++)// IIAfor(int p2 = p1 +1; p2 < satProfiles.Count; p2++)foreach(var(x, y)in satPairs){bool accord =true;for(int vt =0; vt < nVot; vt++)if((satProfiles[p1][vt].IndexOf(x)< satProfiles[p1][vt].IndexOf(y))!=(satProfiles[p2][vt].IndexOf(x)< satProfiles[p2][vt].IndexOf(y))){ accord =false;break;}if(accord){ clausesArrow.Add(new List<int>{-satLit[(p1, x, y)], satLit[(p2, x, y)]}); clausesArrow.Add(new List<int>{ satLit[(p1, x, y)],-satLit[(p2, x, y)]}); statsSat["iia"]+=2;}}for(int vt =0; vt < nVot; vt++)// non-dictature{var clause =new List<int>();for(int pi =0; pi < satProfiles.Count; pi++)foreach(var(x, y)in satPairs)if(satProfiles[pi][vt].IndexOf(x)< satProfiles[pi][vt].IndexOf(y)) clause.Add(-satLit[(pi, x, y)]); clausesArrow.Add(clause); statsSat["non-dictature"]++;}statsSat["variables"]= satLit.Count;Console.WriteLine("ENCODAGE SAT D'ARROW (existence d'une SWF Pareto + IIA + non-dictature)");Console.WriteLine($"Instance : {satProfiles.Count} profils, {satLit.Count} litteraux, {clausesArrow.Count} clauses");foreach(var kv in statsSat)if(kv.Key!="variables") Console.WriteLine($" {kv.Key,-20}: {kv.Value}");
#r "nuget: pythonnet,3.1.0"using Python.Runtime;using System.IO;// === Pont industriel : pysat via PythonNet (axe 5 #10382) sur l'encodage C# ci-dessus ===string[] dllCandidates ={ Environment.GetEnvironmentVariable("PYTHONNET_PYDLL"), @"C:\ProgramData\miniconda3\python313.dll", @"C:\Users\jsboi\AppData\Local\Programs\Python\Python313\python313.dll",};string pyDll = dllCandidates.FirstOrDefault(File.Exists);if(pyDll ==null)thrownewFileNotFoundException("Aucun CPython avec pysat trouve : fixer PYTHONNET_PYDLL (pip install python-sat).");// Resolution des DLL dependantes : le repertoire de CPython precede le PATHstring pyDir = Path.GetDirectoryName(pyDll);Environment.SetEnvironmentVariable("PATH", pyDir + Path.PathSeparator+ Environment.GetEnvironmentVariable("PATH"));Runtime.PythonDLL= pyDll;PythonEngine.Initialize();Console.WriteLine($"Pont PythonNet : CPython {PythonEngine.Version}, pythonnet 3.1.0");Console.WriteLine();string clausesJson ="["+string.Join(",", clausesArrow.Select(c =>"["+string.Join(",", c)+"]"))+"]";Console.WriteLine("PYSAT SUR L'ENCODAGE D'ARROW (3 alternatives, 3 votants)");Console.WriteLine("=".PadRight(54,'='));Console.WriteLine($"Instance CNF : {statsSat["variables"]} litteraux, {clausesArrow.Count} clauses");Console.WriteLine();using(Py.GIL()){ dynamic scope = Py.CreateScope(); scope.Set("clauses_json", clausesJson); scope.Exec(@"import json, timefrom pysat.solvers import Glucose3, Minisat22, Cadical103clauses = json.loads(clauses_json)lines =[]for name, cls in[('Glucose3', Glucose3),('MiniSat22', Minisat22),('CaDiCaL103', Cadical103)]: t0 = time.perf_counter() with cls(bootstrap_with=clauses)as s: sat = s.solve() dt_ms =(time.perf_counter()- t0)*1000.0 verdict = 'SAT(contredit Arrow !)' if sat else 'UNSAT(Arrow verifie)' lines.append(f'{name:12s}:{verdict}[{dt_ms:8.1f} ms]')summary =chr(10).join(lines)"); Console.WriteLine(scope.Get<string>("summary")); Console.WriteLine(); Console.WriteLine("Meme instance, memes verdicts que le twin Python (annexe pysat native).");}PythonEngine.Shutdown();
Installing Packages
pythonnet
Pont PythonNet : CPython 3.13.12 | packaged by Anaconda, Inc. | (main, Feb 24 2026, 16:05:56) [MSC v.1942 64 bit (AMD64)], pythonnet 3.1.0
PYSAT SUR L'ENCODAGE D'ARROW (3 alternatives, 3 votants)
======================================================
Instance CNF : 1296 litteraux, 36453 clauses
Glucose3 : UNSAT (Arrow verifie) [ 20.5 ms]
MiniSat22 : UNSAT (Arrow verifie) [ 16.3 ms]
CaDiCaL103 : UNSAT (Arrow verifie) [ 53.8 ms]
Meme instance, memes verdicts que le twin Python (annexe pysat native).
Lecture du résultat : parité des moteurs
Les trois solveurs CDCL répondent UNSAT sur l’encodage produit par le code C# : la non-existence d’une SWF Pareto + IIA + non-dictature est prouvée pour l’instance (3 alternatives, 3 votants). La force brute le suggérait sur trois règles ; le solveur le démontre pour toutes les \(6^{216}\).
Instance et verdicts (216 profils, 1296 littéraux, 36453 clauses) sont identiques à ceux du twin Python (annexe pysat native) : les deux jumeaux atteignent le même moteur de résolution, chacun par sa voie — pysat natif d’un côté, pont PythonNet de l’autre (« même moteur, deux ponts », cf. CSP-5 pour Tweety).
L’ordre de grandeur du temps de résolution (~10 ms par solveur, runtime machine-dep) illustre l’écart structurel avec la force brute : tester l’existence est exponentiellement moins cher qu’énumérer les candidates.
Exercices
Convention (règle C.1) : les stubs s’exécutent sans erreur (pass/return/print). Le notebook doit tourner de bout en bout même exercices non complétés.
Comment utiliser ces exercices : chaque stub est auto-exécutable (règle C.1 — la sortie affiche « a completer » sans erreur), et les critères de validation détaillés sous chaque énoncé donnent les valeurs ou propriétés attendues : vérifiez votre solution contre eux, pas seulement contre l’absence d’exception. Les exercices 1 et 2 prolongent les démonstrations des sections 2.1 et 1.2 sur des cas plus larges ; les exercices 3 et 4 changent de registre (complexité combinatoire, paradoxe de vote).
Exercice 1 — Lemme extremal avec 4 alternatives
Critère de validation : avec 4 alternatives, « position extrême » signifie 1re ou 4e place. Construisez un profil (5 votants suffisent) où B est toujours 1er ou 4e chez chaque votant, appelez Borda() et vérifiez posB == 0 || posB == 3 dans le classement social. Point de vigilance honnête : le lemme extremal est garanti sous Pareto + IIA — or Borda viole IIA (section 1.2) ; votre exemple peut donc montrer soit que B reste extrême (le lemme « marche » sur ce cas), soit un contre-exemple de plus contre Borda. Les deux issues sont instructives : documentez laquelle vous obtenez.
// Exercice 1 : Lemme extremal avec 4 alternatives// ================================================// Adaptez la demo de la section 2.1 avec alternatives_4 = {A, B, C, D} et la cible 'B'.// Indice : avec 4 alternatives, B peut etre en 1re ou 4e position ; les 3 autres// sont melangees. Generez plusieurs profils et verifiez si Borda place B en position// extreme (1re ou 4e) dans le classement social.var alternatives_4 =new List<string>{"A","B","C","D"};// TODO etudiant : construisez un profil ou B est toujours extreme puis appelez Borda().object result_ex1 =null;// TODO etudiant : votre classement social BordaConsole.WriteLine("Exercice 1 : Lemme extremal avec 4 alternatives (a completer)");
Exercice 1 : Lemme extremal avec 4 alternatives (a completer)
Exercice 2 — Contre-exemple IIA explicite pour Borda
Critère de validation : vos deux profils (3 votants, 3 alternatives) doivent (a) avoir des préférences individuelles A-vs-C identiques votant par votant — vérifiez-le explicitement comme le fait la cellule de la section 1.2 (preferences identiques ? True), (b) donner des verdicts sociaux Borda opposés sur A-vs-C. L’indice de l’énoncé est le mécanisme exact : ne changez que la position de B chez un ou deux votants, en veillant à ce que ce déplacement transfère des points entre A et C (revoir la décomposition \(A : +2, B : -3, C : +1\) de la section 1.2). Si votre verdict ne bascule pas, c’est que votre déplacement de B n’a pas affecté l’écart de scores A-vs-C — recommencez avec un écart initial plus serré.
// Exercice 2 : Contre-exemple IIA explicite pour Borda// =====================================================// Construisez deux profils (3 votants, 3 alternatives) ou les preferences// relatives entre A et C sont identiques pour chaque votant, mais le classement// social Borda de A vs C change.// Indice : changez uniquement la position de B (l'alternative "non pertinente")// dans les preferences d'un votant pour faire basculer le verdict Borda.var profil_1_ex2 =new List<List<string>>{// TODO etudiant : 3 classements};var profil_2_ex2 =new List<List<string>>{// TODO etudiant : memes contraintes A-vs-C, position de B differente};// TODO etudiant : verifiez (a) preferences A-vs-C identiques, (b) Borda bascule.Console.WriteLine("Exercice 2 : Contre-exemple IIA pour Borda (a completer)");
Exercice 2 : Contre-exemple IIA pour Borda (a completer)
Exercice 3 — Complexité de la force brute
Critère de validation : la formule est \((k!)^n\) profils pour \(n\) votants et \(k\) alternatives. Valeurs attendues pour les trois configurations affichées : \((3, 3) \to 6^3 = 216\) (le chiffre du notebook entier), \((5, 3) \to 6^5 = 7\,776\), \((10, 4) \to 24^{10} = 63\,403\,380\,965\,376 \approx 6,3 \times 10^{13}\). La morale du dernier chiffre : la force brute devient physiquement impossible bien avant l’échelle réelle d’une élection — le théorème d’Arrow vaut précisément parce qu’il démontre l’impossibilité pour toute règle, là où l’énumération ne peut tester qu’un univers fini et minuscule. Note d’implémentation : Math.Pow travaille en double (15-16 chiffres significatifs) — pour \((10,4)\) vous frôlez la perte de précision, préférez une boucle de multiplication long comme le suggère l’indice.
// Exercice 3 : Complexite de la force brute// ==========================================// Implementez le nombre de profils possibles pour n votants et k alternatives.// Indice : chaque votant a (k!) classements possibles ; pour n votants independants,// on multiplie : (k!)^n.publicstaticlong?CountProfiles(int nVoters,int nAlternatives){// TODO etudiant : retournez la factorielle(nAlternatives) elevee a nVoters.// Indice : long fact = 1; for (int i=2; i<=nAlternatives; i++) fact *= i; puis (long)Math.Pow(fact, nVoters).returnnull;// remplacez par le calcul correct}Console.WriteLine("Exercice 3 : Complexite de la force brute");var configs =new[]{(3,3),(5,3),(10,4)};foreach(var(nV, nA)in configs){var np =CountProfiles(nV, nA); Console.WriteLine(" ("+ nV +" votants, "+ nA +" alts) -> "+(np?.ToString()??"(a completer)")+" profils");}
Exercice 3 : Complexite de la force brute
(3 votants, 3 alts) -> (a completer) profils
(5 votants, 3 alts) -> (a completer) profils
(10 votants, 4 alts) -> (a completer) profils
Exercice 4 — Profil de préférences paradoxaux (Condorcet vs Borda)
Critère de validation : votre profil doit produire (a) un gagnant de Condorcet — une alternative qui bat chaque autre en duel pairwise à la majorité — et (b) un gagnant Borda différent. Ne confondez pas avec le paradoxe plus facile où le profil cyclique (V1 : A>B>C, V2 : B>C>A, V3 : C>A>B) ne produit aucun gagnant de Condorcet : ici il en faut un, et c’est Borda qui a tort de l’ignorer. Méthode : énumérez les duels avec IndexOf comme l’indique l’énoncé, identifiez le gagnant de Condorcet, puis comparez au premier de Borda(profil). Contrôle d’honnêteté : votre gagnant de Condorcet doit gagner strictement ses duels (majorité stricte), sinon le « paradoxe » n’est qu’une égalité mal comptée.
// Exercice 4 : Profil de preferences paradoxaux// TODO etudiant : construisez un profil (3 votants, 3 alternatives) qui viole le// critere de Condorcet avec la regle de Borda : le gagnant de Condorcet (celui qui// bat tout autre en duel pairwise) n'est PAS le gagnant Borda.// Indice : enumeratez les duels pairwise avec AllPrefer / IndexOf pour identifier// le gagnant de Condorcet, puis comparez au premier de Borda(profil).object result_ex4 =null;// TODO etudiant : votre profil paradoxalConsole.WriteLine("Exercice a completer : Profil de preferences paradoxaux (Condorcet vs Borda)");
Exercice a completer : Profil de preferences paradoxaux (Condorcet vs Borda)
Conclusion
Ce twin C# démontre le théorème d’impossibilité d’Arrow par voie computo-déterministe : énumération exhaustive des 216 profils + contre-exemples construits. La leçon clé (cf. jumeau 03-Voting-Methods-Csharp) : pour la parité pédagogique cross-lang d’un résultat algorithmique, le déterministe bat le stochastique — reproductible, exhaustif, et il montre le pourquoi (le profil coupable) plutôt que le combien (un comptage opaque).
Les chiffres à retenir : 216 profils énumérés (exhaustivement, 0 RNG) ; 0 violation de Pareto pour les trois règles ; un contre-exemple IIA construit où les scores Borda basculent de \(A=6, B=7, C=2\) à \(A=8, B=4, C=3\) sans qu’aucune préférence individuelle A-vs-B ne change ; 1 656 violations IIA pour Borda, 3 312 pour la Pluralité ; pivot Votant 2 dans la démonstration structurelle ; et le verdict final — chaque règle échoue sur un axiome différent, aucune ne les passe tous, exactement comme le théorème de 1951 l’exige.
