Zero Vulnerability Radius

Abstract

Same-class divergent targets at vanishing distance force zero radius.

Theorem 1.1 (Vanishing same-class defects force zero radius).

$$\forall X,B,Y:\mathrm{Type},[\mathrm{PseudoMetricSpace}(X)],C:X\to B,T:X\to Y,S:\mathrm{Set}X,\mathrm{Nonempty}(S)\Rightarrow \mathrm{perfectOn}(C,T,S)\Rightarrow \forall x,y:\mathbb{N}\to X,\forall n:\mathbb{N},C(x(n))=C(y(n))\Rightarrow \forall n:\mathbb{N},T(x(n))\ne T(y(n))\Rightarrow \mathrm{Tendsto}(n\mapsto \mathrm{dist}(x(n),y(n)),\mathrm{atTop},\mathrm{nhds}(0))\Rightarrow \mathrm{vulnerabilityRadius}(C,T)=0.$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ZeroVulnerabilityRadius.zero_vulnerability_radius (✓ std3). ∎

Source. Repository-derived.

Commentary.

The defect-distance set is constructed from the metric, classifier, and target: it contains exactly distances of equal-class, different-target pairs. The vulnerability radius is its infimum.

A sequence of such pairs converging to distance zero makes the infimum zero even under the public hypotheses that a specified training set is nonempty and the classifier is perfect on it.

The proof applies the pinned extended-infimum, real-to-extended-real continuity, and order-convergence lemmas directly; no repository theorem supplied this radius result.

References

• Truth anchor: D5/S3/ConceptDynamics/ZeroVulnerabilityRadius.zero_vulnerability_radius
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition