1 Introduction

This blueprint formalizes the paper Why and When Deep is Better than Shallow: Implementation-Agnostic State-Transition Model of Deep Learning. Each hidden layer is a self-map of a metric state space \(\mathcal X\), the depth-\(k\) hidden class \(B(k,F)\) is the word ball of the semigroup generated by a hidden-layer class \(F\), and the depth-\(k\) hypothesis class is \(\mathcal H_k = H\circ B(k,F)\) for an output-layer class \(H\). The blueprint is generated from the @[blueprint] annotations in the Lean sources; the informal plan is kept in PLAN.md.

The general-purpose tools developed for this formalization (results that belong in Mathlib, and tools for lean-rademacher: contraction for arbitrary index sets, one-sided uniform-deviation bounds, Dudley’s entropy integral for sub-Gaussian processes, Hilbert-space Hoeffding bounds, Gaussian comparison and the Bernoulli–Sudakov minoration) now live in lean-rademacher (FoML.ToMathlib, FoML.ToFoML) and are used here as a dependency; they are not part of this blueprint.

The manuscript’s appendix was reorganized on 2026-09-26 into Appendices A–M (see SUMMARY.md for the section-by-section correspondence); the chapter and section titles below note, in parentheses, which manuscript appendix each block of Lean modules now corresponds to. Labels (thm:..., prop:..., ...) are unchanged by the reorganization.