fix(lean,#17357): Lean-21c -- substrat A lu comme violation d'hstrict, tableau et exercice 1 alignes sur les sorties committes

[jsboige]

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

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

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

Re-vérification

• F1 CONFIRMÉ (stale-claim, cellule 3 2d81e8e5) — la sortie committée du code 1.1 (cellule aa18ddec) affiche pour le substrat A stric. decr. = False (coûts 2→3→4→5 croissants vers la cible a). La lecture rationalisait le dépassement len = 3 > cost(d) = 2 par un « conservatisme » de la borne et enchaînait l'arithmétique 2 - 5 = -3 : le théorème n'est pas lâche sur ce run, il est inapplicable — hstrict est violée par construction.
• F2 CONFIRMÉ (stale-claim, cellule 6 5ccf1314) — ligne 3 du tableau : « OUI triviale (s=10) » alors que la sortie committée de la variante 3 (cellule 16b08cd3) affiche -> longueur au cap = 6, CIBLE ATTEINTE ? False (coûts 0→3→…→18, la valeur 10 n'est jamais visitée). Lignes 1 et 2 vérifiées conformes aux sorties.
• F3 CONFIRMÉ (exercise-mismatch, cellule 14 ff81b035) — l'Indice 2 promettait « ratio attendu proche de 1 » (voire 0.5) pour n_hstrict sur 100 trajectoires du substrat A : le coût croît vers la cible par construction ({a:5, b:4, c:3, d:2}), aucune permutation ne peut produire une marche strictement décroissante — la réponse est structurellement n_hstrict = 0/100, les deux attentes étaient inatteignables.

Le fix (markdown seul, exception C.2 — stub 7fd92681 et toutes les cellules code byte-identiques)

• Cellule 3 : le substrat A est désormais lu comme le témoin de violation qu'il est — la colonne stric. decr. = False décide seule quelles lignes relèvent du théorème ; la rationalisation « conservatisme » et l'arithmétique 2 - 5 = -3 supprimées ; l'atteinte de la cible malgré la violation devient une dissociation positive (lien explicite à la variante 2 du code 2.1) ; la subtilité du Lemme 3 (borne sur le nombre de pas, pas sur le coût restant) repositionnée sur le substrat B, où elle est satisfaite (4 ≤ 4).
• Cellule 6 : ligne 3 corrigée sur la sortie réelle — « NON au cap 6 - le cout saute de 9 a 12, la valeur cible s = 10 n'est jamais visitee ».
• Cellule 14 (Indice 2) : attente honnête — n_hstrict = 0 par construction (renvoi au tableau du code 1.1), et la mesure qui discrimine devient l'autre colonne : n_target_atteinte proche de 100 = dissociation positive, un taux qui baisse = runs poussés hors barrière par un saut non monotone. La structure du dict result, l'Indice 1 (RNG) et le stub sont inchangés.

Vérifications

• Split-reading ratchet (check_split_reading_cells.py --base) : clean à la tête 3c9fffd865.
• Dé-accentage (detect_accent_stripping.py --check) : 59 → 58 (aucune nouvelle forme — les deux ajouts initiaux deja/meme reformulés avant commit).
• Cellules code : 9/9 byte-identiques (aucune re-exécution due, exception C.2 markdown).
• Diff : 1 fichier, 7+/7−, trois cellules markdown uniquement.

Suite de la file : ANALYSE-01-Sendov (F1–F6, c.5849709632), ANALYSE-02-Tao (F1, c.5851352755), 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]

Path-collision (organ #13359/#13615)

Cette PR #20104 (fix(lean,#17357): Lean-21c -- substrat A lu comme violation d'hstrict, tableau et exercice 1 alignes sur les sorties committes) 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,#15629): Lean-21c subprocess encoding=utf-8 — A/B identiques (tapis 3/9) #19410 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb, recouvrement de chemins 100% -- fix(lean,#15629): Lean-21c subprocess encoding=utf-8 — A/B identiques (tapis 3/9) #19410 est deja sur main.
• terminal -- Fix(lean,#19413): Lean-21c cell 39cccd7d -- path canonique + filter mimo_lean #19429 partage : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21c-Descente-Budget.ipynb, recouvrement de chemins 100% -- Fix(lean,#19413): Lean-21c cell 39cccd7d -- path canonique + filter mimo_lean #19429 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.

[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	4.5s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.2s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.7s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.6s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	21.6s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.6s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	13.2s

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

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

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]

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: 9
• 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: 20104
head: 3c9fffd
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 534b3e7a4b9af97470bf7e2a94230abcb89edb9754f5642af775eb8dbffd61a3
diff-files: 1
diff-additions: 7
diff-deletions: 7
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20104
organ-rc: 0
[/ADJOINT PREFLIGHT]