Screening, signal et anticipation : les trois réponses formelles à l’information asymétrique
Série GameTheory · 17d.
Le compagnon 17c a exécuté le certificat d’Akerlof : quand l’information est asymétrique avant le contrat, le marché dégénère. Ce notebook exécute nativement (kernel lean4-wsl) les quatre autres modules du lake asymmetric_information_lean, qui formalisent les trois réponses classiques à cette asymétrie :
L’enjeu, avant les définitions. En 1970, Akerlof montre qu’un marché où le vendeur sait ce que l’acheteur ignore peut mourir de cette ignorance : les acheteurs, ne pouvant départager les bonnes voitures des « lemons », n’offrent que le prix moyen — ce prix chasse les bons vendeurs, la qualité moyenne baisse, le prix suit, et la spirale peut vider le marché. Le compagnon 17c a exécuté ce certificat d’effondrement. La question qui reste ouverte est institutionnelle : quelles réponses les acteurs eux-mêmes peuvent-ils construire pour restaurer le commerce ? La littérature des années 1970 en identifie trois, et ce notebook les exécute toutes dans un cadre formel unique :
la partie non informée structure le choix (screening, Rothschild-Stiglitz 1976) ;
la partie informée paie pour se révéler (signaling, Spence 1973, Riley 1979) ;
les acteurs anticipent les réactions des tiers (Wilson 1977, Miyazaki 1977).
Module
Modèle
Question
Screening
Rothschild-Stiglitz 1976
la partie informée s’autosélectionne dans un menu — l’équilibre existe-t-il ?
Signaling
Spence 1973 / Riley
la partie informée paie un signal pour se révéler — à quel coût minimal ?
MiyazakiWilson
Wilson 1977, Miyazaki 1977
les assureurs anticipent les retraits — le cross-subsidy devient-il tenable ?
BayesianLink
—
le marché des lemons devient un jeu bayésien : le lien isBNE est certifié par decide
Chaque énoncé ci-dessous est chargé depuis le lake (aucune redéfinition) : ce que lit l’étudiant est exactement ce qui compile.
Contrat de validation du kernel : lean4-wsl émet tous ses messages — y compris les erreurs de compilation Lean — en display_data de sévérité info, jamais en output_type=error. Un passage sain se vérifie donc par l’absence de marque ❌ et de toute sévérité error dans les raw outputs (détail : wsl-kernels-detail.md).
Comment lire ce notebook. Chaque section suit le même mouvement : le cadre du lake (types, prédicats, théorèmes), une exécution chiffrée (#eval sur des témoins décidés), puis une lecture économique qui interprète les nombres. Les trois réponses s’enchaînent logiquement — le screening échoue à l’équilibre de Nash, le signaling déplace le problème vers le coût du signal, l’anticipation répare l’équilibre en subventionnant les contrats — et le pont bayésien final referme le tout sur le formalisme des jeux bayésiens de GameTheory-11b.
Raw input{"cmd": "import AsymmetricInformation.Screening\nimport AsymmetricInformation.Signaling\nimport AsymmetricInformation.MiyazakiWilson\nimport AsymmetricInformation.BayesianLink\n"}Raw output{"env": 0}
I. Screening — Rothschild-Stiglitz 1976
Ici l’assureur (partie non informée) bouge le premier : il propose un menu de contrats, et chaque type d’assuré choisit le sien. Le modèle du lake encode :
RiskType : deux types, high (bon risque, p_H petite) et low (mauvais risque, p_L grande) ;
RiskProfile : le couple (pHigh, pLow) en centièmes, avec la contrainte pHigh < pLow ;
Contract : une couverture coverage et une prime premium, en entiers (pas de Mathlib — arithmétique Int close, décidable par omega/decide) ;
expectedProfit c r q = premium * 100 - p_q * coverage : le profit attendu du contrat c sur le type q.
Concrètement, l’assureur ne propose pas un contrat unique mais un menu : plusieurs couples (coverage, premium) parmi lesquels chaque assuré choisit librement. C’est le geste de Rothschild-Stiglitz — si l’assureur ne peut pas observer le type, il peut faire en sorte que le type s’observe lui-même. Un menu est un instrument d’autosélection : à condition que chaque type préfère son contrat dédié à celui de l’autre, le choix révèle l’information. Tout le problème est de savoir si un tel menu survit à la concurrence — la section montre que sur la région cream-skim, non.
-- Le profil canonique des exemples du lake : (p_H, p_L) = (25, 75).
def profilRS : AsymmetricInformation.Screening.RiskProfile := ⟨25, 75, by omega⟩
-- Le contrat temoin du module : couverture 100, prime 20.
def contratTemoin : AsymmetricInformation.Screening.Contract := ⟨100, 20⟩
#check AsymmetricInformation.Screening.expectedProfit
#check AsymmetricInformation.Screening.breakEvenType
#check AsymmetricInformation.Screening.globalExpectedProfit
#eval AsymmetricInformation.Screening.expectedProfit contratTemoin profilRS .high
#eval AsymmetricInformation.Screening.expectedProfit contratTemoin profilRS .low
#eval AsymmetricInformation.Screening.globalExpectedProfit contratTemoin profilRS
-- Le profil canonique des exemples du lake : (p_H, p_L) = (25, 75).
breakEvenType est la condition RS fondamentale : le break-even se teste type par type — pas de cross-subsidy dans Rothschild-Stiglitz (la subvention croisée appartient à Wilson/Miyazaki-Wilson, section III). La prime 20 est simplement trop basse pour couvrir le sinistre, quel que soit le type.
Ce calcul est déjà un critère d’exclusion : un contrat qui perd sur les deux types ne peut appartenir à aucun menu d’équilibre, car le retirer économiserait de l’argent à son offreur — aucune raison de le garder. Les nombres évalués (−500 sur high, −5500 sur low) rendent ce rejet calculé, pas déclaré.
Le cream-skimming casse l’équilibre
L’équilibre de Nash entre assureurs, nashMenu, exige qu’aucun contrat hors-menu ne soit unilatéralement plus profitable. Le prédicat creamSkimProfitable intègre les trois témoins de la déviation : un contrat c' hors-menu globalement profitable, un contrat c du menu perdant sur high avec la borne symétrique ≤ 0 sur low. Le lemme directionnel cream_skim_breaks_nash consomme l’hypothèse complète par obtain et ferme par omega.
Le mécanisme mérite d’être nommé : le cream-skimming (écrémage) est le geste de l’entrant qui cible le type profitable (high, le bon risque ici), lui offre un contrat légèrement plus attractif, et laisse les pertes au menu incumbent. La déviation témoin c' = ⟨100, 100⟩ (coverage totale, prime totale) rapporte +10000 sur high alors que le menu de référence perd partout : aucun équilibre ne peut tenir face à elle.
#check AsymmetricInformation.Screening.nashMenu
#check AsymmetricInformation.Screening.creamSkimProfitable
#check AsymmetricInformation.Screening.cream_skim_breaks_nash
#check AsymmetricInformation.Screening.cream_skim_implies_some_negative_H_profit
-- La deviation hors-menu du module : c' = (100, 100).
def contratSkim : AsymmetricInformation.Screening.Contract := ⟨100, 100⟩
#eval AsymmetricInformation.Screening.globalExpectedProfit contratSkim profilRS
La déviation c' = (100, 100) rapporte (100·100 − 25·100) + (100·100 − 75·100) = 7500 + 2500 = 10000 > 0 alors que le contrat du menu c = (100, 20) perd sur les deux types (−500, −5500). cream_skim_breaks_nash transforme ces trois témoins en réfutation du Nash : sur cette région paramétrique, l’équilibre RS n’existe pas. C’est le résultat central de Rothschild-Stiglitz — non-existence conditionnelle, pas un théorème d’existence. L’échappatoire historique (Wilson 1977 : anticiper les retraits) est exactement la section III.
Cette non-existence n’est pas un échec de formalisation : c’est un résultat économique — le théorème de RS sur la région cream-skim. Mais il porte sur une hypothèse précise : l’assureur ne peut observer le type, et ne peut rien faire d’autre que proposer des contrats. La section suivante relâche exactement cette hypothèse : et si la partie informée pouvait envoyer un signal coûteux pour se révéler d’elle-même ?
II. Signaling — Spence 1973
Renversement du timing : c’est maintenant la partie informée qui bouge. Le candidat de type q choisit un signal s (une formation), paie signalCost q s, et l’employeur paie la productivité du type qu’il infère. Le single-crossing est encodé dans le coût : c_low(s) = 2s, c_high(s) = s — le bon type signale deux fois moins cher.
L’idée de Spence : un signal sans valeur productive — le diplôme dans le modèle original — peut quand même séparer les types si son coût dépend du type. Le lake encode cette dépendance dans signalCost : le type low paie 2s pour le niveau s, le type high ne paie que s. Le single-crossing qui en découle est le mécanisme profond : le même signal coûte deux fois plus cher au type mauvais, donc il existe des niveaux où seul le bon type trouve rentable de signaler.
signalCost .low 3 = 6 et signalCost .high 3 = 3 : à signal égal, le mauvais type paie le double. Toute la séparation de Spence tient dans cet écart — c’est lui qui rend l’imitation du bon type coûteuse au mauvais type spécifiquement.
Un séparateur est une structure Separator portant quatre contraintes explicites : icHigh (H ne préfère pas le signal de L), icLow (L ne veut pas imiter H), irHigh, irLow (participation), plus l’ordre sLow < sHigh. Le salaire est concurrentiel : w_q = y_q.
Économiquement : pour qu’un signal sépare, il ne suffit pas qu’il soit coûteux — il faut que l’écart de coût entre types excède l’écart de bénéfice à mentir. Ici l’écart de coût est exactement le facteur 2 (6 contre 3 au niveau 3), et c’est lui qui ouvrira l’intervalle séparateur [3, 6] de la section suivante : en dessous de 3, le signal ne coûte pas assez cher au type low (il imite) ; au-dessus de 6, il coûte trop cher au type high (il renonce à signaler).
Les bornes de l’intervalle séparateur
Les deux lemmes du lake ne vérifient pas des témoins : ils bornent l’intervalle de tous les séparateurs possibles. Avec c_H(s) = s et c_L(s) = 2s :
separator_icHigh_bound : IC_H se réarrange en sHigh ≤ (yHigh − yLow) + sLow ;
separator_icLow_bound : IC_L se réarrange en 2·sHigh ≥ (yHigh − yLow) + 2·sLow.
Sur l’instance (yLow, yHigh) = (4, 10) avec sLow = 0, l’intervalle est exactement [3, 6] (separator_interval_instance), et la borne inférieure est la minimalité de Riley : riley_sHigh_minimal.
Chaque borne a un visage concret. separator_icLow_bound dit : le signal doit coûter assez cher au type mauvais pour qu’il renonce à imiter (contrainte d’incitation du type low). separator_icHigh_bound dit : le signal ne doit pas coûter si cher que le type bon préfère se taire (contrainte du type high). L’intervalle [3, 6] est l’intersection des deux — l’espace des niveaux de signal qui séparent sans éteindre la révélation.
Lecture — l’égalité frontière et la minimalité de Riley
Le séparateur least-cost (sLow, sHigh) = (0, 3) satisfait IC_L par égalité exacte : 4 − 0 ≥ 10 − 2·3 = 4 — c’est la frontière, d’où la minimalité. Le lake en exhibe trois témoins décidés : (0, 3) (Riley), (0, 6) (extrémité haute), (1, 7) (un deuxième séparateur) — et un contre-témoin : sHigh = 2 viole IC_L (4 ≥ 6 est faux), réfuté via la minimalité, pas par échantillonnage. Pas de claim d’unicité générale : sur la même instance, plusieurs séparateurs coexistent.
Le signaling résout la révélation, mais à un prix : le signal est un coût social pur (le diplôme n’élève pas la productivité chez Spence — il ne fait que séparer). Riley identifie le séparateur efficient : le moins cher de ceux qui séparent encore. Mais lui aussi vit dans un monde concurrentiel — et la question de la stabilité face aux entrants, déjà fatale au screening, revient : c’est l’objet de la section suivante.
III. Équilibres anticipatoires — Wilson 1977, Miyazaki 1977, Spence 1978
La réponse à la non-existence RS : un assureur qui anticipe que retirer un contrat laissera le champ au cream-skimmer. Le lake définit :
anticipatoryMenu : la version statique de Wilson — aucun retrait + entrée hors-menu ne améliore le profit global ;
crossSubsidyTenable : un contrat du menu subventionne un type par l’autre (profit strictement positif sur un type, strictement négatif sur l’autre) — la définition locale, qui n’appartient PAS à RS ;
MenuChoice / EntryWithdrawal / anticipatoryAgainst : une déviation concrète (entrée + retrait) et son invariance de profit agrégé.
L’intuition de Wilson : le screening échoue parce que les contrats sont jugés sur leur profit immédiat, comme si les clients restants après une déviation gardaient la même valeur. Un menu anticipatoire est jugé sur les profits après retrait des contrats devenus non rentables — l’entrant potentiel doit anticiper que son arrivée fera fuir les bonnes risques et ne laissera que les mauvaises. Le cross-subsidy est l’instrument : faire payer le type profitable un peu plus pour garder le type non rentable au menu, précisément parce que sa présence stabilise l’ensemble.
Contre-exemple chiffré du lake : sur le profil (25, 75), le menu [(100, 20), (40, 10)] ne porte aucun profit strictement positif (−500, −5500, 0, −2000) — crossSubsidyTenable y est False (démontré par example : ¬ crossSubsidyTenable ...). À l’inverse, l’entrant (100, 50) de l’état N rapporte 50·100 − 25·100 = +2500 sur high : c’est lui qui fait tomber l’invariance (−2500 → +500). Le cross-subsidy n’est ni toujours tenable ni toujours absent — la formalisation borne honnêtement les deux côtés, sans théorème d’unicité MWS général.
Reste à refermer la boucle. Tous ces modèles — lemons, menus, signaux, anticipation — sont en réalité des jeux bayésiens : des joueurs, des types privés, des croyances (priors) et des stratégies conditionnelles aux types. Le dernier module rend cette identité littérale en important le formalisme du lake amont.
IV. Le pont bayésien — du marché des lemons au BNE
Le dernier module referme la boucle avec le lake amont lean_game_defs_ext (dépendance [[require]] du lakefile.toml) : le marché des lemons devient un BayesGame2 concret — l’acheteur (joueur 1, un seul type) annonce un prix, le vendeur (joueur 2, deux types) accepte ou refuse. Le module consomme réellement l’API amont (Strategy1, Strategy2, isBNE), et le profil (prix bas, accepter toujours) est certifié équilibre bayésien de Nash par decide.
bridgeStrategy_isBNE n’est pas une importation décorative : l’instance close (marché canonique ⟨0, 5, 0, 4⟩, prior 50 %) est décidée par le noyau via isBNE ... := by decide, exerçant la décidabilité de l’API amont telle qu’exposée dans Bayesian.BNE. Le chemin Lemons → BayesGame2 → isBNE est la preuve formelle que le certificat d’Akerlof du 17c vit dans le même monde que la théorie des jeux bayésiens du GameTheory-11b.
Concrètement, bridgeStrategy_isBNE oblige le noyau à calculer l’espérance de chaque joueur sous les croyances du prior et à vérifier qu’aucune déviation unilatérale n’améliore — la définition même du BNE, exécutée terme à terme sur l’instance close plutôt qu’assertée.
Exercice 1 — screening : votre propre profil
On considère le profil (p_H, p_L) = (30, 80) et le contrat ⟨120, 40⟩.
Objectif : 1. Définir profilExo1 et contratExo1, puis évaluer le profit attendu sur high et sur low. 2. Vérifier par decide que ce contrat perd sur les deux types. 3. En une phrase : ce contrat seul peut-il appartenir à un menu Nash ? (Indice : direction de creamSkimProfitable.)
Indices : RiskProfile exige la preuve 30 < 80 (by omega) ; le profit sur un type s’obtient par #eval AsymmetricInformation.Screening.expectedProfit contratExo1 profilExo1 .high.
-- TODO etudiant : definir le profil (30, 80)
-- def profilExo1 : AsymmetricInformation.Screening.RiskProfile := ⟨30, 80, by omega⟩
-- TODO etudiant : definir le contrat (couverture 120, prime 40)
-- def contratExo1 : AsymmetricInformation.Screening.Contract := ⟨120, 40⟩
-- TODO etudiant : evaluer le profit sur high puis sur low
-- Indice : #eval AsymmetricInformation.Screening.expectedProfit contratExo1 profilExo1 .high
-- TODO etudiant : montrer par decide que le contrat perd sur les deux types
-- Indice : example : AsymmetricInformation.Screening.expectedProfit contratExo1 profilExo1 .high < 0 := by decide
-- ancre d'execution (cellule valide meme non completee) :
#check AsymmetricInformation.Screening.expectedProfit
-- TODO etudiant : definir le profil (30, 80)
-- def profilExo1 : AsymmetricInformation.Screening.RiskProfile := ⟨30, 80, by omega⟩
-- TODO etudiant : definir le contrat (couverture 120, prime 40)
Raw input{"cmd": "-- TODO etudiant : definir le profil (30, 80)\n-- def profilExo1 : AsymmetricInformation.Screening.RiskProfile := \u27e830, 80, by omega\u27e9\n\n-- TODO etudiant : definir le contrat (couverture 120, prime 40)\n-- def contratExo1 : AsymmetricInformation.Screening.Contract := \u27e8120, 40\u27e9\n\n-- TODO etudiant : evaluer le profit sur high puis sur low\n-- Indice : #eval AsymmetricInformation.Screening.expectedProfit contratExo1 profilExo1 .high\n\n-- TODO etudiant : montrer par decide que le contrat perd sur les deux types\n-- Indice : example : AsymmetricInformation.Screening.expectedProfit contratExo1 profilExo1 .high < 0 := by decide\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check AsymmetricInformation.Screening.expectedProfit\n", "env": 7}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data":
"AsymmetricInformation.Screening.expectedProfit (c : AsymmetricInformation.Screening.Contract)\n (r : AsymmetricInformation.Screening.RiskProfile) (q : AsymmetricInformation.Screening.RiskType) : Int"}],
"env": 8}
Exercice 2 — signaling : l’intervalle ne dépend que de l’écart
On remplace la productivité (4, 10) par (3, 9) — le même écartyHigh − yLow = 6.
Objectif : 1. Appliquer les deux bornes separator_icHigh_bound / separator_icLow_bound pour prédire l’intervalle séparateur avec sLow = 0. 2. Construire le séparateur de Riley (0, 3) sur cette instance (les quatre contraintes se vérifient par decide). 3. Expliquer pourquoi l’intervalle est identique à celui de (4, 10).
Indices : Productivity exige 3 < 9 ; la structure Separator se construit avec ⟨0, 3, by omega, 0, 0, by decide, by decide, by decide, by decide⟩ sur l’instance — c’est le témoin (0, 3) du module, transposé.
-- TODO etudiant : definir la productivite (3, 9)
-- def prodExo2 : AsymmetricInformation.Signaling.Productivity := ⟨3, 9, by omega⟩
-- TODO etudiant : verifier les deux bornes sur sLow = 0
-- Indice : icLow donne 2 * sHigh >= 6 et icHigh donne sHigh <= 6 + 0
-- TODO etudiant : construire le separateur de Riley (0, 3) sur (3, 9)
-- Indice : example : ∃ sep : AsymmetricInformation.Signaling.Separator ⟨3, 9, by omega⟩,
-- sep.sLow = 0 ∧ sep.sHigh = 3 ∧ sep.reserveLow ≤ 0 ∧ sep.reserveHigh ≤ 0 := by
-- refine ⟨⟨0, 3, by omega, 0, 0, by decide, by decide, by decide, by decide⟩, rfl, rfl, by decide, by decide⟩
-- ancre d'execution (cellule valide meme non completee) :
#check AsymmetricInformation.Signaling.Separator
-- TODO etudiant : definir la productivite (3, 9)
-- def prodExo2 : AsymmetricInformation.Signaling.Productivity := ⟨3, 9, by omega⟩
-- TODO etudiant : verifier les deux bornes sur sLow = 0
-- Indice : icLow donne 2 * sHigh >= 6 et icHigh donne sHigh <= 6 + 0
-- TODO etudiant : construire le separateur de Riley (0, 3) sur (3, 9)
-- Indice : example : ∃ sep : AsymmetricInformation.Signaling.Separator ⟨3, 9, by omega⟩,
Raw input{"cmd": "-- TODO etudiant : definir la productivite (3, 9)\n-- def prodExo2 : AsymmetricInformation.Signaling.Productivity := \u27e83, 9, by omega\u27e9\n\n-- TODO etudiant : verifier les deux bornes sur sLow = 0\n-- Indice : icLow donne 2 * sHigh >= 6 et icHigh donne sHigh <= 6 + 0\n\n-- TODO etudiant : construire le separateur de Riley (0, 3) sur (3, 9)\n-- Indice : example : \u2203 sep : AsymmetricInformation.Signaling.Separator \u27e83, 9, by omega\u27e9,\n-- sep.sLow = 0 \u2227 sep.sHigh = 3 \u2227 sep.reserveLow \u2264 0 \u2227 sep.reserveHigh \u2264 0 := by\n-- refine \u27e8\u27e80, 3, by omega, 0, 0, by decide, by decide, by decide, by decide\u27e9, rfl, rfl, by decide, by decide\u27e9\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check AsymmetricInformation.Signaling.Separator\n", "env": 8}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data":
"AsymmetricInformation.Signaling.Separator (p : AsymmetricInformation.Signaling.Productivity) : Type"}],
"env": 9}
Exercice 3 — Miyazaki-Wilson : un cross-subsidy tenable
Sur le profil (25, 75) (le profilRS de la section I), on considère le menu [(100, 50), (40, 10)].
Objectif : 1. Évaluer le profit de ⟨100, 50⟩ sur high et celui de ⟨40, 10⟩ sur low. 2. Constater que l’un est strictement positif et l’autre strictement négatif : le prédicat crossSubsidyTenable a de quoi tenir sur ce menu. 3. Comparer avec le contre-exemple du lake ([(100, 20), (40, 10)], aucun profit positif) et conclure en une phrase : qu’est-ce que ça change pour l’équilibre anticipatoire ?
Indices : ⟨100, 50⟩ sur high : 50·100 − 25·100 ; ⟨40, 10⟩ sur low : 10·100 − 75·40.
-- TODO etudiant : evaluer le profit de (100, 50) sur high
-- Indice : #eval AsymmetricInformation.Screening.expectedProfit ⟨100, 50⟩ profilRS .high
-- TODO etudiant : evaluer le profit de (40, 10) sur low
-- Indice : #eval AsymmetricInformation.Screening.expectedProfit ⟨40, 10⟩ profilRS .low
-- TODO etudiant : repondre a la question 3 dans cette cellule en commentaire, puis
-- comparer avec le contre-exemple [(100, 20), (40, 10)] du module (tous profits <= 0)
-- ancre d'execution (cellule valide meme non completee) :
#check AsymmetricInformation.MiyazakiWilson.crossSubsidyTenable
-- TODO etudiant : evaluer le profit de (100, 50) sur high
Raw input{"cmd": "-- TODO etudiant : evaluer le profit de (100, 50) sur high\n-- Indice : #eval AsymmetricInformation.Screening.expectedProfit \u27e8100, 50\u27e9 profilRS .high\n\n-- TODO etudiant : evaluer le profit de (40, 10) sur low\n-- Indice : #eval AsymmetricInformation.Screening.expectedProfit \u27e840, 10\u27e9 profilRS .low\n\n-- TODO etudiant : repondre a la question 3 dans cette cellule en commentaire, puis\n-- comparer avec le contre-exemple [(100, 20), (40, 10)] du module (tous profits <= 0)\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check AsymmetricInformation.MiyazakiWilson.crossSubsidyTenable\n", "env": 9}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 6},
"data":
"AsymmetricInformation.MiyazakiWilson.crossSubsidyTenable (menu : AsymmetricInformation.Screening.Menu)\n (r : AsymmetricInformation.Screening.RiskProfile) : Prop"}],
"env": 10}
Conclusion
Les quatre modules exécutés couvrent le triptyque classique de l’information asymétrique et sa boucle de fermeture :
Screening : le menu RS n’a pas d’équilibre Nash sur la région cream-skim (cream_skim_breaks_nash) — non-existence conditionnelle, chiffrée sur un témoin décidé ;
Signaling : l’intervalle séparateur est déterminé par les bornes IC ([3, 6] sur l’instance canonique), Riley en est l’extrémité inférieure, et l’unicité est honnêtement absente (trois séparateurs décidés coexistent) ;
MiyazakiWilson : la trame 0 / 1 / plusieurs remplace un ∃! introuvable — l’invariance de Wilson tient (−2000 → −6000) ou tombe (−2500 → +500) selon le menu, et le cross-subsidy est la variable qui sépare les deux ;
BayesianLink : le tout est raccordé à la théorie des jeux bayésiens du lake amont (isBNE par decide).
Pour aller plus loin : le 17b (narration Python du même thème), le 17c (certificat d’Akerlof exécuté), le README du lake, et le GameTheory-11b pour l’API BayesGame2 amont.
Relus ensemble, les trois modules posent une seule question trois fois : qui paie la révélation de l’information privée ? Chez Rothschild-Stiglitz, personne ne la paie — et l’équilibre meurt. Chez Spence-Riley, la partie informée la paie (le signal) — l’équilibre existe, au prix d’un coût social pur. Chez Wilson-Miyazaki, c’est le menu lui-même qui la paie (subvention croisée) — et l’équilibre survit, conditionnellement au cross-subsidy. Le cadre formel ne choisit pas entre ces réponses : il borne honnêtement ce que chacune peut revendiquer, et c’est précisément ce qu’un #check exécuté rend visible.