Skip to content

docs(lean,#13405): dedupliquer la section assignment_lean de GameTheory/LEAN_INVENTORY - #13431

Merged
jsboige merged 1 commit into
mainfrom
feature/13405-lean-inv-dedup
Aug 29, 2026
Merged

jsboige merged 1 commit into
mainfrom
feature/13405-lean-inv-dedup

Conversation

@jsboige

@jsboige jsboige commented Aug 29, 2026

Copy link
Copy Markdown
Owner

Grain: LIGHT/docs-lean — lane myia-po-2023:CoursIA-2 — prev: LIGHT/pedagogy #13429

Summary

GameTheory/LEAN_INVENTORY.md portait deux sections ### 10. assignment_lean (la 2e après ### 11., numérotation non monotone 11→10). Défaut découvert pendant la francisation #13404 et conservé là-bas (francisation ≠ refonte). Cette PR déduplique en fusionnant.

Fusion = union des deux occurrences, positionnée à l'emplacement de la 1re (ordre 9→10→11 restauré) :

Élément Source
Table 5 lignes (dont row Assignment/*_en.lean ×4, EPIC #4980) 2e occurrence
Descriptions sémantiques par fichier (cost matrix/permutation, potentiels u/v, certificat zero-gap, Hungarian tightening) 1re occurrence, croisées avec les noms de théorèmes de la 2e
Build lake build Assignment Assignment_en — SUCCESS (8665 jobs, PR #12614), 0 sorry (distinct_code_sorry = 0) 2e (surset du build simple de la 1re)
Key theorems + hommage Munkres (1930-2026) 1re
Status COMPLETE + companions GT-27 (scipy) / GT-27b (lean4-wsl, EPIC #11703) 2e

Validation

  • Numérotation finale 1..11 monotone (11 sections, vérifié par regex).
  • check_docs_links.py --check : OK (5209 liens, 0 cassé).
  • Le deletions>insertions (−27/+10) est le but même de la déduplication — contenu UNIQUE des deux sections préservé (grep post-fusion : siblings, 8665 jobs, GT-27b, Key theorems tous présents).
  • ## Remaining Proving Targets et la suite du fichier inchangés.
  • Catalogue byte-identique à main.

Closes #13405

Co-Authored-By: Claude-Code noreply@anthropic.com

…ry/LEAN_INVENTORY

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 <noreply@anthropic.com>
@jsboige

jsboige commented Aug 29, 2026

Copy link
Copy Markdown
Owner Author

[Hermes] — review c7dd5b6b : LGTM — fusion correcte, union sans perte (contrainte token : COMMENT only, auteur jsboige).

Vérifié sur le diff complet (+10/-27, 1 fichier) :

  1. Le défaut était réel : ### 10. assignment_lean apparaissait deux fois, la 2e après ### 11. (numérotation non monotone 11→10).
  2. La fusion est bien une union, pas un choix : la 1re occurrence hérite de la table enrichie de la 2e (ligne Assignment/*_en.lean ×4 EPIC i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 ajoutée), des noms de théorèmes par fichier (dualValue_eq_of_edges, kuhn_munkres_correct...), du build à 8665 jobs réf. feat(gametheory,#12598): lake assignment_lean — squelette de correction Kuhn-Munkres (dualité LP, resserrement hongrois) #12614, et du status COMPLETE avec companions GT-27/GT-27b. Rien de l'une ou l'autre des deux occurrences n'est perdu — j'ai comparé champ par champ.
  3. L'ordre 9→10→11 est restauré et la 2e occurrence entièrement supprimée.
  4. Séparation des responsabilités propre : le défaut découvert pendant docs(lean,#13402): franciser les 4 LEAN_INVENTORY.md EN->FR (Tweety, Planners, QuantConnect, GameTheory) #13404 est traité ici au lieu d'être mélangé à la francisation.

@github-actions github-actions Bot added variation-tag-genre-offlist GENRE hors de l'enumeration variation-protocol §1 lane-claim-absent Closing issue carries no claim at all (#10223) labels Aug 29, 2026
@jsboige
jsboige merged commit 340cea8 into main Aug 29, 2026
17 of 18 checks passed
@jsboige
jsboige deleted the feature/13405-lean-inv-dedup branch September 2, 2026 13:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

lane-claim-absent Closing issue carries no claim at all (#10223) variation-tag-genre-offlist GENRE hors de l'enumeration variation-protocol §1

Projects

None yet

Development

Successfully merging this pull request may close these issues.

docs(lean): GameTheory/LEAN_INVENTORY.md — section dupliquee '### 10. assignment_lean' (numerotation 11->10)

1 participant