feat(lean,#13106): module GradientFlow — évanouissement c^n vs survie (1-c)^n (digestion, forme formalisation)

MyIA.AI.Notebooks/ML/learning_theory_lean/GradientFlow.lean

@@ -0,0 +1,79 @@
+import Mathlib
+import GradientFlow.Plain
+import GradientFlow.Residual
+
+/-!
+# GradientFlow — digestion formelle : pourquoi le gradient survit aux blocs résiduels
+
+Tranche de l'EPIC digestion **#13106** (forme *formalisation*, comme le pilote
+CHSH #14858 de po-2025 et la grille PFR #14566 de ai-01). Le protocole de
+digestion (Tao, ICM 2026 — opération *digérer*) exige, par grain enfant, une
+grille à 10 points ; elle est déroulée ici.
+
+1. **Énoncé exact.** Pour une pile « plain » de `n` blocs dérivables dont
+   chacun contracte la dérivée (`|f'_k| ≤ c`), la dérivée de la composition
+   vérifie `|(f_{n-1} ∘ … ∘ f_0)'| ≤ c ^ n` (`abs_deriv_plainStack_le`), et
+   pour `c < 1` la borne tend vers `0` (`plainStack_gradient_vanishes`).
+   Pour une pile de blocs résiduels `h ↦ h + f h` avec `c ≤ 1`,
+   `(1 - c) ^ n ≤ |(g_{n-1} ∘ … ∘ g_0)'|`
+   (`abs_deriv_residualStack_ge`) : le gradient survit géométriquement.
+2. **Provenance.** Le raccourci identité : He, Zhang, Ren & Sun, *Deep
+   Residual Learning for Image Recognition*, arXiv:1512.03385 (2015) ; la
+   lecture ensembliste : Veit, Wilber & Belongie, *Residual Networks Behave
+   Like Ensembles of Relatively Shallow Networks*, arXiv:1605.06431 (2016).
+   Le contenu digéré est **notre propre notebook**
+   `DataScienceWithAgents/04-Vision/4.2-ConvNet-Profonde-Residuelles.ipynb`
+   (§3 : mesure du facteur ≈ 0,4/bloc ; §6 : plain 43,1 % vs prenorm 58,4 %
+   d'accuracy pairwise sur 3 graines).
+3. **Nouveauté réelle.** Premier module du lake (et du dépôt, grep vain) à
+   formaliser la mécanique du gradient profond : la paire
+   majoration/minoration ci-dessus n'existait sous aucune forme ; les frères
+   `Perceptron` (Novikoff) et `PacLearning` (Valiant) couvrent la convergence
+   algorithmique et la généralisation, pas l'optimisation.
+4. **Carte de dépendances.** Mathlib uniquement (`HasDerivAt.comp`,
+   `HasDerivAt.add`, `abs_mul`, `abs_sub_abs_le_abs_add`,
+   `Real.tendsto_pow_atTop_nhds_0_nat`, `norm_num`) ; aucune dépendance aux
+   modules frères du lake — le module s'ajoute sans coupler.
+5. **Trivial condensé vs nouveau développé.** Les briques sont des
+   condensés honnêtes (règle de chaîne + induction + monotonie du produit) ;
+   ce qui est **neuf** est la paire d'énoncés et le couplage aux ancres
+   numériques du cours (`0,4 ^ 20 < 1e-7` côté plain, `3e-5 < 0,6 ^ 20` côté
+   résiduel).
+6. **Friction naturelle.** Naviguer l'API `Deriv`/`HasDerivAt` (l'ordre des
+   arguments de `.comp`, la forme exacte des lemmes d'absolue) ; maintenir
+   0-sorry sur des récurrences syntaxiques (la valeur dérivée portée par
+   `HasDerivAt` plutôt que ré-exprimée via `deriv`).
+7. **Chemin de découverte.** Le notebook 4.2-ConvNet mesure d'abord (pente
+   droite en semilog : facteur ~0,4/bloc, `0,4 ^ 20 ≈ 1e-8`), le lake démontre
+   ensuite : la mesure précède la preuve, exactement l'ordre que le protocole
+   de digestion veut institutionaliser.
+8. **Limites.** Modèle jouet 1-D sur `ℝ` : pas de Jacobiennes, pas de valeurs
+   propres, pas de pré-norme/LayerNorm. La formalisation capture la survie
+   par raccourci identité, **pas** la réparation par normalisation (le
+   notebook distingue les deux ; le lake ne couvre que la première).
+9. **Raccord corpus.** Notebook `4.2-ConvNet-Profonde-Residuelles` (§3, §6) ;
+   lake `learning_theory_lean` (frères `Perceptron`, `PacLearning`) ; README
+   du lake mis à jour (section module + références).
+10. **Transmission.** Docstrings FR (canoniques) + siblings EN
+    (`GradientFlow_en`, convention #4980) ; grille résumée dans le README ;
+    ancres numériques vérifiées par `norm_num`.
+
+## Statut
+
+Tranche 1 **livrée** : `Plain.lean` (majoration `c ^ n` + évanouissement +
+ancre `0,4 ^ 20`), `Residual.lean` (minoration `(1-c) ^ n` + ancre `0,6 ^ 20`),
+tous deux 0-sorry. Extension naturelle (hors périmètre de cette tranche) :
+le modèle matriciel (jacobiennes, rayon spectral) et la pré-norme.
+-/
+
+namespace GradientFlow
+
+/-- Statut : tranche 1 livrée (digestion #13106) — pile plain majorée par
+`c ^ n` (`abs_deriv_plainStack_le`, évanouissement
+`plainStack_gradient_vanishes`), pile résiduelle minorée par `(1-c) ^ n`
+(`abs_deriv_residualStack_ge`), ancres numériques du notebook 4.2-ConvNet
+(`two_fifths_pow_twenty_lt`, `three_fifths_pow_twenty_gt`). Extensions ouvertes
+hors périmètre : modèle matriciel (jacobiennes/spectral), pré-norme. -/
+abbrev Status : Prop := True
+
+end GradientFlow

MyIA.AI.Notebooks/ML/learning_theory_lean/GradientFlow/Plain.lean

@@ -0,0 +1,85 @@
+import Mathlib
+
+/-!
+# GradientFlow.Plain — évanouissement du gradient dans une pile « plain »
+
+Sous-module de `GradientFlow` (digestion #13106, forme formalisation — cf pilote
+CHSH #14858) : une pile de `n` blocs **sans raccourci** (« plain », l'empilement
+d'études du notebook `4.2-ConvNet-Profonde-Residuelles`) est la composition
+`f_{n-1} ∘ … ∘ f_0`. Si chaque bloc contracte la dérivée (`|f'_k| ≤ c`), la
+règle de chaîne et une induction sur la profondeur donnent
+
+    |(f_{n-1} ∘ … ∘ f_0)'| ≤ c ^ n,
+
+et pour une contraction stricte `c < 1`, la borne `c ^ n` tend vers `0` : **le
+gradient meurt exponentiellement vite avec la profondeur**. C'est exactement le
+phénomène mesuré dans le notebook (§3) : facteur ≈ 0,4 par bloc, donc
+`0,4 ^ 20 ≈ 1e-8` au bout de 20 blocs — un gradient cent million de fois plus
+petit qu'en entrée. L'ancre numérique `two_fifths_pow_twenty_lt` verrouille cette
+valeur du cours (`0,4 ^ 20 < 1e-7`).
+
+Toutes les preuves sont **0-sorry** et élémentaires (règle de chaîne via
+`HasDerivAt.comp`, puis monotonie du produit) : le contenu du module est le
+théorème, pas les tactiques.
+-/
+
+namespace GradientFlow
+
+variable (fs : ℕ → ℝ → ℝ) (c : ℝ)
+
+/-- Pile « plain » de profondeur `n` : composition des blocs `0, …, n-1`, le bloc
+`k` étant la fonction `fs k`. `plainStack fs 0 = id` et
+`plainStack fs (n + 1) = fs n ∘ plainStack fs n`. -/
+def plainStack (fs : ℕ → ℝ → ℝ) : ℕ → ℝ → ℝ
+  | 0 => id
+  | n + 1 => fs n ∘ plainStack fs n
+
+/-- **Lemme central** : par induction sur la profondeur, la pile plain dérive en
+un produit de dérivées de blocs, de valeur absolue bornée par `c ^ n` dès que
+chaque bloc dérive et contracte (`|f'_k| ≤ c`). La valeur dérivée est portée par
+`HasDerivAt` pour que la récurrence reste syntaxique. -/
+theorem plainStack_deriv_bound (hc : 0 ≤ c)
+    (hf : ∀ k x, DifferentiableAt ℝ (fs k) x ∧ |deriv (fs k) x| ≤ c) (x : ℝ) :
+    ∀ n, ∃ d : ℝ, HasDerivAt (plainStack fs n) d x ∧ |d| ≤ c ^ n := by
+  intro n
+  induction n with
+  | zero =>
+    refine ⟨1, ?_, ?_⟩
+    · simpa [plainStack] using hasDerivAt_id x
+    · simp
+  | succ n ih =>
+    obtain ⟨dA, hA, hB⟩ := ih
+    have hfd := (hf n (plainStack fs n x)).1
+    have hcomp := HasDerivAt.comp x hfd.hasDerivAt hA
+    show ∃ d : ℝ, HasDerivAt (fs n ∘ plainStack fs n) d x ∧ |d| ≤ c ^ (n + 1)
+    refine ⟨deriv (fs n) (plainStack fs n x) * dA, hcomp, ?_⟩
+    have hFs : |deriv (fs n) (plainStack fs n x)| ≤ c := (hf n _).2
+    rw [abs_mul, pow_succ, ← mul_comm c (c ^ n)]
+    exact (mul_le_mul_of_nonneg_right hFs (abs_nonneg _)).trans
+      (mul_le_mul_of_nonneg_left hB hc)
+
+/-- **Évanouissement du gradient (pile plain)** : si chaque bloc contracte la
+dérivée (`|f'_k| ≤ c`), la dérivée de la pile de `n` blocs est majorée par
+`c ^ n`. Pour `c < 1`, `plainStack_gradient_vanishes` en tire la mort
+exponentielle. -/
+theorem abs_deriv_plainStack_le (hc : 0 ≤ c)
+    (hf : ∀ k x, DifferentiableAt ℝ (fs k) x ∧ |deriv (fs k) x| ≤ c) (x : ℝ) (n : ℕ) :
+    |deriv (plainStack fs n) x| ≤ c ^ n := by
+  obtain ⟨d, hA, hB⟩ := plainStack_deriv_bound fs c hc hf x n
+  rw [hA.deriv]
+  exact hB
+
+/-- **Évanouissement exponentiel** : pour une contraction stricte `c < 1`, la
+borne `c ^ n` tend vers `0` — la profondeur tue le gradient à vitesse
+géométrique, ce que le notebook 4.2-ConvNet mesure à `c ≈ 0,4` (pente droite en
+échelle semilog). -/
+theorem plainStack_gradient_vanishes (hc : 0 ≤ c) (h1 : c < 1) :
+    Filter.Tendsto (fun n => c ^ n) Filter.atTop (nhds 0) :=
+  tendsto_pow_atTop_nhds_zero_of_abs_lt_one (by rwa [abs_of_nonneg hc])
+
+/-- **Ancre numérique du cours** (notebook `4.2-ConvNet-Profonde-Residuelles`,
+§3) : à facteur `0,4` par bloc, 20 blocs laissent passer moins d'un
+dix-millionième du gradient — `0,4 ^ 20 ≈ 1,1e-8 < 1e-7`. -/
+theorem two_fifths_pow_twenty_lt : (2 / 5 : ℝ) ^ 20 < 1 / 10 ^ 7 := by norm_num
+
+end GradientFlow

MyIA.AI.Notebooks/ML/learning_theory_lean/GradientFlow/Plain_en.lean

@@ -0,0 +1,89 @@
+import Mathlib
+
+/-!
+# GradientFlow.Plain — gradient vanishing in a "plain" stack
+
+English mirror of `GradientFlow/Plain.lean` (FR-first canonical), EPIC #4980
+(i18n Lean). Convention ratified 2026-07-04 (issue #4980): namespace
+`GradientFlow_en` (anti-collision with the FR `GradientFlow` namespace);
+non-docstring proof code unchanged.
+
+Submodule of `GradientFlow` (digestion #13106, formalization form — cf CHSH
+pilot #14858): a stack of `n` blocks **without shortcut** (the plain
+architecture of the notebook `4.2-ConvNet-Profonde-Residuelles`) is the
+composition `f_{n-1} ∘ … ∘ f_0`. If every block contracts the derivative
+(`|f'_k| ≤ c`), the chain rule and an induction on depth give
+
+    |(f_{n-1} ∘ … ∘ f_0)'| ≤ c ^ n,
+
+and for a strict contraction `c < 1` the bound `c ^ n` tends to `0`: **the
+gradient dies exponentially fast with depth**. This is exactly the phenomenon
+measured in the notebook (§3): factor ≈ 0.4 per block, hence
+`0.4 ^ 20 ≈ 1e-8` after 20 blocks. The numeric anchor
+`two_fifths_pow_twenty_lt` locks this course value (`0.4 ^ 20 < 1e-7`).
+
+All proofs are **0-sorry** and elementary (chain rule via `HasDerivAt.comp`,
+then product monotonicity): the content of the module is the theorem, not the
+tactics.
+-/
+
+namespace GradientFlow_en
+
+variable (fs : ℕ → ℝ → ℝ) (c : ℝ)
+
+/-- "Plain" stack of depth `n`: composition of blocks `0, …, n-1`, block `k`
+being the function `fs k`. `plainStack fs 0 = id` and
+`plainStack fs (n + 1) = fs n ∘ plainStack fs n`. -/
+def plainStack (fs : ℕ → ℝ → ℝ) : ℕ → ℝ → ℝ
+  | 0 => id
+  | n + 1 => fs n ∘ plainStack fs n
+
+/-- **Central lemma**: by induction on depth, the plain stack derives to a
+product of block derivatives, with absolute value bounded by `c ^ n` as soon as
+every block derives and contracts (`|f'_k| ≤ c`). The derivative value is
+carried by `HasDerivAt` so the recursion stays syntactic. -/
+theorem plainStack_deriv_bound (hc : 0 ≤ c)
+    (hf : ∀ k x, DifferentiableAt ℝ (fs k) x ∧ |deriv (fs k) x| ≤ c) (x : ℝ) :
+    ∀ n, ∃ d : ℝ, HasDerivAt (plainStack fs n) d x ∧ |d| ≤ c ^ n := by
+  intro n
+  induction n with
+  | zero =>
+    refine ⟨1, ?_, ?_⟩
+    · simpa [plainStack] using hasDerivAt_id x
+    · simp
+  | succ n ih =>
+    obtain ⟨dA, hA, hB⟩ := ih
+    have hfd := (hf n (plainStack fs n x)).1
+    have hcomp := HasDerivAt.comp x hfd.hasDerivAt hA
+    show ∃ d : ℝ, HasDerivAt (fs n ∘ plainStack fs n) d x ∧ |d| ≤ c ^ (n + 1)
+    refine ⟨deriv (fs n) (plainStack fs n x) * dA, hcomp, ?_⟩
+    have hFs : |deriv (fs n) (plainStack fs n x)| ≤ c := (hf n _).2
+    rw [abs_mul, pow_succ, ← mul_comm c (c ^ n)]
+    exact (mul_le_mul_of_nonneg_right hFs (abs_nonneg _)).trans
+      (mul_le_mul_of_nonneg_left hB hc)
+
+/-- **Gradient vanishing (plain stack)**: if every block contracts the
+derivative (`|f'_k| ≤ c`), the derivative of the `n`-block stack is bounded by
+`c ^ n`. For `c < 1`, `plainStack_gradient_vanishes` draws the exponential
+death. -/
+theorem abs_deriv_plainStack_le (hc : 0 ≤ c)
+    (hf : ∀ k x, DifferentiableAt ℝ (fs k) x ∧ |deriv (fs k) x| ≤ c) (x : ℝ) (n : ℕ) :
+    |deriv (plainStack fs n) x| ≤ c ^ n := by
+  obtain ⟨d, hA, hB⟩ := plainStack_deriv_bound fs c hc hf x n
+  rw [hA.deriv]
+  exact hB
+
+/-- **Exponential vanishing**: for a strict contraction `c < 1`, the bound
+`c ^ n` tends to `0` — depth kills the gradient geometrically, which the
+4.2-ConvNet notebook measures at `c ≈ 0.4` (straight line on a semilog scale). -/
+theorem plainStack_gradient_vanishes (hc : 0 ≤ c) (h1 : c < 1) :
+    Filter.Tendsto (fun n => c ^ n) Filter.atTop (nhds 0) :=
+  tendsto_pow_atTop_nhds_zero_of_abs_lt_one (by rwa [abs_of_nonneg hc])
+
+/-- **Numeric anchor of the course** (notebook
+`4.2-ConvNet-Profonde-Residuelles`, §3): at a factor of `0.4` per block, 20
+blocks let through less than one ten-millionth of the gradient —
+`0.4 ^ 20 ≈ 1.1e-8 < 1e-7`. -/
+theorem two_fifths_pow_twenty_lt : (2 / 5 : ℝ) ^ 20 < 1 / 10 ^ 7 := by norm_num
+
+end GradientFlow_en

MyIA.AI.Notebooks/ML/learning_theory_lean/GradientFlow/Residual.lean

@@ -0,0 +1,99 @@
+import Mathlib
+
+/-!
+# GradientFlow.Residual — survie du gradient dans une pile résiduelle
+
+Sous-module de `GradientFlow` (digestion #13106, forme formalisation) : chaque
+bloc de la pile est maintenant un **bloc résiduel** `h ↦ h + f h` — le raccourci
+identité de He, Zhang, Ren & Sun (*Deep Residual Learning for Image
+Recognition*, arXiv:1512.03385, 2015). Si chaque branche contracte la dérivée
+(`|f'_k| ≤ c` avec `c ≤ 1`), le terme `+1` du raccourci change la marche : la
+dérivée de chaque bloc est `1 + f'_k`, de module au moins `1 - c > 0`, et
+l'induction sur la profondeur donne
+
+    (1 - c) ^ n ≤ |(g_{n-1} ∘ … ∘ g_0)'|,
+
+le gradient **survit** géométriquement au lieu de mourir. À contraction de
+branche égale `c = 0,4`, l'écart avec la pile plain est de trois ordres de
+grandeur à profondeur 20 : `0,6 ^ 20 ≈ 3,7e-5` contre `0,4 ^ 20 ≈ 1,1e-8` —
+ancres numériques `three_fifths_pow_twenty_gt` et
+`GradientFlow.two_fifths_pow_twenty_lt`.
+
+La borne inférieure repose sur l'anti-inégalité triangulaire tirée de
+`abs_add_le` (`1 - |t| ≤ |1 + t|`). Toutes les preuves sont **0-sorry**.
+-/
+
+namespace GradientFlow
+
+variable (fs : ℕ → ℝ → ℝ) (c : ℝ)
+
+/-- Bloc résiduel (raccourci identité, He et al. 2016) : `h ↦ h + f h`. La
+dérivée en un point est `1 + f'`, de module au moins `1 - |f'|`. -/
+def residualBlock (f : ℝ → ℝ) : ℝ → ℝ := fun h => h + f h
+
+/-- **Anti-inégalité triangulaire (forme du bloc résiduel)** : le terme `+1` du
+raccourci garantit `1 - |t| ≤ |1 + t|` — la dérivée d'un bloc résiduel ne peut
+pas descendre sous `1 - c` quand la branche contracte à `|f'| ≤ c`. -/
+theorem one_sub_le_abs_add (t : ℝ) : 1 - |t| ≤ |1 + t| := by
+  have h : (1 : ℝ) ≤ |1 + t| + |t| := by
+    simpa using abs_add_le (1 + t) (-t)
+  linarith
+
+/-- Pile résiduelle de profondeur `n` : composition des blocs résiduels
+construits sur `fs 0, …, fs (n-1)`. `residualStack fs 0 = id` et
+`residualStack fs (n + 1) = residualBlock (fs n) ∘ residualStack fs n`. -/
+def residualStack (fs : ℕ → ℝ → ℝ) : ℕ → ℝ → ℝ
+  | 0 => id
+  | n + 1 => residualBlock (fs n) ∘ residualStack fs n
+
+/-- **Lemme central** : par induction sur la profondeur, la pile résiduelle
+dérive en un produit dont le module est **minoré** par `(1 - c) ^ n` dès que
+chaque branche dérive et contracte (`|f'_k| ≤ c`, `c ≤ 1`). -/
+theorem residualStack_deriv_bound (hc1 : c ≤ 1)
+    (hf : ∀ k x, DifferentiableAt ℝ (fs k) x ∧ |deriv (fs k) x| ≤ c) (x : ℝ) :
+    ∀ n, ∃ d : ℝ, HasDerivAt (residualStack fs n) d x ∧ (1 - c) ^ n ≤ |d| := by
+  intro n
+  induction n with
+  | zero =>
+    refine ⟨1, ?_, ?_⟩
+    · simpa [residualStack] using hasDerivAt_id x
+    · simp
+  | succ n ih =>
+    obtain ⟨dA, hA, hB⟩ := ih
+    have hfd := (hf n (residualStack fs n x)).1
+    have hBlock : HasDerivAt (residualBlock (fs n))
+        (1 + deriv (fs n) (residualStack fs n x)) (residualStack fs n x) :=
+      (hasDerivAt_id _).add hfd.hasDerivAt
+    have hcomp := HasDerivAt.comp x hBlock hA
+    show ∃ d : ℝ, HasDerivAt (residualBlock (fs n) ∘ residualStack fs n) d x ∧
+      (1 - c) ^ (n + 1) ≤ |d|
+    refine ⟨(1 + deriv (fs n) (residualStack fs n x)) * dA, hcomp, ?_⟩
+    have hFs : |deriv (fs n) (residualStack fs n x)| ≤ c := (hf n _).2
+    have hLow : 1 - c ≤ |1 + deriv (fs n) (residualStack fs n x)| :=
+      (sub_le_sub_left hFs 1).trans (one_sub_le_abs_add _)
+    have hc0 : 0 ≤ 1 - c := sub_nonneg.mpr hc1
+    rw [abs_mul, pow_succ, ← mul_comm (1 - c) ((1 - c) ^ n)]
+    calc (1 - c) * (1 - c) ^ n
+        ≤ |1 + deriv (fs n) (residualStack fs n x)| * (1 - c) ^ n :=
+          mul_le_mul_of_nonneg_right hLow (pow_nonneg hc0 n)
+      _ ≤ |1 + deriv (fs n) (residualStack fs n x)| * |dA| :=
+          mul_le_mul_of_nonneg_left hB (abs_nonneg _)
+
+/-- **Survie du gradient (pile résiduelle)** : si chaque branche contracte la
+dérivée (`|f'_k| ≤ c`, `c ≤ 1`), la dérivée de la pile de `n` blocs est
+**minorée** par `(1 - c) ^ n` — le raccourci identité empêche l'évanouissement
+exponentiel de la pile plain (`abs_deriv_plainStack_le`). -/
+theorem abs_deriv_residualStack_ge (hc1 : c ≤ 1)
+    (hf : ∀ k x, DifferentiableAt ℝ (fs k) x ∧ |deriv (fs k) x| ≤ c) (x : ℝ) (n : ℕ) :
+    (1 - c) ^ n ≤ |deriv (residualStack fs n) x| := by
+  obtain ⟨d, hA, hB⟩ := residualStack_deriv_bound fs c hc1 hf x n
+  rw [hA.deriv]
+  exact hB
+
+/-- **Ancre numérique jumelle** (notebook `4.2-ConvNet-Profonde-Residuelles`,
+§6) : à contraction de branche égale `c = 0,4`, la pile résiduelle laisse
+passer au moins `0,6 ^ 20 ≈ 3,7e-5` — trois ordres de grandeur au-dessus de la
+pile plain (`0,4 ^ 20 ≈ 1,1e-8`, voir `GradientFlow.two_fifths_pow_twenty_lt`). -/
+theorem three_fifths_pow_twenty_gt : 3 / 10 ^ 5 < (3 / 5 : ℝ) ^ 20 := by norm_num
+
+end GradientFlow