[Epic Origami #19898 — Pli 6] Compter les couplages parfaits : permanent, #P et clôture SDP (113, 126 ; 104 en veille) — ajout additif au lac assignment_lean

Part of #19898 — [Epic Origami] openai/math, Pli 6 (dernier pli pressenti du corpus, confirmé par la carte du Pli 1 : cluster « Jeux algorithmiques & matching », fil « dualité (nôtre) → comptage → SDP »). Déverrouillé par la livraison des plis 2 (#20184/#19908), 3 (#19920), 4 (#19960) et 5 (#19993).

Grain: DEEP/notebook-lean — lane myia-po-2027:CoursIA — prev: LIGHT/guard #21954

Fil narratif

Notre lac assignment_lean prouve déjà la dualité de l'affectation (Kuhn-Munkres : dualité faible, certificat gap nul, resserrement hongrois). Les familles openai/math 113 et 126 prennent le même objet — le couplage parfait d'un graphe biparti — par les deux autres bouts :

113 [formalisée, squelette lean/docs/ publié] : compter les couplages parfaits. FPRAS randomisé pour les graphes finis simples arbitraires + détection exacte du zéro + théorème d'entropie des lois de couplage (conjecture d'Anari–Oveis Gharan–Vinzant).
126 [formalisée] : clôture négative SDP — toute remontée semi-définie exacte du polytope du couplage parfait est de taille exponentielle (réfute la question de Rothvoss), déjà après décalage fixe de la slack matrix odd-cut.

Le pli relie : la dualité donne un couplage optimal en temps polynomial ; compter les couplages est #P-dur et n'admet pas d'expression compacte de type SDP — le polytope est riche exactement là où la dualité est efficace.

Veilles citées, non reprises : 104 (algorithmes quasipolynomiaux pour jeux mean-payoff/stochastiques/parité — objet game_theory_lean/minimax_lean, distinct du fil matching), 114 (comptage de bases communes de polymatroïdes), 120 [PAS-de-skel] (matching exact presque linéaire).

Organ-first (checklist #13564, répondue ici)

Série possédant la sémantique : Mathlib fournit Mathlib.LinearAlgebra.Matrix.Permanent (Matrix.permanent : somme sur permutations, + permanent_zero/one/transpose/permute_rows/cols/unique), vérifié sur la doc Mathlib4 à la création de cette issue.
Invocation du module réel : oui — le fichier neuf importe l'organe (import Mathlib.LinearAlgebra.Matrix.Permanent) et ne redéfinit rien.
Export/refactor requis : aucun — l'organe est directement consommable depuis le lac (Mathlib déjà épinglée db584cd6d46c).
Témoin négatif natif Matrix.permanent_zero / permanent_one serviront de contrôles dans le carnet.
Vérification indépendante : le carnet (tranche B) recoupe chaque valeur de permanent par énumération brute des couplages en Python — l'organe calcule, le carnet contre-vérifie.

Livrables

Tranche A — ajout additif au lac assignment_lean : fichier neuf Assignment/Counting.lean + sibling _en (convention i18n i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980 : docstrings FR/EN, énoncés/tactiques en anglais) :
- perfectMatchingSet : l'ensemble des permutations couvertes par une matrice booléenne d'adjacence ;
- théorème-pont : le permanent (Mathlib) de la matrice 0/1 associée égale le cardinal des couplages parfaits du graphe biparti ;
- cas complet : matrice tout-un → cardinal = n! ;
- exemple dégradé : n = 2, un bord manquant → exactement 1 couplage.
- lake build SUCCESS local (cache Mathlib v4.33.0-db584cd6), aucun sorry ajouté.
Tranche B — carnet ANALYSE-12-Comptage-Matching-Lean-Python.ipynb (ANALYSE-10/11 pris par EPIC Origami: Thurston — distillations exécutables (nœuds hyperboliques, tresses, automates) + « On proof and progress » relu à l'ère de la preuve IA #20404/EPIC origami : Project DarkSnail — distillation vérifiée d'un bi-hémisphère LLM, du Lean math à l'usage système 1 #21310) : statut épistémique par famille (113, 126, 104 en veille — jamais « OpenAI a prouvé X donc X »), notre pont confronté à l'énumération Python, ≥3 exercices stubbés C.1, exécuté kernel lean4-wsl (C.2).
Tranche C — sibling _en du carnet + parité de valeurs FR/EN.

Verdicts SOTA attendus

SOTA-OK : Mathlib Matrix.permanent comme moteur (organ-first ci-dessus).
INTRINSIC (checklist 6 axes répondue dans le body de la PR) : re-preuve du FPRAS (113) et de la borne SDP exponentielle (126) — hors d'échelle pédagogique ; le lac formalise les objets (couplages couverts, pont permanent↔cardinal), le carnet cite les théorèmes avec leur statut.

Acceptance

lake build local SUCCESS sur Assignment.Counting, log joint au body de la PR.
count_code_sorry.py --json (distinct_code_sorry) avant/après : zéro sorry ajouté.
Diff additif : fichiers neufs uniquement (+ imports dans les agrégateurs racine, ligne de table README du lac) ; aucun énoncé existant modifié.
Carnet exécuté C.2 (exec_count, outputs, 0 erreur), ≥3 exercices C.1, statut épistémique par famille.
Verdicts SOTA écrits ; INTRINSIC 6 axes répondus.
Catalogue COURSE_CATALOG.generated.* byte-identique à main dans la PR (régénération séparée).
_quarto.yml : entrée render pour le carnet neuf, compte du header re-mesuré.

Grain: DEEP/notebook-lean — lane myia-po-2027:CoursIA — prev: LIGHT/guard #21954

[CLAIMED] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/GameTheory/assignment_lean/Assignment/Counting.lean, MyIA.AI.Notebooks/GameTheory/assignment_lean/Assignment/Counting_en.lean, MyIA.AI.Notebooks/GameTheory/assignment_lean/Assignment.lean, MyIA.AI.Notebooks/GameTheory/assignment_lean/Assignment_en.lean, MyIA.AI.Notebooks/GameTheory/assignment_lean/README.md -- tranche A du Pli 6 : pont permanent (Mathlib) <-> cardinal des couplages parfaits, organ-first

[DELIVERED] lane myia-po-2027:CoursIA -- PR #21962 (tranche A : pont permanent <-> cardinal des couplages parfaits, lake build SUCCESS 4 cibles 0 warning, sorry reel 0 -> 0). L'issue reste ouverte : tranches B (carnet ANALYSE-12) et C (sibling/parity) a livrer dans les cycles suivants.

[CLAIMED] lane myia-po-2027:CoursIA -- tranche B : carnet ANALYSE-12-Comptage-Matching-Lean-Python.ipynb (pont card_eq_permanent confronte a l'enumeration Python brute, controles natifs permanent_zero/one, statut epistemique 113/126/104, >=3 exercices C.1) -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python.ipynb, _quarto.yml (tranche C sibling/quarto suivra en PR separee)

Grain: DEEP/notebook-lean — lane myia-po-2027:CoursIA — prev: DEEP/lean #21962

Note : branche stackee sur la tete de la tranche A (e846fc0) -- les cellules Lean du carnet consomment Assignment.Counting qui n'existe que sur cette branche jusqu'au merge de #21962 ; retarget vers main au merge.

[DELIVERED] lane myia-po-2027:CoursIA -- PR #22025 (tranche B : carnet ANALYSE-12 exécuté, 10/10 cellules code, axioms propres, 4/4 accords). L'issue reste ouverte pour la tranche C (sibling _en + parité).

Fix(notebook): chaine de navigation ANALYSE -- arete 12 -> 11 et 11 -…

Add(lean,#21958): Pli 6 tranche A -- pont permanent/couplages parfait…

Add(notebook,#21958): Pli 6 tranche B -- carnet ANALYSE-12 Comptage-M…

Grain: DEEP/notebook-lean — lane myia-po-2023:CoursIA — prev: DEEP/notebook-python #22373

[CLAIMED] lane myia-po-2023:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/ANALYSE/README.md, _quarto.yml

Portee : tranche C de cette issue — le sibling _en du carnet. Tranche A livree (#21962 : Counting.lean + Counting_en.lean presents dans le lac) et tranche B livree (#22025 : le carnet FR execute). Reste la traduction anglaise du carnet avec parite de valeurs.

Confrontation prealable, mesuree : check_lane_claim.py 21958 rend CLEAR sur ce chemin (le claim po-2027 de la tranche B est perime) ; la convention de la serie est mesuree sur un jumeau existant, pas supposee — ANALYSE-09-Tuilage-Aperiodique et son _en portent 5/5 cellules de code byte-identiques et 5/5 sorties identiques, exec_counts 1..5 des deux cotes, et le jumeau ne porte pas metadata.papermill. La parite FR/EN n'est donc pas une re-execution mais une egalite verifiable ; je la prouverai par empreinte dans le body de la PR.

Note de collision : _quarto.yml est declare dans le scope d'une PR ouverte d'une autre lane (#21733), mais son diff ne touche pas ce fichier (verifie par gh pr view 21733 --json files) — l'entree render ajoutee porte sur le bloc ANALYSE.

Portee hors de mon geste : la cloture de l'issue revient au coordinateur ; je livre le sibling et son cablage.

[DELIVERED] lane myia-po-2023:CoursIA -- PR #22383 (tranche C : jumeau anglais de ANALYSE-12)

Tranche C livrée. Les trois tranches de l'issue sont désormais servies : A (#21962) et B (#22025) déjà mergées, C dans #22383.

Ce que la tranche C apporte, et ce que je n'ai pas fait :

jumeau ANALYSE-12-Comptage-Matching-Lean-Python_en.ipynb : 30 cellules, 20/20 markdown traduites, 10/10 cellules de code byte-identiques au FR, 10/10 sorties identiques, execution_count 1-10, metadata.papermill absent. La convention est mesurée sur la paire ANALYSE-09 FR/_en déjà sur main, pas supposée ;
la parité annoncée est une byte-identité, pas une ré-exécution : le lac assignment_lean n'est pas construit sur ce siège, donc les sondes lake env lean du carnet ne peuvent pas y être rejouées. Aucune cellule du FR n'est modifiée, donc C.2 n'appelle pas de re-exécution — mais je préfère l'écrire que le laisser deviner ;
la table du README de la série portait deux défauts indépendants du jumeau, corrigés dans le même geste : la ligne ANALYSE-05 y figurait deux fois à l'identique, et ANALYSE-09 en était absente alors que le carnet et son jumeau existent. Les trois jumeaux présents (07, 09, 12) y sont maintenant cités, sur le modèle d'ANALYSE-06 ;
_quarto.yml n'est pas touché : liste générée, régénérée par le cron catalogue (règle HARD 5). L'entrée _en d'ANALYSE-12 apparaîtra au prochain passage.

Gardes au head de la branche : prose rc=0, activity-leak rc=0, source-collapse 0 flagged, output-collapse 0 flagged, outputs-required 0 occurrence, duplicate-index OK, twin-index-collisions OK, deaccent 0 TOTAL, pre-commit complet passé. check_twin_parity.py ne couvre pas la série ANALYSE — son silence n'est pas un vert, d'où la mesure directe.

La clôture de l'issue revient au coordinateur.

Fix(translation,#21958): ANALYSE-12 _en -- ids recopies, arete de nav…

Fix(translation,#21958): ligne reciproque French version dans la Navi…

Fix(analyse,#21958): ligne ANALYSE-09 du README -- 'quatre fenetres' …

Add(notebook,#21958): Pli 6 tranche C -- jumeau anglais de ANALYSE-12…

Navigation Menu

Repository navigation

[Epic Origami #19898 — Pli 6] Compter les couplages parfaits : permanent, #P et clôture SDP (113, 126 ; 104 en veille) — ajout additif au lac assignment_lean #21958

Fil narratif

Organ-first (checklist #13564, répondue ici)

Livrables

Verdicts SOTA attendus

Acceptance

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

[Epic Origami #19898 — Pli 6] Compter les couplages parfaits : permanent, #P et clôture SDP (113, 126 ; 104 en veille) — ajout additif au lac assignment_lean #21958

Description

Fil narratif

Organ-first (checklist #13564, répondue ici)

Livrables

Verdicts SOTA attendus

Acceptance

Activity

jsboige commented on Oct 22, 2026

jsboige commented on Oct 22, 2026

jsboige commented on Oct 22, 2026

jsboige commented on Oct 22, 2026

jsboige commented on Oct 24, 2026

jsboige commented on Oct 24, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions