Section C5 — Corrected Inverse-Hessian Perturbation

Proved

FedRemoval.InversePerturbation

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

convex-optimizationfederated-learningmachine-learningunlearning

For nonempty retained and server datasets and $\mu>0$ , prove

H_P^{-1}-H_S^{-1}=H_P^{-1}(G_S-G_P)H_S^{-1},

\|H_P^{-1}-H_S^{-1}\|\le \|H_P^{-1}\|\|G_S-G_P\|\|H_S^{-1}\|.

Formalization note: explicitly corrected replacement for the general inverse estimate in supplementary Section C5. Both inverse factors are retained; this is not the incorrect single-inverse-factor formula printed there.

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 InversePerturbation :
∀ (n q d k : ℕ) (D : Data n d k) (s : Finset (Fin n)) (P : Data q d k) (μ : ℝ),
    s.Nonempty → 0 < q → 0 < μ →
    inverseHessian P Finset.univ μ - inverseHessian D s μ =
      (inverseHessian P Finset.univ μ).comp
        ((gram D s - gram P Finset.univ).comp (inverseHessian D s μ)) ∧
    ‖inverseHessian P Finset.univ μ - inverseHessian D s μ‖ ≤
      ‖inverseHessian P Finset.univ μ‖ * ‖gram D s - gram P Finset.univ‖ *
        ‖inverseHessian 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$ , write $F_t=\{0,\ldots,t-1\}$ and $E_t=\mathbb R^{F_t}$ with Euclidean structure. Choose data $D$ with 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$ for $i\in F_n$ , and data $P$ with 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$ for $j\in F_q$ . Given any 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$ , $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}$ using Euclidean adjoints. Let $R_D$ and $R_P$ be their respective multiplicative inverses, each assigned the zero endomorphism if its argument is not invertible. Both the operator identity $R_P-R_D=R_P\circ(G_D-G_P)\circ R_D$ and the operator-norm inequality $\|R_P-R_D\|\le\|R_P\|\,\|G_D-G_P\|\,\|R_D\|$ are asserted; compositions act from right to left. The offsets and targets in both data objects are universally quantified but unused here. No relation between the feature collections, no rank condition, and no smallness condition on their Gram difference is assumed. Nonempty $s$ and positive $q$ force $n,q\ge1$ , while zero dimensions and zero features remain allowed. For $d=0$ every endomorphism is the unique zero map; for $k=0$ both Gram operators are zero and both the inverse difference and its asserted upper bound are zero.

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