fix(lean,#17357): Lean-21 F1/F3/F4 -- prose alignee sur la borne reelle noise_norm_tail

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2025:CoursIA — prev: DEEP/notebook-dotnet #20093

See #17357 — premier carnet de la file dispatchée (DM ai-01 13:29Z, tableau c.6081858350). Carnet : Lean-21-MIMO-Detection-Flips.ipynb.

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

Re-vérification (audit c.5850123084)

• F1 CONFIRMÉ (stale-claim, cellule 23) — la prose citait noise_norm_tail : P(‖w‖ ≥ t) ≤ exp(−Mt²/2) (queue absolue, M=200 dans l'exposant). La signature réelle imprimée par le lac en Code 2.5 est une concentration bilatérale autour de l'espérance : P(|‖w‖ − E‖w‖| ≥ t) ≤ 2·exp(−t²/2), constante sans dimension. La cellule Monte-Carlo suivante mesure d'ailleurs la déviation |‖w‖ − E‖w‖| > t (ratios max ~0,27), pas ce que la prose annonçait.
• F3 CONFIRMÉ (exercise-mismatch, cellule 36) — l'Exercice 4 demandait r(t) = P(‖w‖ ≥ t)/exp(−Mt²/2) ≤ 1 : insatisfaisable (~10¹⁰ à t=0,5, puisque ‖w‖ ≈ 14 et l'exposant vaut −Mt²/2). L'écart ne se refermait qu'en réinterprétant t comme dépassement au-delà de l'espérance — ce que l'énoncé n'écrivait pas.
• F4 CONFIRMÉ (stale-claim, cellule 23) — la prose annonçait « Cette cellule #check les six déclarations » alors que la cellule suivante est pure numpy (0 #check, commentaire explicite « sans lake local ») ; les signatures vivent en Code 2.5.
• F2 : faux positif — déjà tranché par ai-01 au dispatch, non retouché.

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

Cellule 23 : prose réécrite sur la borne réelle — les six déclarations sont interrogées en Code 2.5 (rappel du snippet), la cellule suivante est la confrontation numérique autonome ; chiffres mesurés cités depuis la sortie réelle (ratio ≤ 1 partout, plafond ~0,27 stable sur M ∈ {50, 200, 1000} — la concentration autour de la moyenne est sans dimension, exactement ce que dit le théorème).

Cellule 36 (Exercice 4) : réécrit sur la déviation P_emp = P(|‖w‖ − E‖w‖| > t) confrontée à 2·exp(−t²/2) — ratio ≤ 1 vérifiable ; l'aller-plus-loin porte désormais le vrai contenu du théorème (‖w‖ croît comme √M, son écart à la moyenne reste d'ordre constant — l'échelle que capture la borne sans dimension), remplaçant l'observation fausse « ratio chuter vers 0,5 ».

Vérifications

• Dé-accentage : 173 → 173 (aucune nouvelle forme, mesure base/head par stash).
• Split-reading ratchet : CLEAN à la tête.
• Diff : 1 fichier, 40+/29−, deux cellules markdown uniquement.

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

🤖 Generated with Claude Code

[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	8.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	8.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	9.3s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	5.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	3.8s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	45.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	5.4s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	23.9s

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

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20098 (fix(lean,#17357): Lean-21 F1/F3/F4 -- prose alignee sur la borne reelle noise_norm_tail) 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.

• terminal -- fix(lean,#19733): Lean-21 cell[9] WSL/native subprocess fork #19858 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb, recouvrement de chemins 100% -- fix(lean,#19733): Lean-21 cell[9] WSL/native subprocess fork #19858 est deja sur main.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

[clusterManager-Myia]

VERDICT: LGTM

[Hermes] po-2026 — revue du delta (F1/F3/F4) sur Lean-21-MIMO-Detection-Flips.ipynb, head 10ae3950. Carnet extrait intégralement au head (41 cellules), pas seulement le diff.

Vérification firsthand contre les sorties committées

• F1 (stale-claim cellule 23) — la cellule 17 (execution_count 7) imprime les six signatures de NormTails, dont Mimo.norm_concentration_one_sided {n : ℕ} (hn : 0 < n) (t : ℝ) (ht : 0 < t) : ((GaussianMeasure.stdGaussianE n) {x | t ≤ ‖x‖ - ∫ …}. C'est bien une concentration bilatérale autour de l'espérance, conforme à la prose réécrite P(|‖w‖ − E‖w‖| ≥ t) ≤ 2·exp(−t²/2), et la mention de l'ancienne queue absolue exp(−Mt²/2) (ainsi que le M = 200 dans l'exposant) a bien disparu. La cellule Monte-Carlo mesure bien la déviation |‖w‖ − E‖w‖|, comme l'annonce la prose.
• F3 (exercise-mismatch cellule 36) — l'énoncé est réaligné sur r(t) = P_emp / (2·exp(−t²/2)), cohérent avec la borne réellement prouvée ; l'ancienne forme P(‖w‖ ≥ t)/exp(−Mt²/2) ≤ 1 était insatisfaisable (exposant en M, décrit dans le corps du PR).
• F4 (stale-claim cellule 23) — la cellule 24 (exec=9) est bien pure numpy sans #check, et ses sorties committées portent borne 2e^(-t^2/2) = [1.765 1.2131 0.6493 0.2707 0.0879 0.0222] avec les ratios max 0,274 / 0,271 / 0,275 pour M ∈ {50, 200, 1000}. La nouvelle prose (« plafonne à ~0,27 — stable quand M varie ») et les valeurs M ∈ {50, 200, 1000} sont présentes dans les sorties ✓ (l'ancien M = 200 unique est corrigé).
• Sécurité : 0 match credential. Aucun défaut nouveau introduit par ce delta.

Reste un artefact cosmétique du code, déjà auto-documenté par son commentaire : le titre de colonne P(||w||-E>||w||>t) (double >) tandis que le calcul est bilatéral — le commentaire du bloc dit (one-sided, mais le theoreme est bilatere). Non bloquant.

Gate CI — check-nav-chain ROUGE, et ce n'est pas un défaut de ce carnet. Le job s'arrête à Run actions/checkout@v4 : error: Could not read 7de69840584ff3fe970cb5fd59def806eecc454d / fdc9748b74817e60d5910b70455bf97b0a103ac6 puis exit code 128 — le magasin d'objets partagé ne portait pas le blob de base au moment du run. L'organe n'a pas atteint son assertion (Updating files: 100% (2/2), puis échec du checkout). Idem Twin parity audit (9 s). À rejouer, pas à réparer dans la PR (mesuré par gh run view --log-failed, même signature que #19537 aujourd'hui).

[Hermes hermes-pr-review, cycle :15 09/10, host 1ed7af3074fb, sig=8ca9151c]

[jsboige]

Diagnostic du rouge PR gate sur le head 10ae395030 : cause runner, aucun defaut de la PR.

Chaine. Le job PR gate echoue sur un seul verdict — [pr-gate] FAIL -- failing checks: check-nav-chain (failure) (job 113851803734, 15:17:22Z). La jambe check-nav-chain (job 113851803673) n'atteint jamais le checker :

Checking out the ref
[command]/usr/bin/git checkout --progress --force refs/remotes/pull/20098/merge
##[error]error: Could not read 7de69840584ff3fe970cb5fd59def806eecc454d
##[error]error: Could not read fdc9748b74817e60d5910b70455bf97b0a103ac6
##[error]The process '/usr/bin/git' failed with exit code 128

La jambe Twin parity audit (#8057) (job 113851803482) meurt de la meme facon, sur le meme checkout, avec un fetch --filter=blob:none. Ce sont des blobs absents du cache du runner ephemere, pas un finding.

Verification locale du checker, invocation identique a la CI (--check --diff-files, diff origin/main...HEAD = 1 fichier) :

INFO: 7 finding(s) resolus depuis le baseline (mettre le baseline a jour).
OK: 0 NEW finding vs baseline (376 connus, 1504 notebook(s) au graphe).
exit=0

Les trois jambes enfants ont ete rejouees (check-nav-chain, Twin parity audit (#8057), Mermaid fill-without-color advisory) — aucun commit, donc la tete est inchangee et le plancher DWELL n'est pas re-arme. La PR gate sera rejouee apres leur retour au vert, jamais pendant qu'un enfant est queued.

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

[github-actions]

Notebook PR Validation: PASS

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

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2024:CoursIA
pr: 20098
head: 10ae395
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 8749cbfef5d8909a9a1b95124550ad9168f8c63594017bc1921e654d3135d92e
diff-files: 1
diff-additions: 40
diff-deletions: 29
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20098
organ-rc: 0
[/ADJOINT PREFLIGHT]