Appendix E.1 — coefficient energy and empirical statistics

Proved

DAREx.CoefficientEnergyIdentity

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

delta-parameter-pruningmachine-learningprobability

Notation. The fixed-cardinality coordinate set is $I=\{1,\ldots,n\}$ , with $n=|I|$ ; $c_j$ are real coefficients, $Q$ their squared energy, and $\bar c,\sigma^2$ their empirical statistics. For $n>0$ and any deterministic real coefficient vector $c\in\mathbb R^n$ , define $Q=\sum_jc_j^2$ , $\bar c=n^{-1}\sum_jc_j$ , and $\sigma^2=n^{-1}\sum_j(c_j-\bar c)^2$ . Then

Q=n(\bar c^2+\sigma^2).

These are statistics over coordinates, not moments over random pruning. Formalization note: direct algebraic identity used in the source; no coefficient sign assumption.

Source: Deng et al., DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025, arXiv:2410.09344v2, https://arxiv.org/pdf/2410.09344v2, Appendix E.1, PDF p. 31, unnumbered identity immediately after the Berend–Kontorovich paragraph; Section 3.2, PDF p. 5, Theorem 3.1 definitions.

Preamble

import Definitions.Def_DAREx_Model

Formal statement

namespace DAREx
theorem CoefficientEnergyIdentity :
  ∀ (n : ℕ) (c : Fin n → ℝ), 0 < n →
    energy c = (n : ℝ) * (empiricalMean c ^ 2 + empiricalVariance c) := by sorry
end DAREx

Source

Deng et al., DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025, arXiv:2410.09344v2, https://arxiv.org/pdf/2410.09344v2, Appendix E.1, PDF p. 31, unnumbered identity immediately after the Berend–Kontorovich paragraph; Section 3.2, PDF p. 5, Theorem 3.1 definitions.

Read-back

What the Lean code literally says, in plain math · inherited model (exact model identifier unavailable)

This open theorem asserts that, for every natural number $n$ and every real coefficient family $c:I_n\to\mathbb R$ , where $I_n=\{0,\ldots,n-1\}$ , if $0<n$ , then $\sum_{j\in I_n}c_j^2=n\bigl(\bar c^{\,2}+s_c^2\bigr)$ , where $\bar c=(\sum_{j\in I_n}c_j)/n$ and $s_c^2=(\sum_{j\in I_n}(c_j-\bar c)^2)/n$ , and $n$ in real arithmetic is the corresponding real number. The empirical variance has denominator $n$ , not $n-1$ . There is no sign, nonzero, normalization, or probabilistic hypothesis on the coefficients. The case $n=0$ is excluded by the positive-size hypothesis; $n=1$ and the identically zero coefficient family are included, with variance $0$ in the singleton case. The supplied proof slot is a placeholder; no completed proof is supplied.

Human review

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

View graph