docs(14773): social_choice_lean_peters — documenter le blocage amont v4.33 (README converge perime)

[jsboige]

Grain: MED/docs — lane myia-po-2025:CoursIA — prev: LIGHT/ledger #17858

Ce que cette PR fait

Ce lake (GameTheory/social_choice_lean_peters) est l'un des 4 derniers lakes hors cible de l'EPIC #14773 (cible leanprover/lean4:v4.33.0). Sa migration a été tentée, instrumentée, puis déclarée bloquée en amont. Le README affirmait jusqu'ici l'inverse :

• l.9 — « v4.32.1 (alignée sur le parc, pin effectif du lean-toolchain) » ;
• l.53-55 — « la famille du reste du parc. La convergence [Lean][infra] Converger les revisions Mathlib vers v4.31.0-rc1 (10 lakes rc2 + peters v4.27) #4364 s'applique désormais ici aussi » ;
• l.68 — « son propre lean-toolchain v4.32.1 (convergé) ».

Ces trois affirmations étaient vraies quand elles ont été écrites (2026-08-26, la cible du parc était alors v4.32.1). Elles ne le sont plus depuis que la cible est passée à v4.33.0. Cette PR les corrige sans les réécrire : un bloc daté est ajouté au §Statut, un addendum est posé sous le paragraphe concerné, et l'historique du §EPIC #4365 est conservé intact en dessous.

La mesure, pas l'argument

Tentative instrumentée (journal de build conservé, lake build complet) : lean-toolchain basculé sur v4.33.0, les huit dépendances transitives explicitées aux révisions du parc (bloc require … from git … @ <rev> — sans quoi le manifest de SocialChoiceLean impose ses propres revs 4.32 et l'échec se produit dans Batteries/Qq/ProofWidgets, ce qui n'est pas la faute de l'amont), lake update, lake exe cache get, lake build.

Le contournement de version a fonctionné — les erreurs ont quitté Batteries.Tactic.Alias, Qq.Typ et ProofWidgets.Component.MakeEditLink — et ont révélé une incompatibilité réelle dans les sources du paquet externe :

error: SocialChoice/Margin.lean:277:10: Tactic `rfl` failed
error: SocialChoice/Margin.lean:281:10: Type mismatch
error: SocialChoice/Margin.lean:313:10: Tactic `rfl` failed
error: SocialChoice/Margin.lean:317:10: Type mismatch
error: SocialChoice/Margin.lean:756:8:  Tactic `rfl` failed
error: SocialChoice/Margin.lean:759:8:  Tactic `rfl` failed
error: SocialChoice/Impossibilities/GibbardSatterthwaite/InductionStepCase2.lean:1286:2: unsolved goals
error: SocialChoice/Impossibilities/GibbardSatterthwaite/InductionStepCase2.lean:1288:2: unsolved goals

La compilation atteint [3029/3044] puis échoue. La classe d'erreur est unique et cohérente : les buts résiduels opposent la somme indexée V ⊕ Unit au type nu V, par exemple

⊢ Sum.inr w ∈ {v | a < b} ↔ w ∈ {v | a < b}

soit un changement de la normalisation de filter sur les sommes dans Mathlib 4.33.

Pourquoi ce n'est pas réparable ici

Les fichiers fautifs sont ceux du paquet externe DominikPeters/SocialChoiceLean, épinglé à 94a4c650b6a3 — dernier commit amont 2026-07-21 (« Clean up Lean 4.32 warnings »), branches disponibles master, duggan-schwartz, claude/formalize-duggan-schwartz-AyuSa, aucune ne portant de portage 4.33.

On ne patche pas du code vendored : patcher .lake/packages/ serait perdu au prochain lake update et masquerait l'écart. Le verdict est donc bloqué en amont, rapporté comme tel sur #14773 — il n'est pas contourné ici.

Périmètre

• 1 fichier, MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/README.md — +50/−4.
• Aucun notebook, aucun octet de code Lean, aucun lakefile/lake-manifest/lean-toolchain touché : la tentative a été annulée et l'arbre restauré à HEAD (git status --short vide).
• check_prose_quantitative_claims.py --diff "origin/main...HEAD" → [OK] aucun compteur quantitatif en prose. (rc=0).

Ce que le README ne prétend pas

Le bloc ajouté ne dit pas que le lake va migrer bientôt, ni qu'une date est connue. Il dit que le v4.32.1 est une exception assumée jusqu'à ce que l'amont publie un état compatible, et que ce n'est ni un oubli de ce dépôt ni quelque chose que ce dépôt peut corriger.

Part of #14773

🤖 Generated with Claude Code

[github-actions]

Grain tag obligatoire (#10045, bloquant).

Grain tag absent (no Grain: / in body).

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

[github-actions]

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

• GENRE-MISMATCH : declared genre != genre infere depuis les chemins du diff

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.

[github-actions]

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 54 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

[clusterManager-Myia]

[Hermes] VERDICT: LGTM (APPROVE) — documentation du blocage amont de social_choice_lean_peters (#14773). Compagnon cohérent de #17909 : là où l'inventaire GameTheory corrigeait la ligne « convergé » vers « exception documentée », ce README livre la preuve de l'exception.

Vérifications first-hand (head 84725bf) :

1. Revs du manifest — lake-manifest.json au dépôt : mathlib = 520045ab14e2, SocialChoiceLean = 94a4c650b6a3. Le README (avant : revs 7+4, après : 520045ab14e2 / 94a4c650b6a3) passe d'un tronquage incohérent aux revs exactes — correction factuelle, pas cosmétique.
2. Pin v4.32.1 — déjà vérifié ce cycle au dépôt : social_choice_lean_peters/lean-toolchain = v4.32.1, seul lake hors paire d'exceptions attendues. Le nouveau bloc §Statut dit vrai contre le disque.
3. Méthode — le journal de build cité (erreurs rfl/type mismatch sur V ⊕ Unit vs V dans Margin.lean/InductionStepCase2.lean, échec à [3029/3044]) est une mesure instrumentée rapportée, non reproductible côté review — je ne peux pas relancer le build amont ; mais les revs, le pin et la revendication de non-patch du vendored sont vérifiés au dépôt, et la position « ne pas patcher du code vendored, rapporter sur l'EPIC » est la bonne.
4. Historique préservé — le §EPIC #4365 historique est conservé (addendum daté sous la phrase périmée, pas de réécriture) — conforme à la pratique du dépôt sur les corrections datées.

Docs-only, 1 fichier, +50/−4. Aucun secret. Pas un README de compteurs (directive #17633 ne s'applique pas : pas de totaux de notebooks).

[Hermes hermes-pr-review, cycle :05 26/09, host f6be46d1b7a3]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 17908
head: 84725bf
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c46c9a14008ef8bc5ebb98a83e9b283c5413d87a1a68fa082199cdab101685bd
diff-files: 1
diff-additions: 50
diff-deletions: 4
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Perimetre verifie : 1 fichier, social_choice_lean_peters/README.md (+50/-4) — documentation du blocage amont v4.33 (ligne « converge » perimee remplacee par exception documentee). Compagnon declare de #17909 (celle-ci se merge en premier). Grain tag present en premiere ligne du body : MED/docs — lane myia-po-2025:CoursIA — prev: LIGHT/ledger #17858.

Checks, le seul point a lire : check_run_state.py signale 1 rouge residuel Always-on guards failure @04:38:23Z — c'est le tir SANS grain tag (bloc bot vtr-required-block @04:40:18Z), supersede par le vert de la meme jambe @04:46:20Z apres edition du body (declencheur edited). PR gate success @06:58:38Z, mergeStateStatus: CLEAN. Le pli latest-wins est vert ; le residu est documente par l'organe comme supersede, meme suite, meme jambe.

B.0 : check_unaddressed_nits.py rc=0 ; review Hermes VERDICT LGTM (APPROVE) @05:29:56Z — verifie le compagnonnage avec #17909 et la correction de la ligne perimee ; aucun thread inline. Les 2 autres commentaires sont advisory (G-VAR genre signals, trivial-diff) — non bloquants par design.

Domaine : documentation pure (README d'un lake Lean, pas de preuve touchee) — aucune preuve de domaine applicable.