Equation (6) — Removal-Solver Gap and Parameter Error

Proved

FedRemoval.SurrogateGap

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

convex-optimizationfederated-learningmachine-learningunlearning

For nonempty retained and server datasets and $\mu>0$ , for every $w,v$ , prove

\operatorname{gap}(w,v)=\tfrac12\langle v-v_P(w),H_P(v-v_P(w))\rangle,

\frac\mu2\|v-v_P(w)\|^2\le\operatorname{gap}(w,v).

Formalization note: source-derived quadratic identity and coercivity bound for the actual surrogate in equation (6). No convergence rate for SGD is assumed.

Source: Ruinan Jin, Minghui Chen, Qiong Zhang, Xiaoxiao Li, Forgettable Federated Linear Learning with Certified Data Unlearning, IEEE TNNLS (2026), arXiv:2306.02216v3, https://arxiv.org/pdf/2306.02216v3; Section III-B (Section 3), PDF p. 5, equation (6). Supplementary Section C5, PDF p. 16, unnumbered displays.

Notation and hypotheses

The full dataset has $n$ records and the server dataset has $q$ records. Record $i$ has a fixed real linear feature map $A_i:\mathbb R^d\to\mathbb R^k$ , offset $a_i\in\mathbb R^k$ , and target $y_i\in\mathbb R^k$ . For a retained subset $S$ and regularization $\mu$ , define

L_S(w)=\frac1{2|S|}\sum_{i\in S}\|A_iw+a_i-y_i\|^2+ \frac\mu2\|w\|^2,\quad G_S=\frac1{|S|}\sum_{i\in S}A_i^*A_i,\quad H_S=G_S+\mu I,

b_S=\frac1{|S|}\sum_{i\in S}A_i^*(y_i-a_i),\quad u_S=H_S^{-1}b_S,\quad g_S(w)=H_Sw-b_S.

Here $u_D$ uses all full-data indices, and $H_P,G_P$ use all server indices. Only the server feature maps enter its removal surrogate; server targets and offsets are unused. All norms are Euclidean vector or induced operator norms, as appropriate. The inverse is the total ring inverse; theorems must derive its validity from $\mu>0$ , not assume it. Empty empirical averages are defined by Lean's total arithmetic, but the relevant theorems require $S\ne\varnothing$ and, when server data appear, $q>0$ . Zero parameter or output dimension is allowed.

Set

F_w(v)=\tfrac12\langle v,H_Pv\rangle-\langle g_S(w),v\rangle, \quad v_P(w)=H_P^{-1}g_S(w),\quad \operatorname{gap}(w,v)=F_w(v)-F_w(v_P(w)), \quad\kappa=\|H_P^{-1}\|\|G_P-G_S\|.

The probability model used only by the final target is a finite joint law on $\Omega=\{0,\ldots,N-1\}$ : masses $p_\omega\ge0$ sum to one and $\mathbb E[f]=\sum_{\omega\in\Omega}p_\omega f(\omega)$ . It allows arbitrary dependence between outputs. No law exists for $N=0$ . The other targets are deterministic and assume no probability model.

Formalization note: the fixed affine-feature model is source-derived from Jin et al., arXiv:2306.02216v3, Section III-A (Section 3), PDF p. 3, equation (3), and PDF p. 4, equations (4)--(5). Arbitrary real targets and nonempty retained subsets explicitly extend the one-hot/client-removal setting. The finite-law error targets are corrected formulations, not transcriptions or proofs of the printed Theorem 2.

Preamble

import Definitions.Def_FedRemoval_Model

Formal statement

namespace FedRemoval
theorem SurrogateGap :
∀ (n q d k : ℕ) (D : Data n d k) (s : Finset (Fin n)) (P : Data q d k) (μ : ℝ),
    s.Nonempty → 0 < q → 0 < μ →
    ∀ w v,
      solverGap D s P μ w v = (1 / 2 : ℝ) *
        inner ℝ (v - surrogateOptimum D s P μ w)
          (hessian P Finset.univ μ (v - surrogateOptimum D s P μ w)) ∧
      μ / 2 * ‖v - surrogateOptimum D s P μ w‖ ^ 2 ≤ solverGap D s P μ w v := by sorry
end FedRemoval

Source

Ruinan Jin, Minghui Chen, Qiong Zhang, Xiaoxiao Li, Forgettable Federated Linear Learning with Certified Data Unlearning, IEEE TNNLS (2026), arXiv:2306.02216v3, https://arxiv.org/pdf/2306.02216v3; Section III-B (Section 3), PDF p. 5, equation (6). Supplementary Section C5, PDF p. 16, unnumbered displays.

Read-back

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

For all natural numbers $n,q,d,k$ , put $F_t=\{0,\ldots,t-1\}$ and $E_t=\mathbb R^{F_t}$ with Euclidean inner product and norm. Let $D$ consist of arbitrary continuous real-linear features $A_i:E_d\to E_k$ , offsets $a_i\in E_k$ , and targets $y_i\in E_k$ indexed by $F_n$ , and let $P$ consist of arbitrary continuous real-linear features $B_j:E_d\to E_k$ , offsets $\alpha_j\in E_k$ , and targets $\eta_j\in E_k$ indexed by $F_q$ . For every finite $s\subseteq F_n$ and real $\mu$ , assume $s\ne\varnothing$ , $q>0$ , and $\mu>0$ . Define $G_D=|s|^{-1}\sum_{i\in s}A_i^*A_i$ , $b_D=|s|^{-1}\sum_{i\in s}A_i^*(y_i-a_i)$ , $H_D=G_D+\mu I_{E_d}$ , and $H_P=q^{-1}\sum_{j\in F_q}B_j^*B_j+\mu I_{E_d}$ , where stars denote Euclidean adjoints. Let $R_P$ be the multiplicative inverse of $H_P$ when invertible and zero otherwise. For every $w,v\in E_d$ , define $g_w=H_Dw-b_D$ , $u_w=R_Pg_w$ , and $Q_w(x)=\tfrac12\langle x,H_Px\rangle-\langle g_w,x\rangle$ for all $x\in E_d$ . The assertion is the conjunction $Q_w(v)-Q_w(u_w)=\tfrac12\langle v-u_w,H_P(v-u_w)\rangle$ and $(\mu/2)\|v-u_w\|^2\le Q_w(v)-Q_w(u_w)$ . The named solver gap is exactly this difference of quadratic values, with no assumed solver procedure or accuracy for $v$ . The offsets and targets of $P$ are arbitrary and unused, and its features need not be related to those of $D$ . Nonempty $s$ and positive $q$ exclude $n=0$ and $q=0$ from nonvacuous instances; $d=0$ , $k=0$ , and zero features remain permitted. At $d=0$ the scalar quantities are zero; at $k=0$ the formulas apply with $H_D=H_P=\mu I_{E_d}$ and $b_D=0$ .

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