GameTheory 23b — Le lake assignment_lean par son certificat (compagnon natif)

Navigation : << 27-Munkres-Assignment (track principal) | Index | assignment_lean/

Autruche pédagogique : le notebook GT-23 implémente la méthode hongroise en Python (labels, arbre hongrois, scipy.optimize.linear_sum_assignment) et vérifie son triple test numériquement. Ce compagnon 23b exécute le lake Lean assignment_lean sous kernel natif lean4-wsl : les mêmes énoncés — dualité faible, certificat à gap nul, invariant de sortie, resserrement hongrois — deviennent des théorèmes prouvés par le noyau, et nous terminons sur une preuve complète qu’une affectation concrète 3×3 est optimale, sans énumérer les factorielles.

Hommage : James R. Munkres (1930–2026), co-éponyme de l’algorithme de Kuhn-Munkres (Kuhn 1955 ; Munkres 1957) — le récit historique est dans le GT-23.

1. Le lake importé — quatre modules, une chaîne

Le lake suit la convention i18n du dépôt (EPIC #4980) : chaque module français a son sibling _en. La chaîne d’imports est linéaire — KuhnMunkres → Optimality → Duality → Definitions — un seul import charge donc tout le lake.

import Assignment.KuhnMunkres

open Assignment
import Assignment.KuhnMunkres
open Assignment
--% env 0
Raw input {"cmd": "import Assignment.KuhnMunkres\n\nopen Assignment"}
Raw output {"env": 0}

Lecture du résultat

L’import passe sans erreur : les .olean du lake (compilés par lake build Assignment) sont résolus par le kernel. Le lake expose dix déclarations publiques, que nous vérifions d’un coup — ces signatures SONT le plan du cours :

-- Module Definitions — le probleme primal
#check Assignment.value
#check Assignment.IsOptimal

-- Module Duality — le couple dual
#check Assignment.DualFeasible
#check Assignment.dualValue
#check Assignment.weak_duality

-- Module Optimality — le certificat
#check Assignment.dualValue_eq_of_edges
#check Assignment.optimality_of_zero_gap

-- Module KuhnMunkres — la charpente de correction
#check Assignment.EqEdge
#check Assignment.kuhn_munkres_correct
#check Assignment.dualFeasible_tighten
-- Module Definitions — le probleme primal
 Assignment.value {n : ℕ} (C : Fin n → Fin n → ℤ) (σ : Equiv.Perm (Fin n)) : ℤ
 Assignment.IsOptimal {n : ℕ} (C : Fin n → Fin n → ℤ) (σ : Equiv.Perm (Fin n)) : Prop
-- Module Duality — le couple dual
 Assignment.DualFeasible {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) : Prop
 Assignment.dualValue {n : ℕ} (u v : Fin n → ℤ) : ℤ
 Assignment.weak_duality {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (h : DualFeasible C u v)
  (σ : Equiv.Perm (Fin n)) : dualValue u v ≤ value C σ
-- Module Optimality — le certificat
 Assignment.dualValue_eq_of_edges {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (σ : Equiv.Perm (Fin n))
  (h : ∀ (i : Fin n), u i + v (σ i) = C i (σ i)) : dualValue u v = value C σ
 Assignment.optimality_of_zero_gap {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (σ : Equiv.Perm (Fin n))
  (h : DualFeasible C u v) (heq : dualValue u v = value C σ) : IsOptimal C σ
-- Module KuhnMunkres — la charpente de correction
 Assignment.EqEdge {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (i j : Fin n) : Prop
 Assignment.kuhn_munkres_correct {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (σ : Equiv.Perm (Fin n))
  (h : DualFeasible C u v) (heq : ∀ (i : Fin n), EqEdge C u v i (σ i)) : IsOptimal C σ
 Assignment.dualFeasible_tighten {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (S T : Finset (Fin n))
  (h : DualFeasible C u v) (δ : ℤ) (hδ : 0 ≤ δ) (hmargin : ∀ i ∈ S, ∀ j ∉ T, δ ≤ C i j - (u i + v j)) :
  DualFeasible C (fun i => if i ∈ S then u i + δ else u i) fun j => if j ∈ T then v j - δ else v j
--% env 1
Raw input {"cmd": "-- Module Definitions \u2014 le probleme primal\n#check Assignment.value\n#check Assignment.IsOptimal\n\n-- Module Duality \u2014 le couple dual\n#check Assignment.DualFeasible\n#check Assignment.dualValue\n#check Assignment.weak_duality\n\n-- Module Optimality \u2014 le certificat\n#check Assignment.dualValue_eq_of_edges\n#check Assignment.optimality_of_zero_gap\n\n-- Module KuhnMunkres \u2014 la charpente de correction\n#check Assignment.EqEdge\n#check Assignment.kuhn_munkres_correct\n#check Assignment.dualFeasible_tighten", "env": 0}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "Assignment.value {n : ℕ} (C : Fin n → Fin n → ℤ) (σ : Equiv.Perm (Fin n)) : ℤ"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 6}, "data": "Assignment.IsOptimal {n : ℕ} (C : Fin n → Fin n → ℤ) (σ : Equiv.Perm (Fin n)) : Prop"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 6}, "data": "Assignment.DualFeasible {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) : Prop"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 6}, "data": "Assignment.dualValue {n : ℕ} (u v : Fin n → ℤ) : ℤ"}, {"severity": "info", "pos": {"line": 8, "column": 0}, "endPos": {"line": 8, "column": 6}, "data": "Assignment.weak_duality {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (h : DualFeasible C u v)\n (σ : Equiv.Perm (Fin n)) : dualValue u v ≤ value C σ"}, {"severity": "info", "pos": {"line": 11, "column": 0}, "endPos": {"line": 11, "column": 6}, "data": "Assignment.dualValue_eq_of_edges {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (σ : Equiv.Perm (Fin n))\n (h : ∀ (i : Fin n), u i + v (σ i) = C i (σ i)) : dualValue u v = value C σ"}, {"severity": "info", "pos": {"line": 12, "column": 0}, "endPos": {"line": 12, "column": 6}, "data": "Assignment.optimality_of_zero_gap {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (σ : Equiv.Perm (Fin n))\n (h : DualFeasible C u v) (heq : dualValue u v = value C σ) : IsOptimal C σ"}, {"severity": "info", "pos": {"line": 15, "column": 0}, "endPos": {"line": 15, "column": 6}, "data": "Assignment.EqEdge {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (i j : Fin n) : Prop"}, {"severity": "info", "pos": {"line": 16, "column": 0}, "endPos": {"line": 16, "column": 6}, "data": "Assignment.kuhn_munkres_correct {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (σ : Equiv.Perm (Fin n))\n (h : DualFeasible C u v) (heq : ∀ (i : Fin n), EqEdge C u v i (σ i)) : IsOptimal C σ"}, {"severity": "info", "pos": {"line": 17, "column": 0}, "endPos": {"line": 17, "column": 6}, "data": "Assignment.dualFeasible_tighten {n : ℕ} (C : Fin n → Fin n → ℤ) (u v : Fin n → ℤ) (S T : Finset (Fin n))\n (h : DualFeasible C u v) (δ : ℤ) (hδ : 0 ≤ δ) (hmargin : ∀ i ∈ S, ∀ j ∉ T, δ ≤ C i j - (u i + v j)) :\n DualFeasible C (fun i => if i ∈ S then u i + δ else u i) fun j => if j ∈ T then v j - δ else v j"}], "env": 1}

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.

2. Le problème sur un exemple fil rouge : trois agents, trois tâches

Toute la suite travaille sur la même matrice de coûts 3×3 — celle de la section 2 de GT-23 : l’agent \(i\) coûte \(C_{ij}\) à affecter à la tâche \(j\), et on minimise le coût total. En Lean, la matrice est une fonction Fin 3 → Fin 3 → ℤ (arithmétique entière exacte, comme l’algorithme pédagogique de GT-23) :

-- La matrice des couts de GT-23 (section 2)
def C3 : Fin 3 → Fin 3 → ℤ := ![![4, 1, 3], ![2, 0, 5], ![3, 2, 2]]

#eval C3 0 1   -- cout d'affecter l'agent 0 a la tache 1
#eval C3 1 2   -- cout d'affecter l'agent 1 a la tache 2
-- La matrice des couts de GT-23 (section 2)
def C3 : Fin 3 → Fin 3 → ℤ := ![![4, 1, 3], ![2, 0, 5], ![3, 2, 2]]
 1
 5
--% env 2
Raw input {"cmd": "-- La matrice des couts de GT-23 (section 2)\ndef C3 : Fin 3 \u2192 Fin 3 \u2192 \u2124 := ![![4, 1, 3], ![2, 0, 5], ![3, 2, 2]]\n\n#eval C3 0 1 -- cout d'affecter l'agent 0 a la tache 1\n#eval C3 1 2 -- cout d'affecter l'agent 1 a la tache 2", "env": 1}
Raw output {"messages": [{"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 5}, "data": "1"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 5}, "data": "5"}], "env": 2}

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.

3. La valeur d’une affectation (Assignment.value)

Une affectation est un matching parfait : chaque agent reçoit exactement une tâche, chaque tâche un agent — c’est une permutation Equiv.Perm (Fin 3). Sa valeur est la somme des coûts des arêtes empruntées (Assignment.value : \(\sum_i C_{i,\sigma(i)}\)). Il y a \(3! = 6\) affectations ; évaluons-les toutes :

-- Les 6 permutations de Fin 3, de la plus simple aux 3-cycles
#eval Assignment.value C3 (Equiv.refl _)                       -- identite
#eval Assignment.value C3 (Equiv.swap (0 : Fin 3) 1)           -- transposition 0<->1
#eval Assignment.value C3 (Equiv.swap (0 : Fin 3) 2)           -- transposition 0<->2
#eval Assignment.value C3 (Equiv.swap (1 : Fin 3) 2)           -- transposition 1<->2
#eval Assignment.value C3 ((Equiv.swap (0 : Fin 3) 1).trans (Equiv.swap (0 : Fin 3) 2))
#eval Assignment.value C3 ((Equiv.swap (0 : Fin 3) 1).trans (Equiv.swap (0 : Fin 3) 2)).symm
-- Les 6 permutations de Fin 3, de la plus simple aux 3-cycles
 6
 5
 6
 11
 9
 7
--% env 3
Raw input {"cmd": "-- Les 6 permutations de Fin 3, de la plus simple aux 3-cycles\n#eval Assignment.value C3 (Equiv.refl _) -- identite\n#eval Assignment.value C3 (Equiv.swap (0 : Fin 3) 1) -- transposition 0<->1\n#eval Assignment.value C3 (Equiv.swap (0 : Fin 3) 2) -- transposition 0<->2\n#eval Assignment.value C3 (Equiv.swap (1 : Fin 3) 2) -- transposition 1<->2\n#eval Assignment.value C3 ((Equiv.swap (0 : Fin 3) 1).trans (Equiv.swap (0 : Fin 3) 2))\n#eval Assignment.value C3 ((Equiv.swap (0 : Fin 3) 1).trans (Equiv.swap (0 : Fin 3) 2)).symm", "env": 2}
Raw output {"messages": [{"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 5}, "data": "6"}, {"severity": "info", "pos": {"line": 3, "column": 0}, "endPos": {"line": 3, "column": 5}, "data": "5"}, {"severity": "info", "pos": {"line": 4, "column": 0}, "endPos": {"line": 4, "column": 5}, "data": "6"}, {"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 5}, "data": "11"}, {"severity": "info", "pos": {"line": 6, "column": 0}, "endPos": {"line": 6, "column": 5}, "data": "9"}, {"severity": "info", "pos": {"line": 7, "column": 0}, "endPos": {"line": 7, "column": 5}, "data": "7"}], "env": 3}

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.

Lecture du résultat

Le minimum est 5, atteint par la transposition \(\sigma^* = (0 \leftrightarrow 1)\) : l’agent 0 prend la tâche 1 (coût 1), l’agent 1 la tâche 0 (coût 2), l’agent 2 la tâche 2 (coût 2). Ici l’énumération suffit — 6 cas. Mais en taille \(n\) il y a \(n!\) affectations : 23 pour \(n=4\)… mais 362 880 pour \(n=9\). Énumérer n’est pas prouver : il faut un certificat, dont la taille ne croît pas factoriellement. C’est tout l’objet du lake.

4. Le couple dual (Assignment.DualFeasible, Assignment.dualValue)

La lecture LP du problème (GT-23 section 3) associe à chaque ligne \(i\) un potentiel \(u_i\) et à chaque colonne \(j\) un potentiel \(v_j\). Le couple est dual-réalisable si \(u_i + v_j \leq C_{ij}\) pour toute paire — ce sont exactement les labels de l’algorithme hongrois. Sa valeur duale est \(\sum_i u_i + \sum_j v_j\) :

-- Un couple dual pour C3 (celui que la methode hongroise produit en terminant)
def u3 : Fin 3 → ℤ := ![1, 0, 0]
def v3 : Fin 3 → ℤ := ![2, 0, 2]

#eval Assignment.dualValue u3 v3
-- Un couple dual pour C3 (celui que la methode hongroise produit en terminant)
def u3 : Fin 3 → ℤ := ![1, 0, 0]
def v3 : Fin 3 → ℤ := ![2, 0, 2]
 5
--% env 4
Raw input {"cmd": "-- Un couple dual pour C3 (celui que la methode hongroise produit en terminant)\ndef u3 : Fin 3 \u2192 \u2124 := ![1, 0, 0]\ndef v3 : Fin 3 \u2192 \u2124 := ![2, 0, 2]\n\n#eval Assignment.dualValue u3 v3", "env": 3}
Raw output {"messages": [{"severity": "info", "pos": {"line": 5, "column": 0}, "endPos": {"line": 5, "column": 5}, "data": "5"}], "env": 4}

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.

Lecture du résultat

La valeur duale vaut 5 — exactement la valeur de \(\sigma^*\). Cette coïncidence n’en est pas une : c’est le gap de dualité nul, le certificat que la méthode hongroise produit en terminant. Encore faut-il prouver que 5 est inévitable des deux côtés — c’est la dualité faible.

5. Dualité faible (Assignment.weak_duality) : le plancher

Théorème (dualité faible) — pour tout couple dual-réalisable \((u, v)\) et toute affectation \(\sigma\) :

\[\text{dualValue}(u,v) \;\leq\; \text{value}(\sigma)\]

Aucune affectation ne peut descendre sous la valeur duale. La preuve du lake réindexe \(\sum_j v_j\) le long de la permutation (un matching parfait visite chaque colonne exactement une fois) puis majore terme à terme par réalisabilité duale. Vérifions qu’elle ne repose sur rien de caché :

#print axioms Assignment.weak_duality
 'Assignment.weak_duality' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 5
Raw input {"cmd": "#print axioms Assignment.weak_duality", "env": 4}
Raw output {"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "'Assignment.weak_duality' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 5}

Lecture du résultat

[propext, Classical.choice, Quot.sound] — le triple standard : uniquement les axiomes logiques de Lean/Mathlib, aucun axiome mathématique ajouté, aucun sorry. La preuve est close par le noyau.

6. Le certificat à gap nul (Assignment.optimality_of_zero_gap)

Si \(\sigma\) et \((u,v)\) atteignent le même bord — valeur primale = valeur duale — alors \(\sigma\) est optimale : la dualité faible rend impossible tout \(\tau\) strictement meilleur. Le lake décompose ce certificat en deux pas :

  1. Assignment.dualValue_eq_of_edges — si toutes les arêtes du matching sont des arêtes d’égalité (\(u_i + v_{\sigma(i)} = C_{i,\sigma(i)}\), définition Assignment.EqEdge), les valeurs primale et duale coïncident ;
  2. Assignment.optimality_of_zero_gap — dual réalisable + valeurs égales ⇒ Assignment.IsOptimal.

Vérifions les trois arêtes de \(\sigma^*\) sur notre fil rouge :

-- Les 3 aretes du matching sigma* = (0 <-> 1) sont des aretes d'egalite
example : Assignment.EqEdge C3 u3 v3 0 1 := by
  show u3 0 + v3 1 = C3 0 1; decide
example : Assignment.EqEdge C3 u3 v3 1 0 := by
  show u3 1 + v3 0 = C3 1 0; decide
example : Assignment.EqEdge C3 u3 v3 2 2 := by
  show u3 2 + v3 2 = C3 2 2; decide

#print axioms Assignment.dualValue_eq_of_edges
#print axioms Assignment.optimality_of_zero_gap
-- Les 3 aretes du matching sigma* = (0 <-> 1) sont des aretes d'egalite
example : Assignment.EqEdge C3 u3 v3 0 1 := by
  show u3 0 + v3 1 = C3 0 1; decide
example : Assignment.EqEdge C3 u3 v3 1 0 := by
  show u3 1 + v3 0 = C3 1 0; decide
example : Assignment.EqEdge C3 u3 v3 2 2 := by
  show u3 2 + v3 2 = C3 2 2; decide
 'Assignment.dualValue_eq_of_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
 'Assignment.optimality_of_zero_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 6
Raw input {"cmd": "-- Les 3 aretes du matching sigma* = (0 <-> 1) sont des aretes d'egalite\nexample : Assignment.EqEdge C3 u3 v3 0 1 := by\n show u3 0 + v3 1 = C3 0 1; decide\nexample : Assignment.EqEdge C3 u3 v3 1 0 := by\n show u3 1 + v3 0 = C3 1 0; decide\nexample : Assignment.EqEdge C3 u3 v3 2 2 := by\n show u3 2 + v3 2 = C3 2 2; decide\n\n#print axioms Assignment.dualValue_eq_of_edges\n#print axioms Assignment.optimality_of_zero_gap", "env": 5}
Raw output {"messages": [{"severity": "info", "pos": {"line": 9, "column": 0}, "endPos": {"line": 9, "column": 6}, "data": "'Assignment.dualValue_eq_of_edges' depends on axioms: [propext, Classical.choice, Quot.sound]"}, {"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "'Assignment.optimality_of_zero_gap' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 6}

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.

Lecture du résultat

Trois decide passent : \(u_0 + v_1 = 1 + 0 = 1 = C_{01}\), \(u_1 + v_0 = 0 + 2 = 2 = C_{10}\), \(u_2 + v_2 = 0 + 2 = 2 = C_{22}\). Les deux théorèmes du certificat reposent sur le triple standard uniquement.

7. La charpente de correction (Assignment.KuhnMunkres)

Le dernier module assemble l’invariant de sortie de l’algorithme et son étape de progression :

  • Assignment.kuhn_munkres_correct — dual réalisable + toutes les arêtes du matching dans le graphe d’égalité ⇒ optimal. C’est l’assemblage exact des deux sections précédentes : c’est ce que la méthode hongroise garantit en terminant, sans jamais consulter un solveur extérieur ;
  • Assignment.dualFeasible_tighten — le resserrement hongrois (\(u_i \mathrel{+}= \delta\) sur des lignes, \(v_j \mathrel{-}= \delta\) sur des colonnes) préserve la réalisabilité duale, sous l’hypothèse que \(\delta\) ne dépasse la marge d’aucune arête sortante. C’est l’étape qui, répétée, fait croître le graphe d’égalité jusqu’à permettre l’augmentation.
#print axioms Assignment.kuhn_munkres_correct
#print axioms Assignment.dualFeasible_tighten
 'Assignment.kuhn_munkres_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
 'Assignment.dualFeasible_tighten' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 7
Raw input {"cmd": "#print axioms Assignment.kuhn_munkres_correct\n#print axioms Assignment.dualFeasible_tighten", "env": 6}
Raw output {"messages": [{"severity": "info", "pos": {"line": 1, "column": 0}, "endPos": {"line": 1, "column": 6}, "data": "'Assignment.kuhn_munkres_correct' depends on axioms: [propext, Classical.choice, Quot.sound]"}, {"severity": "info", "pos": {"line": 2, "column": 0}, "endPos": {"line": 2, "column": 6}, "data": "'Assignment.dualFeasible_tighten' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 7}

8. Le certificat complet : optimalité prouvée par le noyau

Assemblons tout sur le fil rouge. Deux decide établissent les hypothèses (réalisabilité duale de \((u_3, v_3)\) pour \(C_3\) ; arêtes toutes d’égalité), et Assignment.kuhn_munkres_correct conclut : \(\sigma^*\) est optimale pour \(C_3\) — une preuve vérifiée par le noyau Lean, sans énumération des 6 permutations (et qui passerait identique en taille \(n\), là où l’énumération explose en \(n!\)) :

theorem C3_dual_feasible : Assignment.DualFeasible C3 u3 v3 := by
  show ∀ i j : Fin 3, u3 i + v3 j ≤ C3 i j; decide

theorem optimal_C3 : Assignment.IsOptimal C3 (Equiv.swap (0 : Fin 3) 1) :=
  Assignment.kuhn_munkres_correct C3 u3 v3 (Equiv.swap (0 : Fin 3) 1)
    C3_dual_feasible
    (by show ∀ i : Fin 3, u3 i + v3 ((Equiv.swap (0 : Fin 3) 1) i)
          = C3 i ((Equiv.swap (0 : Fin 3) 1) i); decide)

#print axioms optimal_C3
theorem C3_dual_feasible : Assignment.DualFeasible C3 u3 v3 := by
  show ∀ i j : Fin 3, u3 i + v3 j ≤ C3 i j; decide
theorem optimal_C3 : Assignment.IsOptimal C3 (Equiv.swap (0 : Fin 3) 1) :=
  Assignment.kuhn_munkres_correct C3 u3 v3 (Equiv.swap (0 : Fin 3) 1)
    C3_dual_feasible
    (by show ∀ i : Fin 3, u3 i + v3 ((Equiv.swap (0 : Fin 3) 1) i)
          = C3 i ((Equiv.swap (0 : Fin 3) 1) i); decide)
 'optimal_C3' depends on axioms: [propext, Classical.choice, Quot.sound]
--% env 8
Raw input {"cmd": "theorem C3_dual_feasible : Assignment.DualFeasible C3 u3 v3 := by\n show \u2200 i j : Fin 3, u3 i + v3 j \u2264 C3 i j; decide\n\ntheorem optimal_C3 : Assignment.IsOptimal C3 (Equiv.swap (0 : Fin 3) 1) :=\n Assignment.kuhn_munkres_correct C3 u3 v3 (Equiv.swap (0 : Fin 3) 1)\n C3_dual_feasible\n (by show \u2200 i : Fin 3, u3 i + v3 ((Equiv.swap (0 : Fin 3) 1) i)\n = C3 i ((Equiv.swap (0 : Fin 3) 1) i); decide)\n\n#print axioms optimal_C3", "env": 7}
Raw output {"messages": [{"severity": "info", "pos": {"line": 10, "column": 0}, "endPos": {"line": 10, "column": 6}, "data": "'optimal_C3' depends on axioms: [propext, Classical.choice, Quot.sound]"}], "env": 8}

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.

Lecture du résultat

optimal_C3 ne dépend d’aucun axiome au-delà du triple standard. Le certificat a une taille linéaire en \(n\) (une hypothèse par ligne, une par arête du matching) : c’est précisément ce que scipy.optimize.linear_sum_assignment ne peut pas vous donner — lui répond une affectation, le lake répond une preuve.

9. Le resserrement hongrois en action (Assignment.dualFeasible_tighten)

Sur un dual trivial \(u = v = 0\) (réalisable car \(C_3 \geq 0\)), resserrons \(S = \{0\}\) (lignes) contre \(T = \{1\}\) (colonnes) avec \(\delta = 3\) — le maximum admissible : les arêtes sortantes \((0, j)\) pour \(j \notin T\) ont marges \(C_{00} = 4\) et \(C_{02} = 3\), donc \(\delta\) ne peut excéder \(3\). Le théorème du lake garantit que le couple resserré reste réalisable — et les decide vérifient ses hypothèses une à une :

-- Le couple trivial, realisable car tous les couts sont positifs
def u0 : Fin 3 → ℤ := ![0, 0, 0]
def v0 : Fin 3 → ℤ := ![0, 0, 0]

theorem u0v0_dual_feasible : Assignment.DualFeasible C3 u0 v0 := by
  show ∀ i j : Fin 3, u0 i + v0 j ≤ C3 i j; decide

-- Le couple resserre : u0 + 3 sur la ligne 0, v0 - 3 sur la colonne 1
def uTight : Fin 3 → ℤ := fun i => if i ∈ ({0} : Finset (Fin 3)) then u0 i + 3 else u0 i
def vTight : Fin 3 → ℤ := fun j => if j ∈ ({1} : Finset (Fin 3)) then v0 j - 3 else v0 j

example : Assignment.DualFeasible C3 uTight vTight :=
  Assignment.dualFeasible_tighten C3 u0 v0 {0} {1} u0v0_dual_feasible 3
    (by decide) (by decide)

#eval Assignment.dualValue uTight vTight
-- Le couple trivial, realisable car tous les couts sont positifs
def u0 : Fin 3 → ℤ := ![0, 0, 0]
def v0 : Fin 3 → ℤ := ![0, 0, 0]
theorem u0v0_dual_feasible : Assignment.DualFeasible C3 u0 v0 := by
  show ∀ i j : Fin 3, u0 i + v0 j ≤ C3 i j; decide
-- Le couple resserre : u0 + 3 sur la ligne 0, v0 - 3 sur la colonne 1
def uTight : Fin 3 → ℤ := fun i => if i ∈ ({0} : Finset (Fin 3)) then u0 i + 3 else u0 i
def vTight : Fin 3 → ℤ := fun j => if j ∈ ({1} : Finset (Fin 3)) then v0 j - 3 else v0 j
example : Assignment.DualFeasible C3 uTight vTight :=
  Assignment.dualFeasible_tighten C3 u0 v0 {0} {1} u0v0_dual_feasible 3
    (by decide) (by decide)
 0
--% env 9
Raw input {"cmd": "-- Le couple trivial, realisable car tous les couts sont positifs\ndef u0 : Fin 3 \u2192 \u2124 := ![0, 0, 0]\ndef v0 : Fin 3 \u2192 \u2124 := ![0, 0, 0]\n\ntheorem u0v0_dual_feasible : Assignment.DualFeasible C3 u0 v0 := by\n show \u2200 i j : Fin 3, u0 i + v0 j \u2264 C3 i j; decide\n\n-- Le couple resserre : u0 + 3 sur la ligne 0, v0 - 3 sur la colonne 1\ndef uTight : Fin 3 \u2192 \u2124 := fun i => if i \u2208 ({0} : Finset (Fin 3)) then u0 i + 3 else u0 i\ndef vTight : Fin 3 \u2192 \u2124 := fun j => if j \u2208 ({1} : Finset (Fin 3)) then v0 j - 3 else v0 j\n\nexample : Assignment.DualFeasible C3 uTight vTight :=\n Assignment.dualFeasible_tighten C3 u0 v0 {0} {1} u0v0_dual_feasible 3\n (by decide) (by decide)\n\n#eval Assignment.dualValue uTight vTight", "env": 8}
Raw output {"messages": [{"severity": "info", "pos": {"line": 16, "column": 0}, "endPos": {"line": 16, "column": 5}, "data": "0"}], "env": 9}

Lecture du résultat

Le couple resserré reste dual-réalisable — et sa valeur duale a crû de 0 à 3 : le resserrement est le moteur de la montée duale de l’algorithme (GT-23 section 4), et dualFeasible_tighten en est la garantie de sûreté, prouvée une fois pour toutes.

10. Exercices

Les trois exercices suivent la progression du notebook. À compléter dans une copie des cellules — les stubs ne lèvent pas d’erreur, le notebook reste exécutable de bout en bout.

-- Exercice 1 (Definitions) : votre propre matrice 2x2.
-- Construire une matrice C2 : Fin 2 → Fin 2 → ℤ dont l'affectation optimale
-- N'EST PAS l'identité (la matrice [[1, 0], [0, 1]] en est un bon
-- prototype : identité de coût 2 mais transposition de coût 0, donc
-- l'optimum est la TRANSPOSITION (Equiv.swap) — exactement ce qu'on
-- cherche à faire surgir dans le théorème optimal_C2 ci-dessous).
--
-- Etape 1 : definir C2 avec la notation ![![.., ..], ![.., ..]].
-- Etape 2 : #eval Assignment.value C2 sur Equiv.refl _ et (Equiv.swap (0 : Fin 2) 1).
-- Etape 3 : verifier que la transposition fait strictement mieux.
--
-- def C2 : Fin 2 → Fin 2 → ℤ := ![![..], ![..]]  -- TODO etudiant
example : True := trivial

-- Exercice 1 (Definitions) : votre propre matrice 2x2.
-- Construire une matrice C2 : Fin 2 → Fin 2 → ℤ dont l'affectation optimale
-- N'EST PAS l'identite (indices defies : la matrice [[1, 0], [0, 1]] repond id).
--
-- Etape 1 : definir C2 avec la notation ![![.., ..], ![.., ..]].
-- Etape 2 : #eval Assignment.value C2 sur Equiv.refl _ et (Equiv.swap (0 : Fin 2) 1).
-- Etape 3 : verifier que la transposition fait strictement mieux.
--
-- def C2 : Fin 2 → Fin 2 → ℤ := ![![..], ![..]]  -- TODO etudiant
example : True := trivial
--% env 10
Raw input {"cmd": "-- Exercice 1 (Definitions) : votre propre matrice 2x2.\n-- Construire une matrice C2 : Fin 2 \u2192 Fin 2 \u2192 \u2124 dont l'affectation optimale\n-- N'EST PAS l'identite (indices defies : la matrice [[1, 0], [0, 1]] repond id).\n--\n-- Etape 1 : definir C2 avec la notation ![![.., ..], ![.., ..]].\n-- Etape 2 : #eval Assignment.value C2 sur Equiv.refl _ et (Equiv.swap (0 : Fin 2) 1).\n-- Etape 3 : verifier que la transposition fait strictement mieux.\n--\n-- def C2 : Fin 2 \u2192 Fin 2 \u2192 \u2124 := ![![..], ![..]] -- TODO etudiant\nexample : True := trivial", "env": 9}
Raw output {"env": 10} 
-- Exercice 2 (Duality + Optimality) : le certificat de votre matrice.
-- Pour votre C2 de l'Exercice 1, trouver un couple dual (u2, v2) a gap nul
-- avec l'affectation optimale sigma2 trouvee ci-dessus, puis le PROUVER :
--
-- Etape 1 : deviner u2, v2 (sommes egales a la valeur optimale, u_i + v_j <= C2 i j partout).
-- Indice : partir de u = v = 0 et resserrer, comme en section 9.
-- Etape 2 : theorem C2_dual_feasible : Assignment.DualFeasible C2 u2 v2 := by decide
-- Etape 3 : theorem optimal_C2 : Assignment.IsOptimal C2 (Equiv.swap (0 : Fin 2) 1 :=
--   Assignment.kuhn_munkres_correct C2 u2 v2 _ C2_dual_feasible (by decide)
--
-- TODO etudiant
example : True := trivial
-- Exercice 2 (Duality + Optimality) : le certificat de votre matrice.
-- Pour votre C2 de l'Exercice 1, trouver un couple dual (u2, v2) a gap nul
-- avec l'affectation optimale sigma2 trouvee ci-dessus, puis le PROUVER :
--
-- Etape 1 : deviner u2, v2 (sommes egales a la valeur optimale, u_i + v_j <= C2 i j partout).
-- Indice : partir de u = v = 0 et resserrer, comme en section 9.
-- Etape 2 : theorem C2_dual_feasible : Assignment.DualFeasible C2 u2 v2 := by decide
-- Etape 3 : theorem optimal_C2 : Assignment.IsOptimal C2 (Equiv.swap (0 : Fin 2) 1 :=
--   Assignment.kuhn_munkres_correct C2 u2 v2 _ C2_dual_feasible (by decide)
--
-- TODO etudiant
example : True := trivial
--% env 11
Raw input {"cmd": "-- Exercice 2 (Duality + Optimality) : le certificat de votre matrice.\n-- Pour votre C2 de l'Exercice 1, trouver un couple dual (u2, v2) a gap nul\n-- avec l'affectation optimale sigma2 trouvee ci-dessus, puis le PROUVER :\n--\n-- Etape 1 : deviner u2, v2 (sommes egales a la valeur optimale, u_i + v_j <= C2 i j partout).\n-- Indice : partir de u = v = 0 et resserrer, comme en section 9.\n-- Etape 2 : theorem C2_dual_feasible : Assignment.DualFeasible C2 u2 v2 := by decide\n-- Etape 3 : theorem optimal_C2 : Assignment.IsOptimal C2 (Equiv.swap (0 : Fin 2) 1 :=\n-- Assignment.kuhn_munkres_correct C2 u2 v2 _ C2_dual_feasible (by decide)\n--\n-- TODO etudiant\nexample : True := trivial", "env": 10}
Raw output {"env": 11} 
-- Exercice 3 (KuhnMunkres) : le resserrement maximal sur la ligne 1.
-- Partir du couple trivial u0 = v0 = 0 (section 9) et resserrer S = {1} avec T = ∅ :
-- les aretes sortantes sont (1, 0), (1, 1), (1, 2) de marges 2, 0, 5.
--
-- Etape 1 : quel est le delta maximal admissible ? (reponse attendue : 0 —
-- la marge nulle de l'arete (1, 1) plafonne le resserrement).
-- Etape 2 : le verifier en executant dualFeasible_tighten avec ce delta
-- (structure de la section 9, avec S = {1} et T = ∅) :
-- example : DualFeasible C3 uTightBis vTightBis :=
--   Assignment.dualFeasible_tighten C3 u0 v0 {1} ∅ (by decide) .. (by decide) (by decide)
-- Etape 3 : expliquer (en markdown) pourquoi une marge nulle bloque la montee duale,
-- et ce que l'algorithme fait alors (indice : GT-23 section 4, colonne entree dans T).
--
-- TODO etudiant
example : True := trivial
-- Exercice 3 (KuhnMunkres) : le resserrement maximal sur la ligne 1.
-- Partir du couple trivial u0 = v0 = 0 (section 9) et resserrer S = {1} avec T = ∅ :
-- les aretes sortantes sont (1, 0), (1, 1), (1, 2) de marges 2, 0, 5.
--
-- Etape 1 : quel est le delta maximal admissible ? (reponse attendue : 0 —
-- la marge nulle de l'arete (1, 1) plafonne le resserrement).
-- Etape 2 : le verifier en executant dualFeasible_tighten avec ce delta
-- (structure de la section 9, avec S = {1} et T = ∅) :
-- example : DualFeasible C3 uTightBis vTightBis :=
--   Assignment.dualFeasible_tighten C3 u0 v0 {1} ∅ (by decide) .. (by decide) (by decide)
-- Etape 3 : expliquer (en markdown) pourquoi une marge nulle bloque la montee duale,
-- et ce que l'algorithme fait alors (indice : GT-23 section 4, colonne entree dans T).
--
-- TODO etudiant
example : True := trivial
--% env 12
Raw input {"cmd": "-- Exercice 3 (KuhnMunkres) : le resserrement maximal sur la ligne 1.\n-- Partir du couple trivial u0 = v0 = 0 (section 9) et resserrer S = {1} avec T = \u2205 :\n-- les aretes sortantes sont (1, 0), (1, 1), (1, 2) de marges 2, 0, 5.\n--\n-- Etape 1 : quel est le delta maximal admissible ? (reponse attendue : 0 \u2014\n-- la marge nulle de l'arete (1, 1) plafonne le resserrement).\n-- Etape 2 : le verifier en executant dualFeasible_tighten avec ce delta\n-- (structure de la section 9, avec S = {1} et T = \u2205) :\n-- example : DualFeasible C3 uTightBis vTightBis :=\n-- Assignment.dualFeasible_tighten C3 u0 v0 {1} \u2205 (by decide) .. (by decide) (by decide)\n-- Etape 3 : expliquer (en markdown) pourquoi une marge nulle bloque la montee duale,\n-- et ce que l'algorithme fait alors (indice : GT-23 section 4, colonne entree dans T).\n--\n-- TODO etudiant\nexample : True := trivial", "env": 11}
Raw output {"env": 12}

Attendus et anti-pièges (exercices 1 à 3)

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.

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.

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).

Conclusion

Le lake assignment_lean donne au triple test de GT-23 son statut logique complet : la dualité faible fixe le plancher, le gap nul le certificat, l’invariant de sortie la garantie de terminaison correcte, le resserrement la sûreté de chaque étape. Là où scipy.optimize.linear_sum_assignment rend une affectation, le lake rend une preuve vérifiée par le noyau — et le compagnon 23b est le lieu où ces preuves s’exécutent et se lisent.

Ce qui reste délibérément hors scope du lake (cf son README) : la preuve de terminaison et la complexité \(O(n^3)\) (Edmonds-Karp/Tomizawa), et le pont Shapley-Shubik (cœur du jeu d’affectation = solutions duales optimales), traité numériquement dans GT-23 section 5.

Références

  • Lake : assignment_lean/ — README (charpente, hors-scope, build), issue #12598 (hommage Munkres 1930–2026)
  • Kuhn (1955), The Hungarian Method for the Assignment Problem, Naval Research Logistics Quarterly 2:83–97 ; Munkres (1957), Algorithms for the Assignment and Transportation Problems, J. SIAM 5(1):32–38
  • Implémentation SOTA : scipy.optimize.linear_sum_assignment (GT-23 section 2)
  • EPIC #11703 — visibilité des lakes Lean dans les notebooks (ce compagnon est le volet natif de assignment_lean)
Retour au sommet