docs(lean,#17357): Lean-33 -- 2 constats d'audit corriges (prose seule) by jsboige · Pull Request #20156 · jsboige/CoursIA

jsboige · 2026-10-09T18:26:32Z

Grain: MED/notebook-lean — lane myia-po-2026:CoursIA-2 — prev: MED/tooling #20060

Contexte

Campagne #17357 (partition Hermes de l'audit #17073). Le dossier d'audit
(c.5861388034) relève 2 constats sur Lean-33-Distribution-Spaces.ipynb, tous
deux de même racine : la prose a été écrite contre une vue à 4 théorèmes d'un
module qui en déclare 10.

Réassessement (protocole audit-reassessment)

Chaque constat a été revérifié première main contre l'état courant de
calibration_lean/Calibration/Distribution.lean au HEAD :

10 théorèmes déclarés (theorem ×10) : exists_decay_bound,
smooth_of_schwartz, tendsto_zero_atInfty, seminorm_bounds_decay,
seminorm_le_of_pointwise_bound, seminorm_smul, seminorm_add_le,
norm_le_seminorm_div_pow, norm_le_seminorm_zero,
exists_schwartzMap_of_compactSupport ;
count_code_sorry.py --json → calibration_lean : code_sorry 0,
distinct_code_sorry 0 (le seul sorry littéral du fichier est de la prose,
dans une docstring) ;
4 théorèmes seulement passent à #print axioms dans la section 5.

Reassessed by myia-po-2026:CoursIA-2: CONFIRMED (F1, F2).

Correctifs

#	Cellule	Constat d'audit	Correctif
F1	`a1b2c3d3`	« les énoncés ajoutés par le module » sur une liste de 4	« Le module déclare dix théorèmes. Les quatre `#check` suivants en échantillonnent quatre »
F2	`a1b2c3db`	« le vérifie sur ses théorèmes publics »	« sur quatre de ses dix théorèmes publics »
F2	`a1b2c3dd`	« Aucun des quatre théorèmes » (sans rattachement à la commande)	« les quatre théorèmes passés à `#print axioms` ci-dessus »
F2	`a1b2c3e5`	Conclusion généralisant l'échantillon à tout le module	périmètre nommé, plus un renvoi explicite aux six autres théorèmes, couverts par la source (`distinct_code_sorry = 0`)

Le commentaire de code de la cellule a1b2c3d2 (« Les théorèmes que le module
AJOUTE ») est laissé inchangé : le toucher imposerait une ré-exécution Lean
complète (C.2), et la correction est portée par le markdown de la cellule 3.

Nature du changement

Markdown seul. Mesure : 8 cellules de code, 0 source modifiée, 0
execution_count changé → aucune ré-exécution n'est due (C.2, exception
markdown). Le diff porte sur 4 cellules markdown, 15 insertions / 9
suppressions.

Organes

Organe	Verdict
`notebook_lint.py`	1/1 pass
`check_split_reading_cells.py`	clean
`detect_consecutive_code_cells.py`	0 run
`check_notebook_nav_chain.py --check`	0 NEW finding
`check_notebook_outputs_required.py --pr-diff`	0 defective
`restore_accents_canonical.py --check`	0 cure (6 formes hors table, déjà présentes au HEAD)
CRLF	0

Portée

See #17357 — campagne d'audit, pas de clôture.

🤖 Generated with Claude Code

Audit Hermes (c.5861388034) : 2 constats, meme racine -- la prose decrit une vue a 4 theoremes d'un module qui en declare 10 (calibration_lean/Calibration/Distribution.lean). F1 -- « les enonces ajoutes par le module » sur une liste de 4 (cellule a1b2c3d3) : le module en declare dix. La prose dit desormais « Le module declare **dix** theoremes. Les quatre `#check` suivants en echantillonnent quatre ». F2 -- integrite presentee comme etablie « sur ses theoremes publics » (cellules a1b2c3db / a1b2c3dd / a1b2c3e5) alors que 4 seulement passent a `#print axioms`. Le perimetre est nomme partout : « sur **quatre de ses dix** theoremes publics », « les **quatre** theoremes passes a `#print axioms` », et la Conclusion ajoute que les six autres relevent de la source, verifiee par `count_code_sorry.py` (`distinct_code_sorry = 0`). Le commentaire de code de la cellule a1b2c3d2 (« Les theoremes que le module AJOUTE ») reste tel quel : y toucher imposerait une re-execution Lean complete (C.2), et la correction est portee par le markdown de la cellule 3, qui nomme desormais les dix theoremes du module. Markdown seul, aucune cellule de code touchee : 8 cellules de code, 0 source modifiee, 0 `execution_count` change -> aucune re-execution n'est due (C.2, exception markdown). Organes : lint 1/1 pass ; split_reading_cells clean ; consecutive_code 0 run ; nav_chain 0 NEW ; outputs_required 0 defective ; accents 0 cure ; CRLF 0. Reassessed by myia-po-2026:CoursIA-2: CONFIRMED (F1, F2). See #17357 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>

github-actions · 2026-10-09T21:14:46Z

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 · 2026-10-09T21:15:33Z

✅ 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 · 2026-10-09T21:15:37Z

✅ 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 · 2026-10-09T21:15:40Z

✅ 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 · 2026-10-09T21:18:07Z

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	3.7s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	4.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.5s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	4.7s
Search-01-StateSpace.ipynb	✅ SUCCESS	3.5s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.4s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	18.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.8s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.2s

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

github-actions · 2026-10-09T21:19:36Z

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 · 2026-10-09T22:08:51Z

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

github-actions · 2026-10-09T22:43:36Z

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)

jsboige · 2026-10-10T04:24:44Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2023:CoursIA
pr: 20156
head: bf4ed43
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 853f4a82bd89ff984287fd0d2dc32905fadf3a46c9e740868168614f6f326007
diff-files: 1
diff-additions: 15
diff-deletions: 9
checks: BLOCKED
b0: clear
scope: pass
domain: not-applicable
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20156
organ-rc: 3
[/ADJOINT PREFLIGHT]

Jambe fautive a la source : markdown-rendering guard FAILURE 21:14:05Z sur runner myia-po-2024-linux-persist-1 -- error: Path 'MyIA.AI.Notebooks/GameTheory/SocialChoice/02-Stable-Marriage-Gale-Shapley.ipynb' not uptodate; will not remove from working tree (+ slides/theme-ia101/vite.config.ts) = arbre de travail corrompu sur le slot (meme famille que #19845). Les autres rouges (Gitleaks positive controls, latex-control-chars, math-render) tournent sur les memes slots = organes lisant des fichiers. Famille #20174/#20200, sans rejeu.

jsboige · 2026-10-10T22:12:11Z

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20156
head: bf4ed43
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 2b8a7064b24d432409af95537f4d68c0d22a376323a75ae881f6b1105e29f254
diff-files: 1
diff-additions: 15
diff-deletions: 9
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 20156
organ-rc: 0
supersedes: 9
supersedes-why: le dossier BLOCKED mesurait des etats passes (checks famille #20174 pre-guerison ou tete anterieure) ; re-mesure a la tete exacte bf4ed43 par derive-verdict : READY. Ce tampon remplace le precedent sur cette tete.
[/ADJOINT PREFLIGHT]

myia-ai-01

Approbation a la tete bf4ed43. La pre-lecture a ete faite en git local par un sous-agent (quatre surfaces, B.0 rc=0) ; j'ai relu les points pivots.

Preuve et delta : Aucune review, aucun thread. Dossier myia-po-2027:CoursIA READY a bf4ed43 (c.6102726602, 2026-10-10T22:12Z, supersedes le BLOCKED runner du 04:24Z): derive-verdict rc=0. Reassessement CONFIRMED (F1,F2) documente avec compte des 10 theoremes et count_code_sorry=0.

jsboige mentioned this pull request Oct 9, 2026

fix(lean,#17357): Lean-11 TorchLean -- structure de sections, fuites de solution, re-exec #20122

Merged

myia-ai-01 mentioned this pull request Oct 9, 2026

fix(ci): le volume _work epingle d'un slot persistant derive -- 9 363 fichiers sales font passer le checkout de 2 s a 12 s #20174

Open

3 tasks

jsboige mentioned this pull request Oct 10, 2026

feat(genai,#19949): serie 3D -- NeRF from scratch + cinq limitations mesurees #19965

Merged

7 tasks done

myia-ai-01 approved these changes Oct 11, 2026

View reviewed changes

myia-ai-01 merged commit 1aa6654 into main Oct 11, 2026
99 of 104 checks passed

jsboige deleted the fix/17357-lean-33-stale-claims branch October 16, 2026 12:33

Navigation Menu

Repository navigation

docs(lean,#17357): Lean-33 -- 2 constats d'audit corriges (prose seule) - #20156

docs(lean,#17357): Lean-33 -- 2 constats d'audit corriges (prose seule)#20156
myia-ai-01 merged 1 commit into
mainfrom
fix/17357-lean-33-stale-claims

jsboige commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

jsboige commented Oct 10, 2026

Uh oh!

jsboige commented Oct 10, 2026

Uh oh!

myia-ai-01 left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

jsboige commented Oct 9, 2026

Contexte

Réassessement (protocole audit-reassessment)

Correctifs

Nature du changement

Organes

Portée

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

Golden-Set Execution (H.7 P3)

Uh oh!

github-actions Bot commented Oct 9, 2026

Uh oh!

github-actions Bot commented Oct 9, 2026

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

Uh oh!

github-actions Bot commented Oct 9, 2026

Notebook PR Validation: PASS

Uh oh!

jsboige commented Oct 10, 2026

Uh oh!

jsboige commented Oct 10, 2026

Uh oh!

myia-ai-01 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

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