Repository navigation
feat(lean,#15400): companion exécutable sur les espaces de Schwartz #16108
Description
Activity
[CLAIMED] lane myia-po-2025:CoursIA -- Grain: DEEP/notebook-lean — companion exécutable sur SchwartzMap, module FR/EN et notebook Lean-33 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution_en.lean, MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-33-Distribution-Spaces.ipynb
(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with
[RELEASED]when your PR lands.)[ADMISSION OVERRIDE] Le délai DWELL de 24 h est levé pour ce sous-grain : il ne provient pas d’un audit neuf à dépiler, mais du tirage mécanique de l’umbrella ancienne #4588, suivi d’un census firsthand complet de #15400 et de
origin/main. Le gap est vérifié sous le pin réel Lean 4.32.1 (SchwartzMaprésout dans Mathlib), aucun travail Distribution Spaces n’existe déjà, aucune PR ouverte ne touchecalibration_lean/**ni le slot Lean-33, et les chemins #15665/#16084 sont exclus.Limitation de l’organe observée :
pick_idle_grain.py --admissible 16108 --admit-reason ...retourne encore le refus DWELL parce que la branche--admissiblene consulte pasargs.admit_reason(scripts/pick_idle_grain.py:2148-2165). La justification exigée est donc consignée ici avant toute édition.[CORRECTION PIN] La mention Lean/Mathlib 4.32.1 dans le body et le commentaire d’admission est périmée. La branche fraîche repose sur le contrat actuellement committé du lake : Lean 4.33.0 et Mathlib à la révision exacte portée conjointement par
lean-toolchain,lakefile.leanetlake-manifest.json.L’implémentation et les validations de ce grain utilisent ce pin committé. Aucun fichier de toolchain, de manifeste ou de pin Mathlib n’est modifié, et aucun downgrade n’est introduit.
[DELIVERED] PR #16124 — #16124
Le companion exécutable sur les espaces de Schwartz est livré dans le périmètre exact de trois sources : les modules FR/EN
Calibration.Distributionet le notebookLean-33-Distribution-Spaces.ipynb.Preuves locales post-fix :
- build confiné :
lake build Calibration.Distribution Calibration.Distribution_en— exit 0 en 50,8 s, zéro descendant orphelin ; - notebook réel
lean4-wsl: 8/8 cellules code exécutées, zéro erreur en 25,5 s ; 24 cellules au total et trois exercices C.1 ; - compteur canonique :
code_sorry = 0,distinct_code_sorry = 0, aucun théorème vacueux signalé ; - dix théorèmes publics inspectés : tous dépendent exactement de
[propext, Classical.choice, Quot.sound], sanssorryAxninative_decide.*;Classical.choiceest explicitement attribué aux constructions d'analyse réelle et d'infimum de seminorme héritées de Mathlib ; - parité FR/EN : 5/5 paires, zéro drift/orphan/unbuilt ;
- huit sorties du notebook relues individuellement et cohérentes avec leurs interprétations ; validateurs notebook, santé Lean, C.2, exercices, ordre, ratchets, navigation et hiérarchie markdown propres.
Le travail utilise le pin committé Lean 4.33.0 / Mathlib
db584cd6d46c92f209a44c0f1c829460d327499d, sans modifier aucun fichier de pin. Aucun README, catalogue, Lean-31, chemin #16084 ou #15665 n'est touché. Aucun code Euler/Navier–Stokes externe n'est copié et aucune résolution de ce problème n'est revendiquée.L'issue reste ouverte pour la décision du coordinateur ; cette lane ne la ferme pas.
- build confiné :
- added a commit that references this issue
on Sep 15, 2026 - added a commit that references this issue
on Sep 16, 2026 FERMEE — verification firsthand contre
origin/main@0dcc80c1fb7b748646b500672ef4df1873ba8013.Livree par #16124 (MERGED,
b9045796dd85). Les modules FR et EN sont sur main (calibration_lean/Calibration/Distribution.leanetDistribution_en.lean), le notebookLean-33-Distribution-Spaces.ipynbest execute (8execution_count), et le compte desorryen code est nul — le seul hitgreptombe dans la prose d'un commentaire, ce qui est exactement la difference quecount_code_sorry.pyexiste pour mesurer. Le companion est independant des modules Euler / Navier-Stokes.
Objectif
Transformer la shortlist
ENSEIGNERdu census #15400 en companion pédagogique exécutable sur les espaces de Schwartz, sous le pin Mathlib déjà porté parcalibration_lean.See #15400. See #4588.
Périmètre
Calibration/Distribution.leanet son sibling anglais byte-identique hors commentaires/docstrings ;Lean-33-Distribution-Spaces.ipynb, exécuté avec le kernellean4-wsl;SchwartzMap, notamment décroissance, régularité et semi-normes, à partir de signatures vérifiées sous Lean 4.32.1 ;Hors périmètre
openai/NavierStokesAndEuler;Acceptance
lake build Calibration.Distribution Calibration.Distribution_enréussit sous le pin du lake ;distinct_code_sorryn’augmente pas et aucun axiome interdit n’est introduit ;scripts/notebook_tools/wsl_papermill.pyavec sorties réelles,execution_countnon nuls et zéro erreur ;SchwartzMap, pas une simple fonction lisse sans contrôle de décroissance ;origin/main.