Theorem 1 and Definition 5 — Observational Equivalence Under ReLU Scaling

Proved

DinhSharpness.ScalingSymmetry

by Minghui · Sep 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analysismachine-learningneural-networks

For every network and function-based loss defined below, every parameter $\theta$ , and every $\alpha>0$ ,

f_{T_\alpha\theta}=f_\theta,\qquad L(T_\alpha\theta)=L(\theta),

and $T_\alpha\theta$ is a local minimum of $L$ if and only if $\theta$ is. There is no differentiability or continuity assumption on the loss for this milestone. Formalization note: a source-derived formulation of Theorem 1's homogeneity consequence and Definition 5; the equivalence of local minima makes explicit the interpretation used by Theorem 4.

Source: Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio, Sharp Minima Can Generalize For Deep Nets, ICML 2017, arXiv:1703.04933v2, https://arxiv.org/abs/1703.04933v2; Section 3, PDF p. 4, Theorem 1, Definition 5 and the paragraph following Definition 5; Section 2, PDF p. 2. Displays are unnumbered.

Notation and network conventions

Let $d,h\ge1$ be the input dimension and hidden width. The parameter $\theta=(W,v)$ consists of $W\in\mathbb R^{d\times h}$ and $v\in\mathbb R^h$ , with the Euclidean norm on all $n=dh+h$ entries. The scalar-output network is

f_\theta(x)=\sum_{j=1}^h \max\!\left(\sum_{i=1}^d x_i W_{ij},0\right)v_j, \qquad x\in\mathbb R^d.

There are no biases and no output activation. For any real-valued functional $\ell$ on prediction functions, $L(\theta)=\ell(f_\theta)$ . In particular, losses with additional parameter-dependent penalties are not included unless they also admit this representation. The positive rescaling is

T_\alpha(W,v)=(\alpha W,\alpha^{-1}v),\qquad \alpha>0.

Observational equivalence means equality of predictions on every input.

The local regularity condition means that $L$ is Fréchet differentiable at every point of some neighborhood of $\theta$ , and the map $z\mapsto DL(z)$ is Fréchet differentiable at $\theta$ . Write $H_L(\theta)=D(DL)(\theta)$ , a continuous bilinear form. Its norm is

\|H_L(\theta)\|=\sup_{\|u\|\le1,\,\|w\|\le1} |H_L(\theta)[u,w]|.

Under Euclidean/Riesz identification, this is the spectral operator norm of the Hessian matrix. A local minimum uses the usual Euclidean neighborhood; it need not be isolated or global. No probability model is assumed: the claim is deterministic and compares the same prediction function.

Formalization note: the network and scaling directly encode Section 3, Definition 3 (PDF p. 3), Theorem 1 and Definition 5 (PDF p. 4). The function-based continuous-loss convention is Section 2, PDF p. 2. For the Hessian targets, the local regularity condition makes the source's implicit second differentiability explicit without requiring global smoothness or continuity of second derivatives. The model defines actual Fréchet derivatives, not an arbitrary matrix constrained by desired conclusions. Relevant displayed formulas have no equation numbers.

Preamble

import Definitions.Def_DinhSharpness_Model

Formal statement

namespace DinhSharpness
theorem ScalingSymmetry :
  ∀ (d h : ℕ), 0 < d → 0 < h →
    ∀ (ℓ : (Input d → ℝ) → ℝ) (θ : Parameter d h) (α : ℝ), 0 < α →
      prediction (scale α θ) = prediction θ ∧
      parameterLoss ℓ (scale α θ) = parameterLoss ℓ θ ∧
      (IsLocalMin (parameterLoss ℓ) (scale α θ) ↔ IsLocalMin (parameterLoss ℓ) θ) := by sorry
end DinhSharpness

Source

Laurent Dinh, Razvan Pascanu, Samy Bengio, Yoshua Bengio, Sharp Minima Can Generalize For Deep Nets, ICML 2017, arXiv:1703.04933v2, https://arxiv.org/abs/1703.04933v2; Section 3, PDF p. 4, Theorem 1, Definition 5 and the paragraph following Definition 5; Section 2, PDF p. 2. Displays are unnumbered.

Read-back

What the Lean code literally says, in plain math · gpt-6

For every pair of natural numbers $d,h$ with $d>0$ and $h>0$ , every function $\ell:(\mathbb R^d\to\mathbb R)\to\mathbb R$ , every real array $W=(W_{ij})_{0\le i<d,\,0\le j<h}$ , every vector $v=(v_j)_{0\le j<h}\in\mathbb R^h$ , and every real number $\alpha>0$ , regard $(W,v)$ as a point of the Euclidean parameter space $\mathbb R^{dh+h}$ and define $F_{W,v}:\mathbb R^d\to\mathbb R$ by $F_{W,v}(x)=\sum_{j=0}^{h-1}\max\!\left\{\sum_{i=0}^{d-1}x_iW_{ij},0\right\}v_j$ . Then all three assertions hold: $F_{\alpha W,\alpha^{-1}v}=F_{W,v}$ as functions, meaning equality at every $x\in\mathbb R^d$ ; $\ell(F_{\alpha W,\alpha^{-1}v})=\ell(F_{W,v})$ ; and $(\alpha W,\alpha^{-1}v)$ is a local minimum of the function $(A,b)\mapsto\ell(F_{A,b})$ if and only if $(W,v)$ is a local minimum of that same function. Here a parameter $(A,b)$ is a local minimum precisely when there exists $\varepsilon>0$ such that, for every $(B,c)\in\mathbb R^{dh+h}$ satisfying $\left(\sum_{i=0}^{d-1}\sum_{j=0}^{h-1}(B_{ij}-A_{ij})^2+\sum_{j=0}^{h-1}(c_j-b_j)^2\right)^{1/2}<\varepsilon$ , one has $\ell(F_{A,b})\le\ell(F_{B,c})$ ; the neighborhoods witnessing the two local minima may differ. The local minimum need not be strict. The array and vector may have zero entries or both be identically zero, and $d=1$ , $h=1$ , and $\alpha=1$ are included. The cases $d=0$ , $h=0$ , and $\alpha\le0$ are excluded by the hypotheses, so the displayed inverse is taken only at a nonzero number. No continuity, differentiability, or other restriction is imposed on $\ell$ or on the resulting parameter loss.

Human review

Endorsed by Shuze Chen · Sep 26, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 26, 2026
Confirmed by the mission captain (proposal self-audit).

View graph