feat(lean-notebook,#13106): 4.2b compagnon GradientFlow — c^n vs (1-c)^n exécutés depuis learning_theory_lean

[jsboige]

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

Livrable

Notebook compagnon 4.2b-Lean-GradientFlow-Vanishing (kernel lean4-wsl, 19 cellules : 10 markdown + 9 code) exécutant le lake learning_theory_lean / moitié GradientFlow (#14980) déclaration par déclaration, sur le modèle des companions 2.8b/2.8d :

• #check des signatures : abs_deriv_plainStack_le, abs_deriv_residualStack_ge, plainStack_deriv_bound, residualStack_deriv_bound, one_sub_le_abs_add, ancres two_fifths_pow_twenty_lt / three_fifths_pow_twenty_gt, plainStack_gradient_vanishes ;
• anti-triangulaire au pire cas t = ±2/5 rejouée par example … := by norm_num ;
• balayage en profondeur rejoué en Float (boundTable 0.4 [5, 10, 15, 20] puis exos jusqu'à n = 24) — la version tabulée de la pente semilog du 4.2 §3 ;
• 3 exercices (C.1 : stubs #eval exécutables tels quels, aucune erreur volontaire).

Fix porteur : glob racine du lakefile

globs := #[.submodules GradientFlow, GradientFlow_en] ne couvre que GradientFlow.*, pas le module racine GradientFlow.lean. Conséquence mesurée : lake build rend success sans jamais produire GradientFlow.olean, et import GradientFlow en kernel/repl échoue en environnement vide silencieux (aucun message sur la ligne d'import, unknown namespace sur le open qui suit — diagnostic complet dans la PR). Le glob devient #[.submodules GradientFlow, GradientFlow, GradientFlow_en]`.

• Même défaut latent chez les libs sœurs Perceptron et PacLearning (racines FR jamais bâties) : signalé ici, non touché (hors scope du grain, un sujet par PR).
• Perceptron/PacLearning n'ont pas de notebook qui importe leur racine aujourd'hui (les companions 2.8b/2.8d importent les sous-modules), le piège y est donc latent, pas actif.

Preuves d'exécution (H.1/H.4)

• lake build : lake build GradientFlow dans le miroir WSL → Build completed successfully (8661 jobs) avec le job racine en plus (✔ [8660/8661] Built GradientFlow (30s)), GradientFlow.olean 8648 o produit.
• Kernel : EXEC_OK cells=19 errors=none via nbclient sur kernel lean4-wsl (miroir du lake, feat(ml,#13199): 2.8d companion Lean Novikoff — borne exécutée depuis learning_theory_lean #13202 precedent), 0 marqueur d'erreur dans les outputs (l'inspection manuelle des rendus remplace la détection nbclient — le kernel lean4_jupyter rend les erreurs Lean en display_data, pas en output_type: error).
• Table réelle (#eval boundTable 0.4 [5,10,15,20]) : c^n 0,010240 → 0,000000 contre (1-c)^n 0,077760 → 0,000037 ; à n = 24 le plancher résiduel tient à 5e-06 (outputs commités, C.2).
• Densité pédagogique : 1281 chars/cellule code (pedagogy_density.py, below_threshold: 0).
• C.1 : raise NotImplementedError / assert False / 1/0 → 0 occurrence.

Sorry / axiomes (B.2)

Non applicable aux preuves : le diff ne touche aucun *.lean de preuve — uniquement le lakefile.lean (globs) et le notebook. count_code_sorry.py inchangé par construction.

Scope

See #13106 (tranche compagnon de l'exposition GradientFlow — contribution, l'EPIC reste ouverte). Claim amendé (c.5564599460) pour couvrir le lakefile.

[github-actions]

✅ 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]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 9
• 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)

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.3s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	3.6s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	4.5s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	5.0s
Search-01-StateSpace.ipynb	✅ SUCCESS	7.4s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	4.3s
rl_4_multi_armed_bandits.ipynb	✅ SUCCESS	37.4s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	2.9s

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