From c7dd5b6b74dd4b9f309095223b5e48944577b949 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 29 Aug 2026 02:45:10 +0200 Subject: [PATCH] docs(lean,#13405): dedupliquer la section assignment_lean de GameTheory/LEAN_INVENTORY MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Deux sections '### 10. assignment_lean' (lignes 217 et 256, decouverte pendant la francisation #13404, conservee la-bas : francisation != refonte). Fusion en UNE section positionnee a l'emplacement de la 1re (ordre 9-10-11 correct) : - table 5 lignes de la 2e occurrence (row siblings Assignment/*_en x4, EPIC #4980) enrichie des descriptions semantiques de la 1re (cost matrix/permutation, potentiels u/v, certificat zero-gap, Hungarian tightening) - build double-cible de la 2e (lake build Assignment Assignment_en, 8665 jobs, PR #12614) — surset du build simple de la 1re - Key theorems + hors scope de la 1re, Status COMPLETE + companions GT-27/GT-27b de la 2e Numerotation finale 1..11 monotone. check_docs_links OK (5209). Closes #13405 Co-Authored-By: Claude-Code --- .../GameTheory/LEAN_INVENTORY.md | 37 +++++-------------- 1 file changed, 10 insertions(+), 27 deletions(-) diff --git a/MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md b/MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md index 6c8e67d900..b8f2e26816 100644 --- a/MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md +++ b/MyIA.AI.Notebooks/GameTheory/LEAN_INVENTORY.md @@ -216,20 +216,23 @@ Vickrey truthfulness + first-price counter-example (#1469). Build repris par ### 10. assignment_lean -**Objective**: Formalize the correction skeleton of the Hungarian method (Kuhn 1955, Munkres 1957) — companion lake of the notebook GameTheory-27-Munkres-Assignment, hommage à James R. Munkres (1930-2026). Issue #12598 (1/3). +**Objective**: Correction skeleton of the Kuhn-Munkres (Hungarian) assignment algorithm — companion lake of the notebook GameTheory-27-Munkres-Assignment, hommage à James R. Munkres (1930-2026). Issue #12598 (1/3). The primal (cost matrix, perfect matching, value), the dual (potentials, feasibility, **weak duality**), the zero-gap optimality certificate, and the algorithm's structural invariants (equality graph, **output invariant**, **Hungarian tightening preserves dual feasibility**). Termination and O(n³) complexity deliberately out of scope. **Toolchain**: v4.32.1 | **Dependencies**: Mathlib4 | File (FR + `_en` sibling) | sorry | Description | |---------------------------|-------|-------------| -| `Assignment/Definitions.lean` | 0 | Cost matrix, perfect matching (permutation), value, optimality | -| `Assignment/Duality.lean` | 0 | Dual potentials `u`/`v`, dual feasibility, **weak duality** | -| `Assignment/Optimality.lean` | 0 | Zero-gap optimality certificate (+ equality-edge lemma) | -| `Assignment/KuhnMunkres.lean` | 0 | Equality graph, **output invariant**, **Hungarian tightening** preserves dual feasibility | +| `Assignment/Definitions.lean` | 0 | Cost matrix, perfect matching (permutation), value, optimality (`value`, `IsOptimal`) | +| `Assignment/Duality.lean` | 0 | Dual potentials `u`/`v`, dual feasibility, **weak duality** (`DualFeasible`, `dualValue`, `weak_duality`) | +| `Assignment/Optimality.lean` | 0 | Zero-gap optimality certificate + equality-edge lemma (`dualValue_eq_of_edges`, `optimality_of_zero_gap`) | +| `Assignment/KuhnMunkres.lean` | 0 | Equality graph, **output invariant**, **Hungarian tightening** preserves dual feasibility (`EqEdge`, `kuhn_munkres_correct`, `dualFeasible_tighten`) | +| `Assignment/*_en.lean` (×4) | 0 | i18n siblings (EPIC #4980) | + +**Build**: `lake build Assignment Assignment_en` — SUCCESS (8665 jobs, cf PR #12614) | **COMPLETE: 0 sorry** (distinct_code_sorry = 0) -**Build**: `lake build Assignment` — SUCCESS | **COMPLETE: 0 sorry** +**Key theorems**: `weak_duality`, `dualValue_eq_of_edges`, `optimality_of_zero_gap`, `kuhn_munkres_correct`, `dualFeasible_tighten`. -**Key theorems**: `weak_duality`, `dualValue_eq_of_edges`, `optimality_of_zero_gap`, `kuhn_munkres_correct`, `dualFeasible_tighten`. **Hors scope (délibéré)**: termination / O(n³) complexity (Edmonds-Karp/Tomizawa) — structural correction by duality suffices for the teaching purpose. +**Status**: COMPLETE. Companion notebooks: GT-27 (Python implementation + scipy SOTA) and GT-27b (native `lean4-wsl` companion — `#check` of all 10 declarations + kernel-proved `optimal_C3` certificate, EPIC #11703 visibility). --- @@ -253,26 +256,6 @@ Vickrey truthfulness + first-price counter-example (#1469). Build repris par --- -### 10. assignment_lean - -**Objective**: Correction skeleton of the Kuhn-Munkres (Hungarian) assignment algorithm (issue #12598, Munkres tribute 1930-2026): the primal (cost matrix, perfect matching, value), the dual (potentials, feasibility, **weak duality**), the zero-gap optimality certificate, and the algorithm's structural invariants (equality graph, **output invariant**, **Hungarian tightening preserves dual feasibility**). Termination and O(n³) complexity deliberately out of scope. - -**Toolchain**: v4.32.1 | **Dependencies**: Mathlib4 (v4.32.1) - -| File | sorry | Description | -|------|-------|-------------| -| `Assignment/Definitions.lean` | 0 | `value`, `IsOptimal` (primal problem) | -| `Assignment/Duality.lean` | 0 | `DualFeasible`, `dualValue`, `weak_duality` | -| `Assignment/Optimality.lean` | 0 | `dualValue_eq_of_edges`, `optimality_of_zero_gap` | -| `Assignment/KuhnMunkres.lean` | 0 | `EqEdge`, `kuhn_munkres_correct`, `dualFeasible_tighten` | -| `Assignment/*_en.lean` (×4) | 0 | i18n siblings (EPIC #4980) | - -**Build**: `lake build Assignment Assignment_en` — SUCCESS (8665 jobs, cf PR #12614) | **0 sorry** (distinct_code_sorry = 0) - -**Status**: COMPLETE. Companion notebooks: GT-27 (Python implementation + scipy SOTA) and GT-27b (native `lean4-wsl` companion — `#check` of all 10 declarations + kernel-proved `optimal_C3` certificate, EPIC #11703 visibility). - ---- - ## Remaining Proving Targets | Priority | Target | Dir | sorry | Feasibility |