diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-33-Distribution-Spaces.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-33-Distribution-Spaces.ipynb
new file mode 100644
index 0000000000..eb98c50782
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-33-Distribution-Spaces.ipynb
@@ -0,0 +1,1736 @@
+{
+ "cells": [
+ {
+ "cell_type": "markdown",
+ "id": "a1b2c3d0",
+ "metadata": {
+ "papermill": {
+ "duration": 0.002414,
+ "end_time": "2026-09-14T07:32:53.401227+00:00",
+ "exception": false,
+ "start_time": "2026-09-14T07:32:53.398813+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "# Lean-33 : espaces de Schwartz — décroissance et régularité\n",
+ "\n",
+ "Compagnon **natif** du lake [`calibration_lean`](calibration_lean/) : le module\n",
+ "`Calibration.Distribution` y est **importé et exécuté** dans un kernel Lean 4 réel\n",
+ "(`lean4-wsl`). Chaque définition et chaque théorème est interrogé par `#check`,\n",
+ "`#print` ou `#print axioms` — les sorties de ce notebook sont des sorties du\n",
+ "compilateur Lean, pas de la prose à propos de Lean.\n",
+ "\n",
+ "Le lake `calibration_lean` porte des *cibles de calibration* pour le harnais de preuve\n",
+ "automatique (Epic #1452) : chaque théorème exerce un chemin différent du prouveur\n",
+ "(décision bornée, lemme ciblé à découvrir, erreur distante à diagnostiquer). Ce notebook\n",
+ "visite le module `Calibration.Distribution`, qui porte la capacité distinctive des\n",
+ "**espaces de Schwartz** : la *décroissance* de toutes les dérivées, mesurée par une\n",
+ "famille de *seminormes*.\n",
+ "\n",
+ "Prérequis : le kernel `lean4-wsl` (voir [Lean-1-Setup](Lean-1-Setup.ipynb) pour\n",
+ "l'installation). L'import du module suppose que le lake a été construit une fois\n",
+ "(`lake build Calibration.Distribution`).\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a1b2c3d1",
+ "metadata": {
+ "papermill": {
+ "duration": 0.001895,
+ "end_time": "2026-09-14T07:32:53.405089+00:00",
+ "exception": false,
+ "start_time": "2026-09-14T07:32:53.403194+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "## 1. Le contrat du module\n",
+ "\n",
+ "Une fonction de Schwartz est une fonction **lisse** dont **toutes les dérivées\n",
+ "décroissent plus vite que n'importe quelle puissance** de `‖x‖`. En Mathlib, cette\n",
+ "double exigence est portée par deux champs d'une seule structure :\n",
+ "\n",
+ "| Champ | Ce qu'il dit |\n",
+ "|---|---|\n",
+ "| `smooth'` | la **régularité** : `ContDiff ℝ ∞ toFun` |\n",
+ "| `decay'` | la **décroissance** : `∀ k n, ∃ C, ∀ x, ‖x‖^k * ‖iteratedFDeriv ℝ n toFun x‖ ≤ C` |\n",
+ "\n",
+ "Le module `Calibration.Distribution` **n'invente aucune définition** : il instancie\n",
+ "l'API `Mathlib.Analysis.Distribution.SchwartzSpace.Basic` réellement pinnée par le lake,\n",
+ "et il en expose les énoncés qui rendent le contrat manipulable.\n",
+ "\n",
+ "La cellule suivante est la **tête de session** : toutes les importations d'un notebook\n",
+ "Lean 4 vivent dans une seule cellule, placée en premier. On y interroge le type de la\n",
+ "structure et les signatures des théorèmes que le module ajoute.\n"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "id": "a1b2c3d2",
+ "metadata": {
+ "execution": {
+ "iopub.execute_input": "2026-09-14T07:32:53.410742Z",
+ "iopub.status.busy": "2026-09-14T07:32:53.410482Z",
+ "iopub.status.idle": "2026-09-14T07:33:07.449888Z",
+ "shell.execute_reply": "2026-09-14T07:33:07.448500Z"
+ },
+ "papermill": {
+ "duration": 14.042887,
+ "end_time": "2026-09-14T07:33:07.450540+00:00",
+ "exception": false,
+ "start_time": "2026-09-14T07:32:53.407653+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "outputs": [
+ {
+ "data": {
+ "text/html": [
+ "\n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ " \n",
+ "
\n",
+ "
-- Tete de session : toutes les importations viennent ici.
\n",
+ "
importCalibration.Distribution
\n",
+ "
\n",
+ "
openscopedSchwartzMapContDiff
\n",
+ "
\n",
+ "
-- La structure de Mathlib telle que le module l'emploie :
-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.
\n",
+ "
example:True:=trivial
\n",
+ "
\n",
+ "
--% env 7
\n",
+ "
\n",
+ " \n",
+ " Raw input\n",
+ " {\"cmd\": \"-- TODO etudiant (exercice 3) : deriver la forme en valeur absolue.\\n-- Decommentez et completez.\\n--\\n-- example (f : \\ud835\\udce2(\\u211d, \\u211d)) (c : \\u211d) :\\n-- SchwartzMap.seminorm \\u211d 0 0 (c \\u2022 f) = |c| * SchwartzMap.seminorm \\u211d 0 0 f := by\\n-- -- TODO etudiant : appliquer `seminorm_smul` puis `Real.norm_eq_abs`\\n\\n-- La cible de l'exercice, telle que Lean la lit :\\n#check (\\u2200 (f : \\ud835\\udce2(\\u211d, \\u211d)) (c : \\u211d),\\n SchwartzMap.seminorm \\u211d 0 0 (c \\u2022 f) = |c| * SchwartzMap.seminorm \\u211d 0 0 f)\\n\\n-- Les deux lemmes que l'indice nomme, avec leurs signatures exactes :\\n#check Calibration.Distribution.seminorm_smul\\n#check Real.norm_eq_abs\\n\\n-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.\\nexample : True := trivial\\n\", \"env\": 6}\n",
+ " \n",
+ " \n",
+ " Raw output\n",
+ " {\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 9, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 9, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"∀ (f : 𝓢(ℝ, ℝ)) (c : ℝ), (SchwartzMap.seminorm ℝ 0 0) (c • f) = |c| * (SchwartzMap.seminorm ℝ 0 0) f : Prop\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 13, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 13, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Calibration.Distribution.seminorm_smul.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3}\\n [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\\n [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (f : 𝓢(E, F)) (k n : ℕ) :\\n (SchwartzMap.seminorm 𝕜 k n) (c • f) = ‖c‖ * (SchwartzMap.seminorm 𝕜 k n) f\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 14, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 14, \"column\": 6},\r\n",
+ " \"data\": \"Real.norm_eq_abs (r : ℝ) : ‖r‖ = |r|\"}],\r\n",
+ " \"env\": 7}\n",
+ " \n",
+ " "
+ ],
+ "text/plain": [
+ "-- TODO etudiant (exercice 3) : deriver la forme en valeur absolue.\n",
+ "-- Decommentez et completez.\n",
+ "--\n",
+ "-- example (f : 𝓢(ℝ, ℝ)) (c : ℝ) :\n",
+ "-- SchwartzMap.seminorm ℝ 0 0 (c • f) = |c| * SchwartzMap.seminorm ℝ 0 0 f := by\n",
+ "-- -- TODO etudiant : appliquer `seminorm_smul` puis `Real.norm_eq_abs`\n",
+ "\n",
+ "-- La cible de l'exercice, telle que Lean la lit :\n",
+ "#check (∀ (f : 𝓢(ℝ, ℝ)) (c : ℝ),\n",
+ "──────▶ ∀ (f : 𝓢(ℝ, ℝ)) (c : ℝ), (SchwartzMap.seminorm ℝ 0 0) (c • f) = |c| * (SchwartzMap.seminorm ℝ 0 0) f : Prop\n",
+ " SchwartzMap.seminorm ℝ 0 0 (c • f) = |c| * SchwartzMap.seminorm ℝ 0 0 f)\n",
+ "\n",
+ "-- Les deux lemmes que l'indice nomme, avec leurs signatures exactes :\n",
+ "#check Calibration.Distribution.seminorm_smul\n",
+ "──────▶ Calibration.Distribution.seminorm_smul.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3}\n",
+ " [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\n",
+ " [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (f : 𝓢(E, F)) (k n : ℕ) :\n",
+ " (SchwartzMap.seminorm 𝕜 k n) (c • f) = ‖c‖ * (SchwartzMap.seminorm 𝕜 k n) f\n",
+ "#check Real.norm_eq_abs\n",
+ "──────▶ Real.norm_eq_abs (r : ℝ) : ‖r‖ = |r|\n",
+ "\n",
+ "-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.\n",
+ "example : True := trivial\n",
+ "\n",
+ "--% env 7\n",
+ "\n",
+ "Raw input:\n",
+ "{\"cmd\": \"-- TODO etudiant (exercice 3) : deriver la forme en valeur absolue.\\n-- Decommentez et completez.\\n--\\n-- example (f : \\ud835\\udce2(\\u211d, \\u211d)) (c : \\u211d) :\\n-- SchwartzMap.seminorm \\u211d 0 0 (c \\u2022 f) = |c| * SchwartzMap.seminorm \\u211d 0 0 f := by\\n-- -- TODO etudiant : appliquer `seminorm_smul` puis `Real.norm_eq_abs`\\n\\n-- La cible de l'exercice, telle que Lean la lit :\\n#check (\\u2200 (f : \\ud835\\udce2(\\u211d, \\u211d)) (c : \\u211d),\\n SchwartzMap.seminorm \\u211d 0 0 (c \\u2022 f) = |c| * SchwartzMap.seminorm \\u211d 0 0 f)\\n\\n-- Les deux lemmes que l'indice nomme, avec leurs signatures exactes :\\n#check Calibration.Distribution.seminorm_smul\\n#check Real.norm_eq_abs\\n\\n-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.\\nexample : True := trivial\\n\", \"env\": 6}\n",
+ "Raw output:\n",
+ "{\"messages\":\r\n",
+ " [{\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 9, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 9, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"∀ (f : 𝓢(ℝ, ℝ)) (c : ℝ), (SchwartzMap.seminorm ℝ 0 0) (c • f) = |c| * (SchwartzMap.seminorm ℝ 0 0) f : Prop\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 13, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 13, \"column\": 6},\r\n",
+ " \"data\":\r\n",
+ " \"Calibration.Distribution.seminorm_smul.{u_1, u_2, u_3} {𝕜 : Type u_1} [NormedField 𝕜] {E : Type u_2} {F : Type u_3}\\n [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F]\\n [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (f : 𝓢(E, F)) (k n : ℕ) :\\n (SchwartzMap.seminorm 𝕜 k n) (c • f) = ‖c‖ * (SchwartzMap.seminorm 𝕜 k n) f\"},\r\n",
+ " {\"severity\": \"info\",\r\n",
+ " \"pos\": {\"line\": 14, \"column\": 0},\r\n",
+ " \"endPos\": {\"line\": 14, \"column\": 6},\r\n",
+ " \"data\": \"Real.norm_eq_abs (r : ℝ) : ‖r‖ = |r|\"}],\r\n",
+ " \"env\": 7}"
+ ]
+ },
+ "metadata": {},
+ "output_type": "display_data"
+ }
+ ],
+ "source": [
+ "-- TODO etudiant (exercice 3) : deriver la forme en valeur absolue.\n",
+ "-- Decommentez et completez.\n",
+ "--\n",
+ "-- example (f : 𝓢(ℝ, ℝ)) (c : ℝ) :\n",
+ "-- SchwartzMap.seminorm ℝ 0 0 (c • f) = |c| * SchwartzMap.seminorm ℝ 0 0 f := by\n",
+ "-- -- TODO etudiant : appliquer `seminorm_smul` puis `Real.norm_eq_abs`\n",
+ "\n",
+ "-- La cible de l'exercice, telle que Lean la lit :\n",
+ "#check (∀ (f : 𝓢(ℝ, ℝ)) (c : ℝ),\n",
+ " SchwartzMap.seminorm ℝ 0 0 (c • f) = |c| * SchwartzMap.seminorm ℝ 0 0 f)\n",
+ "\n",
+ "-- Les deux lemmes que l'indice nomme, avec leurs signatures exactes :\n",
+ "#check Calibration.Distribution.seminorm_smul\n",
+ "#check Real.norm_eq_abs\n",
+ "\n",
+ "-- Cellule neutre : rien a faire ici, elle sert a garder la session verte.\n",
+ "example : True := trivial\n"
+ ]
+ },
+ {
+ "cell_type": "markdown",
+ "id": "a1b2c3e5",
+ "metadata": {
+ "papermill": {
+ "duration": 0.004053,
+ "end_time": "2026-09-14T07:33:09.105860+00:00",
+ "exception": false,
+ "start_time": "2026-09-14T07:33:09.101807+00:00",
+ "status": "completed"
+ },
+ "tags": []
+ },
+ "source": [
+ "## 7. Conclusion\n",
+ "\n",
+ "Ce notebook a parcouru le module `Calibration.Distribution` par ses énoncés, dans un\n",
+ "kernel Lean 4 réel.\n",
+ "\n",
+ "**Ce que le module apporte.** La capacité distinctive des espaces de Schwartz est une\n",
+ "*dualité* : régularité (`smooth'`) et décroissance (`decay'`), mesurées d'un seul geste\n",
+ "par la famille `SchwartzMap.seminorm 𝕜 k n` — `k` pour la décroissance, `n` pour l'ordre\n",
+ "de dérivation. Le module n'invente aucune définition : il rend manipulables les énoncés\n",
+ "que Mathlib fournit (le *majorant* `le_seminorm`, le *plus petit majorant*\n",
+ "`seminorm_le_bound`, l'homogénéité, la sous-additivité), et il en extrait un corollaire\n",
+ "qui est le vrai contenu intuitif de la définition — la **décroissance polynômiale\n",
+ "effective** `‖f x‖ ≤ C_k / ‖x‖^k`.\n",
+ "\n",
+ "**Ce que ce notebook n'est pas.** La section 4 est **numérique et illustrative** : un\n",
+ "échantillonnage sur grille finie ne prouve rien. Le seul juge du champ `decay'` reste une\n",
+ "preuve, et c'est ce que le module fournit.\n",
+ "\n",
+ "**Ce que la calibration vérifie.** Les théorèmes du module sont **clos** — `#print axioms`\n",
+ "de la section 5 ne montre ni `sorryAx` ni `native_decide.*`. Ce qui reste\n",
+ "(`propext`, `Classical.choice`, `Quot.sound`) est le socle fondationnel standard de\n",
+ "l'analyse réelle dans Lean 4.\n",
+ "\n",
+ "### Repères\n",
+ "\n",
+ "- Mathlib 4, `Mathlib.Analysis.Distribution.SchwartzSpace.Basic` (structure `SchwartzMap`,\n",
+ " `seminorm`, `le_seminorm`, `seminorm_le_bound`, `norm_pow_mul_le_seminorm`,\n",
+ " `HasCompactSupport.toSchwartzMap`)\n",
+ "- EPIC #1452 — harnais de preuve multi-agents : cibles de calibration\n",
+ "- EPIC #4980 — convention *sibling pair* FR/EN pour les lakes Lean\n",
+ "- Le module : [`calibration_lean/Calibration/Distribution.lean`](calibration_lean/Calibration/Distribution.lean)\n",
+ " (FR) et son jumeau [`Distribution_en.lean`](calibration_lean/Calibration/Distribution_en.lean) (EN)\n",
+ "- Compagnon du même lake : [Lean-24-Calibration-Native-Companion](Lean-24-Calibration-Native-Companion.ipynb)\n"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "Lean 4 (WSL)",
+ "language": "lean4",
+ "name": "lean4-wsl"
+ },
+ "language_info": {
+ "codemirror_mode": "lean4",
+ "file_extension": ".lean",
+ "mimetype": "text/x-lean4",
+ "name": "lean4"
+ },
+ "papermill": {
+ "default_parameters": {},
+ "duration": 24.495976,
+ "end_time": "2026-09-14T07:33:11.959204+00:00",
+ "environment_variables": {},
+ "exception": null,
+ "input_path": "Lean-33-Distribution-Spaces.ipynb",
+ "output_path": "Lean-33-Distribution-Spaces.ipynb",
+ "parameters": {},
+ "start_time": "2026-09-14T07:32:47.463228+00:00",
+ "version": "2.7.0"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}
\ No newline at end of file
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution.lean
new file mode 100644
index 0000000000..a8dcc96c7f
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution.lean
@@ -0,0 +1,172 @@
+/-
+ Cible de calibration : espaces de Schwartz — décroissance et régularité
+ =======================================================================
+
+ L'espace de Schwartz est l'espace des fonctions lisses dont TOUTES les
+ dérivées décroissent plus vite que n'importe quelle puissance de `‖x‖`. Sa
+ capacité distinctive est double, et c'est cette dualité que ce module
+ enseigne :
+
+ * la RÉGULARITÉ — la lissité `C^∞`, portée par le champ `smooth'` ;
+ * la DÉCROISSANCE — le champ `decay'`, qui majore uniformément
+ `‖x‖^k * ‖iteratedFDeriv ℝ n f x‖` par une constante.
+
+ La famille de seminormes `SchwartzMap.seminorm 𝕜 k n` mesure les deux d'un
+ seul geste : `k` indexe la décroissance, `n` l'ordre de dérivation. C'est la
+ structure qui rend l'espace muni d'une topologie localement convexe, et
+ c'est ce que les théorèmes ci-dessous rendent manipulable.
+
+ Le module instancie l'API Mathlib réellement pinnée par le lake
+ (`Mathlib.Analysis.Distribution.SchwartzSpace.Basic`) — aucune définition
+ n'est réinventée, aucune preuve n'est laissée en `sorry`.
+
+ Chemins du harnais exercés :
+ - Cible S1 (exists_decay_bound) : P3 — le prouveur doit découvrir le lemme
+ nommé `SchwartzMap.decay` ; un `simp` nu ne le trouve pas.
+ - Cible S2 (seminorm_bounds_decay) : P3 — le lemme nommé
+ `SchwartzMap.le_seminorm`, à ne pas confondre avec sa réciproque.
+ - Cible S3 (seminorm_le_of_pointwise_bound) : P1 — le pont inverse
+ `SchwartzMap.seminorm_le_bound`, avec son hypothèse de positivité.
+ - Cible S4 (seminorm_smul) : P3 — l'homogénéité sort du lemme générique
+ `SeminormClass.map_smul_eq_mul`, pas de `simp`.
+ - Cible S5 (seminorm_add_le) : P1 — la sous-additivité via le champ
+ `Seminorm.add_le'`.
+ - Cible S6 (norm_le_seminorm_div_pow) : P2 — la décroissance polynômiale
+ RÉELLE se déduit de la seminorme ; requiert `le_div_iff₀` puis une
+ commutation `mul_comm` (preuve en deux temps, l'erreur est distante).
+ - Cible S7 (exists_schwartzMap_of_compactSupport) : P2 — l'énoncé de
+ clôture `HasCompactSupport.toSchwartzMap`, avec l'égalité de la fonction
+ sous-jacente.
+
+ Difficulté visée : zone de Goldilocks (3-10 itérations du prouveur).
+-/
+import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
+import Mathlib.Tactic
+
+open scoped SchwartzMap ContDiff Topology
+
+namespace Calibration.Distribution
+
+/-! ## 1. Le contrat : décroissance contrôlée par une constante -/
+
+section Decay
+
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+ [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+/-- **Décroissance brute (cible S1).** Pour toute fonction de Schwartz `f` et
+tout couple d'indices `(k, n)`, il existe une constante strictement positive
+`C` qui majore `‖x‖^k * ‖iteratedFDeriv ℝ n f x‖` pour tout `x`.
+
+C'est le champ `decay'` de la structure, raffiné par le lemme `decay` qui
+garantit en plus `0 < C` (utile pour diviser). -/
+theorem exists_decay_bound (f : 𝓢(E, F)) (k n : ℕ) :
+ ∃ C : ℝ, 0 < C ∧ ∀ x : E, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C :=
+ f.decay k n
+
+/-- **Régularité (la première moitié du contrat).** Toute fonction de Schwartz
+est lisse à l'ordre infini : c'est le champ `smooth'`, ici lu comme un énoncé
+public sur la fonction sous-jacente. -/
+theorem smooth_of_schwartz (f : 𝓢(E, F)) : ContDiff ℝ ∞ (f : E → F) :=
+ f.smooth'
+
+/-- **La décroissance entraîne l'annulation à l'infini.** C'est le sens
+concret de « décroît plus vite que toute puissance » : `f` tend vers `0`
+le long du filtre `cocompact`. -/
+theorem tendsto_zero_atInfty [ProperSpace E] (f : 𝓢(E, F)) :
+ Filter.Tendsto (f : E → F) (Filter.cocompact E) (𝓝 0) :=
+ f.tendsto_cocompact
+
+end Decay
+
+/-! ## 2. Les seminormes : mesurer décroissance et régularité d'un seul geste
+
+`SchwartzMap.seminorm 𝕜 k n` est la meilleure constante de l'estimation
+`‖x‖^k * ‖iteratedFDeriv ℝ n f x‖ ≤ C`. Le théorème `le_seminorm` dit qu'elle
+la réalise (c'est un majorant), `seminorm_le_bound` qu'elle en est le plus
+petit (toute constante qui marche la majore) : les deux moitiés de la
+définition par infimum, prises par les deux bouts. -/
+
+section Seminorm
+
+variable {𝕜 : Type*} [NormedField 𝕜]
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+ [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
+
+/-- **La seminorme réalise l'estimation (cible S2).** Pour tout point `x`,
+l'estimation de Schwartz est majorée par la seminorme d'indices `(k, n)`.
+
+C'est la moitié « la seminorme est un majorant ». -/
+theorem seminorm_bounds_decay (f : 𝓢(E, F)) (k n : ℕ) (x : E) :
+ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ SchwartzMap.seminorm 𝕜 k n f :=
+ SchwartzMap.le_seminorm 𝕜 k n f x
+
+/-- **La seminorme est le plus petit majorant (cible S3).** Réciproque du
+théorème précédent : borner l'estimation en TOUT point par une constante `M`
+borne la seminorme par `M`. L'hypothèse `hMp : 0 ≤ M` est indispensable (sans
+elle, une constante strictement négative bornerait tout). -/
+theorem seminorm_le_of_pointwise_bound (f : 𝓢(E, F)) (k n : ℕ) {M : ℝ}
+ (hMp : 0 ≤ M)
+ (hM : ∀ x : E, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ M) :
+ SchwartzMap.seminorm 𝕜 k n f ≤ M :=
+ SchwartzMap.seminorm_le_bound 𝕜 k n f hMp hM
+
+/-- **Homogénéité (cible S4).** Le scalaire sort multiplicativement, en norme,
+de la seminorme. C'est l'axiome `SMul` de `Seminorm`, lu par le lemme
+générique `SeminormClass.map_smul_eq_mul`. -/
+theorem seminorm_smul (c : 𝕜) (f : 𝓢(E, F)) (k n : ℕ) :
+ SchwartzMap.seminorm 𝕜 k n (c • f) = ‖c‖ * SchwartzMap.seminorm 𝕜 k n f :=
+ map_smul_eq_mul (SchwartzMap.seminorm 𝕜 k n) c f
+
+/-- **Sous-additivité (cible S5).** Une seminorme n'est pas additive, elle est
+sous-additive : l'inégalité triangulaire est un axiome de la structure, lu par
+le champ `Seminorm.add_le'`. -/
+theorem seminorm_add_le (f g : 𝓢(E, F)) (k n : ℕ) :
+ SchwartzMap.seminorm 𝕜 k n (f + g) ≤
+ SchwartzMap.seminorm 𝕜 k n f + SchwartzMap.seminorm 𝕜 k n g :=
+ (SchwartzMap.seminorm 𝕜 k n).add_le' f g
+
+/-- **Décroissance polynômiale effective (cible S6).** La seminorme d'indices
+`(k, 0)` — décroissance d'ordre `k`, aucune dérivée — fournit une décroissance
+POLYNÔMIALE de la fonction elle-même : hors de l'origine,
+
+ `‖f x‖ ≤ C_k / ‖x‖^k`.
+
+La preuve déplace `‖x‖^k` au dénominateur (`le_div_iff₀`, l'hypothèse
+`0 < ‖x‖` est ce qui l'autorise), puis commute les deux facteurs pour
+retomber sur `norm_pow_mul_le_seminorm`. -/
+theorem norm_le_seminorm_div_pow (f : 𝓢(E, F)) (k : ℕ) {x : E} (hx : 0 < ‖x‖) :
+ ‖f x‖ ≤ SchwartzMap.seminorm 𝕜 k 0 f / ‖x‖ ^ k := by
+ rw [le_div_iff₀ (pow_pos hx k)]
+ exact (mul_comm _ _).trans_le (SchwartzMap.norm_pow_mul_le_seminorm 𝕜 f k x)
+
+/-- **La seminorme `(0, 0)` majore la norme uniforme.** Cas particulier
+`k = 0` du théorème précédent, sans hypothèse : partout,
+`‖f x‖ ≤ seminorm 𝕜 0 0 f`. C'est la seminorme qui contrôle le sup de `f`. -/
+theorem norm_le_seminorm_zero (f : 𝓢(E, F)) (x : E) :
+ ‖f x‖ ≤ SchwartzMap.seminorm 𝕜 0 0 f :=
+ SchwartzMap.norm_le_seminorm 𝕜 f x
+
+end Seminorm
+
+/-! ## 3. Clôture : le support compact fabrique des fonctions de Schwartz -/
+
+section CompactSupport
+
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+ [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+/-- **Une fonction lisse à support compact est de Schwartz (cible S7).** La
+clôture de la classe est un fait du support compact : hors du support, la
+fonction est nulle, donc la décroissance est gagnée sans hypothèse.
+
+La conclusion témoigne EN PLUS de la préservation de la fonction sous-jacente
+— `toSchwartzMap` ne change pas la fonction, il l'habille du contrat. -/
+theorem exists_schwartzMap_of_compactSupport {f : E → F}
+ (hsupp : HasCompactSupport f) (hsmooth : ContDiff ℝ ∞ f) :
+ ∃ g : 𝓢(E, F), (g : E → F) = f :=
+ ⟨hsupp.toSchwartzMap hsmooth, rfl⟩
+
+end CompactSupport
+
+end Calibration.Distribution
diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution_en.lean
new file mode 100644
index 0000000000..653bc14099
--- /dev/null
+++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean/Calibration/Distribution_en.lean
@@ -0,0 +1,176 @@
+/-
+ Calibration target: Schwartz spaces — decay and regularity
+ ==========================================================
+
+ The Schwartz space is the space of smooth functions all of whose
+ derivatives decay faster than any power of `‖x‖`. Its distinctive
+ capability is twofold, and that duality is what this module teaches:
+
+ * REGULARITY — `C^∞` smoothness, carried by the `smooth'` field;
+ * DECAY — the `decay'` field, which uniformly bounds
+ `‖x‖^k * ‖iteratedFDeriv ℝ n f x‖` by a constant.
+
+ The family of seminorms `SchwartzMap.seminorm 𝕜 k n` measures both at once:
+ `k` indexes decay, `n` the order of differentiation. That structure is what
+ gives the space its locally convex topology, and it is what the theorems
+ below make manipulable.
+
+ The module instantiates the Mathlib API actually pinned by the lake
+ (`Mathlib.Analysis.Distribution.SchwartzSpace.Basic`) — no definition is
+ reinvented, no proof is left as `sorry`.
+
+ Harness paths exercised:
+ - Target S1 (exists_decay_bound): P3 — the prover must discover the named
+ lemma `SchwartzMap.decay`; a bare `simp` will not find it.
+ - Target S2 (seminorm_bounds_decay): P3 — the named lemma
+ `SchwartzMap.le_seminorm`, not to be confused with its converse.
+ - Target S3 (seminorm_le_of_pointwise_bound): P1 — the converse bridge
+ `SchwartzMap.seminorm_le_bound`, with its positivity hypothesis.
+ - Target S4 (seminorm_smul): P3 — homogeneity comes from the generic lemma
+ `SeminormClass.map_smul_eq_mul`, not from `simp`.
+ - Target S5 (seminorm_add_le): P1 — subadditivity via the
+ `Seminorm.add_le'` field.
+ - Target S6 (norm_le_seminorm_div_pow): P2 — the REAL polynomial decay is
+ derived from the seminorm; it requires `le_div_iff₀` and then a
+ `mul_comm` swap (a two-step proof, the error is distant).
+ - Target S7 (exists_schwartzMap_of_compactSupport): P2 — the closure
+ statement `HasCompactSupport.toSchwartzMap`, with the equality of the
+ underlying function.
+
+ Target difficulty: Goldilocks zone (3-10 prover iterations).
+
+ i18n convention #4980 (sibling pair): this file is the EN sibling of
+ `Calibration/Distribution.lean`; the two are never imported together.
+-/
+import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
+import Mathlib.Tactic
+
+open scoped SchwartzMap ContDiff Topology
+
+namespace Calibration.Distribution
+
+/-! ## 1. The contract: decay bounded by a constant -/
+
+section Decay
+
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+ [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+/-- **Raw decay (target S1).** For every Schwartz function `f` and every pair
+of indices `(k, n)` there is a strictly positive constant `C` bounding
+`‖x‖^k * ‖iteratedFDeriv ℝ n f x‖` for all `x`.
+
+This is the `decay'` field of the structure, refined by the `decay` lemma
+which additionally guarantees `0 < C` (needed to divide). -/
+theorem exists_decay_bound (f : 𝓢(E, F)) (k n : ℕ) :
+ ∃ C : ℝ, 0 < C ∧ ∀ x : E, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C :=
+ f.decay k n
+
+/-- **Regularity (the first half of the contract).** Every Schwartz function is
+smooth to infinite order: this is the `smooth'` field, read here as a public
+statement about the underlying function. -/
+theorem smooth_of_schwartz (f : 𝓢(E, F)) : ContDiff ℝ ∞ (f : E → F) :=
+ f.smooth'
+
+/-- **Decay implies vanishing at infinity.** This is the concrete meaning of
+"decays faster than any power": `f` tends to `0` along the `cocompact`
+filter. -/
+theorem tendsto_zero_atInfty [ProperSpace E] (f : 𝓢(E, F)) :
+ Filter.Tendsto (f : E → F) (Filter.cocompact E) (𝓝 0) :=
+ f.tendsto_cocompact
+
+end Decay
+
+/-! ## 2. The seminorms: measuring decay and regularity in one gesture
+
+`SchwartzMap.seminorm 𝕜 k n` is the best constant in the estimate
+`‖x‖^k * ‖iteratedFDeriv ℝ n f x‖ ≤ C`. The theorem `le_seminorm` says it
+realizes that estimate (it is an upper bound); `seminorm_le_bound` says it is
+the least such constant (every working constant bounds it): the two halves of
+the infimum definition, taken from both ends. -/
+
+section Seminorm
+
+variable {𝕜 : Type*} [NormedField 𝕜]
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+ [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace 𝕜 F] [SMulCommClass ℝ 𝕜 F]
+
+/-- **The seminorm realizes the estimate (target S2).** At every point `x`, the
+Schwartz estimate is bounded by the seminorm of indices `(k, n)`.
+
+This is the "the seminorm is an upper bound" half. -/
+theorem seminorm_bounds_decay (f : 𝓢(E, F)) (k n : ℕ) (x : E) :
+ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ SchwartzMap.seminorm 𝕜 k n f :=
+ SchwartzMap.le_seminorm 𝕜 k n f x
+
+/-- **The seminorm is the least upper bound (target S3).** Converse of the
+previous theorem: bounding the estimate at EVERY point by a constant `M`
+bounds the seminorm by `M`. The hypothesis `hMp : 0 ≤ M` is indispensable
+(without it, a strictly negative constant would bound everything). -/
+theorem seminorm_le_of_pointwise_bound (f : 𝓢(E, F)) (k n : ℕ) {M : ℝ}
+ (hMp : 0 ≤ M)
+ (hM : ∀ x : E, ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ M) :
+ SchwartzMap.seminorm 𝕜 k n f ≤ M :=
+ SchwartzMap.seminorm_le_bound 𝕜 k n f hMp hM
+
+/-- **Homogeneity (target S4).** The scalar comes out multiplicatively, as a
+norm, of the seminorm. This is the `SMul` axiom of `Seminorm`, read through
+the generic lemma `SeminormClass.map_smul_eq_mul`. -/
+theorem seminorm_smul (c : 𝕜) (f : 𝓢(E, F)) (k n : ℕ) :
+ SchwartzMap.seminorm 𝕜 k n (c • f) = ‖c‖ * SchwartzMap.seminorm 𝕜 k n f :=
+ map_smul_eq_mul (SchwartzMap.seminorm 𝕜 k n) c f
+
+/-- **Subadditivity (target S5).** A seminorm is not additive, it is
+subadditive: the triangle inequality is an axiom of the structure, read
+through the `Seminorm.add_le'` field. -/
+theorem seminorm_add_le (f g : 𝓢(E, F)) (k n : ℕ) :
+ SchwartzMap.seminorm 𝕜 k n (f + g) ≤
+ SchwartzMap.seminorm 𝕜 k n f + SchwartzMap.seminorm 𝕜 k n g :=
+ (SchwartzMap.seminorm 𝕜 k n).add_le' f g
+
+/-- **Effective polynomial decay (target S6).** The seminorm of indices
+`(k, 0)` — decay of order `k`, no derivative — yields POLYNOMIAL decay of the
+function itself: away from the origin,
+
+ `‖f x‖ ≤ C_k / ‖x‖^k`.
+
+The proof moves `‖x‖^k` to the denominator (`le_div_iff₀`, whose hypothesis
+`0 < ‖x‖` is what authorizes it), then commutes the two factors to land on
+`norm_pow_mul_le_seminorm`. -/
+theorem norm_le_seminorm_div_pow (f : 𝓢(E, F)) (k : ℕ) {x : E} (hx : 0 < ‖x‖) :
+ ‖f x‖ ≤ SchwartzMap.seminorm 𝕜 k 0 f / ‖x‖ ^ k := by
+ rw [le_div_iff₀ (pow_pos hx k)]
+ exact (mul_comm _ _).trans_le (SchwartzMap.norm_pow_mul_le_seminorm 𝕜 f k x)
+
+/-- **The `(0, 0)` seminorm bounds the uniform norm.** The `k = 0` special
+case of the previous theorem, without any hypothesis: everywhere,
+`‖f x‖ ≤ seminorm 𝕜 0 0 f`. That seminorm is the one controlling the sup
+of `f`. -/
+theorem norm_le_seminorm_zero (f : 𝓢(E, F)) (x : E) :
+ ‖f x‖ ≤ SchwartzMap.seminorm 𝕜 0 0 f :=
+ SchwartzMap.norm_le_seminorm 𝕜 f x
+
+end Seminorm
+
+/-! ## 3. Closure: compact support manufactures Schwartz functions -/
+
+section CompactSupport
+
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+ [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+/-- **A smooth compactly supported function is Schwartz (target S7).** The
+closure of the class is a fact about compact support: outside the support the
+function is zero, so decay is obtained without any hypothesis.
+
+The conclusion additionally witnesses preservation of the underlying function
+— `toSchwartzMap` does not change the function, it dresses it in the
+contract. -/
+theorem exists_schwartzMap_of_compactSupport {f : E → F}
+ (hsupp : HasCompactSupport f) (hsmooth : ContDiff ℝ ∞ f) :
+ ∃ g : 𝓢(E, F), (g : E → F) = f :=
+ ⟨hsupp.toSchwartzMap hsmooth, rfl⟩
+
+end CompactSupport
+
+end Calibration.Distribution