Add: densite Lean natif — interpretations + attendus, 3 notebooks sous plancher (See #13410)

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, 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."
+   ]
+  },
   {
    "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]]` — 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",
+    "**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",