feat(lean,#12205): obstruction non bornee -- parite des inversions sur les chemins de swaps

[jsboige]

Grain: DEEP/lean — lane myia-po-2026:CoursIA-2 — prev: MED/docs #14377

Le gap, mesuré

Swaps/Basic.lean réfute 7 chemins Dilemme → Chicken — le vide et les six d'un pas — par decide fini (aucun_chemin_court). Le certificat du notebook GameTheory-24b (#14309, mergée le 2026-09-02) réfute tout chemin au-delà d'un budget : IMPOSSIBLE ssi d_row + d_col > k_max, et sa cellule 20 le dit sans détour — « au-delà de k_max = 12 (le diamètre du produit), tout est POSSIBLE par définition ». C'est la seule lecture non-vide, le graphe des chambres étant connexe (576 sommets, degré 6, diamètre 12 : produit cartésien de deux permutoèdres, 6 + 6).

Mesure du substrat Lean au moment de la prise : git log -3 -- .../game_theory_lean/Swaps/ ne rend que 6e47fef35 (zéro-padding, #12586) et e01623ea4 (création, #12222). #14309 n'a touché aucun fichier Lean.

Aucune des deux obstructions ne quantifie sur les chemins de longueur quelconque. C'est le volet §6 que cette PR ferme.

L'invariant

Chaque Etape est une transposition sur un seul côté, donc bascule la parité jointe du nombre d'inversions. Par récurrence sur la longueur, la parité d'un chemin est déterminée par ses deux extrémités :

theorem parite_determinee (g h : Jeu) (hg : estJeu g = true) (p : List Etape)
    (hp : applique g p = h) :
    decide (p.length % 2 = 1) = Bool.xor (signature g) (signature h)

Dilemme et Chicken partagent leur signature (true des deux côtés — row 3 inversions / col 4 pour l'un, row 4 / col 5 pour l'autre), donc tout chemin de longueur impaire est réfuté : une famille infinie (6 + 6³ + 6⁵ + …), là où l'énumération plafonne à 7 et où GT-24b plafonne à k_max.

Les deux obstructions sont complémentaires, aucune ne subsume l'autre : la distance réfute tout en dessous d'une borne mais exige de calculer la borne ; la parité ne réfute qu'une classe de longueurs, mais sans borne.

Pourquoi la relativisation aux 24 ordres stricts est obligatoire

Le lemme de bascule est faux sur les listes arbitraires : [1,1] porte 0 inversion, son image sous k = 1 est [2,2], 0 également — la parité ne bascule pas. D'où un ordresStricts : List Table littéral (les 24 permutations de 1-4) et le prédicat estJeu, qui gardent tout décidable : le lemme bascule porte 72 instances (24 tables × 3 valeurs de k) closes par un seul decide, et il transporte conjointement la validité et le renversement de parité.

Ce qui atteint main

Théorème	Ce qu'il établit
bascule	72 instances : une transposition adjacente préserve la validité et renverse la parité
signature_etape	passage à un jeu : validité préservée, signature renversée
signature_chemin	récurrence sur un chemin de longueur quelconque
parite_determinee	la parité de la longueur se lit sur les deux extrémités
aucun_chemin_impair_si_signatures_egales	forme générale (signatures égales ⇒ pas de chemin impair)
aucun_chemin_pair_si_signatures_differentes	forme duale
aucun_chemin_impair_dilemme_chicken	le témoin : famille infinie réfutée
chemin_dilemme_chicken_pair	contraposée : tout chemin Dilemme → Chicken est de longueur paire
coherence_certificat	le certificat de Basic.lean satisfait l'invariant
aucun_chemin_pair_voisin	témoin dual via voisinR12 (signature différente)

Corroboration interne : les deux autres chemins valides de Basic.lean sont de longueur 4 (chemin_valide_non_minimal) et 2 (certificat_cerf) — paires, exactement comme l'invariant le prédit. coherence_certificat le certifie pour le premier.

Preuves de validation (§B de pr-review-discipline)

B.1 — compte de sorry réel. Instrument canonique, pas grep -c :

$ python scripts/lean/count_code_sorry.py --json
  MyIA.AI.Notebooks/GameTheory/game_theory_lean :
    files 53 | naive_sorry 33 | code_sorry 2 | distinct_code_sorry 1
$ grep -c 'sorry' .../Swaps/Parite.lean
  0

distinct_code_sorry du lake inchangé à 1 avant/après — le module ajouté n'en porte aucun. (Le lake compte 33 sorry naïfs pour 1 réel : la prose des modules documente sa propre absence de sorry, d'où l'écart 33×.)

B.2 — lake build SUCCESS, local sur cette machine :

$ cd MyIA.AI.Notebooks/GameTheory/game_theory_lean && lake build Swaps
✔ [4/5] Built Swaps.Parite (1.4s)
✔ [4/5] Built Swaps (737ms)
Build completed successfully (5 jobs).
exit 0

Zéro avertissement (deux helpers Bool écrits à la main, signalés unusedSimpArgs parce que le simp set du core normalise déjà l'algèbre du xor, ont été retirés plutôt que gardés — un lemme mort dans un module certifié est du bruit pour le relecteur suivant).

B.3 — Proof integrity : NON APPLICABLE, et pour les deux raisons que la règle demande d'écrire explicitement plutôt que de sauter en silence :

• (a) le job n'est pas câblé sur ce lake. Mesure mécanique : grep -ln 'lean-axiom' .github/workflows/*.yml (moins lean-axiom.yml) rend 8 workflows — asymmetric-information, conway, galois, grothendieck, knot, mimo, sensitivity, social-choice. lean-game-theory.yml n'y est pas : c'est lui qui se déclenche sur game_theory_lean/**.lean (donc sur cette PR), et il appelle lean-build.yml, pas lean-axiom.yml.
• (b) les target-modules du seul workflow axiom touchant ce lake n'atteignent pas le module. lean-social-choice.yml appelle bien lean-axiom.yml, mais ses paths: sont bornés à SocialChoice/** + Abstraction/** — une PR ne touchant que Swaps/ ne le déclenche pas — et ses target-modules sont épinglés à une liste explicite de modules SocialChoice.* / Abstraction, que Swaps.Parite n'atteint ni directement ni par clôture d'imports (Swaps n'importe rien de SocialChoice, ni l'inverse).

Ce qui couvre effectivement cette PR : lean-game-theory.yml → lean-build.yml avec sorry-filter-mode: real — un build complet du lake plus le filtre sorry réel. C'est un gate de compilation + dette, pas le gate d'axiomes (native_decide / sorryAx / Classical.choice). Le module n'utilise que rfl, decide, omega, simp, rcases et cases du core.

B.4 — sans objet : aucun refactor du prover Python.

Portée

Volontairement sans Mathlib, comme Basic.lean : tout est calcul fini décidable sur listes littérales. Le lakefile déclare globs := #[Swaps.*], mais la racine Swaps.lean` est mise à jour tout de même — son docstring énumère les théorèmes de la bibliothèque et décrirait faussement celle-ci si seul le glob la ramassait.

See #12205 — le §6 porte d'autres volets (le volet Python est livré par #14309) ; celui-ci ferme l'obstruction non bornée côté Lean.

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-02) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=3 genre=7 cap=6)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 genre=7 cap=6)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[jsboige]

[Hermes] — CoursIA #14381 obstruction non bornée par parité des inversions (#12205 §6, Swaps/Parite.lean). Lecture complète (+243, 2 fichiers : 1 nouveau module + import/doc du root).

Vérifié :

• Lean CI SUCCESS sur la PR — le module compile, donc bascule (72 instances close par un seul decide : 24 tables × 3 générateurs) et toute la chaîne signature_etape → signature_chemin → parite_determinee sont machine-checkées, pas déclarées.
• ordresStricts exhaustif et sans doublon : les 24 permutations de 1-4 en ordre lexicographique — recompté dans le diff.
• La relativisation est honnête et nécessaire : le contre-exemple [1,1] → [2,2] (parité invariante sur listes arbitraires) motive estJeu/estOrdre — l'invariant n'est affirmé que sur l'univers valide, et le lemme transporte validité ET parité conjointement. Bonne hygiène.
• Complémentarité réelle, pas rhétorique : aucun_chemin_court (7 chemins, énumération) vs GT-24b (k_max=12, budget) vs parité (famille infinie impaire, sans borne). La contraposée chemin_dilemme_chicken_pair + coherence_certificat (le certificat existant de longueur 2 est pair, cohérent) + le témoin dual aucun_chemin_pair_voisin ferment la boucle : l'invariant ne contredit pas les certificats, il les complète.
• Corroboration interne : les 2 autres chemins valides de Basic.lean (longueurs 4 et 2) sont pairs — l'invariant le prédit.
• Security scan : 0 match. Sans Mathlib comme annoncé.

Remarque mineure (aucune action requise) : 6 + 6³ + 6⁵ + … compte les chemins de longueur impaire comme 6^L — c'est le nombre de séquences d'étapes, pas de chemins simples ; la formulation « famille infinie » reste correcte, seul l'ordre de grandeur mériterait « séquences » pour être irréprochable.

Solide. LGTM au fond (contrainte token : COMMENT only — self-review).