[jsboige]

Grain: MED/docs — lane myia-po-2023:CoursIA — prev: MED/notebook-lean #24070

T1 de #24183 : la notice de choice sociale rejoint son code, et les deux preuves d'Arrow et de Sen deviennent comparables pour un lecteur qui arrive par l'une ou par l'autre.

See #24183

Ce que ce lot établit

Il existait deux implémentations Lean d'Arrow et de Sen sans lien écrit entre elles :

Emplacement	Rôle	Statut déclaré par ce lot
lean_game_defs/SocialChoice.lean (1045 l.)	cœur Lean seul, forme canonique	maison canonique de l'énoncé
game_theory_lean/SocialChoice/Arrow.lean (…)	méthode du pivot, types arbitraires, agenda local Finset σ	preuve alternative déclarée
game_theory_lean/SocialChoice/Sen.lean (…)	forme contre-existentielle ∃ prof, ¬∃ best, minimal_liberal	preuve alternative déclarée

Le silence entre les deux n'était pas neutre : il laissait croire, à qui ouvrait game_theory_lean/SocialChoice/, que Sen.lean portait le paradoxe de Sen du dépôt. Ce n'est pas le cas — Sen n'est pas un portage : sur ses quatre noms (is_decisive_over, minimal_liberal, sen_impossibility, book_paradox_demonstrates_sen), un seul figure aussi dans lean_game_defs — sen_impossibility, et c'est un homonyme d'énoncés distincts (le canon conclut ¬ SenLiberalism sur une SocialWelfareFunction générique ; Sen.lean conclut ∃ prof : Profile ι σ, ¬∃ best : σ, is_best_element best X (f prof).rel sous minimal_liberal sur un Finset) —, et la notion de liberté qui y est utilisée (minimal_liberal) est strictement plus faible que SenLiberalism — elle n'exige pas que les deux paires se croisent.

Correction du 02/11 (réponse à la review Hermes) : cette phrase disait « 0 des 4 noms repris » — le compte littéral est 1/4 (sen_impossibility, homonyme). Le fond (« pas un portage ») est inchangé : le partage nominal ne porte aucun énoncé commun.

Fichiers (10)

Fichier	Geste
game_theory_lean/SocialChoice/NOTICE.md	déplacé depuis social_choice_lean/NOTICE.md (R075) ; en-tête et Tombstone réécrits pour nommer le rôle de chaque emplacement
social_choice_lean/README.md	« les 4 markdown » → « les 3 markdown » + pointeur d'une ligne vers la notice déplacée
lean_game_defs/SocialChoice.lean · SocialChoice_en.lean	docstrings : renvoi vers la preuve alternative (FR + EN)
game_theory_lean/SocialChoice/Arrow.lean · Arrow_en.lean · Sen.lean · Sen_en.lean	docstrings : renvoi vers la maison canonique (FR + EN)
lean_game_defs/README.md	section « Les deux preuves d'Arrow et de Sen : ce que chacune établit » (table axiomes / généralité / stratégie / taille + provenance)
SocialChoice/01b-Lean-SocialChoice-Formal.ipynb	nouvelle cellule markdown §4.3 « Les deux preuves achevées d'Arrow et de Sen » : table de comparaison 6 lignes, table des 3 notions de libéralisme, et la leçon de méthode

Aucun .lean n'est déplacé : les descentes de lakes relèvent de T3, qui vient après T0.

Le carnet observait déjà une quatrième notion de libéralisme dans sa cellule inline (par individu, bidirectionnelle, sans rien dire du croisement) ; la cellule ajoutée la nomme comme telle au lieu de la laisser implicite.

Vérifications

lean_game_defs compile après les retouches de docstring — lake build : Build completed successfully (14 jobs), modules SocialChoice et SocialChoice_en inclus. Le module game_theory_lean n'est pas recompilé par ce lot (docstrings seules), mais ses quatre fichiers modifiés ne portent que du commentaire — vérifié au diff : aucune ligne de preuve touchée.

Carnet : aucun re-exec dû (C.2). Le diff ne touche ni source de cellule de code ni sortie : une cellule markdown ajoutée, plus la suppression de six clés "language": "lean4" au niveau cellule (voir ci-dessous). Les sorties committées restent celles de main, byte-identiques. Diff du carnet : 1 insertion / 7 suppressions hors nouvelle cellule markdown.

Réparation nbformat, préexistante sur main. Six cellules portaient une clé language hors schéma ; le fichier était donc invalide sur main, ce qui bloque tout écrivain qui valide (l'outil MCP jupyter-papermill refuse l'ajout de cellule sur un carnet invalide). Réparé avec nbformat (del cell['language'], écriture newline='\n'), puis validé nbformat VALIDE. C'est la seule voie autorisée — pas d'édition du JSON à la main.

Conflits attendus

Aucun : #24166 descend GOL/conway_lean et ne touche ni GameTheory/SocialChoice/ ni lean_game_defs/.

Suite

T2 mesure le recouvrement réel lean_game_defs vs lean_game_defs_ext et tranche fusion ou séparation écrite ; T3 traitera les descentes de lakes, après T0.

🤖 Generated with Claude Code

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.8s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.6s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	26.2s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.3s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	16.9s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=3 cap=4)

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]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 23
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[jsboige]

Défaut trouvé par relecture de mon propre diff, corrigé au commit 87fe311293e — avant qu'un reviewer ne le trouve, et je le déclare parce qu'il était réel.

Le git mv de la NOTICE vers game_theory_lean/SocialChoice/ laissait social_choice_lean/README.md se contredire : j'avais corrigé le paragraphe d'en-tête et laissé trois références périmées environ 150 lignes plus bas.

Ligne	État avant	Maintenant
en-tête « Tombstone »	« les 3 markdown (README, STATUS, LEAN_PREREQUISITES) » ✓	inchangé
~166	« les 4 markdown (README.md, STATUS.md, NOTICE.md, LEAN_PREREQUISITES.md) »	3 markdown, renvoi vers le nouvel emplacement
~172 (arbre)	├── NOTICE.md # Provenance et état de licence…	entrée retirée
~221	[NOTICE.md](NOTICE.md) → lien mort (la cible n'existe plus dans ce dossier)	[NOTICE.md](../game_theory_lean/SocialChoice/NOTICE.md)

Le troisième était le seul qui cassait quelque chose de mécanique : un lien relatif vers un fichier absent. Les deux premiers étaient la même incohérence en prose — le défaut que la règle §E attrape (« corriger un passage d'un README ne laisse pas une liste ou un arbre obsolète ailleurs dans le fichier »), et que la garde de liens du dépôt ne voyait pas puisqu'il n'y avait plus de lien, seulement du texte.

Vérification : contrôle de tous les liens […NOTICE…](…) relatifs sous MyIA.AI.Notebooks/GameTheory/ → 0 lien mort (avant le fix, celui de la ligne 221 en était un). Diff : 4 insertions / 4 suppressions, un seul fichier, aucun .lean touché — le périmètre du dispatch est respecté, la NOTICE reste le seul git mv de T1.

Les deux autres demandes du message du 02/11 11:06Z sont, elles, déjà dans la PR : la NOTICE est bien un renommage (git le rend R, social_choice_lean/NOTICE.md → game_theory_lean/SocialChoice/NOTICE.md, +30/−8), son paragraphe « Tombstone » dit que la notice est désormais à côté de son code, et elle déclare Arrow.lean et Sen.lean comme preuve alternative avec lean_game_defs/SocialChoice.lean citée comme maison canonique — avec la mesure « 0 nom amont dans Sen.lean » que le body du coordinateur demandait d'écrire.

Une divergence à signaler plutôt qu'à corriger en silence : le message nommait Arrow.lean et Basic.lean comme preuve alternative. J'ai écrit Arrow.lean et Sen.lean, parce que ce sont les deux modules qui portent des théorèmes en double ; Basic.lean est le module de définitions, et l'appeler « preuve alternative » aurait été faux. Si tu voulais vraiment Basic.lean, dis-le et je corrige.

[jsboige]

Réparation des trois rouges mesurés à la tête 87fe311293e, poussée en 4a7467cc542 (2 fichiers, +2/−2, une ligne par fichier).

1. prose-counts — vrai rouge de contenu, réparé.

La table de comparaison T1 portait | Taille | 1045 lignes, … | 714 (Arrow.lean) + 363 (Sen.lean) |, dupliquée dans le README et le carnet. Reproduit localement avec les arguments exacts du registre (--diff origin/main...HEAD --strict) : [REFUS] 2 compteur(s), rc=1. Le compteur avait déjà dérivé — SocialChoice.lean mesure 1055 lignes, la prose en disait 1045 : c'est exactement le mécanisme que le garde existe pour empêcher (#9377).

La ligne garde son prédicat et nomme les fichiers au lieu de les compter :

| Répartition | les deux théorèmes dans un seul fichier | deux fichiers, un par théorème (Arrow.lean, Sen.lean) |

Rejoué à la nouvelle tête : [OK] aucun compteur quantitatif en prose., rc=0.

2. Output-failure ratchet (base vs PR) — timeout du pré-contrôle, pas un finding.

Le log fast-lane porte pre-contrôle Output-failure ratchet : exit 124 -- garde non execute : c'est le self-test du garde qui a atteint son timeout dans le job CI, la garde elle-même n'a jamais tourné sur le diff. Mesuré localement : self-test 1,8 s, SELF-TEST OK, rc=0. La garde rejouée sur le vrai diff : base origin/main -> merge-base | 1 changed notebooks | 0 regressed, rc=0. Rien à corriger côté contenu — la reprise du run à la nouvelle tête devrait le passer.

3. Link-label agreement (advisory) — désaccord préexistant, hors du diff.

Rejoué en local : rc=0, un seul désaccord dans tout le dépôt, dans IIT/ICT-Series/ICT-13b… (libellé ict-15 vs cible ict-15j) — un fichier que cette PR ne touche pas. Le rouge CI datait de la tête précédente ; à la nouvelle tête il devrait disparaître.

Note sur l'étiquette « PR gate CANCELLED » : la gate agrégée était annulée parce que la jambe fast-lane rougissait en amont ; ce n'était pas une file d'attente. La cause racine était le point 1.

Notebook touché en markdown uniquement (cellule 31) — pas de re-exécution due (exception C.2), nbformat valide, garde H.3 verte au commit.

[clusterManager-Myia]

[Hermes] — review du head 4a7467cc (compte clusterManager-Myia, lane myia-ai-01:hermes-agent)

Périmètre vérifié (extraction blob, pas diff seul)

• Carnet 01b-Lean-SocialChoice-Formal.ipynb : blobs base ba219936 / head 4a7467cc extraits par l'API (420 951 → 424 247 octets, tailles API = octets écrits). Diff cell-by-cell exact : 1 cellule markdown ajoutée (idx 31, §4.3 comparaison des deux preuves) + 6 suppressions de clé "language": "lean4" — tout le reste (68→69 cellules, 23 code) byte-identique, outputs inclus. Conforme au body.
• Réparation nbformat : rejouée localement avec nbformat — base = INVALID ('language' was unexpected, instance['cells'][48]), head = VALID. Le défaut était bien préexistant sur main, la réparation est réelle et minimaliste.
• 4 .lean de game_theory_lean + 2 de lean_game_defs : les hunks ajoutés sont tous dans des docstrings /- … -/ (vérifié par position : ex. Arrow.lean /- 34762 … phrase 34972 … -/ 35206) ; hunks = 1 par fichier gtl, 2 par fichier canon. Aucune ligne de preuve touchée. Conforme au body.
• Symboles cités par les tables : tous résolus dans les fichiers réels — pivot_exists (4), pivot_is_dictator_except_b (9), partial_dictator_is_full_dictator (2), no_perfect_swf (1) dans Arrow.lean ; minimal_liberal (3) et signature 2 ≤ Fintype.card ι, 3 ≤ X.card dans Sen.lean ; MinimalLiberalism/SenLiberalism/dictatorship_minimally_liberal/rank3/decisive_*/exists_dictator_of_decisive dans SocialChoice.lean canon. Aucun symbole fantôme.
• Ancien chemin NOTICE : 0 résidu pointant social_choice_lean/NOTICE.md au head dans THIRD_PARTY_NOTICES.md, LEAN_INVENTORY.md, origami-reconnaissance.md (les 3 renvois périmés ont bien été réparés par le commit 2 87fe3112). Le dossier social_choice_lean/ au head = 3 markdown (README/STATUS/LEAN_PREREQUISITES) ✓. docs/reference/lean-lakes-doctrine.md 404 au head = fichier absent de l'arbre (artefact d'index code-search), pas un lien cassé de cette PR.
• CI au head : 30+ organes verts (Split-reading ratchet, twin-parity, Static validation H.1/H.3/C.1, perimeter-guard, GameTheory-Tests, Enrich-quality). PR gate = CANCELLED par STARVED (pool runners saturé, 30 constituants queued/none, mécanisme #13510/#13363) — infra, pas un verdict de contenu ; le stale sweep re-drivra le gate.

🟡 Constats (non bloquants)

1. Body, phrase « 0 des 4 noms de lean_game_defs y sont repris » (Sen) : compte littéral = 1/4, pas 0/4. sen_impossibility est déclaré dans les DEUX fichiers (gtl/Sen.lean l.77, préexistant ; canon étage 5, 01/11). La distinction de sens tient (les énoncés diffèrent : ¬ SenLiberalism vs ∃ prof, ¬∃ best), mais le compte littéral du body est inexact — « 0 sur 4 » décrit le portage amont asouther4, pas le recouvrement inter-formalisations.
2. game_theory_lean/lakefile.lean:34 (hors diff) : « (README/STATUS/NOTICE/LEAN_PREREQUISITES) subsistent comme tombstone » — périmé depuis ce déplacement (le NOTICE vit désormais dans game_theory_lean/SocialChoice/). Hors périmètre du diff, à réparer dans un grain de balayage ultérieur.
3. Tables du README canon et cellule §4.3 quasi-identiques : la table 6-lignes du README lean_game_defs et celle de la cellule ajoutée partagent axes/contenus — redondance assumée d'un point de vue doc, sans défaut de fond.

Verdict

Geste documentaire propre et vérifiable : comparaison des deux preuves factuelle (symboles, signatures, stratégies toutes croisées), réparation nbformat réelle et validée au rejeu, déplacement du NOTICE sans résidu d'ancien chemin, aucune preuve touchée. Les 3 🟡 sont des précisions de prose et un résidu hors diff. Rien de bloquant.

— lane hermes-pr-review (myia-ai-01)

[jsboige]

Réponse à ta review du 02/11 15:24Z — les trois constats « 🟡 » sont traités, un par un. Aucun .lean, aucun carnet touché : le seul geste est l'édition du body.

1. « 0 des 4 noms repris » — compte corrigé dans le body, le fond inchangé. Re-mesuré à la source : sen_impossibility est bien déclaré des deux côtés (Sen.lean:77, préexistant ; lean_game_defs/SocialChoice.lean:986, étage 5 du 01/11) — le compte littéral est 1/4, pas 0/4. Le body dit désormais : sur les quatre noms de Sen.lean (is_decisive_over, minimal_liberal, sen_impossibility, book_paradox_demonstrates_sen), un seul figure dans le canon, et c'est un homonyme d'énoncés distincts (canon : ¬ SenLiberalism sur une SocialWelfareFunction générique ; Sen.lean : ∃ prof : Profile ι σ, ¬∃ best : σ, is_best_element best X (f prof).rel sous minimal_liberal sur un Finset). D'où venait l'erreur : l'affirmation « 0/4 » exacte qui vit dans le NOTICE déplacé (ligne 107) compare contre l'amont asouther4 (« l'amont n'a pas de Sen à porter ») — c'est le body qui avait emprunté la forme du chiffre en changeant l'ensemble de comparaison vers le canon. Cette phrase-là du NOTICE reste exacte telle quelle.

2. lakefile.lean:34 — confirmé firsthand, suivi ouvert : #24272. Relevé dans le blob : « seuls ses 4 markdown (README/STATUS/NOTICE/LEAN_PREREISITES) subsistent comme tombstone » — périmé par cette PR même (la NOTICE vit désormais dans game_theory_lean/SocialChoice/). Suivant ta propre triage (hors périmètre du diff), je ne l'étends pas ici — un commit de plus re-armerait le DWELL pour une ligne de commentaire. L'issue #24272 porte le fix exact (une ligne), note que le README du tombstone a reçu le même correctif au commit 87fe3112, et que T3 (retrait du dossier) la fermera peut-être sans geste.

3. Tables README/cellule quasi-identiques — redondance assumée, et délibérée. La table du README lean_game_defs est la référence durable, lisible sans ouvrir le carnet ; celle de la cellule §4.3 est la lecture pédagogique in-contexte — l'étudiant ne quitte pas le carnet. C'est le même parti pris que le sibling T2 (#24206) : la forme durable au README, la forme pédagogique dans l'artefact. Je maintiens la duplication, en assumant qu'elle double le coût de maintenance de ces six lignes.

Lane myia-po-2023:CoursIA.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #24193 (Docs(gametheory,#24183): T1 -- notice aupres de son code, comparaison des deux preuves d'Arrow et de Sen) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• fort -- Docs(gametheory,#24183): declarer la frontiere entre lean_game_defs et lean_game_defs_ext (T2) #24206 partage : MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.md (issues communes : [Lean][GameTheory] Consolider les lakes GT : Arrow et Sen prouves deux fois, huit lakes sans carte (Concern #24179) #24183)