Le marché des lemons : le certificat formel exécuté
Série GameTheory — 17c. Le notebook 17b a modélisé l’information asymétrique (types privés, antisélection, signal, screening) en Python. Ce complément fait le chemin inverse : il exécute en direct le certificat formel du lake asymmetric_information_lean — la formalisation Lean 4 (sans Mathlib) du modèle d’Akerlof 1970 — et met la mécanique du marché en scène dans le langage du certificat lui-même.
Positionnement. 17b simule l’économie en Python ; 17c exécute la preuve en Lean. Les deux notebooks sont indépendants — aucun ne requiert l’autre.
Le certificat et sa mécanique
Le lake asymmetric_information_lean (dossier asymmetric_information_lean/ de cette série) formalise les modèles fondateurs de l’information asymétrique : Akerlof 1970 (lemons), Spence 1973 (signaling), Rothschild-Stiglitz 1976 (screening), Wilson-Miyazaki-Spence (règle anticipative) — 51 déclarations, zéro sorry, sous gates CI continues.
Ce notebook importe le module Lemons du lake : chaque #check, #eval et example ... := by decide ci-dessous tourne contre le code compilé du lake, pas contre une copie recopiée dans le notebook. Le kernel Lean se branche sur la racine du lake et récupère son LEAN_PATH.
import AsymmetricInformation.Lemons
open AsymmetricInformation.Lemons
#check Quality
#check TwoQualityMarket
#check Prior
Lecture — deux qualités, des entiers, un prior au centième
Le marché à deux qualités porte quatre paramètres entiers :
cLow, cHigh : coûts d’opportunité des vendeurs (prix de réservation) — en dessous de son coût, un vendeur retire sa voiture du marché ;
vLow, vHigh : valeurs pour l’acheteur ;
avec deux contraintes de cohérence portées par la structure : vLow < vHigh (hValue) et cLow < cHigh (hCost). Le prior π — probabilité a priori de la haute qualité — est encodé en numérateur sur 100 (piNum), ce qui garde toute l’arithmétique en entiers exacts.
offered m P est l’ensemble S(P) des qualités encore proposées au prix P : un vendeur ne reste que si le prix couvre son coût d’opportunité.
à P = 0 : seul low reste (son coût est nul) ;
à P = 3 : toujours low seul — la haute qualité exige 5 ;
à P = 5 : les deux restent.
C’est LE mécanisme de l’antisélection : le prix filtre la qualité. L’acheteur, lui, ne voit jamais l’étiquette — seulement la moyenne de ce qui reste offert.
expectedValue conditionne la valeur espérée à ce qui est réellement offert :
à P = 0 ou P = 3 : seule la qualité basse reste, l’espérance tombe à vLow = 0 ;
à P = 5 : les deux restent, l’espérance mixe selon le prior — (50·4 + 50·0)/100 = 2.
Et là est le nœud d’Akerlof : le prix qui retient la haute qualité (≥ 5) dépasse la valeur espérée du panier (2). L’acheteur rationnel refuse de payer 5 pour un lot qui n’en vaut en espérance que 2 — la haute qualité n’est pas chassée par un choc externe, mais par la seule rationalité de l’anticipation.
Trois régimes, un point fixe
Le module caractérise le marché par trois régions exclusives :
poolingTenable : c_H·100 ≤ π·v_H + (100−π)·v_L
(un prix unique garde les deux types)
lemonsOnlyPossible : ∃ P ∈ [c_L, c_H), P ≤ E[v | S(P)] ∧ S(P) = [low]
(un marché dégénéré au seul L)
noTrade : aucun P ∈ [c_L, c_H) n'est accepté
(le marché meurt)
La condition acheteur buyerAccepts est le point fixe : le prix doit couvrir la valeur espérée du lot que ce prix même constitue.
#check poolingTenable
#check lemonsOnlyPossible
#check noTrade
-- Exemple (a) du module, re-prouvé ici en direct : lemons-only possible sur
-- le marché canonique avec P = 0 (S(0) = [low], E = 0, l'acheteur accepte 0 ≤ 0).
example : lemonsOnlyPossible marche prior50 := by
refine ⟨0, by decide, by decide, ?_, by decide⟩
simp [marche, expectedValue, offered]
-- Et le pooling y est mort (exemple (d) du module).
example : ¬ poolingTenable marche prior50 := by decide
-- Exemple (a) du module, re-prouvé ici en direct : lemons-only possible sur
-- le marché canonique avec P = 0 (S(0) = [low], E = 0, l'acheteur accepte 0 ≤ 0).
example:lemonsOnlyPossiblemarcheprior50:=by
refine⟨0,bydecide,bydecide,?_,bydecide⟩
simp[marche,expectedValue,offered]
-- Et le pooling y est mort (exemple (d) du module).
example:¬poolingTenablemarcheprior50:=bydecide
--% env 3
Raw input{"cmd": "#check poolingTenable\n#check lemonsOnlyPossible\n#check noTrade\n\n-- Exemple (a) du module, re-prouv\u00e9 ici en direct : lemons-only possible sur\n-- le march\u00e9 canonique avec P = 0 (S(0) = [low], E = 0, l'acheteur accepte 0 \u2264 0).\nexample : lemonsOnlyPossible marche prior50 := by\n refine \u27e80, by decide, by decide, ?_, by decide\u27e9\n simp [marche, expectedValue, offered]\n\n-- Et le pooling y est mort (exemple (d) du module).\nexample : \u00ac poolingTenable marche prior50 := by decide", "env": 2}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 1, "column": 0},
"endPos": {"line": 1, "column": 6},
"data":
"AsymmetricInformation.Lemons.poolingTenable (m : TwoQualityMarket) (π : Prior) : Prop"},
{"severity": "info",
"pos": {"line": 2, "column": 0},
"endPos": {"line": 2, "column": 6},
"data":
"AsymmetricInformation.Lemons.lemonsOnlyPossible (m : TwoQualityMarket) (π : Prior) : Prop"},
{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"AsymmetricInformation.Lemons.noTrade (m : TwoQualityMarket) (π : Prior) : Prop"}],
"env": 3}
Lecture — trois prédicats d’une même signature
La sortie aligne les trois régimes du marché comme trois prédicats de même signature : poolingTenable, lemonsOnlyPossible, noTrade prennent tous un marché et un prior et rendent une Prop. Le lexique est complet dès le départ : les trois états que la suite distinguera (pooling tenable, marché réduit aux lemons, interdiction d’échanger) sont des propositions, pas des valeurs — c’est le notebook qui prouvera chaque instance. Les deux example qui suivent montrent le registre « preuve » sur le marché canonique : l’exemple (a) du module est re-prouvé en direct (témoin P = 0, S(0) = [low], E = 0) et l’exemple (d) — pooling mort à pi = 50 — est clos par decide. Les cellules suivantes citeront encore (e), (f), (g) : le notebook re-prouve les exemples du module un par un au lieu de les admettre.
Lecture — le marché ne meurt pas, il dégénère
Sur le marché canonique, le pooling est refusé par decide (5·100 = 500 > 50·4 + 50·0 = 200) mais le régime lemons-only est prouvé atteignable : l’exemple exhibe le prix P = 0, l’offre [low], l’acceptation 0 ≤ 0. C’est la lecture fine d’Akerlof : la mauvaise qualité ne chasse pas toujours tout le monde — elle chasse la bonne, et le marché survit à prix nul. Le régime noTrade est la version extrême (exercice 2).
Le seuil de pooling : une caractérisation exacte
La condition brute cHigh·100 ≤ π·vHigh + (100−π)·vLow se réarrange linéairement en un produit croisé :
Sous vHigh > vLow, le membre de droite croît avec π : le seuil π_min = 100·(c_H − v_L)/(v_H − v_L) est un plancher. L’intérêt n’est pas cosmétique : l’équivalence couvre tout couple (marché, prior) en arithmétique entière close — pas d’approximation numérique, pas de cas limite oublié.
#print axioms répond [propext, Quot.sound] : les deux seuls axiomes standards de la logique de Lean (extensionnalité propositionnelle et quotients). Aucun sorryAx — la preuve est close de bout en bout.
C’est toute la différence entre « ça marche sur mes exemples » et « ça marche pour tous les marchés à deux qualités » : la simulation balaye quelques points, le théorème couvre le continuum.
-- Marché-seuil : (0, 30, 0, 40). Le produit croisé prédit π_min = 100·30/40 = 75.
def marcheSeuil : TwoQualityMarket := ⟨0, 30, 0, 40, by omega, by omega⟩
#eval poolingThresholdNum marcheSeuil
-- pi = 74 : sous le seuil, pooling NON tenable (exemple (e) du module).
example : ¬ poolingTenable marcheSeuil ⟨74, by decide⟩ := by decide
-- pi = 75 : exactement au seuil, pooling tenable (exemple (f) du module).
example : poolingTenable marcheSeuil ⟨75, by decide⟩ := by decide
-- Marché-seuil : (0, 30, 0, 40). Le produit croisé prédit π_min = 100·30/40 = 75.
Raw input{"cmd": "-- March\u00e9-seuil : (0, 30, 0, 40). Le produit crois\u00e9 pr\u00e9dit \u03c0_min = 100\u00b730/40 = 75.\ndef marcheSeuil : TwoQualityMarket := \u27e80, 30, 0, 40, by omega, by omega\u27e9\n\n#eval poolingThresholdNum marcheSeuil\n\n-- pi = 74 : sous le seuil, pooling NON tenable (exemple (e) du module).\nexample : \u00ac poolingTenable marcheSeuil \u27e874, by decide\u27e9 := by decide\n\n-- pi = 75 : exactement au seuil, pooling tenable (exemple (f) du module).\nexample : poolingTenable marcheSeuil \u27e875, by decide\u27e9 := by decide", "env": 4}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 5},
"data": "3000"}],
"env": 5}
Ce que la sortie ne dit pas : la preuve par le silence
Dans la sortie de la cellule, le contraste est instructif : le #eval poolingThresholdNum marcheSeuil imprime ─────▶ 3000, et les deux example qui suivent — ¬ poolingTenable ... ⟨74⟩ puis poolingTenable ... ⟨75⟩ — n’impriment rien du tout. Ce silence est le succès : en Lean, une preuve publiée ne produit aucun message ; seul son échec afficherait une erreur. Le fichier brut de la sortie le confirme — un seul message data: "3000", aucun pour les deux exemples. La falaise que le balayage mesurera (74 casse, 75 tient) est ici décidée par le kernel à chaque exécution : contrairement à une table pré-calculée, les deux lignes ne peuvent pas vieillir séparément.
Lecture — la falaise est raide, et sa position est prouvée
poolingThresholdNum renvoie 3000 = 100·(c_H − v_L) ; le seuil en prior est 3000/40 = 75. Un point de prior de moins (74) et le pooling casse ; un point de plus (75) et il tient. La frontière n’est pas mesurée, elle est décidée — decide ré-exécute la preuve sur chaque valeur.
À π = 75 exactement, le prix pooling vaut (75·40 + 25·0)/100 = 30 = c_H : la haute qualité se vend exactement à son coût de réservation. Le seuil est l’endroit où le pooling devient tout juste possible.
#check poolingTenable_mono
-- Exemple (g) du module : pi = 100 l'est aussi — par la borne inférieure,
-- sans re-arbitrer la condition a la main.
example : poolingTenable marcheSeuil ⟨100, by decide⟩ :=
poolingTenable_mono _ ⟨75, by decide⟩ ⟨100, by decide⟩ (by decide) (by decide)
Raw input{"cmd": "#check poolingTenable_mono\n\n-- Exemple (g) du module : pi = 100 l'est aussi \u2014 par la borne inf\u00e9rieure,\n-- sans re-arbitrer la condition a la main.\nexample : poolingTenable marcheSeuil \u27e8100, by decide\u27e9 :=\n poolingTenable_mono _ \u27e875, by decide\u27e9 \u27e8100, by decide\u27e9 (by decide) (by decide)", "env": 5}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 1, "column": 0},
"endPos": {"line": 1, "column": 6},
"data":
"AsymmetricInformation.Lemons.poolingTenable_mono (m : TwoQualityMarket) (π π' : Prior) (hπ : π.piNum ≤ π'.piNum)\n (h : poolingTenable m π) : poolingTenable m π'"}],
"env": 6}
Lecture — un plancher, pas une fenêtre
poolingTenable_mono dit : si le pooling tient à π, il tient à tout prior plus élevé. Économiquement, une externalité positive — plus la part de haute qualité est grande, plus l’acheteur peut payer, plus la haute qualité reste en offre. L’antisélection est exactement ce mécanisme lu à l’envers : c’est pourquoi elle s’emballe (la spirale ci-dessous la rejoue).
La falaise calculée : balayage du prior
On classifie chaque prior de 60 % à 100 % sur le marché-seuil — avec les définitions du lake (poolingTenable, offered), pas une réimplémentation Python. Pour chaque prior : le pooling tient-il ? Quel prix espéré couvre le panier ? Que reste-t-il en offre à ce prix ?
/-- Classification d'un prior sur un marche, avec les definitions du lake :
pooling tenable ? prix pooling espere ? ensemble offert a ce prix ? -/
def demoRegime (m : TwoQualityMarket) (pi : Nat) : String :=
let pi' := min pi 100
let π : Prior := ⟨pi', by omega⟩
let prixPooling := ((pi' : Int) * m.vHigh + (100 - (pi' : Int)) * m.vLow) / 100
let pooling := decide (poolingTenable m π)
let offre := offered m prixPooling
s!"pi = {pi'} % : pooling = {pooling}, prix espere = {prixPooling}, S(prix) = {repr offre}"
#eval (List.range 9).map (fun i => demoRegime marcheSeuil (60 + 5 * i))
/-- Classification d'un prior sur un marche, avec les definitions du lake :
Raw input{"cmd": "/-- Classification d'un prior sur un marche, avec les definitions du lake :\n pooling tenable ? prix pooling espere ? ensemble offert a ce prix ? -/\ndef demoRegime (m : TwoQualityMarket) (pi : Nat) : String :=\n let pi' := min pi 100\n let \u03c0 : Prior := \u27e8pi', by omega\u27e9\n let prixPooling := ((pi' : Int) * m.vHigh + (100 - (pi' : Int)) * m.vLow) / 100\n let pooling := decide (poolingTenable m \u03c0)\n let offre := offered m prixPooling\n s!\"pi = {pi'} % : pooling = {pooling}, prix espere = {prixPooling}, S(prix) = {repr offre}\"\n\n#eval (List.range 9).map (fun i => demoRegime marcheSeuil (60 + 5 * i))", "env": 6}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 5},
"data":
"[\"pi = 60 % : pooling = false, prix espere = 24, S(prix) = [AsymmetricInformation.Lemons.Quality.low]\",\n \"pi = 65 % : pooling = false, prix espere = 26, S(prix) = [AsymmetricInformation.Lemons.Quality.low]\",\n \"pi = 70 % : pooling = false, prix espere = 28, S(prix) = [AsymmetricInformation.Lemons.Quality.low]\",\n \"pi = 75 % : pooling = true, prix espere = 30, S(prix) = [AsymmetricInformation.Lemons.Quality.low, AsymmetricInformation.Lemons.Quality.high]\",\n \"pi = 80 % : pooling = true, prix espere = 32, S(prix) = [AsymmetricInformation.Lemons.Quality.low, AsymmetricInformation.Lemons.Quality.high]\",\n \"pi = 85 % : pooling = true, prix espere = 34, S(prix) = [AsymmetricInformation.Lemons.Quality.low, AsymmetricInformation.Lemons.Quality.high]\",\n \"pi = 90 % : pooling = true, prix espere = 36, S(prix) = [AsymmetricInformation.Lemons.Quality.low, AsymmetricInformation.Lemons.Quality.high]\",\n \"pi = 95 % : pooling = true, prix espere = 38, S(prix) = [AsymmetricInformation.Lemons.Quality.low, AsymmetricInformation.Lemons.Quality.high]\",\n \"pi = 100 % : pooling = true, prix espere = 40, S(prix) = [AsymmetricInformation.Lemons.Quality.low, AsymmetricInformation.Lemons.Quality.high]\"]"}],
"env": 7}
Lecture — ce que montre le balayage
De π = 60 % à 70 % : pooling = false, prix espéré < 30, offre [low] — l’acheteur ne peut pas atteindre c_H = 30. À 75 % : bascule — pooling = true, prix = 30 = c_H, offre [low, high]. Au-dessus : le prix espéré dépasse le coût de réservation et l’offre reste double.
Le théorème de monotonie ajoute ce que le balayage ne peut pas montrer : que la région tenable est un intervalle sans trou[75 ; 100] — le balayage échantillonne, poolingTenable_mono garantit la structure.
La spirale d’Akerlof : le point fixe en mouvement
Le certificat est statique : il dit quels régimes existent. La dynamique montre comment le marché y glisse. Mécanisme : l’acheteur affiche son prix rationnel P = E[v | S(P)], l’offre se met à jour, le prix suit — jusqu’au point fixe (ou l’extinction).
-- Prix de depart optimiste : l'acheteur paie comme si les deux types restaient.
def demoPrixInitial (m : TwoQualityMarket) (pi : Nat) : Int :=
((min pi 100 : Int) * m.vHigh + (100 - (min pi 100 : Int)) * m.vLow) / 100
/-- Trajectoire (prix affiche, valeur esperee) jusqu'au point fixe, max 8 étapes.
Chaque étape : l'offre se met à jour au prix courant, puis le prix suit
l'espérance du lot restant. -/
def demoSpiral (m : TwoQualityMarket) (π : Prior) (P₀ : Int) : List (Int × Int) :=
let rec step (acc : List (Int × Int)) (P : Int) : Nat → List (Int × Int)
| 0 => acc.reverse
| fuel + 1 =>
let e := expectedValue m π P
if e = P then ((P, e) :: acc).reverse
else step ((P, e) :: acc) e fuel
step [] P₀ 8
-- Marché canonique (0, 5, 0, 4), pi = 50 % : le prix s'effondre de 2 à 0.
#eval demoSpiral marche prior50 (demoPrixInitial marche 50)
-- Marché tenable (0, 2, 0, 4), pi = 50 % : le prix pooling tient d'emblée.
def marcheTenable : TwoQualityMarket := ⟨0, 2, 0, 4, by omega, by omega⟩
#eval demoSpiral marcheTenable prior50 (demoPrixInitial marcheTenable 50)
-- Marché mort (3, 5, 0, 4), pi = 50 % : plus personne n'offre, prix → 0.
def marcheMort : TwoQualityMarket := ⟨3, 5, 0, 4, by omega, by omega⟩
#eval demoSpiral marcheMort prior50 (demoPrixInitial marcheMort 50)
-- Prix de depart optimiste : l'acheteur paie comme si les deux types restaient.
Raw input{"cmd": "-- Prix de depart optimiste : l'acheteur paie comme si les deux types restaient.\ndef demoPrixInitial (m : TwoQualityMarket) (pi : Nat) : Int :=\n ((min pi 100 : Int) * m.vHigh + (100 - (min pi 100 : Int)) * m.vLow) / 100\n\n/-- Trajectoire (prix affiche, valeur esperee) jusqu'au point fixe, max 8 \u00e9tapes.\n Chaque \u00e9tape : l'offre se met \u00e0 jour au prix courant, puis le prix suit\n l'esp\u00e9rance du lot restant. -/\ndef demoSpiral (m : TwoQualityMarket) (\u03c0 : Prior) (P\u2080 : Int) : List (Int \u00d7 Int) :=\n let rec step (acc : List (Int \u00d7 Int)) (P : Int) : Nat \u2192 List (Int \u00d7 Int)\n | 0 => acc.reverse\n | fuel + 1 =>\n let e := expectedValue m \u03c0 P\n if e = P then ((P, e) :: acc).reverse\n else step ((P, e) :: acc) e fuel\n step [] P\u2080 8\n\n-- March\u00e9 canonique (0, 5, 0, 4), pi = 50 % : le prix s'effondre de 2 \u00e0 0.\n#eval demoSpiral marche prior50 (demoPrixInitial marche 50)\n\n-- March\u00e9 tenable (0, 2, 0, 4), pi = 50 % : le prix pooling tient d'embl\u00e9e.\ndef marcheTenable : TwoQualityMarket := \u27e80, 2, 0, 4, by omega, by omega\u27e9\n#eval demoSpiral marcheTenable prior50 (demoPrixInitial marcheTenable 50)\n\n-- March\u00e9 mort (3, 5, 0, 4), pi = 50 % : plus personne n'offre, prix \u2192 0.\ndef marcheMort : TwoQualityMarket := \u27e83, 5, 0, 4, by omega, by omega\u27e9\n#eval demoSpiral marcheMort prior50 (demoPrixInitial marcheMort 50)", "env": 7}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 18, "column": 0},
"endPos": {"line": 18, "column": 5},
"data": "[(2, 0), (0, 0)]"},
{"severity": "info",
"pos": {"line": 22, "column": 0},
"endPos": {"line": 22, "column": 5},
"data": "[(2, 2)]"},
{"severity": "info",
"pos": {"line": 26, "column": 0},
"endPos": {"line": 26, "column": 5},
"data": "[(2, 0), (0, 0)]"}],
"env": 8}
Anatomie de la spirale : trois mécanismes, zéro surprise
demoSpiral montre mieux que sa table ce que le certificat délimite. Trois détails de la cellule sont à lire. (1) Le point fixe est un test d’égalité — if e = P arrête la boucle quand le prix n’évolue plus : la spirale n’a pas besoin de savoir pourquoi elle s’arrête, seule la coïncidence des deux nombres l’intéresse. (2) Le carburant — fuel plafonne à 8 étapes : la simulation est bornée, le théorème ne l’est pas, et c’est le partage de travail honnête annoncé par la section précédente. (3) La reconstruction — acc.reverse remet la liste dans l’ordre chronologique après accumulation à l’envers. Sur les trois marchés, le prix initial est le même — P₀ = 2, l’anticipation où l’acheteur paie comme si les deux types restaient — et les spirales divergent ensuite : [(2, 2)] pour le marché tenable, [(2, 0), (0, 0)] pour les deux autres. La même donnée de départ, trois destins : c’est la copie visible de ce que poolingTenable_iff_cross prévoyait à l’avance.
Lecture — trois trajectoires, trois régimes
Marché
Trajectoire
Régime atteint
canonique (0, 5, 0, 4)
2 → 0
lemons-only : H exclu, L échangé au prix nul
tenable (0, 2, 0, 4)
2 (immédiat)
pooling : les deux types au prix 2
mort (3, 5, 0, 4)
2 → 0 (offre vide)
no-trade : plus personne n’offre
Et le lien au certificat : poolingTenable_iff_cross prédit à l’avance quelle trajectoire se produira (tenable ⟺ le point fixe pooling existe) — la spirale ne fait que la rejouer en dynamique.
Ce que le certificat ne dit pas : la trajectoire (combien d’étapes, dans quel ordre). C’est le partage de travail honnête entre preuve et simulation : le théorème délimite les états possibles, la simulation montre le chemin.
Exercice 1 — le seuil hors d’atteinte
On considère le marché \((c_L, c_H, v_L, v_H) = (1, 12, 2, 10)\).
Objectif : 1. Calculer le numérateur du seuil poolingThresholdNum et le seuil en prior qu’il implique. 2. Vérifier par decide que le pooling échoue même à π = 100 %. 3. Expliquer en une phrase pourquoi aucun prior ne peut sauver ce marché.
Indices : - poolingThresholdNum vaut 100·(c_H − v_L) ; le membre de droite du produit croisé vaut au maximum 100·(v_H − v_L). - Comparez c_H et v_H : que se passe-t-il quand le coût de réservation de la haute qualité dépasse sa valeur pour l’acheteur ?
-- TODO etudiant : definir le marche (1, 12, 2, 10)
-- def marcheExo1 : TwoQualityMarket := ⟨1, 12, 2, 10, by omega, by omega⟩
-- TODO etudiant : evaluer le numerateur du seuil
-- Indice : #eval poolingThresholdNum marcheExo1
-- TODO etudiant : montrer par decide que le pooling echoue meme a pi = 100
-- Indice : example : ¬ poolingTenable marcheExo1 ⟨100, by decide⟩ := by decide
-- TODO etudiant (reponse 3, en commentaire) : pourquoi aucun prior ne suffit ?
-- Indice : comparer cHigh = 12 et vHigh = 10
-- ancre d'execution (cellule valide meme non completee) :
#check poolingThresholdNum
-- TODO etudiant : definir le marche (1, 12, 2, 10)
-- def marcheExo1 : TwoQualityMarket := ⟨1, 12, 2, 10, by omega, by omega⟩
-- TODO etudiant : evaluer le numerateur du seuil
-- Indice : #eval poolingThresholdNum marcheExo1
-- TODO etudiant : montrer par decide que le pooling echoue meme a pi = 100
-- Indice : example : ¬ poolingTenable marcheExo1 ⟨100, by decide⟩ := by decide
-- TODO etudiant (reponse 3, en commentaire) : pourquoi aucun prior ne suffit ?
-- Indice : comparer cHigh = 12 et vHigh = 10
-- ancre d'execution (cellule valide meme non completee) :
Raw input{"cmd": "-- TODO etudiant : definir le marche (1, 12, 2, 10)\n-- def marcheExo1 : TwoQualityMarket := \u27e81, 12, 2, 10, by omega, by omega\u27e9\n\n-- TODO etudiant : evaluer le numerateur du seuil\n-- Indice : #eval poolingThresholdNum marcheExo1\n\n-- TODO etudiant : montrer par decide que le pooling echoue meme a pi = 100\n-- Indice : example : \u00ac poolingTenable marcheExo1 \u27e8100, by decide\u27e9 := by decide\n\n-- TODO etudiant (reponse 3, en commentaire) : pourquoi aucun prior ne suffit ?\n-- Indice : comparer cHigh = 12 et vHigh = 10\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check poolingThresholdNum\n", "env": 8}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 14, "column": 0},
"endPos": {"line": 14, "column": 6},
"data":
"AsymmetricInformation.Lemons.poolingThresholdNum (m : TwoQualityMarket) : Int"}],
"env": 9}
Exercice 2 — construire un no-trade
Objectif : construire un marché et un prior où la spirale se termine sur une offre vide — et où même la qualité basse ne s’échange pas.
Indices : - Pour que low lui-même ne s’échange pas, il faut que sa valeur pour l’acheteur reste sous son coût de réservation : v_L < c_L. - Vérifiez avec demoSpiral : la trajectoire doit converger vers un prix où offered est vide. - Contrastez avec le marché canonique : là, v_L = c_L = 0 et le régime lemons-only survit à prix nul — d’un cheveu.
-- TODO etudiant : definir un marche no-trade (indice : v_L < c_L, ex (3, 5, 1, 4))
-- def marcheExo2 : TwoQualityMarket := ⟨3, 5, 1, 4, by omega, by omega⟩
-- TODO etudiant : lancer la spirale et observer l'offre vide au point fixe
-- Indice : #eval demoSpiral marcheExo2 prior50 (demoPrixInitial marcheExo2 50)
-- Etape 2 : verifier que meme P = c_L laisse l'acheteur perdicataire
-- Indice : #eval expectedValue marcheExo2 prior50 3
-- TODO etudiant (lecture, en commentaire) : ce marche est-il pooling-tenable
-- a quelque prior que ce soit ? Utiliser l'exercice 1 pour repondre.
-- ancre d'execution (cellule valide meme non completee) :
#check expectedValue
-- TODO etudiant : definir un marche no-trade (indice : v_L < c_L, ex (3, 5, 1, 4))
-- def marcheExo2 : TwoQualityMarket := ⟨3, 5, 1, 4, by omega, by omega⟩
-- TODO etudiant : lancer la spirale et observer l'offre vide au point fixe
Raw input{"cmd": "-- TODO etudiant : definir un marche no-trade (indice : v_L < c_L, ex (3, 5, 1, 4))\n-- def marcheExo2 : TwoQualityMarket := \u27e83, 5, 1, 4, by omega, by omega\u27e9\n\n-- TODO etudiant : lancer la spirale et observer l'offre vide au point fixe\n-- Indice : #eval demoSpiral marcheExo2 prior50 (demoPrixInitial marcheExo2 50)\n-- Etape 2 : verifier que meme P = c_L laisse l'acheteur perdicataire\n-- Indice : #eval expectedValue marcheExo2 prior50 3\n\n-- TODO etudiant (lecture, en commentaire) : ce marche est-il pooling-tenable\n-- a quelque prior que ce soit ? Utiliser l'exercice 1 pour repondre.\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check expectedValue\n", "env": 9}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data":
"AsymmetricInformation.Lemons.expectedValue (m : TwoQualityMarket) (π : Prior) (P : Int) : Int"}],
"env": 10}
Exercice 3 — le plancher par monotonie, sans ré-arbitrage
On admet (exemples (f)-(g) du module) que marcheSeuil est pooling-tenable à π = 75.
Objectif : prouver le pooling à π = 90 sans re-décider la condition arithmétique — uniquement par transfert de poolingTenable_mono.
Indices : - poolingTenable_mono _ ⟨75, by decide⟩ ⟨90, by decide⟩ (by decide) (...) transfère la tenabilité du premier prior au second. - Question bonus (en commentaire) : que donne decide directement à π = 90, et pourquoi la monotonie est-elle plus qu’un raccourci de preuve ? (Réponse attendue : decide re-vérifie les entiers point à point ; mono établit un fait structurel — réutilisable pour tout prior au-dessus du seuil, y compris ceux qu’on ne teste jamais un par un.)
-- TODO etudiant : prouver le pooling a pi = 90 par monotonie seule
-- Indice : example : poolingTenable marcheSeuil ⟨90, by decide⟩ :=
-- poolingTenable_mono _ ⟨75, by decide⟩ ⟨90, by decide⟩ (by decide) ??
-- TODO etudiant : remplacer ?? par la preuve du pooling au seuil
-- Indice : l'exemple (f) du notebook la fournit deja — on la reutilise,
-- on ne la refait pas
-- ancre d'execution (cellule valide meme non completee) :
#check poolingTenable_mono
-- TODO etudiant : prouver le pooling a pi = 90 par monotonie seule
-- Indice : example : poolingTenable marcheSeuil ⟨90, by decide⟩ :=
-- poolingTenable_mono _ ⟨75, by decide⟩ ⟨90, by decide⟩ (by decide) ??
-- TODO etudiant : remplacer ?? par la preuve du pooling au seuil
-- Indice : l'exemple (f) du notebook la fournit deja — on la reutilise,
-- on ne la refait pas
-- ancre d'execution (cellule valide meme non completee) :
Raw input{"cmd": "-- TODO etudiant : prouver le pooling a pi = 90 par monotonie seule\n-- Indice : example : poolingTenable marcheSeuil \u27e890, by decide\u27e9 :=\n-- poolingTenable_mono _ \u27e875, by decide\u27e9 \u27e890, by decide\u27e9 (by decide) ??\n\n-- TODO etudiant : remplacer ?? par la preuve du pooling au seuil\n-- Indice : l'exemple (f) du notebook la fournit deja \u2014 on la reutilise,\n-- on ne la refait pas\n\n-- ancre d'execution (cellule valide meme non completee) :\n#check poolingTenable_mono\n", "env": 10}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 6},
"data":
"AsymmetricInformation.Lemons.poolingTenable_mono (m : TwoQualityMarket) (π π' : Prior) (hπ : π.piNum ≤ π'.piNum)\n (h : poolingTenable m π) : poolingTenable m π'"}],
"env": 11}
Les trois exercices : une échelle, trois gestes
Les trois stubs forment une progression. Exercice 1 — marché (1, 12, 2, 10) : le coût de la haute qualité (12) excède sa valeur (10) ; aucun prior ne peut sauver le pooling, et la question finale du commentaire demande exactement cette lecture c_H > v_H. Exercice 2 — marché (3, 5, 1, 4) : le coût de la basse qualité (3) excède sa valeur (1) — v_L < c_L — le marché construit est no-trade ; la dernière question demande d’y répondre en utilisant l’exercice 1 : c_H = 5 > v_H = 4, le marché n’est tenable à aucun prior. L’échelle est explicite : l’exercice 2 se résout par l’insight de l’exercice 1. Exercice 3 — bascule de registre : on ne construit plus rien, on réutilise — l’exemple (f) (pooling à 75) est monté à 90 par poolingTenable_mono ; la preuve du seuil n’est pas refaite, elle est importée. Définir, inférer, réutiliser : les trois gestes du certificat.
Ce que le certificat garantit — et ce qu’il ne garantit pas
Fait
Statut
Où
Seuil de pooling = produit croisé exact
prouvé (propext, Quot.sound uniquement)
poolingTenable_iff_cross
Région tenable = intervalle [π_min ; 100]
prouvée
poolingTenable_mono
Frontière raide (74 casse, 75 tient)
décidée sur valeurs témoins
exemples (e), (f)
Trois régimes existent et sont disjoints
formalisés
poolingTenable / lemonsOnlyPossible / noTrade
Trajectoire de prix, vitesse d’effondrement
simulée, non prouvée
demoSpiral
La colonne de droite est le contrat du notebook : ce qui est prouvé l’est dans le lake ; ce qui est simulé le dit honnêtement.
Les trois autres piliers du lake — signal de Spence (Signaling.lean), screening de Rothschild-Stiglitz (Screening.lean), règle anticipative de Wilson-Miyazaki (MiyazakiWilson.lean), pont bayésien (BayesianLink.lean) — sont couverts en simulation dans le 17b et documentés dans le README du lake.
Lien vers l’IA et conclusion
L’antisélection apparaît partout où une partie cache une qualité à l’autre : places de marché de modèles (acheter un modèle sans connaître sa distribution d’erreurs), jeux de données d’entraînement acquis à l’aveugle, agents qui sélectionnent leurs sources. Les réponses mécanistes du lake sont les classiques : signaler à ses coûts (Spence — un modèle ne publie son rapport d’évaluation que si celui-ci est bon), screener par menu (Rothschild-Stiglitz — proposer deux contrats et laisser chaque type se révéler), anticiper les retraits (Wilson-Miyazaki).
La certification formelle joue ici le rôle du tiers de confiance : elle transforme « le seuil semble être 75 % » en « le seuil est 75 %, preuve à l’appui, clôture axiomatique minimale ». C’est exactement ce qu’on demande à un audit de modèle en production.
Ce qu’il faut retenir :
Le prix filtre la qualité ; l’anticipation rationnelle de l’acheteur referme la boucle — c’est le point fixe P ≤ E[v | S(P)].
Le pooling n’est tenable qu’au-dessus d’un seuil exact, caractérisé par produit croisé et monotone : un plancher, pas une fenêtre.
Le certificat délimite les régimes ; la simulation montre les chemins — sur ce marché à deux qualités, les deux se disent dans le même langage : des entiers et des décisions.