Section C5 — Corrected Signed Removal-Error Identity

Proved

FedRemoval.RemovalErrorIdentity

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 trained parameter $w$ , correction $v$ , and retrained parameter $r$ , prove

w-v-r=H_P^{-1}(G_P-G_S)(w-u_S)+(v_P(w)-v)+(u_S-r).

Formalization note: corrected source-derived decomposition. Every sign is fixed by the removal convention $w-v$ , and the retained optimum is the reference point. No optimality of $w,v,r$ 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-C (Section 3), PDF p. 5 and PDF p. 6, Theorem 2; supplementary Section C5, PDF p. 16, unnumbered error-decomposition and inverse-perturbation 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 RemovalErrorIdentity :
∀ (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 r,
      w - v - r =
        inverseHessian P Finset.univ μ
          ((gram P Finset.univ - gram D s) (w - optimum D s μ)) +
        (surrogateOptimum D s P μ w - v) + (optimum D s μ - r) := 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-C (Section 3), PDF p. 5 and PDF p. 6, Theorem 2; supplementary Section C5, PDF p. 16, unnumbered error-decomposition and inverse-perturbation 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$ , let $F_t=\{0,\ldots,t-1\}$ and $E_t=\mathbb R^{F_t}$ with Euclidean structure. Choose arbitrary data $D$ comprising 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 arbitrary data $P$ comprising 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$ satisfying $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)$ , $G_P=q^{-1}\sum_{j\in F_q}B_j^*B_j$ , $H_D=G_D+\mu I_{E_d}$ , and $H_P=G_P+\mu I_{E_d}$ , with Euclidean adjoints. Let $R_D$ and $R_P$ be the respective multiplicative inverses of $H_D$ and $H_P$ , each set to zero if its argument is not invertible, and put $o=R_Db_D$ . For every $w,v,r\in E_d$ , define $u_w=R_P(H_Dw-b_D)$ . The assertion is $w-v-r=R_P\bigl((G_P-G_D)(w-o)\bigr)+(u_w-v)+(o-r)$ . The three vectors $w,v,r$ are unrestricted, including the comparison vector $r$ and the correction vector $v$ ; there are no optimizer, training, or solver assumptions. The subset $s$ is not required to come from client ownership, the feature collections need not be related, and the offsets and targets of $P$ do not enter the identity. The hypotheses force $n,q\ge1$ but allow $d=0$ , $k=0$ , and zero features. For $d=0$ all vectors in the equation are zero; for $k=0$ one has $G_D=G_P=0$ , $b_D=0$ , and $H_D=H_P=\mu I_{E_d}$ .

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