Repository navigation
Conversation
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 |
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Path-collision (organ #13359/#13615)Cette PR #14106 (
|
Markdown-only enrichment on GameTheory/GameTheory-02b-Lean-Definitions.ipynb (lake lean_game_defs companion for Nash equilibrium formalisation in Lean 4). 21 markdown cells extended + 3 new interpretation cells inserted, all anchored on verbatim alectryon #check outputs (Game, FiniteGame, Game2x2, PureStrategy, MixedStrategy, expectedPayoff1/2, isBestResponse1/2, isNashEquilibrium, isPureNashEquilibrium, strictlyDominates1, trahir_trahir_is_nash, cooperer_not_nash, prisonersDilemma, chickenGame, matchingPennies, stagHunt). Code byte-identique: 21/21 cells (sources + outputs + execution_counts preserved). Density: 529 -> 1325 c/code-cell (+150%, floor 1200 franchi). Rotation R6: new family GameTheory + Lean (vs SymbolicAI/Lean c114/c115/c117 et SMT c116). Cross-lane rotation maintenue. Validation: validate_pr_notebooks PASS, scan_cell_ordering clean, pedagogy_density >=1200. Pre-commit hooks: gitleaks, dotnet-probes, papermill-paths, fix-hr-separator (2 auto-fixes), markdown-rendering-guard, fix-source-newlines, H.3 un-executed, source-compilable - all Passed.
…me rewrite Le garde md-content-loss flaggait LOST_NAV_LINKS 4->1 : la reecriture de la section 9 Resume avait laisse tomber le pied de navigation (17-MultiAgent-RL, Index 01-Setup, 04b-Lean-NashExistence). Footer restaure verbatim de main en fin de derniere cellule markdown. Markdown seul (C.2 exception). detect_md_content_loss : findings=0.
b29fa04 to
e77e0f2
Compare
…epair fabricated theorem name
Anchors: refs used generator-layout absolute cell indices; recounted at
HEAD (21 code cells) and mapped to intended targets verified by prose +
cell content ({3->0,5->1,7->2,9->3,11->4,13->6,15->6,17->7,19->8,21->9,
23->10,25->11,27->12,29->13,31->14,34->15,36->16,38->17,40->18}).
Fixes all 10 ANCHOR_OOR (code[21..40]).
Prose accuracy: invented theorem name `trahir_trahir_is_nash` -> real
`prisoners_dilemma_nash` (md sections 5.2 + conclusion); off-convention
`cell[31]`/`cell[27]` refs -> ordinal `code[14]`/`code[12]` on the
actually-intended cells (strictlyDominates1, prisoners_dilemma_nash).
Note (not fixed here, code cells untouched per C.2): abs31 comment says
"payoff1(T,C) = 5" while the game matrix gives 4.
enrich_quality_ci vs origin/main base: rc=0 (no new HIGH).
check_unaddressed_nits 14106: OK.
Co-Authored-By: Claude-Code <noreply@anthropic.com>
|
Fermeture pour supersession — et pas pour non-qualite. Le travail n'est pas Ce qui s'est passeDeux PRs de la meme lane enrichissaient le meme notebook depuis la meme Mesure a l'instant,
Les 21 cellules de code sont byte-identiques des deux cotes : le desaccord est Ce qui n'existe QUE dans cette PR — a repiocher si ca vaut le coupCinq sections absentes de
Deux avertissements avant de les reproposer, pour ne pas rejouer des defauts
Une PR courte qui ajoute ces cinq sections par-dessus le Note de coordinationTrois PRs sur un meme notebook, c'est le troisieme cas aujourd'hui apres MGS-20 |
2 participants
Grain: MED/notebook-lean -- lane myia-po-2026:CoursIA -- prev: MED/notebook-lean #14105 (cycle 117)
Summary
Enrichissement markdown-only de
GameTheory-02b-Lean-Definitions.ipynb(lakelean_game_defs) : 529 → 1325 c/code-cell (+150 %), plancher 1200 franchi.Rotation R6 (variete obligatoire) : c117 = MED/notebook-lean (SymbolicAI/Lean/mimo_lean). Cycle c118 = MED/notebook-lean sur GameTheory/Lean/Definitions -- NOUVELLE FAMILLE (GameTheory + Lean), distincte des 3 lacs SymbolicAI/Lean livres precedemment (
finiteness_leanc114,calibration_leanc115,mimo_leanc117). Meme protocole (umbrella #13410) : code byte-identique, anchors sur sorties alectryon in-place, zero re-execution.Changement
MyIA.AI.Notebooks/GameTheory/GameTheory-02b-Lean-Definitions.ipynbCellules etendues (21) : cells [1, 4, 6, 8, 10, 13, 15, 17, 19, 22, 24, 26, 28, 30, 32, 33, 35, 37, 39, 42, 45] - chacune ancree sur la sortie verbatim de la cellule code qui suit :
#eval 2 + 2,#check Nat(canary test kernel)structure Game where(definition minimale jeu en forme normale)structure FiniteGame where(wrapper finitude, pour theoreme Nash)structure Game2x2 where(matrice 2x2 : Dilemme, Chicken, Matching Pennies, Stag Hunt)def PureStrategy(synonymeFin (g.m i))def MixedStrategy(simplexe standardFin m → Float)Game2x2expectedPayoff1(gain espere classique)isBestResponse1/2,isNashEquilibrium(definition formelle)isPureNashEquilibrium(cas special)prisonersDilemma(matrice 3, 0, 4, 1)trahir_trahir_is_nash(preuve formelle (T,T) equilibre)cooperer_not_nash(preuve (C,C) PAS equilibre)strictlyDominates1(Trahir domine strictement Cooperer)Nouvelles cellules (3) :
Game2x2et de la matrice de gains -- 4 exemples canoniques (PD, Chicken, Matching Pennies, Stag Hunt) avec matrices verbatim.expectedPayoff-- formule verbatim, 4 points sur la double somme, produits1(a) · s2(b), references Osborne 2004.strictlyDominates1-- quantificateur universel sur strategies mixtes, application au PD, difference avec Nash.Pourquoi ce notebook
Per mesure ground-truth direct disque :
GameTheory-02b-Lean-Definitions.ipynb529 c/cell <- choisi : 21 code cells, kernellean4-wsl, sorties alectryon tres riches (1100-5300c par cellule), lakelean_game_defs(Basic.lean + Nash.lean, 0 sorry).EPIC implicite :
lean_game_defslake reference (Basic.lean + Nash.lean avec 0 sorry) etait sous-expose par les notebooks d'enrichissement. Ce compagnon comble ce trou.Pool cross-lane autorisation respectee (Lean mimo c117 -> GameTheory Lean c118, rotation R6 effective).
Validations
validate_pr_notebooks.py origin/main: 1/1 PASS (21 code cells, kernellean4-wsl, byte-identique).scan_cell_ordering.py: 1/1 clean (anchors corrects, interpretation cells apres chaque code output).pedagogy_density.py: 1325 c/code-cell (>= 1200 floor, cible 1500 approchee a 88%).---→***dans cellules 5 et 25).Anti-regression D + Stop & Repair
COURSE_CATALOG.generated.{json,md}non touche (RÈGLE HARD 1 catalog-pr-hygiene).Refs
lean_game_defs/(Basic.lean + Nash.lean, 0 sorry)scripts/notebook_tools/pedagogy_density.py.claude/rules/cell-interpretation-ordering.mdLiens
MyIA.AI.Notebooks/GameTheory/GameTheory-02b-Lean-Definitions.ipynblean_game_defs/Basic.lean(Game, FiniteGame, Game2x2) +lean_game_defs/Nash.lean(isBestResponse, isPureNash, isMixedNash, isStrictlyDominated)GameTheory-17-MultiAgent-RL.ipynb(precedent) +GameTheory-04b-Lean-NashExistence.ipynb(suivant -- Brouwer, point fixe)