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

[jsboige]

Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/notebook-dotnet #14971

Summary

Tranche « forme formalisation » de l'EPIC digestion #13106 (cf pilote CHSH #14858) : nouveau module GradientFlow dans le lake learning_theory_lean (série ML), troisième frère après Perceptron (Novikoff) et PacLearning (Valiant).

Le contenu digéré est notre propre corpus : le notebook 4.2-ConvNet-Profonde-Residuelles.ipynb (série DataScienceWithAgents) mesure au §3 le facteur ≈ 0,4/bloc de contraction du gradient (0,4^20 ≈ 1e-8) et au §6 la réparation par blocs pré-normés. La tranche formalise la moitié raccourci-identité de cette mécanique :

• Pile plain (GradientFlow/Plain.lean) : plainStack fs n = composition des n blocs. Si |f'_k| ≤ c en chaque point → |deriv (plainStack fs n) x| ≤ c ^ n (abs_deriv_plainStack_le, lemme central plainStack_deriv_bound par induction), et pour c < 1 la borne tend vers 0 (plainStack_gradient_vanishes). Ancre numérique du cours : two_fifths_pow_twenty_lt ((2/5)^20 < 1/10^7, par norm_num).
• Pile résiduelle (GradientFlow/Residual.lean) : bloc h ↦ h + f h (He et al. 2015). Pour c ≤ 1 → (1-c)^n ≤ |deriv (residualStack fs n) x| (abs_deriv_residualStack_ge), via l'anti-inégalité triangulaire 1 - |t| ≤ |1+t|. Ancre jumelle : three_fifths_pow_twenty_gt (3/10^5 < (3/5)^20) — à contraction de branche égale c = 0,4, trois ordres de grandeur d'écart à profondeur 20.

La grille de digestion 10 points (énoncé exact, provenance, nouveauté réelle, carte de dépendances, trivial condensé vs nouveau développé, friction, chemin de découverte, limites, raccord corpus, transmission) est déroulée dans l'en-tête de GradientFlow.lean (FR) et GradientFlow_en.lean (EN).

Limites assumées (grille point 8) : modèle jouet 1-D sur ℝ — pas de Jacobiennes, pas de rayon spectral, pas de pré-norme/LayerNorm. La formalisation capture la survie par raccourci identité, pas la réparation par normalisation.

Validation

• lake build GradientFlow : SUCCESS (local, WSL natif, Mathlib v4.32.1 via cache — 8660 jobs, 0 erreur) ; la CI Lean CI (learning_theory_lean) re-vérifie. Le root aggregator FR (GradientFlow.lean, hors globs .submodules comme Perceptron/PacLearning) vérifié séparément : lake env lean GradientFlow.lean exit 0.
• #print axioms sur les 8 théorèmes FR + 2 miroirs EN : tous [propext, Classical.choice, Quot.sound] uniquement — aucun sorryAx, aucun native_decide.
• Sorry : python scripts/lean/count_code_sorry.py --json — learning_theory_lean distinct_code_sorry 0 avant (main) / 0 après (43 fichiers = 37 + 6 nouveaux, tous 0-sorry ; le naive 26 est de la prose seule, dont les mentions « 0-sorry » des en-têtes nouveaux — le comptage code-only est inchangé).
• B.3 (proof-integrity) : non applicable, câblage ne l'expose pas — lean-build.yml (réutilisé par lean-learning-theory.yml) ne porte pas de job proof-integrity/LeanVerifier ; le gate réel de ce lake est sorry-baseline: 0, sorry-filter-mode: real. Substitut local : #print axioms ci-dessus.
• i18n : FR canonique + siblings EN (namespace GradientFlow_en, imports croisés _en, convention i18n(lean): harmoniser les fichiers .lean en francais + traduction anglaise — inventaire, convention, PR pilote #4980) ; check_i18n_siblings.py --all : 3 nouvelles paires OK byte-identical, 0 drift, 0 orphan cluster-wide.
• README du lake : section module + ancre EPIC: Digestion et canonicalisation des mathématiques assistées par IA #13106 + références He (1512.03385) / Veit (1605.06431) + liste i18n + ligne build ; correction au passage d'un drift de statut (le README disait toolchain v4.31.0-rc1, le lake est à v4.32.1 depuis fix(lean,#11256): bump v4.32.0 -> v4.32.1 — tranche 4a (galois_lean, repeated_games_lean, learning_theory_lean) #11334).
• Périmètre : 8 fichiers (6 .lean + lakefile + README), un seul sujet (module GradientFlow).

See #13106

[jsboige]

[Hermes] COMMENTED — GradientFlow #13106, lecture complète du head d78b3e3b (contrainte token : COMMENT only)

Diff intégral lu (675 lignes, 8 fichiers). Vérifications indépendantes :

• Maths : les preuves tiennent. one_sub_le_abs_add (1-|t| ≤ |1+t|) via abs_add_le (1+t) (-t) + linarith est la bonne anti-inégalité triangulaire ; les inductions plainStack_deriv_bound / residualStack_deriv_bound portent la valeur dérivée par HasDerivAt (récurrence syntaxique propre) et les chaînages calc sont corrects. Ancres vérifiées numériquement : (2/5)^20 ≈ 1,1e-8 < 1e-7 ✓ ; 3/10^5 = 3e-5 < (3/5)^20 ≈ 3,66e-5 ✓.
• 0-sorry confirmé : les 9 matches « sorry » du diff sont tous de la prose (en-têtes « 0-sorry », tableau README) — aucun sorry de preuve.
• CI : Lean CI (learning_theory_lean) vert 4m34s, i18n sibling drift vert (3 paires FR/EN byte-identical côté preuves — vérifié au diff visuel), CodeQL/Gitleaks verts, 0 secret.
• README : correction du drift toolchain v4.31.0-rc1 → v4.32.1 est un bonus légitime au passage, cohérent avec #11334.

Seule réserve (mineure, non bloquante) : la docstring FR de Residual.lean cite « He et al. 2015 » dans l'en-tête mais « 2016 » dans la docstring de residualBlock — arXiv:1512.03385 est bien 2015, la seconde mention est une coquille cosmétique.