Corrected Finite-Run Mean-Square FedRemoval Bound

Proved

FedRemoval.CorrectedMeanSquareRemovalBound

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

convex-optimizationfederated-learningmachine-learningunlearning

Let the retained and server datasets be nonempty and $\mu>0$ . On any finite joint probability law, let $W,V,R$ be arbitrary parameter-valued output maps. The unlearned parameter is $W-V$ . Define $E_{\rm train}=\mathbb E\|W-u_D\|^2$ , $E_{\rm retrain}=\mathbb E\|R-u_S\|^2$ , and $Q=\mathbb E[\operatorname{gap}(W,V)]$ . Prove

\mathbb E\|W-V-R\|^2\le\frac6\mu Q+ 6\kappa^2\bigl(E_{\rm train}+\|u_D-u_S\|^2\bigr)+3E_{\rm retrain}.

This quantifies how the actual finite-run optimization errors and the server/retained Hessian mismatch affect parameter error.

Formalization note: user-authorized corrected, source-derived formulation motivated by Theorem 2 and Section C5. It retains the full-to-retained optimum displacement, the inverse-Hessian scale, and unfinished retraining error. It applies to arbitrary finite-support output laws, with no independence assumption. It does not assert the printed constants/rate, does not define a FedAvg or SGD run, and does not imply statistical indistinguishability or differential privacy. Algorithm-specific bounds on $Q,E_{\rm train},E_{\rm retrain}$ remain separate work.

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 CorrectedMeanSquareRemovalBound :
∀ (n q d k N : ℕ) (D : Data n d k) (s : Finset (Fin n)) (P : Data q d k)
    (μ : ℝ) (p : Law N) (w v r : Fin N → E d),
    s.Nonempty → 0 < q → 0 < μ →
    mean p (fun i ↦ ‖w i - v i - r i‖ ^ 2) ≤
      (6 / μ) * mean p (fun i ↦ solverGap D s P μ (w i) (v i)) +
      6 * mismatch D s P μ ^ 2 *
        (mse p w (optimum D Finset.univ μ) +
          ‖optimum D Finset.univ μ - optimum D s μ‖ ^ 2) +
      3 * mse p r (optimum D s μ) := 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,N$ , write $F_t=\{0,\ldots,t-1\}$ and $E_t=\mathbb R^{F_t}$ with Euclidean inner product and norm. Choose arbitrary data $D$ with continuous real-linear features $A_i:E_d\to E_k$ , offsets $a_i\in E_k$ , and targets $y_i\in E_k$ for $i\in F_n$ , arbitrary data $P$ with continuous real-linear features $B_j:E_d\to E_k$ , offsets $\alpha_j\in E_k$ , and targets $\eta_j\in E_k$ for $j\in F_q$ , a finite subset $s\subseteq F_n$ , a real $\mu$ , real masses $p_a\ge0$ for $a\in F_N$ with $\sum_{a\in F_N}p_a=1$ , and arbitrary functions $w,v,r:F_N\to E_d$ . Assume $s\ne\varnothing$ , $q>0$ , and $\mu>0$ . For each $t\in\{s,F_n\}$ define $G_t=|t|^{-1}\sum_{i\in t}A_i^*A_i$ , $b_t=|t|^{-1}\sum_{i\in t}A_i^*(y_i-a_i)$ , $H_t=G_t+\mu I_{E_d}$ , $R_t=\mathcal I(H_t)$ , and $o_t=R_tb_t$ , where stars denote Euclidean adjoints and $\mathcal I(H)$ is the multiplicative inverse when $H$ is invertible and zero otherwise. Define $G_P=q^{-1}\sum_{j\in F_q}B_j^*B_j$ , $H_P=G_P+\mu I_{E_d}$ , $R_P=\mathcal I(H_P)$ , and $\kappa=\|R_P\|\,\|G_P-G_s\|$ , using operator norms. For every $x,z\in E_d$ , define $g_x=H_sx-b_s$ , $u_x=R_Pg_x$ , $Q_x(z)=\tfrac12\langle z,H_Pz\rangle-\langle g_x,z\rangle$ , and $\Delta_x(z)=Q_x(z)-Q_x(u_x)$ . The assertion is $\sum_{a\in F_N}p_a\|w(a)-v(a)-r(a)\|^2\le\frac{6}{\mu}\sum_{a\in F_N}p_a\Delta_{w(a)}(v(a))+6\kappa^2\bigl(\sum_{a\in F_N}p_a\|w(a)-o_{F_n}\|^2+\|o_{F_n}-o_s\|^2\bigr)+3\sum_{a\in F_N}p_a\|r(a)-o_s\|^2$ . All three functions use the same law index and may have arbitrary dependence; there is no independence, mean-zero, optimizer, or solver-accuracy hypothesis. The data, subset, and regularization parameter are fixed across this finite law. The offsets and targets of $P$ are unused. There is no assumed relationship between the feature collections, no condition $\kappa<1$ , and no required client-removal description of $s$ . Nonempty $s$ and positive $q$ force $n,q\ge1$ ; zero dimensions, zero features, and zero individual masses are permitted. No law exists for $N=0$ because its total mass would be $0=1$ , while $N=1$ yields a deterministic inequality. For $d=0$ every term is zero; for $k=0$ the formulas hold with $G_t=G_P=0$ , $b_t=0$ , $H_t=H_P=\mu I_{E_d}$ , $o_t=0$ , and $\kappa=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