TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Wide fully connected networks converge geometrically to zero empirical training loss

Statement

Assume AC, DC and countable choice. Fix positive integers $d, n, H, m$ , training data $x_{1}, \dots, x_{n} \in R^{d}$ and labels $y_{1}, \dots, y_{n} \in R$ with $∥ x_{i} ∥_{2} = 1$ and $∣ y_{i} ∣ \leq C_{y}$ for a fixed finite constant $C_{y}$ . Let the activation satisfy the Lipschitz and smoothness conditions $∣ σ (0) ∣ \leq C_{σ}$ , $∣ σ (z) - σ (z^{'}) ∣ \leq L ∣ z - z^{'} ∣$ , and $∣ σ^{'} (z) - σ^{'} (z^{'}) ∣ \leq β ∣ z - z^{'} ∣$ for finite constants, and also be analytic and nonpolynomial. Use the fully connected architecture and population matrix $K_{f c}^{(H)}$ defined on this page, initialized with independent standard normal entries in all weight matrices and the output vector, and trained in all layers by full-batch gradient descent on $L (θ) = \frac{1}{2} \sum_{i = 1}^{n} (f (x_{i}, θ) - y_{i})^{2}$ . Write $K^{(H)} = K_{f c}^{(H)}$ and put $λ_{0} = λ_{\min} (K^{(H)})$ and assume $λ_{0} > 0$ . For $0 < δ < 1$ , if the width and fixed step size satisfy

$m = Ω ⁣ (2^{O (H)} \max {\frac{n^{4}}{λ_{0}^{4}}, \frac{n}{δ}, \frac{n^{2} \log (H n / δ)}{λ_{0}^{2}}}), 0 < η = O ⁣ (\frac{λ_{0}}{n^{2} 2^{O (H)}}),$

then with probability at least $1 - δ$ over initialization, every gradient-descent iterate $k \geq 1$ satisfies

$L (θ^{(k)}) \leq {(1 - \frac{η λ_{0}}{2})}^{k} L (θ^{(0)}) .$

The constants hidden in $O$ and $Ω$ may depend on the fixed activation and label bounds but not on $n, H, m, δ$ ; the step-size constant is small enough that $0 < η λ_{0} / 2 < 1$ . In particular, $L (θ^{(k)}) \to 0$ geometrically as $k \to \infty$ .

Statement references

Du et al., Theorem 5.1 and §3.3

Du et al., Appendix B, Lemmas B.1–B.7 and proof of Theorem 5.1

Facts & Assumptions

Given: The data, architecture, activation, Gaussian initialization, positive terminal population eigenvalue $λ_{0}$ , width, confidence and step-size hypotheses of the Statement.

[F1]

The architecture-specific population kernel, including residual means and scaling, is defined locally and is positive semidefinite. Fully connected and residual networks with the Du Gram kernel The recursively defined population Gram matrices are finite, symmetric, and positive semidefinite

[F2]

The simultaneous Gaussian initialization event gives feature, parameter, backward-coordinate, last-layer Gram, and initial-residual bounds at the stated width. Simultaneous initialization estimates for the Du architectures

[F3]

On parameter balls, the last-layer Gram perturbation and output/loss Hessian have explicit width-dependent bounds. Parameter-ball control of the last-layer Gram and loss Hessian

[F4]

Local Gram positivity and loss-Hessian control confine all GD iterates by a first-exit argument and give geometric loss contraction. Local Gram positivity and loss smoothness give confined gradient descent

Proof

1.1F1F2givenalgebra

Put $λ = λ_{0}$ and $q = 1 + \log (16 / δ)$ . Fix an exponential envelope $E = A_{0}^{H}$ for all initialization constants in [F2] and another $F = A_{1}^{H}$ for [F3] with those initialization bounds. These bases depend only on the permitted fixed bounds. The source-width form permits $m \geq W \max {n^{4} / λ^{4}, n / δ, n^{2} \log (16 H n / δ) / λ^{2}}$ , where $W = A_{2}^{H}$ is chosen sufficiently large in terms of the fixed bases of $E, F$ ; in particular take $W \geq C E F^{2}$ . All these choices are fixed before selecting the radius. On the event from [F2], of probability at least $1 - δ$ , $r_{0} = u (0) - y$ satisfies $∥ r_{0} ∥^{2} \leq E n q$ , the initialized last-layer Gram is at least $3 λ I / 4$ , and all other hypotheses of [F3] hold. Also $λ \leq c_{σ} L^{2}$ by the diagonal of [F1].

2.1F1F3step 1.1algebra

The displayed width also implies $m \geq C E F^{2} n^{3} q / λ^{3}$ , after fixing $W$ sufficiently large. For the logarithmic term this follows without an extra logarithmic width factor: writing $A_{*} = n^{4} / λ^{4}$ and $B_{*} = n / δ$ , one has $n^{3} λ^{- 3} \log (1 / δ) = n^{- 1 / 4} A_{*}^{3 / 4} B_{*}^{1 / 4} δ^{1 / 4} \log (1 / δ) \leq (4 / e) \max (A_{*}, B_{*})$ , since $t e^{- t / 4} \leq 4 / e$ for $t \geq 0$ . The constant part of $q$ is absorbed by $A_{*}$ using $λ \leq c_{σ} L^{2}$ and $n \geq 1$ . Choose the fixed radius $D = 4 \sqrt{E n q / λ}$ . These inequalities give $D / \sqrt{m} \leq c / F$ and $F n D / \sqrt{m} \leq λ / 4$ . Hence [F3] supplies $J_{H} (θ) J_{H} (θ)^{T} ⪰ λ I / 2$ on the entire ball of radius $D$ .

3.1F3step 1.1step 2.1algebra

The same width implies $m \geq C \max (n, H, 1 / δ)$ , so $M = \sqrt{1 + \log (16 m n H / δ)} \leq C \sqrt{\log (e m)}$ and $q \leq C \log (e m)$ . The loss-Hessian bound in [F3], $D = 4 \sqrt{E n q / λ}$ , and $λ \leq c_{σ} L^{2}$ yield $∥ \nabla^{2} L ∥ \leq T^{'} n^{2} λ^{- 1} (1 + q M / \sqrt{m})$ , where $T^{'} = A^{' H}$ after enlarging its fixed base. Indeed expand $(\sqrt{E n q} + F \sqrt{n} D) (1 + D)$ in that bound; because $n, q \geq 1$ and $λ$ is bounded above, every term is at most an allowed exponential constant times $n^{3 / 2} q / λ$ , before the exterior factor $\sqrt{n} M / \sqrt{m}$ . The function $\log (e m)^{3 / 2} / \sqrt{m}$ is bounded for $m \geq 1$ , so the Hessian is bounded by $S = T^{''} n^{2} / λ$ on the ball, with $T^{''} = A^{'' H}$ . The allowed sufficiently small step-size constant ensures $η \leq 1 / S$ .

4.1F3F4step 1.1step 2.1step 3.1algebra∎

The radius satisfies $D > 2 \sqrt{2} ∥ r_{0} ∥ / \sqrt{λ}$ . Apply [F4] with the last-hidden-layer Jacobian block and the ball and smoothness bounds from steps 2.1 and 3.1. Every iterate stays in that ball, and $L (θ^{(k)}) \leq (1 - η λ / 2)^{k} L (θ^{(0)})$ for all $k$ . Choosing the step-size constant also ensures $0 < η λ / 2 < 1$ , so geometric convergence to zero follows. The initialization event has probability at least $1 - δ$ , proving the claim. The same application bounds the total parameter path by $2 \sqrt{2} ∥ r_{0} ∥ / \sqrt{λ}$ ; [F3] therefore supplies last-layer Gram stability and the displayed output Taylor-remainder bound on every accepted update segment, for all iterates simultaneously.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Simon S. Du, Jason D. Lee, Haochuan Li, Liwei Wang, and Xiyu Zhai, Gradient Descent Finds Global Minima of Deep Neural Networks, Theorem 5.1 (standard reference, not scraped)
Simon S. Du, Jason D. Lee, Haochuan Li, Liwei Wang, and Xiyu Zhai, Gradient Descent Finds Global Minima of Deep Neural Networks, Appendix B (standard reference, not scraped)