Documentation

LeanMlir.Proofs.Certificates.LipschitzCert.Instance

A concrete instantiation of the Lipschitz-margin certified radius #

REDUCED CERTIFICATE MODEL — this file's concrete net is the 4×4-pooled 49-dim MNIST family (width-8 hidden, /128–/256 rational weights), NOT the canonical 784→512→512→10 mlpVerified; chosen so every margin/norm/SOS check is exact rational arithmetic in-kernel. Canonical surface: Proofs/MlpCanonical.lean.

Fixed-weight networks whose Lipschitz constant is proved in Lean (no power iteration, no hypothesis), whose margin at a concrete input is computed in-kernel, and whose certified radius is provably positive.

Three instances:

linear_demo_certified — a 2×2 linear classifier, L = 5 (Frobenius), margin 3 at x = e₀, certified radius 3/(√2·5) > 0.
mlp_demo_certified — a 2 → 2 → 2 dense → ReLU → dense MLP, L = the per-layer product 3·(1·2) = 6 via LipschitzL2.comp (the exact product bound the PGD demos estimate numerically), margin 2, radius 2/(√2·6) > 0.
trained_demo_certified, trained_demo_certified_gram, trained_demo_certified_gram2 — the trained 49→8→10 MLP mlpT at the pooled MNIST test image xt, with Frobenius (mlpT_lip), Schatten-4 (mlpT_lip_gram) and Schatten-8 (mlpT_lip_gram2) product constants. The certified lower bounds W1t_lip_lower / W2t_lip_lower bound each layer's best Lipschitz constant from below. mlpT, its weights and mlpT_logit_continuous are what LipschitzCert.Scorecard, Smoothing.NetSemantics and Smoothing.NetWitness build on.

def Proofs.LipschitzCertDemo.Wlin :

Fin 2 → Fin 2 → ℝ

Fixed 2×2 weight matrix: logits (3x₀, 4x₁). Frobenius norm exactly 5.

Equations

Proofs.LipschitzCertDemo.Wlin = ![![3, 0], ![0, 4]]

Instances For

noncomputable def Proofs.LipschitzCertDemo.xlin :

EuclideanSpace ℝ (Fin 2)

The concrete input x = e₀.

Equations

Proofs.LipschitzCertDemo.xlin = !₂[1, 0]

Instances For

theorem Proofs.LipschitzCertDemo.Wlin_lip :

LipschitzL2 5 (denseE Wlin)

theorem Proofs.LipschitzCertDemo.xlin_margin (j : Fin 2) :

j ≠ 0 → 3 ≤ (denseE Wlin xlin).ofLp 0 - (denseE Wlin xlin).ofLp j

Margin computed in-kernel: logits at xlin are (3, 0), so class 0 leads by 3.

theorem Proofs.LipschitzCertDemo.linear_radius_pos :

0 < 3 / (√2 * 5)

The certified radius is strictly positive — the certificate is non-vacuous. Numerically 3/(√2·5) ≈ 0.424.

theorem Proofs.LipschitzCertDemo.linear_demo_certified (δ : EuclideanSpace ℝ (Fin 2)) (hδ : ‖δ‖ < 3 / (√2 * 5)) (j : Fin 2) :

j ≠ 0 → (denseE Wlin (xlin + δ)).ofLp j < (denseE Wlin (xlin + δ)).ofLp 0

The instantiated Tsuzuku certificate (linear). Every L2 perturbation of norm < 3/(√2·5) of the concrete input leaves class 0 the strict argmax of the concrete network x ↦ (3x₀, 4x₁).

def Proofs.LipschitzCertDemo.Wmlp :

Fin 2 → Fin 2 → ℝ

Hidden layer: identity mixing (Frobenius √2 ≤ 2).

Equations

Proofs.LipschitzCertDemo.Wmlp = ![![1, 0], ![0, 1]]

Instances For

def Proofs.LipschitzCertDemo.Vmlp :

Fin 2 → Fin 2 → ℝ

Output layer: (2h₀, h₁) (Frobenius √5 ≤ 3).

Equations

Proofs.LipschitzCertDemo.Vmlp = ![![2, 0], ![0, 1]]

Instances For

noncomputable def Proofs.LipschitzCertDemo.mlp :

EuclideanSpace ℝ (Fin 2) → EuclideanSpace ℝ (Fin 2)

The concrete 2-layer MLP dense ∘ relu ∘ dense.

Equations

Proofs.LipschitzCertDemo.mlp = Proofs.LipschitzCertDemo.denseE Proofs.LipschitzCertDemo.Vmlp ∘ Proofs.LipschitzCertDemo.reluE ∘ Proofs.LipschitzCertDemo.denseE Proofs.LipschitzCertDemo.Wmlp

Instances For

theorem Proofs.LipschitzCertDemo.mlp_lip :

LipschitzL2 6 mlp

The per-layer product certificate L = 3·(1·2) = 6, assembled by LipschitzL2.comp from proved Frobenius bounds — the certified analogue of the ∏ᵢ‖Wᵢ‖₂ product the PGD demos compute numerically.

theorem Proofs.LipschitzCertDemo.mlp_margin (j : Fin 2) :

j ≠ 0 → 2 ≤ (mlp xlin).ofLp 0 - (mlp xlin).ofLp j

Margin computed in-kernel through the whole MLP: forward of e₀ is (1,0) ↦ relu (1,0) = (1,0) ↦ (2,0), so class 0 leads by 2.

theorem Proofs.LipschitzCertDemo.mlp_radius_pos :

0 < 2 / (√2 * 6)

theorem Proofs.LipschitzCertDemo.mlp_demo_certified (δ : EuclideanSpace ℝ (Fin 2)) (hδ : ‖δ‖ < 2 / (√2 * 6)) (j : Fin 2) :

j ≠ 0 → (mlp (xlin + δ)).ofLp j < (mlp (xlin + δ)).ofLp 0

The instantiated Tsuzuku certificate (MLP). Every L2 perturbation of norm < 2/(√2·6) ≈ 0.236 leaves class 0 the strict argmax of the concrete dense→ReLU→dense network — kink and all: the certificate is architecture-agnostic, no smoothness hypotheses needed.

def Proofs.LipschitzCertDemo.W1tQ :

Fin 8 → Fin 49 → ℚ

Trained hidden-layer weights (8×49), entries k/128.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.W1t :

Fin 8 → Fin 49 → ℝ

Equations

Proofs.LipschitzCertDemo.W1t = Proofs.castM Proofs.LipschitzCertDemo.W1tQ

Instances For

def Proofs.LipschitzCertDemo.W2tQ :

Fin 10 → Fin 8 → ℚ

Trained output-layer weights (10×8), entries k/128.

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.W2t :

Fin 10 → Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.W2t = Proofs.castM Proofs.LipschitzCertDemo.W2tQ

Instances For

noncomputable def Proofs.LipschitzCertDemo.xt :

EuclideanSpace ℝ (Fin 49)

MNIST test image #1895 (digit 2), 4×4-average-pooled: exact pixel sums over 4080 (= 255·16).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.mlpT :

EuclideanSpace ℝ (Fin 49) → EuclideanSpace ℝ (Fin 10)

The trained MLP: dense → ReLU → dense.

Equations

Proofs.LipschitzCertDemo.mlpT = Proofs.LipschitzCertDemo.denseE Proofs.LipschitzCertDemo.W2t ∘ Proofs.LipschitzCertDemo.reluE ∘ Proofs.LipschitzCertDemo.denseE Proofs.LipschitzCertDemo.W1t

Instances For

noncomputable def Proofs.LipschitzCertDemo.hpreVals :

Fin 8 → ℝ

Exact hidden pre-activations of xt (denominator 128·4080).

Equations

Proofs.LipschitzCertDemo.hpreVals = ![507504 / 522240, 730889 / 522240, 164933 / 522240, 245813 / 522240, 2734742 / 522240, -21615 / 522240, 1483431 / 522240, 2664061 / 522240]

Instances For

theorem Proofs.LipschitzCertDemo.hpre_eval (k : Fin 8) :

(denseE W1t xt).ofLp k = hpreVals k

theorem Proofs.LipschitzCertDemo.W1t_lip :

LipschitzL2 (2911 / 200) (denseE W1t)

Frobenius² of W1t is ≤ C₁² for C₁ = 2911/200 ≈ ‖W1t‖_F.

theorem Proofs.LipschitzCertDemo.W2t_lip :

LipschitzL2 (1822 / 125) (denseE W2t)

theorem Proofs.LipschitzCertDemo.mlpT_lip :

LipschitzL2 (2651921 / 12500) mlpT

Product certificate for the trained net: L = C₂·(1·C₁) = 2651921/12500.

theorem Proofs.LipschitzCertDemo.xt_margin (j : Fin 10) :

j ≠ 2 → 6953 / 500 ≤ (mlpT xt).ofLp 2 - (mlpT xt).ofLp j

In-kernel margin: class 2 leads every other class at xt by ≥ 6953/500.

theorem Proofs.LipschitzCertDemo.trained_radius_pos :

0 < 6953 / 500 / (√2 * (2651921 / 12500))

theorem Proofs.LipschitzCertDemo.trained_demo_certified (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 6953 / 500 / (√2 * (2651921 / 12500))) (j : Fin 10) :

j ≠ 2 → (mlpT (xt + δ)).ofLp j < (mlpT (xt + δ)).ofLp 2

The Tsuzuku certificate at TRAINED weights. Every L2 perturbation of the pooled MNIST digit-2 with ‖δ‖ < 13.906/(√2·212.154) ≈ 0.0463 leaves class 2 the strict argmax of the trained, rationalized network.

def Proofs.LipschitzCertDemo.G1tQ :

Fin 8 → Fin 8 → ℚ

Exact Gram matrix G1t = W1t·W1tᵀ (8×8, denominators 128² = 16384).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.G1t :

Fin 8 → Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.G1t = Proofs.castM Proofs.LipschitzCertDemo.G1tQ

Instances For

def Proofs.LipschitzCertDemo.G2tQ :

Fin 10 → Fin 10 → ℚ

Exact Gram matrix G2t = W2t·W2tᵀ (10×10).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.G2t :

Fin 10 → Fin 10 → ℝ

Equations

Proofs.LipschitzCertDemo.G2t = Proofs.castM Proofs.LipschitzCertDemo.G2tQ

Instances For

theorem Proofs.LipschitzCertDemo.G1t_eq (a b : Fin 8) :

G1t a b = ∑ j : Fin 49, W1t a j * W1t b j

theorem Proofs.LipschitzCertDemo.G2t_eq (a b : Fin 10) :

G2t a b = ∑ j : Fin 8, W2t a j * W2t b j

theorem Proofs.LipschitzCertDemo.W1t_lip_gram :

LipschitzL2 (46 / 5) (denseE W1t)

Schatten-4 Lipschitz bound for the hidden layer: B₁ = 46/5 ≈ (Σσ⁴)^(1/4).

theorem Proofs.LipschitzCertDemo.W2t_lip_gram :

LipschitzL2 (9661 / 1000) (denseE W2t)

theorem Proofs.LipschitzCertDemo.mlpT_lip_gram :

LipschitzL2 (222203 / 2500) mlpT

The tightened product certificate: L = B₂·(1·B₁) = 222203/2500.

theorem Proofs.LipschitzCertDemo.trained_radius_gram_pos :

0 < 6953 / 500 / (√2 * (222203 / 2500))

theorem Proofs.LipschitzCertDemo.trained_demo_certified_gram (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 6953 / 500 / (√2 * (222203 / 2500))) (j : Fin 10) :

j ≠ 2 → (mlpT (xt + δ)).ofLp j < (mlpT (xt + δ)).ofLp 2

The tightened trained certificate. Same trained net, same margin, the Gram bound in place of Frobenius: every ‖δ‖ < 13.906/(√2·88.88) ≈ 0.1106 (2.4× the Frobenius radius) leaves the prediction fixed.

noncomputable def Proofs.LipschitzCertDemo.v1t :

EuclideanSpace ℝ (Fin 49)

Rationalized power-iteration vector for W1t (top right-singular direction ×1000).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.v2t :

EuclideanSpace ℝ (Fin 8)

Rationalized power-iteration vector for W2t.

Equations

Proofs.LipschitzCertDemo.v2t = !₂[712, 160, -442, -286, -38, -140, -248, -328]

Instances For

theorem Proofs.LipschitzCertDemo.W1t_lip_lower (L : ℝ) :

LipschitzL2 L (denseE W1t) → 1863 / 250 ≤ L

Certified lower bound: ANY L with LipschitzL2 L (denseE W1t) is ≥ 1863/250. With W1t_lip_gram : LipschitzL2 9.2 …, the true ‖W1t‖₂ is sandwiched in [7.452, 9.2] — the Gram bound is provably ≤ 1.235× optimal.

theorem Proofs.LipschitzCertDemo.W2t_lip_lower (L : ℝ) :

LipschitzL2 L (denseE W2t) → 77 / 10 ≤ L

def Proofs.LipschitzCertDemo.H1tQ :

Fin 8 → Fin 8 → ℚ

H1t = G1t² (= G1tᵀ·G1t, 8×8, denominators 16384² = 268435456).

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.H1t :

Fin 8 → Fin 8 → ℝ

Equations

Proofs.LipschitzCertDemo.H1t = Proofs.castM Proofs.LipschitzCertDemo.H1tQ

Instances For

def Proofs.LipschitzCertDemo.H2tQ :

Fin 10 → Fin 10 → ℚ

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def Proofs.LipschitzCertDemo.H2t :

Fin 10 → Fin 10 → ℝ

Equations

Proofs.LipschitzCertDemo.H2t = Proofs.castM Proofs.LipschitzCertDemo.H2tQ

Instances For

theorem Proofs.LipschitzCertDemo.H1t_eq (a b : Fin 8) :

H1t a b = ∑ c : Fin 8, G1t c a * G1t c b

theorem Proofs.LipschitzCertDemo.H2t_eq (a b : Fin 10) :

H2t a b = ∑ c : Fin 10, G2t c a * G2t c b

theorem Proofs.LipschitzCertDemo.W1t_lip_gram2 :

LipschitzL2 (7769 / 1000) (denseE W1t)

Schatten-8 bound: B₁' = 7769/1000 ≈ (Σσ⁸)^(1/8) (true σ₁ ≈ 7.4525).

theorem Proofs.LipschitzCertDemo.W2t_lip_gram2 :

LipschitzL2 (8211 / 1000) (denseE W2t)

theorem Proofs.LipschitzCertDemo.mlpT_lip_gram2 :

LipschitzL2 (63791259 / 1000000) mlpT

Schatten-8 product certificate: L = B₂'·(1·B₁') = 63791259/1000000 ≈ 63.79 — vs the certified lower bounds ℓ₁·ℓ₂ = 57.38, provably within 11.2% of the per-layer-optimal product.

theorem Proofs.LipschitzCertDemo.trained_radius_gram2_pos :

0 < 6953 / 500 / (√2 * (63791259 / 1000000))

theorem Proofs.LipschitzCertDemo.trained_demo_certified_gram2 (δ : EuclideanSpace ℝ (Fin 49)) (hδ : ‖δ‖ < 6953 / 500 / (√2 * (63791259 / 1000000))) (j : Fin 10) :

j ≠ 2 → (mlpT (xt + δ)).ofLp j < (mlpT (xt + δ)).ofLp 2

Schatten-8 trained certificate: radius ≈ 0.1541 (3.3× Frobenius, 1.4× Schatten-4; the true-σ ceiling for the product method is 0.171).

theorem Proofs.LipschitzCertDemo.mlpT_logit_continuous (j : Fin 10) :

Continuous fun (x : EuclideanSpace ℝ (Fin 49)) => (mlpT x).ofLp j

Each logit of the trained pooled-MNIST MLP is continuous: the coordinate formula ∑ k, W2ⱼₖ·max(∑ l, W1ₖₗ·xₗ, 0) is definitional.