Equations (3)–(5), Condition 5 — Ridge Structure and Unique Minimizer

Proved

FedRemoval.RidgeStructure

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

convex-optimizationfederated-learningmachine-learningunlearning

For every full dataset, every nonempty retained index set $S$ , and every $\mu>0$ , show that $H_S$ is invertible and $\|H_S^{-1}\|\le1/\mu$ . For all $w$ , the actual gradient of $L_S$ is $g_S(w)$ , and

\mu\|w\|^2\le\langle w,H_Sw\rangle,

L_S(w)=L_S(u_S)+\tfrac12\langle w-u_S,H_S(w-u_S)\rangle.

Finally, $w$ is a global minimizer of $L_S$ if and only if $w=u_S$ . Formalization note: source-derived quadratic structure, making the computed minimizer, uniqueness, and inverse-norm justification explicit.

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-A (Section 3), PDF p. 3 and PDF p. 4, equations (3)--(5); supplementary Section C2, PDF p. 13, Condition 5.

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 RidgeStructure :
∀ (n d k : ℕ) (D : Data n d k) (s : Finset (Fin n)) (μ : ℝ),
    s.Nonempty → 0 < μ →
    IsUnit (hessian D s μ) ∧
    ‖inverseHessian D s μ‖ ≤ μ⁻¹ ∧
    (∀ w, HasGradientAt (loss D s μ) (ridgeGradient D s μ w) w) ∧
    (∀ w, μ * ‖w‖ ^ 2 ≤ inner ℝ w (hessian D s μ w)) ∧
    (∀ w, loss D s μ w = loss D s μ (optimum D s μ) +
      (1 / 2 : ℝ) * inner ℝ (w - optimum D s μ)
        (hessian D s μ (w - optimum D s μ))) ∧
    (∀ w, (∀ z, loss D s μ w ≤ loss D s μ z) ↔ w = 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-A (Section 3), PDF p. 3 and PDF p. 4, equations (3)--(5); supplementary Section C2, PDF p. 13, Condition 5.

Read-back

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

For all natural numbers $n,d,k$ , write $F_t=\{0,\ldots,t-1\}$ and $E_t=\mathbb R^{F_t}$ with Euclidean structure. Choose 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$ , a finite subset $s\subseteq F_n$ , and a real $\mu$ . Assume $s\ne\varnothing$ and $\mu>0$ . Using Euclidean adjoints, define $G=|s|^{-1}\sum_{i\in s}A_i^*A_i$ , $b=|s|^{-1}\sum_{i\in s}A_i^*(y_i-a_i)$ , $H=G+\mu I_{E_d}$ , $\ell(w)=(2|s|)^{-1}\sum_{i\in s}\|A_iw+a_i-y_i\|^2+(\mu/2)\|w\|^2$ , and $g(w)=Hw-b$ . Let $R$ be the multiplicative inverse of $H$ if it is invertible and the zero endomorphism otherwise, and let $o=Rb$ . The assertion is the conjunction of six claims: $H$ has a two-sided continuous linear inverse; $\|R\|\le\mu^{-1}$ in operator norm; for every $w\in E_d$ , $\ell$ has gradient $g(w)$ at $w$ ; for every $w\in E_d$ , $\mu\|w\|^2\le\langle w,Hw\rangle$ ; for every $w\in E_d$ , $\ell(w)=\ell(o)+\tfrac12\langle w-o,H(w-o)\rangle$ ; and for every $w\in E_d$ , $(\forall z\in E_d,\ \ell(w)\le\ell(z))$ if and only if $w=o$ . The nonempty-set hypothesis excludes $n=0$ from nonvacuous instances. There is no positive-dimension or feature-rank assumption: $d=0$ is permitted, with its sole zero vector and its unique endomorphism serving as both identity and inverse, while $k=0$ is permitted with $G=b=0$ and $\ell(w)=(\mu/2)\|w\|^2$ . Offsets and targets are unrestricted.

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