Robustness verification proofs

This entrypoint collects proof-level links between robustness specifications and analytic certificates. The files underneath prove:

• Lipschitz continuity implies adversarial robustness;
• logit margins plus output perturbation bounds preserve the argmax classifier; and
• basic MLP/ReLU Lipschitz lemmas used by certified-robustness statements.

Executable verifiers live elsewhere. These modules state the mathematical consequences of their robustness certificates.

References:

• Hein and Andriushchenko, "Formal guarantees on the robustness of a classifier against adversarial manipulation", NeurIPS 2017.
• Wong and Kolter, "Provable defenses against adversarial examples via the convex outer adversarial polytope", ICML 2018.