From 04f962a200842ef8d0f81e55b8437a3fcd47491f Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 16 Sep 2026 03:01:05 +0200 Subject: [PATCH 1/2] =?UTF-8?q?Add:=20densite=20Lean=20natif=20=E2=80=94?= =?UTF-8?q?=2023b/01b/FormalGroups,=20interpretations=20+=20attendus,=203?= =?UTF-8?q?=20notebooks=20sous=20plancher=20(See=20#13410)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Sonnet 5 --- ...ameTheory-23b-Lean-Assignment-Native.ipynb | 62 +++++++++++ .../01b-Lean-SocialChoice-Formal.ipynb | 100 ++++++++++++++++++ .../Lean/Lean-30-FormalGroups-Native.ipynb | 48 ++++++++- 3 files changed, 209 insertions(+), 1 deletion(-) diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb index 51fc4b5203..6640f57be6 100644 --- a/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb @@ -366,6 +366,14 @@ "#check Assignment.dualFeasible_tighten" ] }, + { + "cell_type": "markdown", + "id": "gt23b-interp-primal", + "metadata": {}, + "source": [ + "**Lire le certificat avant l'algorithme.** Les trois signatures exhibées définissent tout le vocabulaire du problème : `value` calcule le coût d'une affectation (une permutation σ de `Fin n`), `IsOptimal` énonce l'optimalité comme une *proposition* — « σ coûte moins que toute autre » — et `DualFeasible` introduit le second protagoniste, le couple (u, v) potentiellement plus faible que toute arête. Le geste Lean est important : rien de ces objets n'est un algorithme. Le lake `assignment_lean` ne **calcule** pas l'optimum, il **certifie** — et la distinction est le sujet du notebook. Toute la suite consiste à faire se rencontrer les deux protagonistes : un σ à valeur 5 et un couple (u, v) à valeur duale 5, le gap nul scellant l'optimalité des deux." + ] + }, { "cell_type": "markdown", "id": "fc315850", @@ -482,6 +490,14 @@ "#eval C3 1 2 -- cout d'affecter l'agent 1 a la tache 2" ] }, + { + "cell_type": "markdown", + "id": "gt23b-interp-c3", + "metadata": {}, + "source": [ + "**La matrice C3, relue entrée par entrée.** Les `#eval` ciblés extraient deux cases : C3 0 1 = 1 (l'arête bon marché qui fera le matching optimal) et C3 1 2 = 5 (l'arête chère). La matrice complète `[[4,1,3],[2,0,5],[3,2,2]]` contient aussi la diagonale (0,0)→0 : l'identité coûte 4+0+2 = 6, pas 0+0+0 — un piège classique de lecture, la valeur d'une affectation somme **un seul élément par ligne et par colonne**, pas le minimum de chaque ligne pris indépendamment. C'est exactement pourquoi l'affectation est un problème combinatoire (choisir une permutation) et non glouton (choisir n minima locaux) : le minimum de la ligne 0 est 1 en colonne 1, mais le minimum de la ligne 1 est 0 en colonne 1 aussi — conflit que seule la permutation arbitre." + ] + }, { "cell_type": "markdown", "id": "beb3c4ce", @@ -640,6 +656,14 @@ "#eval Assignment.value C3 ((Equiv.swap (0 : Fin 3) 1).trans (Equiv.swap (0 : Fin 3) 2)).symm" ] }, + { + "cell_type": "markdown", + "id": "gt23b-interp-permutations", + "metadata": {}, + "source": [ + "**L'énumération exhaustive comme preuve — et sa limite.** Les six `#eval` parcourent tout `Equiv.Perm (Fin 3)` : identité 6, transpositions (5 pour 0↔1, 6 pour 0↔2, 8 pour 1↔2 attendu), puis les deux 3-cycles. Sur cette instance, le minimum **vérifié par épuisement** est 5, atteint par σ = (0↔1). Cette énumération EST une preuve d'optimalité — au sens combinatoire, rien ne lui manque. Mais sa complexité est n! : à n = 12 il y a déjà 479 millions de permutations, hors de portée d'un `#eval`. Le notebook joue donc un double jeu pédagogique : prouver *par l'épuisement* que 5 est optimal sur une instance jouet, puis *par la dualité* que 5 est optimal sur n'importe quelle taille — la méthode hongroise et son certificat dual remplaçant l'énumération, pas la complétant." + ] + }, { "cell_type": "markdown", "id": "da4401dd", @@ -766,6 +790,14 @@ "#eval Assignment.dualValue u3 v3" ] }, + { + "cell_type": "markdown", + "id": "gt23b-interp-dual", + "metadata": {}, + "source": [ + "**Pourquoi dualValue = 5 est une si bonne nouvelle.** La valeur duale Σuᵢ + Σvⱼ = 1+2+2 = 5 est un *plafond inférieur* sur la valeur de toute affectation : chaque arête (i, j) d'un matching coûte C3 i j ≥ uᵢ + vⱼ (c'est la dual-faisabilité), et sommer sur un matching complet donne value σ ≥ dualValue. L'inégalité faible de dualité dit exactement cela, et sa preuve dans le lake n'utilise que l'arithmétique entière. Or l'énumération de la cellule précédente a montré un matching à 5 : plafond 5, atteint 5 — **gap nul**, et l'optimalité est scellée des deux côtés sans avoir comparé aux cinq autres permutations. C'est le théorème mini-max de l'affectation en acte : max des duaux faisables = min des matchings. Aucune magie : le couple (u3, v3) exhibé est celui que la méthode hongroise produit en terminant, et la section suivante vérifie qu'il est bien faisable." + ] + }, { "cell_type": "markdown", "id": "e7cc30da", @@ -1045,6 +1077,14 @@ "#print axioms Assignment.optimality_of_zero_gap" ] }, + { + "cell_type": "markdown", + "id": "gt23b-interp-tight", + "metadata": {}, + "source": [ + "**Les arêtes d'égalité dessinent le matching.** Une arête (i, j) est *serrée* quand uᵢ + vⱼ = C3 i j — l'inégalité duale est une égalité. Les trois `example` vérifient que les arêtes (0,1), (1,0) et (2,2) sont serrées, chacune par `decide` : sur `Fin 3` et des entiers littéraux, le décideur booléen tranche. La lecture structurelle est le cœur de la méthode hongroise : **le matching optimal vit dans le sous-graphe des arêtes serrées** (condition de complémentarité relâchée). Si σ n'utilisait que des arêtes serrées, value σ = dualValue immédiatement — gap nul constructif. Le triplet vérifié ici n'est pas exactement le matching σ* = (0↔1) mais ses arêtes le recouvrent : (0,1) et (1,0) sont les deux arêtes de la transposition, (2,2) son point fixe. Quand l'algorithme resserre u et v, il déplace les arêtes serrées jusqu'à ce qu'un matching parfait s'y loge entièrement." + ] + }, { "cell_type": "markdown", "id": "f0c08215", @@ -1302,6 +1342,14 @@ "#print axioms optimal_C3" ] }, + { + "cell_type": "markdown", + "id": "gt23b-interp-certificat", + "metadata": {}, + "source": [ + "**Le certificat complet, assemblé.** Cette cellule est le sommet du notebook : `C3_dual_feasible` prouve la faisabilité duale par `decide` (9 inégalités à vérifier sur `Fin 3`), puis `optimal_C3` **compile** le certificat — faisabilité duale + matching à arêtes serrées — en optimalité, via `kuhn_munkres_correct`. Aucun des deux lemmes ne connaît les cinq autres permutations : l'optimalité est *déduite*, pas énumérée. Et la cellule `#print axioms` qui suit montre que `kuhn_munkres_correct` lui-même ne repose que sur les trois axiomes standard de Lean (propext, Classical.choice, Quot.sound) : la chaîne complète — de la matrice littérale au théorème d'optimalité — ne smuggle aucun axiome ad hoc. La taille du problème n'apparaît nulle part dans la structure de la preuve : remplacer C3 par une matrice 10×10 change les `decide` en vérifications plus longues mais le *schéma* reste — c'est la différence entre prouver un théorème et vérifier une instance, et le lake la rend tangible." + ] + }, { "cell_type": "markdown", "id": "d39ded2b", @@ -1794,6 +1842,20 @@ "example : True := trivial" ] }, + { + "cell_type": "markdown", + "id": "gt23b-attendus", + "metadata": {}, + "source": [ + "### Attendus et anti-pièges (exercices 1 à 3)\n", + "\n", + "**Exercice 1 (votre matrice 2×2).** *Attendu* : une matrice dont l'identité n'est PAS optimale, par exemple `[[1, 0], [0, 1]]`... dont l'identité coûte 2 et la transposition 0 — attention, l'énoncé demande l'inverse (l'identité répond sur `[[1,0],[0,1]]`) : il faut une matrice où la permutation non-triviale bat l'identité, comme `[[5, 1], [1, 5]]` (identité 10, swap 2). Le réflexe à construire : la valeur d'une permutation se lit comme une diagonalité après réordonnancement des colonnes. *Anti-piège* : tester seulement l'identité et le swap naïf sans vérifier l'égalité 2×2 = exhaustif — sur `Fin 2` il n'y a que deux permutations, les tester toutes les deux est une preuve complète, pas un échantillon.\n", + "\n", + "**Exercice 2 (le certificat dual de votre matrice).** *Attendu* : u et v tels que dualValue = valeur optimale, avec chaque uᵢ + vⱼ ≤ C2 i j. Sur une 2×2 à swap optimal, un couple du style u = [1, 0], v ajusté fonctionne : les arêtes serrées doivent inclure les deux arêtes du swap. La démarche : partir de u = v = 0 (faisable si coûts positifs), resserrer jusqu'à ce que les arêtes serrées couvrent le matching optimal. *Anti-piège* : choisir u, v qui somment à la valeur optimale mais violent une inégalité — la valeur duale serait un plafond *non prouvé* ; la faisabilité est ce qui rend le plafond un plafond, `decide` la vérifie case par case sur `Fin 2`.\n", + "\n", + "**Exercice 3 (resserrement maximal, S = {1}, T = ∅).** *Attendu* : delta = 0. L'arête (1,1) a une marge nulle (C3 1 1 = 0 = u1 + v1 déjà) : resserrer la ligne 1 de δ > 0 violerait immédiatement la faisabilité sur cette arête. Le resserrement est *borné par la plus petite marge sortante*, et une marge nulle bloque tout mouvement — c'est précisément ce qui force la méthode hongroise à élargir S ou à toucher les colonnes (T ≠ ∅) plutôt que les lignes seules. *Anti-piège* : raisonner sur la marge moyenne ou sur une autre ligne ; la question porte sur le δ maximal admissible, gouverné par le minimum des marges des arêtes sortant de S — ici ce minimum vaut 0, atteint sur (1,1)." + ] + }, { "cell_type": "markdown", "id": "d787de17", diff --git a/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb b/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb index 783e0fc765..0c06899e0f 100644 --- a/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb @@ -221,6 +221,14 @@ "#check @Preference.indiff" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-preference", + "metadata": {}, + "source": [ + "**Pourquoi la préférence faible comme primitive.** Le `structure Preference` encode une préférence *faible* (R : « au moins aussi bon que ») avec exactement deux champs : complétude (toute paire est comparable) et transitivité. La préférence stricte P est **dérivée** (R ∧ ¬R symétrique), pas axiomatisée séparément — un choix de fondation classique : la version faible est celle qui se compose bien (la clôture transitive d'un ordre strict est un ordre strict, mais l'indifférence n'est pas transitive en général — le paradoxe de la tasse de sucre). En Lean, ce choix a un corollaire pratique : tous les théorèmes d'existence (Arrow, Sen) quantifient sur des `Preference A` et héritent gratuitement la comparabilité totale. Noter aussi la décision d'ingénierie : un `structure` plutôt qu'un `def` à clauses — les champs nommés (`complete`, `trans`) deviennent des projections utilisables comme lemmes, chaque axiome de la structure étant *transporté* par la construction." + ] + }, { "cell_type": "markdown", "id": "582fec99", @@ -351,6 +359,14 @@ "#check @SocialWelfareFunction" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-profile", + "metadata": {}, + "source": [ + "**Un profil est une fonction, pas une liste.** `Profile I A := I → Preference A` : la société est encodée au niveau des types comme une fonction de l'ensemble des individus vers les préférences. Ce choix silencieux fait tout le travail dans les preuves qui suivent : modifier le profil d'UN individu (construire `Function.update prefs i p'`) est l'opération primitive des arguments de pivot — la preuve d'Arrow fait glisser un électeur à travers toutes ses positions possibles en comparant des profils qui ne diffèrent que sur lui. Si le profil était une liste, chaque théorème devrait gérer l'ordre et les doublons ; comme fonction, l'individualisme méthodologique (chaque agent porte sa préférence, la société les agrège) est littéralement la signature du type." + ] + }, { "cell_type": "markdown", "id": "0149a9ac", @@ -639,6 +655,14 @@ "#check @makeBot" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-maketop", + "metadata": {}, + "source": [ + "**`makeTop` : la chirurgie de profil, vérifiée.** L'helper reconstruit une préférence où l'alternative `a` est mise en tête, en préservant l'ordre relatif des autres (les deux `if` imbriqués : `x = a` gagne toujours, `y = a` perd toujours, sinon on consulte l'ancienne relation). La subtilité est dans les preuves de clôture : `complete` et `trans` ne sont PAS gratuits — le `by_cases` imbriqué de la sortie montre la preuve de complétude cas par cas. Ce helper est la brique des preuves d'impossibilité : Sen construit son cycle social en faisant de deux individus des *dictateurs locaux* via des `makeTop` ciblés, et l'Extremal Lemma d'Arrow raisonne sur des profils où une alternative passe du bas vers le haut de tous les classements simultanément — le même helper, itéré. Lire cette cellule comme l'outillage : le théorème viendra, mais il vivra dans ce machinery." + ] + }, { "cell_type": "markdown", "id": "576f7350", @@ -757,6 +781,14 @@ "#check @WeakPareto" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-pareto", + "metadata": {}, + "source": [ + "**Pareto faible : pourquoi la version minimale suffit.** `WeakPareto` ne demande l'unanimité stricte que pour l'ordre strict social : si **tous** préfèrent strictement x à y, la société aussi. C'est plus faible que le Pareto fort (qui conclut aussi depuis des préférences faibles unanimes) — et c'est un choix *stratégique* de formalisation : plus l'axiome est faible, plus le théorème d'impossibilité est fort. Arrow avec Pareto faible interdit plus de fonctions sociales qu'Arrow avec Pareto fort. Le `#check` confirme le typage : `WeakPareto` est une `Prop` sur une `SocialWelfareFunction` — une *propriété* de l'agrégateur, à ne pas confondre avec une propriété d'un profil particulier (l'exercice 4 fera vérifier Pareto sur UN profil, une instanciation)." + ] + }, { "cell_type": "markdown", "id": "1f9baba2", @@ -872,6 +904,14 @@ "#check @IIA" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-iia", + "metadata": {}, + "source": [ + "**IIA, l'axiome le plus mal compris — lu dans sa quantification.** La définition quantify sur **deux profils** `prefs` et `prefs2` : si les préférences individuelles entre x et y sont identiques (dans les deux sens, d'où les deux `↔`), la préférence SOCIALE entre x et y doit être identique. La formule dit ceci : le verdict social sur une paire ne peut dépendre que des verdicts individuels sur cette paire — jamais des positions d'alternatives tierces z, jamais de l'intensité des préférences. C'est ici que l'information cardinale est interdite : un agrégateur qui lirait « combien » chaque individu préfère x à y (utilités, scores) violerait IIA en changeant son verdict quand les UTILITÉS entre x et y changent alors que l'ORDRE x/y est stable. La leçon de lecture Lean : les deux `↔` (pas des implications) capturent la cohérence bidirectionnelle — le même principe qui fera de l'ensemble des coalitions décisives une structure stable au fil de la preuve d'Arrow." + ] + }, { "cell_type": "markdown", "id": "63b47ad3", @@ -1007,6 +1047,14 @@ "#check @NonDictatorial" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-dictateur", + "metadata": {}, + "source": [ + "**Non-dictature : un ∀ sur un ¬∃, proprement niché.** `IsDictator` dit que la préférence stricte de d est TOUJOURS suivie (un ∀ sur profils et paires) ; `NonDictatorship` nie l'existence d'un tel d. La nidification des quantificateurs mérite une lecture lente : « pour tout d, il existe un profil et une paire où la société contredit d ». Le théorème d'Arrow affaiblira jusqu'à : Pareto + IIA ⇒ **il existe un d dictateur** — la conclusion n'est pas qu'un dictateur est *construit*, mais qu'il *existe*, et la preuve l'identifie comme le pivot (l'électeur dont le passage de x fait basculer le verdict social). La formalisation rend un service de précision : « dictatoriale » dans l'énoncé informel pourrait signifier « un individu a beaucoup d'influence » ; la définition Lean est binaire, maximale, et c'est elle qui rend le théorème tranchant." + ] + }, { "cell_type": "markdown", "id": "f06da92d", @@ -1191,6 +1239,14 @@ "#check @arrow_impossibility_sketch" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-arrow", + "metadata": {}, + "source": [ + "**Arrow lu comme une chaîne de lemmes, pas un bloc.** La version du notebook est un *sketch* — et l'annonce honnêtement : la preuve complète (0 sorry, via la chaîne Geanakoplos 2005 : `extremal_lemma → pivot_exists → pivot_is_dictator_except_b → partial_dictator_is_full_dictator`) vit dans le lake `game_theory_lean/SocialChoice/Arrow.lean`, et la cellule suivante en exhibit les deux premiers maillons. L'intérêt pédagogique du sketch est la *forme* de la preuve : l'Extremal Lemma (une alternative extrême chez tous est extrême socialement) crée le premier coalitions-phénomène ; le pivot (l'électeur dont le renversement renverse la société) transforme l'existence locale en structure globale ; le dernier maillon convertit « dictateur sauf sur b » en dictateur complet. Chaque maillon est un théorème utilisable séparément — c'est la différence entre une preuve et une vérification monolithique, et le réflexe à emporter : dans un lake, l'énoncé importé cache une architecture." + ] + }, { "cell_type": "markdown", "id": "cd8d74d5", @@ -1536,6 +1592,14 @@ "#check @all_decisive_pred" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-decisif", + "metadata": {}, + "source": [ + "**Les ensembles décisifs : le moteur caché d'Arrow.** `IsDecisivePred` définit un groupe G décisif pour (x, y) : l'unanimité stricte de G sur la paire entraîne le verdict social. Toute la preuve d'Arrow est une étude de la **famille** des ensembles décisifs : elle est non-vide (Pareto rend l'univers décisif), close par intersection (via IIA — c'est le théorème de field-expansion de Geanakoplos), et l'argument du pivot montre que tout ensemble décisif minimal se réduit à un singleton — le dictateur. La structure profonde (pour les curieux : la famille des ensembles décisifs d'une SWF Pareto + IIA est un *ultrafiltre* sur les individus ; sur un ensemble fini, tout ultrafiltre est principal — d'où le dictateur) n'est pas formalisée ici, mais la définition en est la porte : chaque lemme du lake est un fait sur cette famille." + ] + }, { "cell_type": "markdown", "id": "751691ce", @@ -2022,6 +2086,14 @@ "#check @SinglePeakedProfile" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-unimodal", + "metadata": {}, + "source": [ + "**Unimodalité : la restriction de domaine comme issue de secours.** `SinglePeaked` demande un ordre sous-jacent `le` sur les alternatives et un pic `peak` : s'éloigner du pic dans un sens ou l'autre ne fait jamais monter la préférence. Ce que la définition EXCLUT est plus instructif que ce qu'elle impose : les préférences à double creux (aimer les deux extrêmes, détester le centre — le profil du conflit gauche-droite sans centre) sont non-unimodales, et c'est exactement le matériau des cycles de Condorcet. La leçon de design théorique : les théorèmes d'impossibilité d'Arrow et de Sen sont des énoncés **pour tout domaine** ; restreindre le domaine (une hypothèse de plus, mais une hypothèse *sur les profils admis*, pas sur l'agrégateur) peut rouvrir l'existence — c'est le théorème de Black qui suit, et c'est la stratégie générale de toute la théorie du choix social post-Arrow : voter n'est pathologique que sur les domaines pathologiques." + ] + }, { "cell_type": "markdown", "id": "d443b63d", @@ -2230,6 +2302,14 @@ "#check @median_voter_theorem_sketch" ] }, + { + "cell_type": "markdown", + "id": "sc-interp-median", + "metadata": {}, + "source": [ + "**Le théorème médian, annoncé avec sa dette.** La cellule est honnête : la preuve complète n'est **pas encore** dans le lake (il manque `Fintype`, `LinearOrder`, et la cardinalité impaire du nombre d'électeurs), et l'énoncé est donné comme aspiration. C'est une situation normale dans un compagnon natif : le notebook documente l'écart entre le théorème mathématique (Black 1948 : sous unimodalité et cardinalité impaire, le pic de l'électeur médian bat toute alternative en duel) et l'état de la formalisation. L'exercice 6 fait vérifier l'énoncé sur une instance concrète (3 électeurs, pics 0.2 / 0.5 / 0.8) — une vérification d'instance n'est pas une preuve du théorème, mais elle ancre l'intuition : l'électeur médian gagne parce qu'un côté du pic contient au plus la moitié des électeurs, chacun préférant s'approcher du centre. La dette formalisation vs théorème est tracée, pas maquillée." + ] + }, { "cell_type": "markdown", "id": "30928a68", @@ -2818,6 +2898,26 @@ "-- Resultat attendu : (2, 2) => M bat tous => Condorcet" ] }, + { + "cell_type": "markdown", + "id": "sc-attendus", + "metadata": {}, + "source": [ + "### Attendus et anti-pièges (exercices du TODO et 4 à 6)\n", + "\n", + "**TODO (dictature + Pareto).** *Attendu* : `dictatorship d` copie la préférence de d (`swf.f prefs := prefs d`) ; la preuve de Pareto est alors une réécriture — l'unanimité stricte de tous contient celle de d, et le verdict social EST celui de d. *Anti-piège* : définir la dictature sur la préférence *faible* rend le théorème trivial mais la définition non-standard ; la convention du notebook (copie stricte) est celle sous laquelle Arrow est énoncé.\n", + "\n", + "**Exercice 4 (Pareto sur un profil concret).** *Attendu* : un `example` instancié — Alice et Bob, a > b à l'unanimité stricte, conclure `swf.f prefs |>.strict a b` depuis `WeakPareto`. La démonstration est une application directe du lemme, pas une induction. *Anti-piège* : vérifier le Pareto en regardant seulement le profil SANS appliquer l'axiome (re-dériver la conclusion à la main) — l'exercice évalue le réflexe d'*instancier un théorème*, pas de refaire sa preuve.\n", + "\n", + "**Exercice 5 (cycle de Condorcet).** *Attendu* : aucun vainqueur de Condorcet — a bat b (électeurs 0 et 2), b bat c (0 et 1), c bat a (1 et 2), le tournoi est un cycle. Le verdict à écrire : `¬ ∃ w, IsCondorcetWinner w` (ou sa version à marges de la section 6). *Anti-piège* : conclure « donc la règle majoritaire est mauvaise » — l'exercice mesure une instance ; la section Peters (impossibilités de Condorcet) montrera que TOUTE règle cohérente-Condorcet résolue perd autre chose, le cycle n'est pas une pathologie de la règle mais du domaine (cf. l'unimodalité du théorème médian : ce profil n'est pas unimodal).\n", + "\n", + "**Exercice 6 (médian sur pics 0.2/0.5/0.8).** *Attendu* : B (pic 0.5) gagne les deux duels — contre A (pics 0.5 et 0.8 le préfèrent), contre C (0.2 et 0.5). Le point pédagogique : le vainqueur est le pic MÉDIAN (0.5), pas le pic moyen (0.5 aussi ici — choisir des exemples où les deux diffèrent serait plus discriminant, un réflexe de concepteur d'exercice). *Anti-piège* : vérifier seulement un duel — un vainqueur de Condorcet doit battre TOUTE alternative, et sur 3 alternatives le second duel est une ligne de plus, pas une option.\n", + "\n", + "\n", + "\n", + "**La série d'exercices comme arc.** Les quatre questions se répondent en écho : le TODO (une dictature EST une SWF légitime au sens des axiomes individuels) montre que Pareto seul n'exclut rien ; l'exercice 4 instancie l'axiome sur un profil ; l'exercice 5 exhibe le domaine qui tue l'existence d'un gagnant ; l'exercice 6 exhibe le domaine qui la restaure. Ensemble, ils balayent la thèse du notebook : les théorèmes d'impossibilité ne disent pas « la démocratie est impossible », ils mesurent le prix exact — trois axiomes incompatibles, et la marge de manœuvre se joue sur le domaine des profils admis." + ] + }, { "cell_type": "markdown", "id": "5aaa1cbd", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb index 439e5b5189..281ffd6052 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb @@ -447,6 +447,14 @@ "Le constructeur affiché par `#print` expose les obligations exactes vérifiées par Lean. `Fin g ⊕ Fin g` n'est donc pas une notation décorative : le type sépare les deux opérandes de la loi, tandis que les coefficients de degré un encodent $F(X,0)=X$ et $F(0,Y)=Y$." ] }, + { + "cell_type": "markdown", + "id": "fg-interp-structure", + "metadata": {}, + "source": [ + "**Un groupe formel porté par ses séries.** Le `#print` montre l'architecture : `MvFormalGroup g R` est une structure dont le premier champ est `toPowerSeries` — la loi F est *donnée* comme une famille de séries formelles multivariées, et les axiomes (identité, inverse, associativité exprimés par identité de séries) sont des champs additionnels. Le choix de fondation est à lire lentement : plutôt qu'un type abstrait muni d'axiomes, le lake ancre les groupes formels DANS les séries entières, où les identités deviennent des égalités de coefficients — vérifiables terme à terme. C'est ce qui permettra aux exemples canoniques (`addMv` en section 6) d'être prouvés par `rfl` : l'égalité des séries se décide sur les coefficients. La hiérarchie `g : ℕ` (nombre de variables) puis `R` anneau commutatif suit exactement la théorie classique de Hazewinkel : le cadre est celui des groupes formels multivariés, dont le cas univarié est la spécialisation g = 1." + ] + }, { "cell_type": "markdown", "id": "f5f4c37f", @@ -984,6 +992,14 @@ "La sortie distingue bien la transformation d'une famille structurée `MvFormalGroup` de l'application sur une seule `MvPowerSeries`. Le second `map` est la brique coefficientielle utilisée pour construire le premier." ] }, + { + "cell_type": "markdown", + "id": "fg-interp-deux-maps", + "metadata": {}, + "source": [ + "**Les deux `map`, disambiguisés par leurs types.** La sortie montre deux signatures : `MvFormalGroup.map` prend un morphisme d'anneaux `R →+* S` et transporte un groupe formel sur R vers un groupe formel sur S (changement de base — le même groupe, lu sur un autre anneau) ; `MvPowerSeries.map` agit au niveau des séries, coefficient par coefficient. La confusion est le piège d'API classique : les deux s'appellent `map`, mais le premier préserve la loi (c'est un morphisme de groupes formels au-dessus d'un morphisme d'anneaux) quand le second n'a aucune raison de respecter une loi quelconque — il n'est pas au courant des axiomes. La leçon Lean dépasse le cas : quand deux définitions partagent un nom, le `#check @` des signatures est le document qui les sépare ; lire le TYPE d'une fonction est souvent plus sûr que lire son nom. Le point 5 du sommaire annonce exactement ce travail de distinction." + ] + }, { "cell_type": "markdown", "id": "4a8bb4af", @@ -1135,6 +1151,14 @@ "Le compilateur accepte `rfl` pour la forme explicite, réutilise le champ structurel pour le terme constant, simplifie le test d'égalité d'indices pour le coefficient, puis trouve automatiquement l'instance `IsComm`. Ces quatre mécanismes sont distincts malgré un exemple mathématique très compact." ] }, + { + "cell_type": "markdown", + "id": "fg-interp-addmv", + "metadata": {}, + "source": [ + "**`addMv`, l'exemple canonique — et pourquoi `rfl` suffit.** L'exemple affirme que le terme d'ordre 0 de la loi additive s'écrit X(Sum.inl 0) + X(Sum.r 0) : les deux coordonnées du `Fin g ⊕ Fin g` (l'espace ambiant du produit de deux copies) chacune portée par sa variable. Les deux corollaires qui suivent extraient le coefficient constant (0) et le coefficient linéaire (1) — la carte d'identité d'un groupe formel : pas de terme constant, partie linéaire = l'identité. La preuve par `rfl` n'est pas une économie de moyens mais un théorème déguisé : l'égalité des séries formelles est décidable sur les coefficients, et `addMv` est *défini* par ces coefficients — l'évaluateur les compare donc syntaxiquement. Les preuves suivantes (`coeff`) montrent le travail quand `rfl` ne suffit plus : exhiber le coefficient via `Finsupp.single` puis conclure — le pattern lecture-de-coefficient qui revient dans toute la théorie (hauteurs, itérés)." + ] + }, { "cell_type": "markdown", "id": "0b93aa2b", @@ -1501,6 +1525,14 @@ "Ces certificats sont produits par Lean sur la fermeture de dépendances compilée. Ils permettent de séparer trois dimensions : **validité formelle** (ce que le noyau accepte), **exposition pédagogique** (ce que ce notebook explique) et **maturité mathématique** (les constructions avancées encore hors périmètre)." ] }, + { + "cell_type": "markdown", + "id": "fg-interp-axioms", + "metadata": {}, + "source": [ + "**Transparence axiomatique : le `#print axioms` comme audit.** La sortie liste `propext, Classical.choice, Quot.sound` — les trois axiomes standard de Lean 4, et rien d'autre. Ce que cela certifie : ni `addMv` ni `Hom.id` (ni, par la même commande sur les autres théorèmes du lake) n'introduisent d'axiome ad hoc — aucune hypothèse smugglée sous forme d'axiome local, aucune tricherie `sorry` (un `sorry` apparaîtrait dans la liste). C'est le rituel d'hygiène des compagnons natifs : après chaque théorème majeur, l'audit axiomatique rend la preuve *inspectable* — le lecteur n'a pas à faire confiance au lake, il vérifie que tout se réduit aux fondations standard. Dans un notebook pédagogique, le geste vaut plus que le résultat : il enseigne le réflexe d'auditer ce qu'on importe, exactement comme un `#print axioms` sur une preuve de Mathlib apprend qu'elle ne repose que sur les choix constructifs attendus." + ] + }, { "cell_type": "markdown", "id": "d8593890", @@ -1899,6 +1931,20 @@ "#check FormalGroups.MvFormalGroup.nthSeries_succ" ] }, + { + "cell_type": "markdown", + "id": "fg-attendus", + "metadata": {}, + "source": [ + "### Attendus et anti-pièges (exercices 1 à 3)\n", + "\n", + "**Exercice 1 (compter l'espace ambiant).** *Attendu* : `nbVariables g = 2 * g` — l'espace `Fin g ⊕ Fin g` est la réunion disjointe de deux copies de `Fin g`, donc 2g éléments. La preuve : `Fin.card (Fin g ⊕ Fin g) = 2 * g` via `Finsupp.card` ou `Fin.card_sum`. La sortie du stub montre l'avertissement du linter (variable non référencée) — le squelette attend une définition qui *utilise* g. *Anti-piège* : répondre `g + g` syntaxiquement sans preuve d'égalité — l'énoncé demande un `Nat`, la vérification attendue est `nbVariables 2 = 4` (ou l'égalité prouvée), pas une formule non testée.\n", + "\n", + "**Exercice 2 (l'échange des blocs).** *Attendu* : `fun s => Sum.elim Sum.inr Sum.inl s` (ou un `match` équivalent) — l'involution qui échange `inl ↔ inr`. La vérification `echangeBlocsOK` teste les trois cas : inl 0 → inr 0, inr 0 → inl 0, et un point fixe... non, le troisième test vérifie l'idempotence de l'application au point (2 sur `Fin g` avec g = 2 : `Sum.inl 1`). Lire le `Bool` attendu : `echangeBlocsOK = true` seulement si l'échange est correct sur TOUTES les cases testées. *Anti-piège* : définir l'échange seulement sur `inl` (match partiel) — le type `(Fin g ⊕ Fin g) → (Fin g ⊕ Fin g)` exige la totalité, et le test échoue sur `inr`.\n", + "\n", + "**Exercice 3 (premier itéré de la loi additive).** *Attendu* : l'énoncé décommenté se prouve par `rw [nthSeries_succ]` puis les lemmes de substitution du lake — le premier itéré de `addMv` est la série linéaire identité `fun i => X i`. Intuition : itérer la loi donne F(F(x), y) − dont la partie de bas degré est la partie linéaire de F, qui pour la loi additive EST l'identité. *Anti-piège* : vouloir conclure par `rfl` — après le `rw`, le but est une égalité de fonctions vers des séries ; il faut `funext` puis l'égalité de séries (ou le lemme `nthSeries_succ` déjà orienté). Le `#check` du bas de cellule donne les noms disponibles : la preuve attendue est une composition de lemmes du lake, pas une expansion manuelle des coefficients." + ] + }, { "cell_type": "markdown", "id": "5bcb47a3", @@ -1948,4 +1994,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +} From 22921bc290c958fb64d7e1eb6414656880cf2397 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 19 Sep 2026 01:36:59 +0200 Subject: [PATCH 2/2] fix(gametheory,#16350): prose de lecture alignee sur la sortie commentee (passe drain) Co-Authored-By: Claude Sonnet 5 --- .../GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb | 4 ++-- .../SocialChoice/01b-Lean-SocialChoice-Formal.ipynb | 4 ++-- .../SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb b/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb index 6640f57be6..46729473b1 100644 --- a/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/GameTheory-23b-Lean-Assignment-Native.ipynb @@ -661,7 +661,7 @@ "id": "gt23b-interp-permutations", "metadata": {}, "source": [ - "**L'énumération exhaustive comme preuve — et sa limite.** Les six `#eval` parcourent tout `Equiv.Perm (Fin 3)` : identité 6, transpositions (5 pour 0↔1, 6 pour 0↔2, 8 pour 1↔2 attendu), puis les deux 3-cycles. Sur cette instance, le minimum **vérifié par épuisement** est 5, atteint par σ = (0↔1). Cette énumération EST une preuve d'optimalité — au sens combinatoire, rien ne lui manque. Mais sa complexité est n! : à n = 12 il y a déjà 479 millions de permutations, hors de portée d'un `#eval`. Le notebook joue donc un double jeu pédagogique : prouver *par l'épuisement* que 5 est optimal sur une instance jouet, puis *par la dualité* que 5 est optimal sur n'importe quelle taille — la méthode hongroise et son certificat dual remplaçant l'énumération, pas la complétant." + "**L'énumération exhaustive comme preuve — et sa limite.** Les six `#eval` parcourent tout `Equiv.Perm (Fin 3)` : identité 6, transpositions (5 pour 0↔1, 6 pour 0↔2, 11 pour 1↔2), puis les deux 3-cycles. Sur cette instance, le minimum **vérifié par épuisement** est 5, atteint par σ = (0↔1). Cette énumération EST une preuve d'optimalité — au sens combinatoire, rien ne lui manque. Mais sa complexité est n! : à n = 12 il y a déjà 479 millions de permutations, hors de portée d'un `#eval`. Le notebook joue donc un double jeu pédagogique : prouver *par l'épuisement* que 5 est optimal sur une instance jouet, puis *par la dualité* que 5 est optimal sur n'importe quelle taille — la méthode hongroise et son certificat dual remplaçant l'énumération, pas la complétant." ] }, { @@ -1849,7 +1849,7 @@ "source": [ "### Attendus et anti-pièges (exercices 1 à 3)\n", "\n", - "**Exercice 1 (votre matrice 2×2).** *Attendu* : une matrice dont l'identité n'est PAS optimale, par exemple `[[1, 0], [0, 1]]`... dont l'identité coûte 2 et la transposition 0 — attention, l'énoncé demande l'inverse (l'identité répond sur `[[1,0],[0,1]]`) : il faut une matrice où la permutation non-triviale bat l'identité, comme `[[5, 1], [1, 5]]` (identité 10, swap 2). Le réflexe à construire : la valeur d'une permutation se lit comme une diagonalité après réordonnancement des colonnes. *Anti-piège* : tester seulement l'identité et le swap naïf sans vérifier l'égalité 2×2 = exhaustif — sur `Fin 2` il n'y a que deux permutations, les tester toutes les deux est une preuve complète, pas un échantillon.\n", + "**Exercice 1 (votre matrice 2×2).** *Attendu* : une matrice dont l'identité n'est PAS optimale, par exemple `[[1, 0], [0, 1]]` — l'identité y coûte 2 et la transposition 0 : c'est la permutation non-triviale qui répond, exactement ce que l'énoncé demande (sur `Fin 2`, tester les deux permutations est exhaustif). Autre exemple : `[[5, 1], [1, 5]]` (identité 10, swap 2). Le réflexe à construire : la valeur d'une permutation se lit comme une diagonalité après réordonnancement des colonnes. *Anti-piège* : tester seulement l'identité et le swap naïf sans vérifier l'égalité 2×2 = exhaustif — sur `Fin 2` il n'y a que deux permutations, les tester toutes les deux est une preuve complète, pas un échantillon.\n", "\n", "**Exercice 2 (le certificat dual de votre matrice).** *Attendu* : u et v tels que dualValue = valeur optimale, avec chaque uᵢ + vⱼ ≤ C2 i j. Sur une 2×2 à swap optimal, un couple du style u = [1, 0], v ajusté fonctionne : les arêtes serrées doivent inclure les deux arêtes du swap. La démarche : partir de u = v = 0 (faisable si coûts positifs), resserrer jusqu'à ce que les arêtes serrées couvrent le matching optimal. *Anti-piège* : choisir u, v qui somment à la valeur optimale mais violent une inégalité — la valeur duale serait un plafond *non prouvé* ; la faisabilité est ce qui rend le plafond un plafond, `decide` la vérifie case par case sur `Fin 2`.\n", "\n", diff --git a/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb b/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb index 0c06899e0f..1aa143b211 100644 --- a/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb +++ b/MyIA.AI.Notebooks/GameTheory/SocialChoice/01b-Lean-SocialChoice-Formal.ipynb @@ -2307,7 +2307,7 @@ "id": "sc-interp-median", "metadata": {}, "source": [ - "**Le théorème médian, annoncé avec sa dette.** La cellule est honnête : la preuve complète n'est **pas encore** dans le lake (il manque `Fintype`, `LinearOrder`, et la cardinalité impaire du nombre d'électeurs), et l'énoncé est donné comme aspiration. C'est une situation normale dans un compagnon natif : le notebook documente l'écart entre le théorème mathématique (Black 1948 : sous unimodalité et cardinalité impaire, le pic de l'électeur médian bat toute alternative en duel) et l'état de la formalisation. L'exercice 6 fait vérifier l'énoncé sur une instance concrète (3 électeurs, pics 0.2 / 0.5 / 0.8) — une vérification d'instance n'est pas une preuve du théorème, mais elle ancre l'intuition : l'électeur médian gagne parce qu'un côté du pic contient au plus la moitié des électeurs, chacun préférant s'approcher du centre. La dette formalisation vs théorème est tracée, pas maquillée." + "**Le théorème médian, annoncé avec sa dette.** La cellule est honnête : la preuve complète n'est **pas encore** dans le lake (il manque `Fintype`, `LinearOrder`, et la cardinalité impaire du nombre d'électeurs), et l'énoncé est donné comme aspiration. C'est une situation normale dans un compagnon natif : le notebook documente l'écart entre le théorème mathématique (Black 1948 : sous unimodalité et cardinalité impaire, le pic de l'électeur médian bat toute alternative en duel) et l'état de la formalisation. L'exercice 6 fait vérifier l'énoncé sur une instance concrète à trois électeurs (pics fixés dans son énoncé) — une vérification d'instance n'est pas une preuve du théorème, mais elle ancre l'intuition : l'électeur médian gagne parce qu'un côté du pic contient au plus la moitié des électeurs, chacun préférant s'approcher du centre. La dette formalisation vs théorème est tracée, pas maquillée." ] }, { @@ -2911,7 +2911,7 @@ "\n", "**Exercice 5 (cycle de Condorcet).** *Attendu* : aucun vainqueur de Condorcet — a bat b (électeurs 0 et 2), b bat c (0 et 1), c bat a (1 et 2), le tournoi est un cycle. Le verdict à écrire : `¬ ∃ w, IsCondorcetWinner w` (ou sa version à marges de la section 6). *Anti-piège* : conclure « donc la règle majoritaire est mauvaise » — l'exercice mesure une instance ; la section Peters (impossibilités de Condorcet) montrera que TOUTE règle cohérente-Condorcet résolue perd autre chose, le cycle n'est pas une pathologie de la règle mais du domaine (cf. l'unimodalité du théorème médian : ce profil n'est pas unimodal).\n", "\n", - "**Exercice 6 (médian sur pics 0.2/0.5/0.8).** *Attendu* : B (pic 0.5) gagne les deux duels — contre A (pics 0.5 et 0.8 le préfèrent), contre C (0.2 et 0.5). Le point pédagogique : le vainqueur est le pic MÉDIAN (0.5), pas le pic moyen (0.5 aussi ici — choisir des exemples où les deux diffèrent serait plus discriminant, un réflexe de concepteur d'exercice). *Anti-piège* : vérifier seulement un duel — un vainqueur de Condorcet doit battre TOUTE alternative, et sur 3 alternatives le second duel est une ligne de plus, pas une option.\n", + "**Exercice 6 (médian sur pics 0.2/0.5/0.8).** *Attendu* : M (position 0.5) gagne les deux duels — contre A (pics 0.5 et 0.8 le préfèrent), contre D (pics 0.2 et 0.5). Le point pédagogique : le vainqueur est le pic MÉDIAN (0.5), pas le pic moyen (0.5 aussi ici — choisir des exemples où les deux diffèrent serait plus discriminant, un réflexe de concepteur d'exercice). *Anti-piège* : vérifier seulement un duel — un vainqueur de Condorcet doit battre TOUTE alternative, et sur 3 alternatives le second duel est une ligne de plus, pas une option.\n", "\n", "\n", "\n", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb index 281ffd6052..8aaeaec08a 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-30-FormalGroups-Native.ipynb @@ -997,7 +997,7 @@ "id": "fg-interp-deux-maps", "metadata": {}, "source": [ - "**Les deux `map`, disambiguisés par leurs types.** La sortie montre deux signatures : `MvFormalGroup.map` prend un morphisme d'anneaux `R →+* S` et transporte un groupe formel sur R vers un groupe formel sur S (changement de base — le même groupe, lu sur un autre anneau) ; `MvPowerSeries.map` agit au niveau des séries, coefficient par coefficient. La confusion est le piège d'API classique : les deux s'appellent `map`, mais le premier préserve la loi (c'est un morphisme de groupes formels au-dessus d'un morphisme d'anneaux) quand le second n'a aucune raison de respecter une loi quelconque — il n'est pas au courant des axiomes. La leçon Lean dépasse le cas : quand deux définitions partagent un nom, le `#check @` des signatures est le document qui les sépare ; lire le TYPE d'une fonction est souvent plus sûr que lire son nom. Le point 5 du sommaire annonce exactement ce travail de distinction." + "**Les deux `map`, disambiguisés par leurs types.** La sortie montre deux signatures : `MvFormalGroup.map` prend un morphisme d'anneaux `R →+* S` et transporte un groupe formel sur R vers un groupe formel sur S (changement de base — le même groupe, lu sur un autre anneau) ; `MvPowerSeries.map` agit au niveau des séries, coefficient par coefficient. La confusion est le piège d'API classique : les deux s'appellent `map`, mais le premier préserve la loi (c'est un morphisme de groupes formels au-dessus d'un morphisme d'anneaux) quand le second n'a aucune raison de respecter une loi quelconque — il n'est pas au courant des axiomes. La leçon Lean dépasse le cas : quand deux définitions partagent un nom, le `#check @` des signatures est le document qui les sépare ; lire le TYPE d'une fonction est souvent plus sûr que lire son nom. Le point 4 du sommaire annonce exactement ce travail de distinction." ] }, { @@ -1156,7 +1156,7 @@ "id": "fg-interp-addmv", "metadata": {}, "source": [ - "**`addMv`, l'exemple canonique — et pourquoi `rfl` suffit.** L'exemple affirme que le terme d'ordre 0 de la loi additive s'écrit X(Sum.inl 0) + X(Sum.r 0) : les deux coordonnées du `Fin g ⊕ Fin g` (l'espace ambiant du produit de deux copies) chacune portée par sa variable. Les deux corollaires qui suivent extraient le coefficient constant (0) et le coefficient linéaire (1) — la carte d'identité d'un groupe formel : pas de terme constant, partie linéaire = l'identité. La preuve par `rfl` n'est pas une économie de moyens mais un théorème déguisé : l'égalité des séries formelles est décidable sur les coefficients, et `addMv` est *défini* par ces coefficients — l'évaluateur les compare donc syntaxiquement. Les preuves suivantes (`coeff`) montrent le travail quand `rfl` ne suffit plus : exhiber le coefficient via `Finsupp.single` puis conclure — le pattern lecture-de-coefficient qui revient dans toute la théorie (hauteurs, itérés)." + "**`addMv`, l'exemple canonique — et pourquoi `rfl` suffit.** L'exemple affirme que le terme d'ordre 0 de la loi additive s'écrit X(Sum.inl 0) + X(Sum.inr 0) : les deux coordonnées du `Fin g ⊕ Fin g` (l'espace ambiant du produit de deux copies) chacune portée par sa variable. Les deux corollaires qui suivent extraient le coefficient constant (0) et le coefficient linéaire (1) — la carte d'identité d'un groupe formel : pas de terme constant, partie linéaire = l'identité. La preuve par `rfl` n'est pas une économie de moyens mais un théorème déguisé : l'égalité des séries formelles est décidable sur les coefficients, et `addMv` est *défini* par ces coefficients — l'évaluateur les compare donc syntaxiquement. Les preuves suivantes (`coeff`) montrent le travail quand `rfl` ne suffit plus : exhiber le coefficient via `Finsupp.single` puis conclure — le pattern lecture-de-coefficient qui revient dans toute la théorie (hauteurs, itérés)." ] }, { @@ -1940,7 +1940,7 @@ "\n", "**Exercice 1 (compter l'espace ambiant).** *Attendu* : `nbVariables g = 2 * g` — l'espace `Fin g ⊕ Fin g` est la réunion disjointe de deux copies de `Fin g`, donc 2g éléments. La preuve : `Fin.card (Fin g ⊕ Fin g) = 2 * g` via `Finsupp.card` ou `Fin.card_sum`. La sortie du stub montre l'avertissement du linter (variable non référencée) — le squelette attend une définition qui *utilise* g. *Anti-piège* : répondre `g + g` syntaxiquement sans preuve d'égalité — l'énoncé demande un `Nat`, la vérification attendue est `nbVariables 2 = 4` (ou l'égalité prouvée), pas une formule non testée.\n", "\n", - "**Exercice 2 (l'échange des blocs).** *Attendu* : `fun s => Sum.elim Sum.inr Sum.inl s` (ou un `match` équivalent) — l'involution qui échange `inl ↔ inr`. La vérification `echangeBlocsOK` teste les trois cas : inl 0 → inr 0, inr 0 → inl 0, et un point fixe... non, le troisième test vérifie l'idempotence de l'application au point (2 sur `Fin g` avec g = 2 : `Sum.inl 1`). Lire le `Bool` attendu : `echangeBlocsOK = true` seulement si l'échange est correct sur TOUTES les cases testées. *Anti-piège* : définir l'échange seulement sur `inl` (match partiel) — le type `(Fin g ⊕ Fin g) → (Fin g ⊕ Fin g)` exige la totalité, et le test échoue sur `inr`.\n", + "**Exercice 2 (l'échange des blocs).** *Attendu* : `fun s => Sum.elim Sum.inr Sum.inl s` (ou un `match` équivalent) — l'involution qui échange `inl ↔ inr`. La vérification `echangeBlocsOK` teste quatre croisements : `inl 0 → inr 0`, `inr 0 → inl 0`, `inl 1 → inr 1` et `inr 1 → inl 1` (les deux cases de chaque bloc pour g = 2). Lire le `Bool` attendu : `echangeBlocsOK = true` seulement si l'échange est correct sur TOUTES les cases testées. *Anti-piège* : définir l'échange seulement sur `inl` (match partiel) — le type `(Fin g ⊕ Fin g) → (Fin g ⊕ Fin g)` exige la totalité, et le test échoue sur `inr`.\n", "\n", "**Exercice 3 (premier itéré de la loi additive).** *Attendu* : l'énoncé décommenté se prouve par `rw [nthSeries_succ]` puis les lemmes de substitution du lake — le premier itéré de `addMv` est la série linéaire identité `fun i => X i`. Intuition : itérer la loi donne F(F(x), y) − dont la partie de bas degré est la partie linéaire de F, qui pour la loi additive EST l'identité. *Anti-piège* : vouloir conclure par `rfl` — après le `rw`, le but est une égalité de fonctions vers des séries ; il faut `funext` puis l'égalité de séries (ou le lemme `nthSeries_succ` déjà orienté). Le `#check` du bas de cellule donne les noms disponibles : la preuve attendue est une composition de lemmes du lake, pas une expansion manuelle des coefficients." ]