[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2024:CoursIA — prev: DEEP/notebook-lean #22903

Carnet 5/5 de #17357 : Lean-13b-CHSH-Tsirelson-Native.ipynb (26 cellules, 18 markdown,
8 de code, kernel lean4-wsl-conway).

Ce que ce carnet avait, et ce qu'il n'a pas

Le contre-audit a commence par une liste de six candidats. Trois ont resiste a la
mesure, trois sont tombes. Le carnet est nettement plus solide que sa lecture de
surface ne le laissait croire, et c'est la partie du rapport qui a le plus de valeur :
un contre-audit qui ne rapporte que ses prises laisse croire que tout le reste a ete
verifie.

Defauts confirmes — 3 cellules, toutes markdown

#	Cellule	Affirmation	Ce qui la contredit
D1	0	la borne de Tsirelson (1980) est « la premiere separation quantique/classique prouvee de l'histoire de la physique »	la primaute est fausse (la separation est etablie par Bell en 1964, la forme testable par CHSH en 1969 ; 1980 donne la borne quantique). Attribution inverifiable ici : le gisement bibliographique partage n'est pas montable sur cette machine, et la regle d'hygiene bibliographique interdit d'ecrire une attribution depuis un resume. Route soustractive : le superlatif est retire, la reference datee est conservee
D2	7	« Deux lignes disent "prouve dans ce lake", une dit "importe" »	la table de la meme cellule en porte trois (« classique deterministe », « classique randomise », « separation ») et une importee. Le compte faux est dans la phrase qui commente le tableau qu'elle surplombe
D3	19	« le profile est-il maximal ? »	accord : profil

Verifie exact — et donc NON corrige (mesure, pas lecture)

Six candidats examines, six ecartes. La liste est le vrai contenu de ce passage :

• Symetrie de la cellule 16 — score(a, a_barre, b, b_barre) = -score(a,a,b,b).
  Calcul exhaustif des 16 profils : aucun contre-exemple. Algebre : avec a_barre = -a
  et b_barre = -b, on a score = -2ab = -score(a,a,b,b) ; la forme fermee tombe de
  CHSH.score et de score_factorization, que le carnet ne cite pas mais qui la fonde.
  La cellule 16 est exacte.
• |score| <= 2 (cellule 0) vs |score| = 2 (module) — pas une contradiction :
  Conway.CHSH.classical_bound enonce litteralement |score| <= 2, et les 16 profils
  donnent tous |score| = 2, ce que la cellule 16 dit etre « sature ». Les deux formes
  coexistent sans se contredire.
• Pin dual v4.32.1 / v4.33.0 (cellule 25) — c'est la forme « Famille B » posee
  par fix(lean,#17357): sweep pin v4.32.1 Famille B -- mention duale provenance/pin courant (3 carnets) #18238 (git show e61db7ed6ae), deliberee. Ne pas la « corriger ».
• #15700 nomme le kernel lean4-wsl (cellule 1) — exact : le body de l'issue le
  dit ligne 50 et ligne 76. La divergence assumee vers lean4-wsl-conway est donc
  correctement attribuee.
• Enveloppe {"env": 0} (cellule 3) — exact : la sortie committee de la cellule 2
  est {"env": 0} sans message, ce qui fonde la phrase sur l'import paresseux.
• Comptes et sorties — 8 #check sont 8, 5 #print axioms rendent bien
  [propext, Classical.choice, Quot.sound], le tableau des sept classes de types de la
  cellule 10 correspond exactement a la signature de tsirelson_bound, le statut
  « importe / prouve localement » de chaque ligne est conforme au module, et les trois
  #eval de controle des exercices rendent les valeurs annoncees (2, 2, -2).

Resync traduction — la moitie qu'on oublie

Les trois cellules editees portaient une ligne dans
translations/symbolicai-lean/symbolicai-lean.csv (pivot rempli a 100 %, colonnes cibles
vides pour cette serie). La PR resynchronise ces trois lignes avec l'outil du depot :

python scripts/translation/extract_cells_to_csv.py <carnet> --update <csv> --repo-root .
# OK (--update) : 3 ligne(s) rafraichie(s), 23 deja in-sync, 4066 ligne(s) d'autres notebooks preservees

Seuls src_hash, text_fr et hash_fr changent, sur trois lignes
(3666be08, ae99c202, 72b4abe4) ; les colonnes cibles restent intactes.

Mesures :

• check_translation_sync.py : 20 anomalies avant, 20 apres, zero sur Lean-13b
  (les 20 sont la dette preexistante d'autres carnets de la serie) ;
• check_pr_translation_drift.py origin/main : 1 changed notebook | 1 covered by translations/ | 0 cell(s) flagged — aucune cellule n'entre dans le sous-ensemble chaud.

Rejeu (C.2) — non du, et pourquoi

Aucune cellule de code n'est touchee : les trois editions tombent dans les cellules
markdown 0, 7 et 19. Verifie champ par champ sur le JSON avant/apres : les 8 cellules
de code sont byte-identiques (outputs, execution_count, metadata, source),
round-trip JSON byte-identique garde avant ecriture (131937 -> 131844 octets), et le
fichier committed re-serialise a l'identique.

Gates passees sur la tete

Gate	Verdict
check_output_failure_text.py origin/main	1 carnet, 0 regresse
check_output_collapse.py origin/main	1 carnet, 0 flag
check_source_collapse.py origin/main	1 carnet, 0 flag
check_prose_quantitative_claims.py --diff	OK
check_activity_leak.py --diff	OK
check_pr_translation_drift.py origin/main	OK

Reliquat hors perimetre — les deux siblings du module

Le docstring de Conway/CHSHQuantum.lean et de Conway/CHSHQuantum_en.lean
(lignes 74-80) porte trois affirmations devenues fausses :

1. le carnet serait « prevu … pas encore livre : ce renvoi est prospectif, pas un
   fichier existant » — il existe depuis Add(lean,#20204): GOL-08/GOL-09 -- GameTheory-20d/20e rejoignent la sous-série GOL #20515 ;
2. il tournerait sous le kernel lean4-wsl — il declare lean4-wsl-conway ;
3. il pointe Lean-16f-Conway-Free-Will-Theorem.ipynb, qui n'existe pas ; le fichier
   reel est Lean-16c-Conway-Free-Will-Theorem.ipynb (c'est celui que citent la
   cellule 0 et la cellule 25).

Corriger un docstring de module change l'empreinte du lake et exige un rebuild : autre
sujet qu'un carnet, a dispatcher.

See #17357

🤖 Generated with Claude Code

[github-actions]

Translation guard violation (#10332).

translation-guard violation: no override label 'translation-override' and no comment marker '[TRANSLATION-OVERRIDE] '. NOTE (#15198): translation-sync is on manual-maintainer hold since 2026-08-12 (#10038) -- editing the FR source does not refresh the derived file until the hold is lifted; while it stands, the dual-key override (#10332) is the expected exit for a legitimate change.

Three exits to clear this gate:

1. Restore the derived files (git checkout origin/main -- translations/ <lang-notebooks>) and edit the source notebook instead -- the bot re-derives when it runs again: translation-sync is on manual-only hold since 2026-08-12 (i18n notebooks : T4 renderer + CI autonome — sortir du moteur qui tourne a vide (mandat user 2026-08-08) #10038), so the derived file stays stale until the hold is lifted (ci(guard): translation-guard prescrit un remede inapplicable -- le bot qui 're-derive' est dormant depuis 25 jours (hold #10038), l'override d'exception devient le seul chemin #15198).
2. While the i18n notebooks : T4 renderer + CI autonome — sortir du moteur qui tourne a vide (mandat user 2026-08-08) #10038 hold stands, this is the expected exit for a legitimate derived-file change: add the translation-override label AND a PR comment whose FIRST line is [TRANSLATION-OVERRIDE] <motif> (both required -- dual-key, see translation-guard : aucun mecanisme d'arbitrage ecrit — 2 overrides legitimes ce cycle passes par un bypass admin non auditable #10332).
3. Ask the coordinator to re-arbitrate (override motif must be journalised in this gate's log; a bare admin bypass leaves no trace).

See #10332 for the override protocol.

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

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]

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

[jsboige]

[TRANSLATION-OVERRIDE] resync per-cellule du CSV exige par le ratchet hot-drift (#20232/#13551) apres edition de 3 cellules FR -- lignes produites par scripts/translation/extract_cells_to_csv.py --update, aucune edition a la main

PR #22908 (contre-audit de fond #17357, carnet 5/5).

Trois cellules markdown du carnet Lean-13b-CHSH-Tsirelson-Native.ipynb sont corrigees (cellules 0, 7, 19). Ces trois cellules portent une ligne dans translations/symbolicai-lean/symbolicai-lean.csv, et le ratchet hot-subset (#13551) exige une resynchronisation per-cellule apres une edition FR.

Le resync n'est pas une edition a la main : il est produit par l'outil du depot, scripts/translation/extract_cells_to_csv.py --update, qui ne rafraichit que src_hash, text_fr et hash_fr des lignes dont la source a change.

Mesures :

• 3 lignes rafraichies (3666be08, ae99c202, 72b4abe4), 23 deja in-sync, 4066 lignes d'autres carnets preservees ;
• colonnes cibles (src_hash_*, hash_*) intactes ;
• check_translation_sync.py : 20 anomalies avant, 20 apres, zero sur Lean-13b ;
• check_pr_translation_drift.py origin/main : 0 cell(s) flagged.

translation-sync.yml est en hold manuel depuis le 2026-08-12 (#10038 / #15198) : aucune re-derivation automatique ne reprendra ces lignes, donc l'etat derive juste est celui qui doit partir avec la PR.

Voir #10332 pour le protocole d'override a double cle.

[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.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.2s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.7s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.7s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.8s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.5s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	20.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.9s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	12.1s

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

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 8
• 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]

Path-collision (organ #13359/#13615)

Cette PR #22908 (Fix(notebooks,#17357): Lean-13b -- 3 defauts confirmes, 6 candidats mesures et ecartes) 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.

• faible -- Rename(Lean,#17545): T6 -- descente Lean-31 vers ANALYSE-13-Euler-Navier-Stokes-Python #22643 partage : translations/symbolicai-lean/symbolicai-lean.csv
• faible -- Docs(Lean,#22649): ANALYSE -- la vraie ligne 09, la ligne du 06 Python, marches recohérentes #22670 partage : translations/symbolicai-lean/symbolicai-lean.csv
• faible -- Rename(#17545): T2 GALOIS - descente de l'ilot (carnet 22 + lake galois_lean) #23116 partage : translations/symbolicai-lean/symbolicai-lean.csv

[clusterManager-Myia]

[Hermes] Review Lean-13b (tête cb5ea94e, blobs carnet 9c77bce0→dfdc1f68, 26 cellules stables base↔head).

Les 3 corrections du body sont vérifiées au blob, et chacune est la bonne correction :

• D1 (c0) — le superlatif « la première séparation quantique/classique prouvée de l'histoire de la physique » est retiré, la « borne de Tsirelson (1980) » conservée. Diff = exactement ces 2 lignes → 1. La route soustractive est la bonne : la primauté appartient à Bell 1964/CHSH 1969, 1980 ne donne que la borne ; retirer le superlatif plutôt que de le ré-attribuer respecte la règle d'hygiène bibliographique. histoire de la physique : 0 hit au head.
• D2 (c7) — recompté mécaniquement sur la table committée : les 4 lignes de régimes portent « prouvé dans ce lake » ×3 (classique déterministe, classique randomisé, séparation) + « importé de Mathlib » ×1 (quantique). La phrase « Trois lignes disent… une dit importé » est maintenant exacte. (Note : Conway.CHSHRandomized.randomized_bound est bien « lake » aussi — le compte de 3 est le bon.)
• D3 (c19) — « le profile est-il maximal ? » → « le profil » : 0 profile restant au head, 7 profil (tous conformes).

Resync traduction vérifiée par diff CSV complet (5 Mo, extraits par git/blobs) : 4093 lignes base↔head, exactement 3 lignes changées, uniquement les colonnes src_hash, text_fr, hash_fr — colonnes cibles intactes, 4090 autres lignes préservées. Conforme au compte de l'outil du body (3 rafraîchies / 23 in-sync / 4066 préservées).

Sur les 6 candidats écartés : j'ai vérifié les deux plus sujets à caution par lecture du head — (a) |score| ≤ 2 (c0, énoncé de borne) vs = 2 (c16, saturation des 16 profils) : les deux formes coexistent sans contradiction, le body a raison de ne pas « corriger » ; (b) l'enveloppe {"env": 0} de la c3 fond bien la phrase sur l'import paresseux (sortie committee de c2). Les claims d'exactitude des #print axioms (5× [propext, Classical.choice, Quot.sound]) et des 3 #eval (2, 2, −2) sont corroborés par les sorties committées au head — non re-compilés (kernel lean4-wsl-conway non montable sur ce siège, comme le gisement bibliographique ; la CI Lean couvre cette jambe).

CI au head cb5ea94e : 90 success / 0 failure, PR gate: PASS. Le seul check non-vert était Exec-sequence ratchet (base vs PR) cancelled à l'attempt 1 (07:05→07:20Z) — pas un échec du head ; j'ai relancé le job (gh run rerun, attempt 2 en cours au moment du POST, je ne le compte ni vert ni rouge).

Verdict : micro-PR exemplaire de discipline — 3 défauts confirmés, 6 candidats mesurés puis écartés avec leurs raisons, périmètre strictement confiné (3 cellules markdown + 3 lignes CSV). Rien à ajouter.