Documentation

LeanMlir.Proofs.Certificates.LipschitzCertPairSDP

Per-pair LipSDP certificates (Fazlyab–Robey–Hassani–Morari–Pappas 2019) #

The tighter-Lipschitz lever for the scorecard: replace the global product bound √2·‖W₂‖·‖W₁‖ on a pairwise logit gap by the per-pair LipSDP constant — for the gap g(x) = ⟨v, relu(W₁x)⟩ with v = W₂ᵢ − W₂ⱼ,

(g x − g x')² ≤ ρ·‖x − x'‖²

holds whenever S = 2·diag(T) − vvᵀ − (1/ρ)·T G₁ T is PSD for some diagonal T ⪰ 0 (G₁ = W₁W₁ᵀ, so S is h×h — hidden-width-sized, not input-sized, by Schur complement). The PSD witness entering Lean is an exact rational LDLᵀ factorization (S = L·diag(d)·Lᵀ, d ≥ 0) — kernel-checkable, no √, no eigenvalues, no native_decide.

The mathematical content: ReLU is slope-restricted in [0,1] (relu_slope_restricted), so for any T ⪰ 0 the incremental quadratic constraint Σₖ Tₖ·Δyₖ(Δuₖ − Δyₖ) ≥ 0 holds between any two activation patterns; adding it to the target and completing the square in Δx reduces (vᵀΔy)² ≤ ρ‖Δx‖² to ΔyᵀSΔy ≥ 0 (pair_sq_bound). Everything stays in squares — the final per-image check is Lp·ε ≤ margin with a rational Lp, ρ ≤ Lp² (certified_at_eps_pair); √ρ never appears.

This is the one-hidden-layer instance of LipSDP-Neuron; the SDP is solved numerically OFF-line (scripts/lipschitz_cert_pair_sdp.py) and only the rationalized certificate (ρ, T, L, d) enters Lean as DATA, verified exactly.

source
theorem Proofs.LipschitzCertDemo.relu_slope_restricted (a b : ℝ) :
0 ≤ (max a 0 - max b 0) * (a - b - (max a 0 - max b 0))

ReLU is slope-restricted in [0,1]: the increment Δy = relu a − relu b satisfies Δy·(Δu − Δy) ≥ 0 where Δu = a − b. The four sign cases.

source
theorem Proofs.LipschitzCertDemo.pair_sq_bound {n h : ℕ} (W : Fin h → Fin n → ℝ) (G : Fin h → Fin h → ℝ) (hG : ∀ (a b : Fin h), G a b = ∑ j : Fin n, W a j * W b j) (v T : Fin h → ℝ) (hT : ∀ (k : Fin h), 0 ≤ T k) {ρ : ℝ} (hρ : 0 < ρ) (hS : ∀ (z : Fin h → ℝ), (∑ k : Fin h, v k * z k) ^ 2 + 1 / ρ * ∑ a : Fin h, ∑ b : Fin h, T a * z a * (G a b * (T b * z b)) ≤ 2 * ∑ k : Fin h, T k * z k ^ 2) (x x' : EuclideanSpace ℝ (Fin n)) :
(∑ k : Fin h, v k * max ((denseE W x).ofLp k) 0 - ∑ k : Fin h, v k * max ((denseE W x').ofLp k) 0) ^ 2 ≤ ρ * ‖x - x'‖ ^ 2

Per-pair LipSDP squared bound. If the slack inequality holds for all z (discharged from a rational LDLᵀ witness: one linarith over its column squares), then the ReLU-network gap g(x) = Σₖ vₖ·relu((W x)ₖ) satisfies (g x − g x')² ≤ ρ·‖x − x'‖². No √ρ: everything in squares.

source
theorem Proofs.LipschitzCertDemo.mlp_gap_eq {n h k : ℕ} (W1 : Fin h → Fin n → ℝ) (W2 : Fin k → Fin h → ℝ) (i j : Fin k) (x : EuclideanSpace ℝ (Fin n)) :
((denseE W2 ∘ reluE ∘ denseE W1) x).ofLp i - ((denseE W2 ∘ reluE ∘ denseE W1) x).ofLp j = ∑ t : Fin h, (W2 i t - W2 j t) * max ((denseE W1 x).ofLp t) 0

A pairwise logit gap of dense ∘ relu ∘ dense is the ⟨rowᵢ−rowⱼ, relu·⟩ form pair_sq_bound speaks about.

source
theorem Proofs.LipschitzCertDemo.pair_sq_bound_mlp {n h k : ℕ} (W1 : Fin h → Fin n → ℝ) (W2 : Fin k → Fin h → ℝ) (G : Fin h → Fin h → ℝ) (hG : ∀ (a b : Fin h), G a b = ∑ j : Fin n, W1 a j * W1 b j) (i j : Fin k) (v T : Fin h → ℝ) (hv : ∀ (t : Fin h), v t = W2 i t - W2 j t) (hT : ∀ (t : Fin h), 0 ≤ T t) {ρ : ℝ} (hρ : 0 < ρ) (hS : ∀ (z : Fin h → ℝ), (∑ t : Fin h, v t * z t) ^ 2 + 1 / ρ * ∑ a : Fin h, ∑ b : Fin h, T a * z a * (G a b * (T b * z b)) ≤ 2 * ∑ t : Fin h, T t * z t ^ 2) (x x' : EuclideanSpace ℝ (Fin n)) :
(((denseE W2 ∘ reluE ∘ denseE W1) x).ofLp i - ((denseE W2 ∘ reluE ∘ denseE W1) x).ofLp j - (((denseE W2 ∘ reluE ∘ denseE W1) x').ofLp i - ((denseE W2 ∘ reluE ∘ denseE W1) x').ofLp j)) ^ 2 ≤ ρ * ‖x - x'‖ ^ 2

pair_sq_bound on the net's own logits. The gap f · i − f · j of f = denseE W2 ∘ reluE ∘ denseE W1, with v the row difference W2 i − W2 j, satisfies the squared LipSDP bound whenever the slack certificate hS does; every emitted pairSq* theorem is this at one class pair.

source
theorem Proofs.LipschitzCertDemo.pair_sq_symm {n k : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} {i j : Fin k} {ρ : ℝ} (h : ∀ (u u' : EuclideanSpace ℝ (Fin n)), ((f u).ofLp i - (f u).ofLp j - ((f u').ofLp i - (f u').ofLp j)) ^ 2 ≤ ρ * ‖u - u'‖ ^ 2) (u u' : EuclideanSpace ℝ (Fin n)) :
((f u).ofLp j - (f u).ofLp i - ((f u').ofLp j - (f u').ofLp i)) ^ 2 ≤ ρ * ‖u - u'‖ ^ 2

The squared pair bound is symmetric in the class pair: the gap for (j, i) is the negated gap for (i, j). The emitted reverse-order pairSq* theorems are this.

source
theorem Proofs.LipschitzCertDemo.certified_at_eps_pair {n k : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin k)} {i j : Fin k} {ρ Lp ε : ℝ} (hgap : ∀ (u u' : EuclideanSpace ℝ (Fin n)), ((f u).ofLp i - (f u).ofLp j - ((f u').ofLp i - (f u').ofLp j)) ^ 2 ≤ ρ * ‖u - u'‖ ^ 2) (hρL : ρ ≤ Lp ^ 2) (hLp : 0 < Lp) {x : EuclideanSpace ℝ (Fin n)} (hmargin : Lp * ε ≤ (f x).ofLp i - (f x).ofLp j) (δ : EuclideanSpace ℝ (Fin n)) (hδ : ‖δ‖ < ε) :
(f (x + δ)).ofLp j < (f (x + δ)).ofLp i

Fixed-ε certificate from a per-pair squared bound. If the gap f · i − f · j satisfies the squared LipSDP bound with constant ρ, Lp is a rational majorant (ρ ≤ Lp²), and the margin at x clears Lp·ε, then every ‖δ‖ < ε keeps class j strictly below class i. The per-pair peer of certified_at_eps — no √2, no global L.