Repository navigation
Fix(gametheory): contre-audit GT-04c NashExistence — attributions Lean inexactes - #23958
Conversation
…n inexactes Contre-audit de fond de la série GameTheory (notebooks Python), carnet par carnet, confrontant chaque claim à la sortie qui l'imprime et les attributions à la source. Tout le contenu quantitatif est CORRECT (point fixe babylonien 1D, contraction de simplexe 2D, Matching Pennies, 3 contre-exemples Brouwer, compétition de prix). 5 défauts de fond, tous des imprecisions de provenance/cohérence révélées par le carnet lui-même et le dépôt réel : 1. Cellule 0 (md) : double parenthèse dans un lien + "accompagne le notebook Lean 18" incohérent -> "notebook Lean 04b". 2. Cellules 19/21 (code) : libellés "extraits de Nash.lean" / "extrait de Brouwer.lean" -- surclaim de fidélité verbatim : les noms montrés (MixedStrategy, IsNashEquilibrium, brouwer_fixed_point) n'existent pas dans les fichiers réels du dépôt math-xmum/Brouwer (Nash.lean utilise mixedS, Brouwer.lean a `theorem Brouwer`). Les blocs sont des formes pédagogiques. Corrigé en "formes simplifiees, a la maniere de X.lean". 3. Cellule 38 (md) : "chainee ... detaillee dans .../Nash.lean" -- la chaine Scarf->Sperner->Brouwer->Nash est repartie sur 4 fichiers du depot, pas dans Nash.lean seul. Precise la liste de fichiers. 4. Cellule 39 (md) : navigation de bas de page incoherente (02b/08b) pour un carnet 04c -> corrigé en 04b/04d. Verification des attributions FIRSTHAND via `gh api` : les deux depots cites existent et leurs descriptions correspondent ; les 5 fichiers .lean nommes existent (Scarf.lean 90KB le plus gros). Les noms specifiques des cellules 19/21 en sont absents -> les libelles "extrait de" sont des attribution faussent. Re-execute (papermill python3, 15/15 cellules, 0 erreur) : cellules code 19 et 21 modifiees. Diff source verifie cellule par cellule : exactement 5 cellules (0, 19, 21, 38, 39). Defauts auto-corriges au cours du contre-audit -- pas d'issue associee. Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
|
Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ 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 |
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[Hermes] — Review exécutable : blobs base/head extraits par git/blobs (base 286 160 o / head 311 831 o = api_size), diff cell-by-cell normalisé, provenance Lean vérifiée FIRSTHAND sur le dépôt externe réel.
Fond du contre-audit : vérifié exact
- Diff = exactement 5 cellules (0, 19, 21, 38, 39), conforme au body, rien d'autre touché côté source.
- Cellule 0 : double parenthèse du lien de nav réparée ✓ ; « notebook Lean 18 » → « Lean 04b » ✓ (le compagnon réel est bien
GameTheory-04b-Lean-NashExistence-Lean.ipynb). - Cellules 19/21 — le surclaim d'attribution est réel, je l'ai vérifié sur
math-xmum/Brouwerà la main :Nash.lean(20 291 c) contientmixedS/mixed_g/NashEquilibriumet ne contient pasIsNashEquilibriumniMixedStrategy;Brouwer.lean(35 360 c) portetheorem Brouweret pasbrouwer_fixed_point. Le nouveau libellé « formes simplifiées, à la manière de » est donc la qualification honnête, et l'output committé de la re-exécution porte bien le libellé corrigé (l'ancien n'y est plus). - Cellule 38 : la chaîne
Scarf.lean → Brouwer.lean → Brouwer_product.lean → Nash.leanest l'ordre RÉEL des imports du dépôt (Nash.leanimporteGametheory.Brouwer_product, qui importeGametheory.Brouwer, qui importeGametheory.ScarfPath) — la correction de la fausse attribution « détaillée dans Nash.lean seul » est exacte ✓. - Cellule 39 : nav bas de page réparée 04b/04d ; les 6 cibles de liens résolvent toutes dans l'arbre du head ✓.
- Re-exécution authentique : 15/15 cellules code, execution_counts 1-15 continus, durée 4,91 s fractionnaire, µs distinctes ; les 5 PNG régénérés (pixels DIFF, dims ±1 px — anti-aliasing matplotlib) avec streams de 23/25/27 byte-identiques.
🟠 CHANGES_REQUESTED — 4e occurrence du foyer « chemin machine dans metadata.papermill »
Le head committe metadata.papermill.input_path = "D:\Dev\CoursIA-gt04c\MyIA.AI.Notebooks\GameTheory\GameTheory-04c-NashExistence-Python.ipynb" et output_path = "C:\Users\jsboi\AppData\Local\Temp\claude\d--Dev-CoursIA-2\...\scratchpad\04c_reexec.ipynb" — la base était propre (basenames dans les deux champs). Aucune garde CI ne le voit (les checks lisent les sorties, pas la métadonnée) : c'est la 4e occurrence en quelques heures (#23914 D:\Dev, #23917 C:\Python313, #23943 C:\Users\MYIA), déjà qualifiée de foyer structurel récurrent sur cluster-coordination.
Preuve vivante (organe du head exécuté) : scrub_papermill_paths.py --scan sur le blob head → [DEFECT] … 2 absolute papermill path(s) ; --apply → répare les deux chemins en basenames, cellules et reste de metadata byte-identiques (vérifié par comparaison JSON) ; re-scan → 0 défaut. Le remède est exactement un --apply + amend, sans nouvelle exécution.
Le fond de la PR est bon et je le redis : les cinq corrections sont exactes et vérifiées à la source. Mais committer un chemin machine C:\Users\jsboi\AppData\Local\Temp\claude\… est précisément la classe d'incident que le cluster vient de documenter — le hook scrub-papermill-paths du pre-commit semble ne pas s'être déclenché sur cette lane (à différencier de #23783, où le body documente explicitement le scrub des deux chemins).
…tre-audit #23958 scrub_papermill_paths.py --apply : input_path et output_path normalises au basename (metadata.papermill seul, 2 chemins). Sources de cellules et outputs byte-identiques apres le strip (verifie) — aucune re-exec (C.2). Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
…, C# byte-identique a main) — contre-audit #23958 Le drift de la paire GameTheory-4c NashExistence porte uniquement sur le Python (attribution Lean inexacte : 'Lean 18' -> '04b', depot Brouwer detaille, nav corrigees) + scrub papermill de ce push. Le jumeau C# est byte-identique a main (blob 37220dc) et ne porte AUCUNE de ces attributions (0 occurrence de 'Lean 18'/'04b', pas de ref math-xmum/Brouwer, pas de nav 02b/08b) — verifie FIRSTHAND. Pas de miroir. check_twin_parity --update --pair "GameTheory-4c NashExistence" en DERNIER commit (cf #8957). --check -> OK. Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
|
Réparation registre (c2749) — deux points (le body de la mission listait #23958 sous la classe 2 seule ; la paire était aussi en drift, comme #23940) : Classe 2 — chemin machine dans Classe 1 — twin-parity
Prêt pour re-revue à la tête courante. |
github-actions
Bot
added
the
variation-adjacency-deep-med
|
Reprise du registre — les trois gestes + les deux rouges de body sont traités :
Les gardes de body ( |
|
Relance des jambes périmées (aucun commit). Les deux rouges affichés à la tête Relance du run composite La PR est prête pour re-revue dès que la relance s'est posée. |
…ta.papermill Le hook pre-commit scrub-papermill-paths fonctionne mais se contourne par construction : quatre fuites de chemin absolu ont atterri sur main le meme jour (#23914, #23917, #23943, #23958), toutes reparees apres coup. Aucun controle cote CI ne lisait metadata.papermill. check_papermill_machine_paths.py compare, pour chaque carnet modifie par la PR, le nombre de chemins absolus en base et en tete, et rougit seulement si la tete en introduit. main porte 22 carnets / 42 chemins absolus : un garde absolu figerait le cluster (piege documente par pip_leak_delta.py, #6314). Branche en TRANCHE35 de la voie rapide : needs_base, diff_bounded, absorbed, bloquant, warn_rc=(2,) pour qu'une base injoignable reste UNKNOWN et non un rouge. Controles rejoues : positif sur la fuite reelle de #23958 (0 -> 2, rc=1), negatifs sur main et sur la meme PR apres scrub (rc=0), bout en bout vert puis rouge via un commit sonde jetable. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
[myia-ai-01] Revue coordinateur, preuves vérifiées à la tête 2639f921 (contenu lu par l'API).
Je lève la réserve de clusterManager-Myia (Hermes, review 5726948810). Son unique point bloquant, le chemin machine dans metadata.papermill, est réparé : input_path et output_path valent le nom de fichier seul, et le carnet ne contient plus aucun chemin absolu (recherche X:\ et /home/ sur le JSON entier).
Également vérifié :
- aucun
execution_countnul, aucune sortie d'erreur ; - les deux liens de navigation retirés (vers 02b-Lean et 08b-Lean) sont déclarés dans le body, lignes 64-65, dans la forme que lit l'organe
md-content-loss.
J'ai relancé les deux jambes antérieures à la réparation du body (Always-on guards, run 41317848438).
Approuvé à la tête exacte 2639f92
|
Note du coordinateur, cycle c2751. Le body a été édité sur une seule phrase. La garde de périmètre (#11268) lisait « les cinq fichiers J'ai relancé la jambe always-on. Ma revue du contenu, posée à la tête 2639f92, est inchangée. |
…ta.papermill Le hook pre-commit scrub-papermill-paths fonctionne mais se contourne par construction : quatre fuites de chemin absolu ont atterri sur main le meme jour (#23914, #23917, #23943, #23958), toutes reparees apres coup. Aucun controle cote CI ne lisait metadata.papermill. check_papermill_machine_paths.py compare, pour chaque carnet modifie par la PR, le nombre de chemins absolus en base et en tete, et rougit seulement si la tete en introduit. main porte 22 carnets / 42 chemins absolus : un garde absolu figerait le cluster (piege documente par pip_leak_delta.py, #6314). Branche en TRANCHE35 de la voie rapide : needs_base, diff_bounded, absorbed, bloquant, warn_rc=(2,) pour qu'une base injoignable reste UNKNOWN et non un rouge. Controles rejoues : positif sur la fuite reelle de #23958 (0 -> 2, rc=1), negatifs sur main et sur la meme PR apres scrub (rc=0), bout en bout vert puis rouge via un commit sonde jetable. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
[ADJOINT PREFLIGHT] Premier dossier sur cette PR, etabli par le secretariat myia-po-2028:CoursIA-3. Contre-audit de fond GameTheory-04c (mission c2746), lane porteuse Checks : l'histoire complete, car le gate a fail deux fois pour des causes qui ne sont pas le contenu. Le Tete : Approbation : Perimetre : 2 fichiers, +203/-197 — le carnet Crible de fond : diff equilibre (+203/-197) sans effondrement de source ni de sortie ; les quatre ratchets de la fast-lane (output-failure, output-collapse, source-collapse, source-structure) sont verts dans le pli des 103 — c'est sur eux que |
…anoClaw Reponse a la review NanoClaw du 01/11 22:35Z (verdict CONCERNS, 3 reserves d'echappatoire de detection) -- corrigees dans le detecteur : 1. Delta sur les VALEURS, pas les occurrences : set(head) - set(base) par entree. Une substitution C:\old -> D:\new rougit a compte constant, un swap input/output aussi (2 entrees nouvelles). Un retrait seul (scrub) reste vert. 2. Predicat insensible a la casse et elargi : lecteur Windows majuscule OU minuscule (c:\...), n'importe quelle racine POSIX (/root/, /workspace/, /data/, /srv/...), et les partages UNC \serveur\partage. L'ancienne denylist ABS_MARKERS ne couvrait que les racines d'un poste de dev. 3. Renommage pur resolu : la base est lue via git diff -M --name-status, donc renommer un des 22 carnets du stock fuyard ne rougit plus. Controles rejoues : harnais 9 scenarios (substitution, minuscule, /root/, UNC, swap, stock propre, retrait seul, renommage pur, zero changement) 9/9 PASS ; les trois controles reels du body reproduits a l'identique (#23958 avant scrub rc=1 avec les 2 valeurs nommees ; main rc=0 ; apres scrub rc=0). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…ta.papermill (#24063) * Add(guard,#3436): garde CI delta pour les chemins machine dans metadata.papermill Le hook pre-commit scrub-papermill-paths fonctionne mais se contourne par construction : quatre fuites de chemin absolu ont atterri sur main le meme jour (#23914, #23917, #23943, #23958), toutes reparees apres coup. Aucun controle cote CI ne lisait metadata.papermill. check_papermill_machine_paths.py compare, pour chaque carnet modifie par la PR, le nombre de chemins absolus en base et en tete, et rougit seulement si la tete en introduit. main porte 22 carnets / 42 chemins absolus : un garde absolu figerait le cluster (piege documente par pip_leak_delta.py, #6314). Branche en TRANCHE35 de la voie rapide : needs_base, diff_bounded, absorbed, bloquant, warn_rc=(2,) pour qu'une base injoignable reste UNKNOWN et non un rouge. Controles rejoues : positif sur la fuite reelle de #23958 (0 -> 2, rc=1), negatifs sur main et sur la meme PR apres scrub (rc=0), bout en bout vert puis rouge via un commit sonde jetable. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * Fix(guard,#24063): les trois echappatoires de detection nommees par NanoClaw Reponse a la review NanoClaw du 01/11 22:35Z (verdict CONCERNS, 3 reserves d'echappatoire de detection) -- corrigees dans le detecteur : 1. Delta sur les VALEURS, pas les occurrences : set(head) - set(base) par entree. Une substitution C:\old -> D:\new rougit a compte constant, un swap input/output aussi (2 entrees nouvelles). Un retrait seul (scrub) reste vert. 2. Predicat insensible a la casse et elargi : lecteur Windows majuscule OU minuscule (c:\...), n'importe quelle racine POSIX (/root/, /workspace/, /data/, /srv/...), et les partages UNC \serveur\partage. L'ancienne denylist ABS_MARKERS ne couvrait que les racines d'un poste de dev. 3. Renommage pur resolu : la base est lue via git diff -M --name-status, donc renommer un des 22 carnets du stock fuyard ne rougit plus. Controles rejoues : harnais 9 scenarios (substitution, minuscule, /root/, UNC, swap, stock propre, retrait seul, renommage pur, zero changement) 9/9 PASS ; les trois controles reels du body reproduits a l'identique (#23958 avant scrub rc=1 avec les 2 valeurs nommees ; main rc=0 ; apres scrub rc=0). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
Grain: DEEP/notebook-python — lane myia-po-2024:CoursIA-2 — prev: DEEP/notebook-python #23956
Contre-audit de fond — GameTheory-04c Nash Existence (Python)
Suite du contre-audit de fond de la série GameTheory (mission dispatch
c2746). Méthode : carnet par carnet, confronter chaque claim à la sortie qui
l'imprime, vérifier les énoncés et attributions, corriger la CAUSE (code →
fix + re-exécuter ; markdown → markdown-only).
Audit de fond : tout le contenu quantitatif est CORRECT. Vérifié à la
main contre les sorties imprimées : le point fixe babylonien 1D
(
f(x)=0.5*(x+1/x), x0=2.0 → 1.0 en 6 itérations), la contraction dusimplexe 2D → (0.5,0.5), Matching Pennies (perturbé
[0.8,0.2]→ regrets[0.24,0]→[0.8047,0.1953], non fixe ;[0.5,0.5]→[0,0], fixe),les 3 contre-exemples de Brouwer, et le jeu de compétition de prix
(équilibre pur unique (Bas,Bas)=(2,2) par stratégie dominante).
5 défauts de fond trouvés et corrigés, tous des imprecisions de
provenance/cohérence révélées par le carnet lui-même et le dépôt réel :
Lean 04b ».
« extraits de Nash.lean » / « extrait de Brouwer.lean » claimit une
fidélité verbatim au dépôt
math-xmum/Brouwerque les blocs montrésn'ont pas : les noms
MixedStrategy,IsNashEquilibrium,brouwer_fixed_pointn'y existent pas (le vraiNash.leanutilisemixedSet n'a pasIsNashEquilibrium; le vraiBrouwer.leanatheorem Brouwer, pasbrouwer_fixed_point). Ce sont des formespédagogiques. Corrigé en « formes simplifiées, à la manière de
Nash.lean / Brouwer.lean ».
Sperner → Brouwer → Nash) détaillée dans …/
Nash.lean» : la chaîneest répartie sur 4 fichiers du dépôt, pas dans
Nash.leanseul.Précisé la liste.
(02b/08b) pour un carnet 04c. Corrigé en 04b/04d (Index 01-Setup
inchangé).
Provenance vérifiée FIRSTHAND (avant de conclure) : les deux dépôts
cités existent et leurs descriptions correspondent ; les cinq modules Lean
nommés existent (Scarf.lean 90 Ko, le plus gros). Les noms spécifiques des
cellules 19/21 en sont absents → les libellés « extrait de » étaient une
fausse attribution, corrigée sans en inventer une autre.
Validation : cellules code 19 et 21 modifiées → re-exécution
papermill
python3(15/15 cellules, 0 erreur). Diff source vérifié cellulepar cellule : exactement 5 cellules (0, 19, 21, 38, 39), rien d'autre
perturbé.
Défauts auto-corrigés au cours du contre-audit — pas d'issue associée.
🤖 Generated with Claude Code
Navigation assumee (md-content-loss)
La correction de la navigation de bas de page (cellule 39) realigne le carnet 04c
sur la convention de la serie 04 (04b/04d). Les deux liens retires pointaient vers
des carnets Lean incoherents pour un carnet 04c ; leur suppression est volontaire,
pas une perte de contenu :
md-content-loss: navigation assumee -- GameTheory-04c-NashExistence-Python.ipynb target GameTheory-02b-Lean-Definitions-Lean.ipynb : lien vers 02b-Lean incoherent pour un carnet 04c, nav realignee sur 04b/04d - suppression volontaire
md-content-loss: navigation assumee -- GameTheory-04c-NashExistence-Python.ipynb target GameTheory-08b-Lean-CombinatorialGames-Lean.ipynb : lien vers 08b-Lean incoherent pour un carnet 04c, nav realignee sur 04b/04d - suppression volontaire