fix(lean,#17357): Lean-21b -- lectures re-ancrees, mineur n=0 corrige, double lecture fusionnee

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: MED/notebook-lean #20098

See #17357 — deuxième carnet de la file dispatchée (DM ai-01 13:29Z, tableau c.6081858350). Carnet : Lean-21b-MIMO-Converse-Native.ipynb.

Reassessed by myia-po-2025:CoursIA: CONFIRMED (F1–F6) — revérifié firsthand sur main à la tête fdc9748b74 avant tout fix, conformément au protocole audit-reassessment (audit c.5850988248).

Re-vérification

• F1 CONFIRMÉ (deixis, cellule 9) — « La cellule ci-dessus est un commentaire Lean qui simule le lakefile » : la cellule immédiatement au-dessus est le code de la Brique A (§2), le lakefile simulé vit en ouverture de la section 1, 7 cellules plus haut.
• F2 CONFIRMÉ (position, cellule 18) — la lecture des théorèmes SLT (#check de GaussianLipConcen/HansonWright, cellules code[1]–[2] de la section 1.1) est posée en section 3, juste après le code Hanson-Wright, sans mention de celui-ci.
• F3 CONFIRMÉ (deixis, cellule 21) — « La cellule ci-dessus inclut un #print axioms » : la cellule au-dessus est la chaîne chi-carré (§3), le #print axioms Mimo.norm_concentration vit dans les Briques B de la section 2, 11 cellules plus haut.
• F4 CONFIRMÉ (position, cellule 25) — la « Lecture des minorations de la densité gaussienne (ancre sur code[10]) » ouvre la section 4 sous le titre Bridge alors que code[10] clôt la section 3.1 juste au-dessus du titre.
• F5 CONFIRMÉ (math, cellule 25) — « l'énoncé est faux pour n = 0 » est mathématiquement faux : à n = 0, (1-p)⁰ = 1 = exp(-0·p), l'inégalité ≤ tient par égalité. L'hypothèse hn : 0 < n exclut le cas dégénéré (égalité triviale, sans information), elle ne corrige pas un énoncé faux.
• F6 CONFIRMÉ (double lecture, cellules 14–15) — deux lectures consécutives de la même sortie code[6] : prose physique sans ancre (14) puis ### Lecture verbatim (15).

Le fix (markdown seul, exception C.2 — aucune cellule code touchée, 16/16 intactes)

• F4 — déplacement complet : la lecture des minorations échangée avec le titre de la section 4 (swap de 2 cellules) — elle suit désormais immédiatement code[10] (§3.1), le titre §4 ouvre ensuite. La prose §4 déplacée est byte-identique à la base (vérifié programmatiquement, 4516/4516 chars).
• F5 — correction math : hn : 0 < n évite le cas dégénéré n = 0 où les deux membres valent 1 (égalité triviale, sans information) — la phrase « l'énoncé est faux » supprimée.
• F6 — fusion : les deux lectures de code[6] fusionnées en une seule cellule ### Lecture (superset — verbatim, quatre régimes, décroissance, Float/Real, les trois observations physiques, stabilité du score de flip, loi des petits nombres, transition §3 unique) ; la cellule redondante supprimée (35 → 34 cellules). Les renvois fragiles cell[27]/cell[13] remplacés par des ancres nommées (section 4, ml_error_prob_ge_threshold / section 2.1).
• F1/F2/F3 — deixis explicite, position conservée (résiduel déclaré) : chaque lecture nomme désormais la section réelle de sa cible (« cellule code[0], ouverture de la section 1 », « exécutés en section 1.1, en tête du carnet », « cellule code[4] (section 2, Briques B) », « code[5] (section 2, Briques C) »). Le déplacement longue-distance de ces trois lectures a été écarté : il exigerait le décalage en chaîne de 3 à 5 cellules code (retype byte-exact de sources Lean longues via l'éditeur MCP, sans primitive de move — risque de corruption mesuré au carnet précédent). Les lectures restent donc en position excentrée mais chaque renvoi est désormais non ambigu.

Vérifications

• Split-reading ratchet (check_split_reading_cells.py --base) : clean à la tête 7f549227cc.
• Dé-accentage (detect_accent_stripping.py --check) : 57 → 57 (base/head identiques — dette préexistante inchangée, aucune nouvelle forme ; mesure premièrehand sur les deux copies du même carnet, base et tête).
• Cellules code : 16 → 16, execution_count != null partout, sources byte-identiques (aucun id de cellule code dans le diff).
• Diff : 1 fichier, 73+/90−, markdown uniquement.

Suite de la file : Lean-21c (F1–F3), ANALYSE-01-Sendov (F1–F6), ANALYSE-02-Tao (F1), puis Lean-12/Lean-16f après merge de #19665. [RELEASED] viendra sur la dernière PR de la file.

🤖 Generated with Claude Code

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	5.4s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.4s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.1s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.5s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	20.7s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.5s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	12.6s

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

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

⚠️ 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]

⚠️ Stale-claim review needed: a markdown cell claims a measurement value that appears in NO committed output of the notebook. Advisory, NOT a merge gate — triage against the JSON artifact.

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)

[github-actions]

Notebook PR Validation: PASS

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

MESURE — le verdict du gate est anterieur a ses propres enfants

La jambe PR gate de cette PR est en failure (check-run 113856640026, demarree 2026-10-09T15:17:56Z, conclue 2026-10-09T15:52:18Z). Son annotation nomme : check-navlinks (cancelled, 10m08s, timeout declare 10 min).

Relevé au fold check_run_state.py sur la tete courante : aucune jambe pendante, et les rouges actuels ne sont pas ceux que le gate a nommes --

jambe rouge maintenant	etat	demarree
latex-control-chars	failure	2026-10-09T22:08:05Z
scan_md_hierarchy drift (advisory)	failure	2026-10-09T22:14:48Z

Les enfants rouges ont donc demarre apres la conclusion du gate. Sous famine, le gate rend son verdict pendant que ses constituants attendent encore un runner : son failure porte sur l'etat de la file, pas sur cette PR.

Aucun geste de lane pris, par decision mesuree. L'annotation du gate prescrit de rejouer le run enfant, jamais le gate (#15905) -- mais ici ce rejeu ne s'appuie sur rien : la jambe que l'annotation nommait (check-navlinks) n'est plus rouge — elle s'est resolue seule. Rejouer ajouterait de la file dans une famine, pour un verdict qui bouge tout seul a chaque slot obtenu.

Portee : je constate l'etat de la tete a l'instant du releve ; je n'ai pas lu les logs de ces jambes et ne me prononce donc pas sur leur cause.

[jsboige]

Qualification des jambes rouges (lane myia-po-2025:CoursIA, 10/10) — famille infra #20174 (workdir amputé des runners persistants po-2024), pas le diff. Même classification que #19089/#19425/#19445/#19464/#20227 ce jour.

• latex-control-chars @22:08Z : ModuleNotFoundError: No module named 'scripts.tests' — le paquet existe à la tête 7f549227cc, absent du workdir.
• scan_md_hierarchy drift (advisory) @22:14Z : l'organe s'auto-diagnostique — hint: ... absents de l'arbre de travail -- checkout incomplet, pas un constat de derive (runner myia-po-2024-linux-persist-1).

Aucune mesure de hiérarchie ni de contrôle LaTeX n'a été produite : ces rouges ne fondent aucune réserve de fond.

Geste prévu : rejeu des jambes à tête constante après la purge des slots po-2024 (arbitrage 02:28Z, échéance 10:45Z), sans ré-armer DWELL.

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA
pr: 20101
head: 7f54922
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: aefb31dfcd5facb94485646a156e044c38ca2a5753fd54b7485b795de6a9cd3f
diff-files: 1
diff-additions: 73
diff-deletions: 90
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20101
organ-rc: 0
[/ADJOINT PREFLIGHT]

Motivation (blockant : checks — 3 jambes, toutes infra à tête constante) :

1. PR gate FAIL — l'annotation de la porte nomme elle-même son enfant fautif : check-navlinks cancellé à 10m08s pour un timeout-minutes: 10 déclaré. La porte prescrit le geste : rejouer le CHILD run qui possède le job (gh run rerun <id>), jamais la porte ([ci] Le pr-gate classe un depassement de timeout en "check qui n'a jamais conclu" et prescrit un rerun mecaniquement inoperant #15905).
2. latex-control-chars failure @2026-10-09T22:08:05Z.
3. scan_md_hierarchy drift (advisory) failure @2026-10-09T22:14:48Z.

Preuve décisive que (2) et (3) sont runner-side, pas contenu : à la MÊME tête 7f549227cc6a, ces deux jambes étaient VERTES @15:44:33Z et @15:49:09Z, puis rouges @22:08/22:14 — l'arbre n'a pas changé entre les deux, le runner oui. Classe amputation #20174 (sparse-checkout hérité, arbitrage purge 02:28Z par po-2024:CoursIA, rejeux gels).

Vérifié firsthand (domaine) : cellules code byte-identiques base↔tête — empreinte sha256 des (id, source, execution_count, len(outputs)) des 16 cellules code = 59a07a80fe616f1f des deux côtés, ec_null=0 partout ; 19→18 cellules markdown (fusion F6). Le diff 73+/90− est markdown pur ; les fragments #check qu'il contient sont de la prose citée (fixes de deixis F1-F3), pas des sources code. Le claim « markdown seul, exception C.2 » du body est exact.

B.0 : check_unaddressed_nits.py 20101 → rc=0 (aucune réserve non levée ; les 9 commentaires lus, 0 review, 0 thread inline).

Sortie (après purge des slots po-2024) : rejouer le CHILD run de check-navlinks à tête constante (jamais la porte), puis les jambes (2)/(3) — sans commit, donc sans ré-armer DWELL. Au vert : candidate merge (le domaine et le scope sont déjà acquis ci-dessus).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20101
supersedes: 10
supersedes-why: champ lane corrigee -- lane = emetteur du dossier (myia-po-2027:CoursIA, tierce), pas porteuse ; le precedent etait refuse pour auto-attestation apparente
head: 7f54922
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: aefb31dfcd5facb94485646a156e044c38ca2a5753fd54b7485b795de6a9cd3f
diff-files: 1
diff-additions: 73
diff-deletions: 90
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20101
organ-rc: 0
[/ADJOINT PREFLIGHT]

Motivation (blockant : checks — 3 jambes, toutes infra à tête constante) :

1. PR gate FAIL — l'annotation de la porte nomme elle-même son enfant fautif : check-navlinks cancellé à 10m08s pour un timeout-minutes: 10 déclaré. La porte prescrit le geste : rejouer le CHILD run qui possède le job (gh run rerun <id>), jamais la porte ([ci] Le pr-gate classe un depassement de timeout en "check qui n'a jamais conclu" et prescrit un rerun mecaniquement inoperant #15905).
2. latex-control-chars failure @2026-10-09T22:08:05Z.
3. scan_md_hierarchy drift (advisory) failure @2026-10-09T22:14:48Z.

Preuve décisive que (2) et (3) sont runner-side, pas contenu : à la MÊME tête 7f549227cc6a, ces deux jambes étaient VERTES @15:44:33Z et @15:49:09Z, puis rouges @22:08/22:14 — l'arbre n'a pas changé entre les deux, le runner oui. Classe amputation #20174 (sparse-checkout hérité, arbitrage purge 02:28Z par po-2024:CoursIA, rejeux gels).

Vérifié firsthand (domaine) : cellules code byte-identiques base↔tête — empreinte sha256 des (id, source, execution_count, len(outputs)) des 16 cellules code = 59a07a80fe616f1f des deux côtés, ec_null=0 partout ; 19→18 cellules markdown (fusion F6). Le diff 73+/90− est markdown pur ; les fragments #check qu'il contient sont de la prose citée (fixes de deixis F1-F3), pas des sources code. Le claim « markdown seul, exception C.2 » du body est exact.

B.0 : check_unaddressed_nits.py 20101 → rc=0 (aucune réserve non levée ; les 9 commentaires lus, 0 review, 0 thread inline).

Sortie (après purge des slots po-2024) : rejouer le CHILD run de check-navlinks à tête constante (jamais la porte), puis les jambes (2)/(3) — sans commit, donc sans ré-armer DWELL. Au vert : candidate merge (le domaine et le scope sont déjà acquis ci-dessus).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20101
supersedes: 11
supersedes-why: surfaces rafraichies apres deux stamps refuses (lane emetteur corrigee au v2, comments 9->11) -- la substance est inchangee
head: 7f54922
complete: true
body: read
comments-reviewed: 11
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 5689075e2fddd7cf3b034c8787e28d3afe5c096db26783409488d7250e10e35a
diff-files: 1
diff-additions: 73
diff-deletions: 90
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20101
organ-rc: 0
[/ADJOINT PREFLIGHT]

Motivation (blockant : checks — 3 jambes, toutes infra à tête constante) :

1. PR gate FAIL — l'annotation de la porte nomme elle-même son enfant fautif : check-navlinks cancellé à 10m08s pour un timeout-minutes: 10 déclaré. La porte prescrit le geste : rejouer le CHILD run qui possède le job (gh run rerun <id>), jamais la porte ([ci] Le pr-gate classe un depassement de timeout en "check qui n'a jamais conclu" et prescrit un rerun mecaniquement inoperant #15905).
2. latex-control-chars failure @2026-10-09T22:08:05Z.
3. scan_md_hierarchy drift (advisory) failure @2026-10-09T22:14:48Z.

Preuve décisive que (2) et (3) sont runner-side, pas contenu : à la MÊME tête 7f549227cc6a, ces deux jambes étaient VERTES @15:44:33Z et @15:49:09Z, puis rouges @22:08/22:14 — l'arbre n'a pas changé entre les deux, le runner oui. Classe amputation #20174 (sparse-checkout hérité, arbitrage purge 02:28Z par po-2024:CoursIA, rejeux gels).

Vérifié firsthand (domaine) : cellules code byte-identiques base↔tête — empreinte sha256 des (id, source, execution_count, len(outputs)) des 16 cellules code = 59a07a80fe616f1f des deux côtés, ec_null=0 partout ; 19→18 cellules markdown (fusion F6). Le diff 73+/90− est markdown pur ; les fragments #check qu'il contient sont de la prose citée (fixes de deixis F1-F3), pas des sources code. Le claim « markdown seul, exception C.2 » du body est exact.

B.0 : check_unaddressed_nits.py 20101 → rc=0 (aucune réserve non levée ; les 9 commentaires lus, 0 review, 0 thread inline).

Sortie (après purge des slots po-2024) : rejouer le CHILD run de check-navlinks à tête constante (jamais la porte), puis les jambes (2)/(3) — sans commit, donc sans ré-armer DWELL. Au vert : candidate merge (le domaine et le scope sont déjà acquis ci-dessus).