fix(notebook,#17357): Lean-03b -- attente d axiomes alignee sur la sortie committee (F1)

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2026:CoursIA-2 — prev: LIGHT/docs #19974

Lean-03b — le constat stale-claim de l'audit #17357 (c.5857761593), reverifie sur main avant fix. L'attente d'axiomes annoncee etait contredite par la sortie committee sous les yeux de l'apprenant. Prose seule : aucune cellule de code touchee.

F1 — l'attente d'axiomes est contredite par la sortie

Cellules 76c9a712 (prose d'annonce) et 71b83b9f (sortie de l'audit). La prose promettait « l'axiome minimal : aucun sorry, aucune declaration non constructive importee en contrebande ». La sortie committée, cinq lignes plus bas, dit autre chose :

theoreme	axiomes imprimes
peirce_valid	propext, Classical.choice, Quot.sound
or_not_valid	propext, Quot.sound
or_satisfiable	propext, Quot.sound
valuations_exhaustive	propext, Classical.choice, Quot.sound
peirce_provable	aucun

Classical.choice est exactement l'axiome non constructif que la prose venait d'ecarter, et aucune cellule ulterieure (3cda04dd, conclusion 8f006f74) ne reconciliait l'ecart : l'apprenant qui vient de lire Lean-03 §9 (open Classical) tenait une contradiction sans explication.

Cause racine, verifiee dans formal_logic_lean/FormalLogic/Bridge.lean : Valuation est Prop-valuee (α → Prop, l.47) ; valuations_exhaustive decide v 0 : Prop par by_cases (l.64) — ce qui passe par Classical.propDecidable → Classical.choice — et peirce_valid l'herite par rcases valuations_exhaustive v (l.97). Le pont ne pouvait pas satisfaire l'attente annoncee : le defaut est dans la prose, jamais dans la preuve. C'est ce qui commande la forme du fix.

Fix — reecrire l'attente, puis la lire

• 76c9a712 : l'attendu reel — aucun sorry, et les axiomes du pont la ou la semantique Prop-valuee les exige (Classical.choice en plus de propext et Quot.sound) ; le seul theoreme purement syntaxique du lot, peirce_provable, n'en utilise aucun.
• 3cda04dd (Interpretation) : ajout de la puce qui lit la liste effectivement imprimee — absente jusqu'ici, et c'est precisement ce que le constat reprochait. Elle nomme les deux regimes, dans l'ordre des cinq lignes ci-dessus : peirce_provable sans axiome ; or_not_valid / or_satisfiable sous les seuls axiomes du noyau ; peirce_valid / valuations_exhaustive sous Classical.choice, avec le by_cases sur v 0 : Prop comme origine. La validite semantique se paie d'un axiome non constructif ; elle ne se paie pas d'un sorry.

Reassessment (audit-reassessment, 4 etapes)

Reassessed by myia-po-2026:CoursIA-2: CONFIRMED stale-claim -- 1 constat, 0 faux positif.

Constat	Verdict	Preuve
F1	CONFIRMED	les 5 lignes de #print axioms relues cellule par cellule : peirce_valid et valuations_exhaustive portent bien Classical.choice ; cause racine reproduite dans Bridge.lean (by_cases sur v 0 : Prop, rcases du theoreme appelant)

Aucun faux positif : le constat se reproduit tel quel sur main.

Perimetre et validation

• 1 fichier : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-03b-Formalized-Formal-Logic-Lean-Python.ipynb — 10 insertions / 5 suppressions, 2 cellules markdown (76c9a712, 3cda04dd).
• Markdown seul : les 9 cellules de code gardent source, execution_count (1..9) et sorties identiques a main — verification machine, pas de re-execution due (C.2/C.3).
• Organes : check_split_reading_cells clean · notebook_lint 1/1 · ratchet check_output_failure_text 1 carnet change, 0 regressed · check_lane_claim --paths <carnet> CLEAR (0 collision de PR ouverte) · les 10 hooks pre-commit verts.
• Re-executer n'aurait rien prouve de plus : aucune cellule de code ne bouge, et le carnet porte un kernel python3 dont les sorties sont les traces du dernier passage reel.

See #17357

🤖 Generated with Claude Code

[github-actions]

Path-collision (organ #13359) — résolue

La collision de chemins signalée sur #20116 n'existe plus au passage du 2026-10-10T02:53Z : aucune autre PR ouverte ne partage désormais de chemin de fichier avec elle. Note laissée en place de l'avertissement (retraction non destructive).

[github-actions]

✅ No prose/output mismatch detected in the notebooks this PR changed.

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]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2026:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-09) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=2 genre=6 cap=4)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=2 genre=6 cap=4)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste 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	3.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	5.2s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.8s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.2s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.6s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	29.7s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	7.4s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	23.5s

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

[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-2023:CoursIA
pr: 20116
head: 00ebc26
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: c2b5f7e61b62877d838590a6bf11f00aa90d0569143f9878be0589afd6ef4497
diff-files: 1
diff-additions: 10
diff-deletions: 5
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 20116
organ-rc: 0
[/ADJOINT PREFLIGHT]

Etat a la tete exacte 00ebc262 :

• Reviews : aucune review posee (reviews-reviewed: 0) — la lecture B.0 finale reste integrale au coordinateur ; ce dossier atteste les surfaces, pas une approbation. PR jumelle de fix(notebook,#17357): Lean-03 -- plan reancre sur les 10 sections reelles, renvois cellule/absurdity corriges (F1-F4) #20112 (meme issue [Audit #17073] Série Lean — partition Hermes #17357, F1 specifique : attente d'axiomes alignee sur la sortie commitee).
• B.0 : check_unaddressed_nits.py 20116 rc=0 — aucun nit non leve.
• Checks : 95/95 latest-wins vert, aucun rouge a la tete courante. Dernier commentaire = attestation bot Notebook PR Validation PASS. mergeStateStatus: UNKNOWN = recompute transitoire.
• Scope : 1 fichier, +10/−5 — correction ciblee, conforme au titre.