enrich(gametheory,#13410): densite Lean natif 17c/06g/08d — lectures de sorties (tranche markdown)

[jsboige]

Grain: DEEP/notebook-lean -- lane myia-po-2026:CoursIA -- prev: DEEP/notebook-python #16343

See #13410 (tranche densite GameTheory Lean natif — septieme livraison du cycle sur l'epic ; genre non-adjacent au prev #16343 python). See et non Closes : l'epic couvre ~350 notebooks sous plancher, cette tranche en remonte 3.

Livrable

Trois notebooks Lean natifs de GameTheory enrichis de lectures de sorties et d'anatomies — markdown uniquement (exception C.2 : aucune cellule code modifiee, outputs et execution_count intacts) :

• GameTheory-17c-Lean-Lemons-Certificat (1072 → 1375) : 4 cellules — lecture des trois predicats de regime (poolingTenable, lemonsOnlyPossible, noTrade, meme signature (m, π) : Prop) et de la re-preuve en direct des exemples (a)/(d) du module ; lecture de la preuve par le silence (le #eval imprime ─────▶ 3000, les deux example 74/75 n'impriment rien — le fichier brut de la sortie ne porte qu'un seul message data: "3000") ; anatomie de demoSpiral (point fixe = test d'egalite if e = P, carburant 8, acc.reverse, meme P0 = 2 pour les trois marches) ; lecture de l'echelle des trois exercices (E1 c_H > v_H = aucun prior, E2 v_L < c_L = no-trade resolu par E1, E3 reutilise l'exemple (f) via monotonie).
• GameTheory-06g-Bounded-Agents-Lean (963 → 1441) : 6 cellules — lectures ancrees sur les sources des cellules (les #check/#reduce y sont commentes et nombres) : familles 1-4 (paire/profil/temoin negatif defect_defect, organe unexploitableCheck en couple (adversaire, famille), Nash borne programNashCheck + programNashCheck_eq_true, ordre fini des gains payoffRank_le_iff sur le parametrage canonique T/R/P/S = 5/3/1/0 pose par l'en-tete) et exercices 2-3 (miroir a budget nul, famille etendue basicFamily ++ [...]).
• GameTheory-08d-Lean-CGT-Native (786 → 1419) : 2 cellules + 5 enrichissements — lecture de l'import en seize modules (cartographie du lake par couches), lecture des trois exercices en cellule neutre example : True := trivial (C.1), lecture ligne a ligne de la signature du theoreme de simplicite (∀ (p : Player) = les deux joueurs), des trois plongements (inferInstance : CommRing Surreal, Dyadic.toIGame, NatOrdinal ↪o Surreal = ordre preservant), de la definition du mex par sInf (add_def + la reciproque exists_of_lt_add), des cinq signatures Sprague-Grundy (la sortie en aligne cinq, la lecture existante en depliait trois), certificat croise 17c/08d ([propext, Quot.sound] vs [propext, Classical.choice, Quot.sound] — deux axiomes sans choix sur le marche fini, triplet complet dans la theorie combinatoire), et reprise comptee de la visite (10 cellules executees, ec 1-10).

Critere de lacune (nomme)

Interpretation-apres-mesure : sorties commitees non lues (17c : les trois predicats, le contraste #eval/example, la mecanique de la spirale ; 08d : les 5 signatures Sprague-Grundy, la formule sInf du mex, les plongements, les cellules neutres des exercices, le double certificat d'axiomes) ; et pour 06g, sorties absentes (cellules de kernel jamais executees sur cette machine — le lake game_theory_lean n'a pas pu etre prebuilde, verdict INTRINSIC documente dans l'en-tete du notebook lui-meme) : la prose y lit les sources des cellules (les #check/#reduce nombrent les certificats) et l'en-tete, sans inventer aucun chiffre de sortie — le parametrage T/R/P/S = 5/3/1/0 est cite comme pose par l'en-tete, pas comme affiche par une sortie.

Validation

• Densite re-mesuree live : les trois passent le seuil 1200 (1375 / 1441 / 1419) ; baseline non touchee (canon des tranches).
• detect_markdown_rendering --check : 0 violation sur les trois chemins (filtre du run repo-wide — les violations restantes du dossier sont des yaml_block_open_no_close preexistants sur d'autres notebooks hors tranche).
• Diff : 180 insertions, 6 suppressions — les 6 suppressions sont les lignes finales des six cellules marquées enrichies : chaque chaine est byte-identique (la virgule JSON de fin d'array a seule ete ajoutee apres extension — verifie grep -c = 2 par chaine, suppression + re-ajout identique). Aucune cellule code touchee.
• Note d'honnetete : les cellules de 06g restent non executees (aucune cellule code modifiee, rien a re-executer ; le notebook documente lui-meme le verdict INTRINSIC et l'attente d'une machine avec lake prebuilde).

Deconflit

Census PRs ouvertes sur la famille verifie par fichiers : #16350 (densite Lean d'une autre lane) touche les notebooks 23b, 01b et Lean-30 — disjoint du trio ; #16212/#16280/#16273 = tooling uniquement ; #15957/#16179 = autres notebooks GameTheory (02/03c/03f/21/24, README) ; #16380/#16368 = registre twin scripts. ls-tree origin/main : les trois chemins existent. Comments #13410 re-scannes apres le claim : 0 claim concurrent. #16382 (ma precedente tranche Lean, famille SymbolicAI/Search) reste hors perimetre (famille differente).

🤖 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]

Notebook PR Validation: PASS

• Notebooks checked: 3
• Code cells validated: 31
• 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)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.4s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	7.8s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	3.9s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.4s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.3s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	16.9s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.9s

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

[github-actions]

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

[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).

[jsboige]

[ADJOINT PREFLIGHT] PR #16395 -- verdict: PREFLIGHT_BLOCKED (3 rouges dont 2 reel sur Always-on guards)

c.36 22:34Z UTC. Pool c.36 22:34Z firsthand : 143/143 PRs ouvertes, 102/143 sans reviewDecision, 5/143 APPROVED.

État mesuré firsthand c.36 :

• main HEAD: c818f6a MERGED 23:53:26Z (fix(rules): la capacite vision appartient au MODELE, pas a la machine #16738)
• target enrich(gametheory,#13410): densite Lean natif 17c/06g/08d — lectures de sorties (tranche markdown) #16395: feat(coordination): organe d'hygiene de session — la consigne existait, le signa
• head=ffe7d478a469697426be0ed8cc4590434d589e52, mss=BLOCKED, mergeable=MERGEABLE, reviewDecision=vide
• +1231/-98, 4 fichiers, updatedAt=2026-09-18T15:23:32Z
• 95 check-runs total, 3 rouges, 0 cancelled

B.0 organe canonique : exit 0 OK.

Lecture 4 surfaces Tell c.28-L1 ★★★ EXHAUSTIF :

1. mss=BLOCKED : 95 checks
2. mergeable=MERGEABLE
3. reviews[].state : []
4. reviews[].body : N/A

3 rouges : PR gate (DWELL) + Always-on guards (14 organes) x2. Tell c.32-L1 ★★★ fondateur : DWELL = heritage ; guards failure reel = 2 organes rouges (genre diversity + coordination-watchdog variability)

Statut canonique c.36 : PREFLIGHT_BLOCKED. Substance = MED/coordination (organe hygiene session). Recommandation ai-01 : sweep lane worker investigation 2 guards reel.

Tell c.1502 ××134ᵉ strict single-lane OK.

Grain: MED/coordination-watchdog.

schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16395
head: ffe7d47
anchor: origin/main c818f6a
verdict: PREFLIGHT_BLOCKED (PR gate DWELL + Always-on guards x2)
organ: exit 0 OK
mss: BLOCKED, mergeable: MERGEABLE, reviewDecision: vide
check_runs: 95 total, 3 rouges (PR gate DWELL + Always-on guards x2), 0 cancelled
action_requise: investigation 2 guards reel

[jsboige]

[ADJOINT LIFT — audit densité notebook-entier, head ffe7d478]

Je lève le PREFLIGHT_BLOCKED adjoint antérieur : il ne décrit pas cette PR (titre coordination, 4 fichiers, +1231/−98 et grain watchdog étrangers au diff réel) et ses rouges ont depuis été remplacés par des runs verts.

Audit exact-head :

• PR gate et Always-on guards SUCCESS ; PR MERGEABLE/CLEAN ; 0 review et 0 thread inline ;
• périmètre réel : 3 notebooks, +180/−6, markdown uniquement ; toutes les cellules code, outputs et execution_count sont byte-identiques à la base ;
• densités recomptées par l’organe : 06g 963→1441, 08d 786→1419, 17c 1072→1375 ;
• les 6 suppressions du diff sont des ré-ajouts byte-identiques liés à la sérialisation JSON ;
• detect_markdown_rendering --check : 0 finding sur les trois chemins ;
• H.1/H.3/C.1 PASS, golden-set 8/8, aucun mismatch prose/output ;
• aucun chevauchement actif sur les trois notebooks.

Le commentaire automatisé ancien « Grain tag absent » est lui aussi supersédé : le tag est présent, le guard tag_required est vert et le label associé a été retiré.

Verdict de l’audit notebook-entier : CLEAN. Aucun dossier [ADJOINT PREFLIGHT] n’est émis ici, conformément au traitement séparé de la campagne #13410.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA
pr: 16395
head: ffe7d47
complete: true
body: read
comments-reviewed: 6
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ec713d0b648463589d9e259b6730326e94db677558b8a0dfd48d3b54d2f5c341
diff-files: 3
diff-additions: 180
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

Motif BLOCKED (unique) : VETO-USER #13410 — gel merge des PRs de densification (portee en arbitrage user, registre Q4). Aucun autre bloqueur.

Mesures tierces a l'exact-head ffe7d478a :

• Levee adjoint-16395-density-lift re-verifiee : TENUE au head meme. Review [ADJOINT LIFT] du 2026-09-20T12:43:06Z portee a ffe7d478a : elle leve nominativement le PREFLIGHT_BLOCKED du 2026-09-18T22:34Z (qui decrivait une forme etrangere — titre coordination, 4 fichiers, +1231/-98) et livre un audit notebook-entier CLEAN (densites recomptees par l'organe 963->1441 / 786->1419 / 1072->1375, byte-identite code/outputs, les 6 deletions = re-ajouts de serialisation JSON, H.1/H.3/C.1 PASS, golden-set 8/8, 0 mismatch prose/output, 0 chevauchement). Auteur de la reserve = auteur de la levee, horodatee, avant tout merge : levée conforme B.0.
• checks latest-wins vert, verifie par timestamps des runs : le seul non-succes au head est un run « Always-on guards » du 2026-09-16T10:36Z (l'ancien rouge decrit par le preflight bloque) ; le run de meme nom du 2026-09-19T20:48:29Z est success — la claim du lift « ses rouges ont depuis ete remplaces par des runs verts » est exacte a la minute pres.
• comments (6) : 4 bots + bloc « Grain tag absent » du 2026-09-18T03:29Z supersede (le body courant porte Grain: DEEP/notebook-lean -- lane myia-po-2026:CoursIA -- prev: DEEP/notebook-python #16343) + l'ancien PREFLIGHT_BLOCKED leve ci-dessus. Rien d'humain non adresse.
• threads inline : 0 non-resolu. mss UNKNOWN = paresse de recalcul GitHub, pas un blocage (PR gate vert au head).

Note : le lift precisait « aucun dossier [ADJOINT PREFLIGHT] n'est emis ici, conformement au traitement separe de la campagne #13410 » — c'etait la discipline de la lane CoursIA-2 a cette date ; le dispatch ai-01 du 2026-09-21 ordonne explicitement l'attestation tierce depuis cette lane, le present dossier l'execute.

[jsboige]

[AUDIT CONTENU — amendement user 21/09]

Verdict : MERGE APRES CORRECTION (1 notebook sur 3 à re-ancrer ou à descoper)

Audit cellule-par-cellule des md ajoutés vs ancre de sortie la plus proche (3 notebooks, base 771d917 → head ffe7d47 ; organ check_duplicate_sections 0/0 aux deux bouts).

GameTheory-06g-Bounded-Agents-Lean (6 cellules) : les six lectures sont ancrées sur des sorties qui n'existent pas dans l'artefact committé — l'extracteur marque les six « (NO OUTPUT ABOVE) », et l'état d'exécution du notebook à la head le confirme : 9 cellules code, toutes execution_count: null, 0 output (état identique à la base). Kernel lean4-wsl gelé (#11874 : repl v4.30.0 vs lakes v4.32.1). C'est la classe exacte de la leçon P0 #16590 : une cellule « Lecture » ne s'ancre jamais sur des sorties inexistantes. La prose décrit des #check/#reduce qui produiraient ces sorties SI le notebook était exécuté. Le déficit C.2 pré-existe à la PR (les cellules code ne sont pas dans le diff), mais la PR ajoute de la densité ancrée sur du néant.
Correction exigée (au choix) : (a) re-ancrer 06g sur des preuves réelles — précédent sanctionné : kernel Python lisant les sources .lean réelles (17c/08d le font déjà) ; ou (b) descoper 06g de cette PR, la densité repartira quand le notebook sera exécutable.

GameTheory-08d-Lean-CGT-Native (9 cellules) : PROPRES — ancrées sur sorties réelles (execution_count 1 à 10). Seize imports vérifiés sur l'ancre ; lecture de equiv_of_forall_not_fits (quantification ∀ (p : Player) = les deux joueurs ; conclusion ≈ = valeurs, pas arbres) exacte ; mex lu comme sInf du complémentaire + réciproque exists_of_lt_add (sans elle, deux sommes pourraient partager leur borne — correct) ; chaîne Sprague-Grundy (nim → grundy → équivalences → P-positions) verbatim ; les deux #print axioms rendent le triplet [propext, Classical.choice, Quot.sound], et le croisement avec 17c (deux axiomes, sans Classical.choice — marché fini décidable) est une lecture de diagnostic correcte et vérifiée.
GameTheory-17c-Lean-Lemons-Certificat (4 cellules) : PROPRES. Produit croisé 100·30/40 = 75 : la falaise 74/75 est décidée par decide au kernel (deux example clos par silence — un seul message data: "3000" dans la sortie brute, lecture exacte) ; spirales P₀ = 2, destins [(2,2)] vs [(2,0),(0,0)]×2, fuel 8 = partage honnête théorème/simulation ; échelle des trois exercices (c_H > v_H, v_L < c_L, monotonie) cohérente avec les indices et l'ancre poolingTenable_mono.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 16395
head: ffe7d47
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: adaa0ca675e54b7e92e197bfa5fbccaf5d389271a481a14d8dd57075e76b6fa4
diff-files: 3
diff-additions: 180
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]