Frobenius bound, proved. If the entrywise square sum of W is at most C², the dense layer is C-Lipschitz in L2. This is the certified replacement for the power-iteration estimate specNormW: ‖W‖₂ ≤ ‖W‖_F, so any rational C ≥ ‖W‖_F is a sound Lipschitz constant.

A one-hidden-layer net's logits from its hidden pre-activations. Given the exact pre-activations pre of x, each logit of denseE W2 ∘ reluE ∘ denseE W1 is the finite sum the per-image margin and argmax proofs expand; every generated scorecard reads its logits through this.

√2 ≤ 14143/10000 — the rational majorant the per-image radius checks use.

Specialize the Tsuzuku certificate to a FIXED radius ε: if the margin clears the rational check (14143/10000)·L·ε ≤ m (kernel-checkable — no √2), every ‖δ‖ < ε leaves class i the strict argmax.

ReLU is 1-Lipschitz in L2 — coordinatewise |max(a,0) − max(b,0)| ≤ |a − b| summed. The activation contributes factor 1 to the product certificate.

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

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

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₁).

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.

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.

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.

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

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

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

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.

Row-wise Cauchy–Schwarz summed: ‖Mv‖² ≤ ‖M‖_F²·‖v‖² at the raw-sum level.

Gram (Schatten-4) bound, proved. If G = W·Wᵀ (supplied as data, verified entrywise) and ‖G‖_F² ≤ B⁴, then the dense layer is B-Lipschitz in L2. Since ‖G‖_F = (Σᵢσᵢ⁴)^½, this is ‖W‖₂ ≤ (Σσᵢ⁴)^¼ — strictly tighter than Frobenius (Σσᵢ²)^½ whenever the spectrum has any spread. The Gram matrix is only k×k (output-side), so the kernel arithmetic stays small even for wide layers.

Certified lower bound on any L2 Lipschitz constant (the power-iteration direction): if ‖f u − f w‖ ≥ ℓ·‖u − w‖ at one concrete pair (verified as a squared-sum inequality in-kernel), then every valid L satisfies ℓ ≤ L. With u the (rationalized) power-iteration singular vector and w = 0, this certifies how close a proven upper bound sits to the true ‖W‖₂.

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

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

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.

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.

Sum-shuffle: ‖Aᵀy‖² = ⟨y, K y⟩ for K = A·Aᵀ supplied as data. The rearrangement engine both Gram bounds share.

Iterated Gram (Schatten-8) bound, proved. One more squaring: with G = W·Wᵀ and H = Gᵀ·G (= G² for the symmetric G) supplied as data, ‖H‖_F² ≤ B⁸ gives LipschitzL2 B (denseE W) — i.e. ‖W‖₂ ≤ ‖G²‖_F^(1/4) = (Σσᵢ⁸)^(1/8), one Cauchy–Schwarz level tighter than the Schatten-4 bound.

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

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.

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