One-hot [bs, d1] f32 batch from int32-LE labels (1.0 = bytes 00 00 80 3F), for a possibly partial final batch: rows past total records get an all-zero row (their padded images are never scored, so the gradient they induce is irrelevant — the row just has to exist because the batch dim is baked into the compiled module).

The rows of one padded eval batch that are classified correctly: of the first min bs (total - start) rows of logits ([bs, d1]), those whose argmax is the label of record start + j. The pad rows past total are never scored.

Batches over the split, the last one partial and zero-padded, not dropped.

Eval batch bi, zero-padded to bs rows.

The forward's [bs, d1] logits at params on the input batch x.

Correctly classified eval images at params.

The Lipschitz-margin certificate over the split at params: returns the correctly classified count and, for each radius in radii, how many of those points the certificate covers. A point is covered at ε when it is classified correctly and its certified radius m/(√2·L) is at least ε, m being the gap between the top and the runner-up logit (the radius of lipschitz_margin_certified_radius, L the network's Lipschitz bound).

PGD over the split: writes kernelText to kernelPath, opens it, and from each clean batch x0 runs K steps of kernelFn (its params blob pgdParams ++ [onehot, x0]), then counts the adversarial batch's correct rows under the forward at params.

Relative slack on every host-computed bound. The Gram sums are evaluated in Float (f64) from f32 weights, so the computed ‖H‖_F carries accumulation error far below this factor at these layer sizes; the slack is the soundness margin for that rounding, not a proved one.

The output-side Gram G a b = Σⱼ M a j · M b j (k×k, row-major) of the k×n matrix M a j = get a j, row a being output a — the orientation of denseE, so G is the hG data of denseE_lipschitzL2_gram2. M is copied into a contiguous buffer first.

The Schatten-8 bound from the Gram: H = Gᵀ·G, then B = (Σ H²)^{1/8} times roundingSlack — the B of denseE_lipschitzL2_gram2's hHF : Σ H² ≤ B⁸.

Power-iteration estimate of σ₁ = √λ_max(G) (a lower bound, up to convergence).

Both numbers for the k×n matrix get (row = output).

A dense layer W : [d0,d1] (row-major, logits = x·W + b). Its denseE matrix is Wᵀ (d1 outputs), so the Gram is the d1×d1 WᵀW. The bias is a translation and leaves the Lipschitz constant unchanged.

A zero-padded 2-D convolution with kernel W : [outC, inC, kh, kw] (row-major). Writing the conv as a sum over spatial taps T = Σ_{ky,kx} S_{ky,kx} ∘ M_{ky,kx}, each S a zero-filled shift (norm ≤ 1, at any stride) and each M the [outC,inC] channel-mixing matrix at that tap, the triangle inequality gives ‖T‖₂ ≤ Σ_tap ‖M_tap‖₂; each tap's ‖M_tap‖₂ is bounded by its Schatten-8 bound. The per-tap bound is denseE_lipschitzL2_gram2; the tap-sum step has no Lean theorem. Both steps are loose against the exact (Sedghi–Gupta–Long) conv norm. est sums the taps' power-iteration values: the tap-sum at the true per-tap norms, not an estimate of ‖T‖₂.

Matrix-free spectral norm ‖W‖₂ of W : [d0,d1] (row-major) — power iteration that applies W and Wᵀ as mat-vecs (σ = ‖W v‖, v the top right singular vector) instead of forming the d1×d1 Gram. ~2·d0·d1 per iteration vs d0·d1² for the Gram (gramOut), so it's cheap enough to call during training (the spectral-norm projection below). Fewer iters (iters) trade a little precision for speed. An estimate from below, so never a certificate constant (denseLip is).

Spectral-norm projection (projected SGD toward the spectral ball): rescale every weight whose L2 norm exceeds c down to c, leaving biases untouched. Conv [o,i,kh,kw]: cap the same tap-sum bound the certificate uses (convLip) by scaling the whole kernel, so for the convs the projection and the certificate control the identical quantity. Dense [d0,d1]: cap the matrix-free power-iteration estimate of ‖W‖₂ (specNormMV) — the certificate's Schatten-8 bound costs a full Gram, too much to recompute every few steps — so a projected dense layer's certified Lᵢ (denseLip) sits somewhat above c. This is the lever that turns the (vacuous) product certificate non-vacuous. F32.scaleShift does the rescale.

PGD attack on the verified MNIST MLP. Trains the 784→512→512→10 ReLU MLP on the proof-rendered SGD step, then runs PGD with genMlpPgdStep, a hand-typed StableHLO kernel that follows the formula of Proofs.mlpInputGrad (no theorem ties the kernel's text). The Lipschitz certificate is the product of the three layers' spectral norms, which is where the bound, and so the certificate, goes loose.

Spectral-norm-constrained training of the verified MNIST MLP. Trains the 784→512→512→10 net with projected SGD onto the spectral ball — after every projEvery proof-rendered steps (and once at the end) each weight Wᵢ is rescaled so its power-iteration ‖Wᵢ‖₂ estimate is ≤ c (projectSpectral) — then runs the same cert ≤ TRUE ≤ PGD sandwich. Sweeps a few caps c (plus an unconstrained baseline) so the table shows the trade: shrinking c pulls the certified L = ∏ᵢ Lᵢ (the Schatten-8 bounds, each somewhat above c) down, turning the vacuous product certificate non-vacuous — at the cost of clean accuracy. The empirical face of lipschitz_margin_certified_radius (LeanMlir/Proofs/Certificates/LipschitzCert/Basic.lean): smaller L ⇒ larger certified radius m/(√2·L). The training gradient comes from the proof-rendered train step; the projection is host-side weight rescaling, and the PGD kernel is the hand-typed genMlpPgdStep.

Refuse a net certProduct cannot bound. The check is by shape and init kind only: it refuses any parameter of rank other than 1, 2 or 4, and any of init kind 1 (mkParam's constant-one init, which is how a BN or LayerNorm γ starts). The product skips every rank-1 parameter, so a scale it does not catch this way (another init kind) would still make it return a number that is no bound; today's callers, the BN-free MNIST and CIFAR CNNs, have none.

The conv-aware certificate product over a packed parameter list: convLip for each [o,i,kh,kw] kernel, denseLip for each [d0,d1] weight, biases skipped. Returns the product of the bounds (the certificate's L), the product of the estimates, and a per-layer bound (estimate) line. Sound only for nets requireCertModelled accepts.

Generic conv-net PGD attack. Trains any packed conv net on its proof-rendered SGD step, then runs PGD with genKernel: a hand-typed StableHLO kernel that computes the input gradient dx (conv input-VJPs and maxpool select_and_scatter backs, following the backward ops of the net's <slug>_train_step.mlir); no theorem ties the kernel's text. Certificate = the conv-aware product of per-layer upper bounds (convLip for convs × denseLip for denses; ReLU and the disjoint 2×2 max-pools are 1-Lipschitz) — astronomically loose, the depth-cliff. genKernel and net.slug select the architecture (genCnnPgdStep/MNIST-CNN, genCifarPgdStep/CIFAR-CNN).

PGD attack on the verified MNIST CNN (the first conv rung).

PGD attack on the verified CIFAR-10 CNN (the deeper conv rung: 4 conv + 2 pool + 3 dense).

Spectral-norm-constrained training of the verified MNIST CNN. The CNN sibling of attackPgdSpectralMlp: projected SGD toward the spectral ball — every projEvery proof-rendered steps (and once at the end) projectSpectral caps the dense ‖Wᵢ‖₂ estimate and the conv tap-sum bound at c — then the cert ≤ TRUE ≤ PGD sandwich (PGD via genKernel, cert = the conv-aware product). Harder than the MLP: it's a k-layer product and the conv tap-sum is a loose bound, so projection over-penalizes the convs — the cert needs a tighter c (and pays more clean accuracy) than the MLP did, and certifies only at smaller radii. The honest "depth + loose conv-norm ⇒ certifying the conv net is harder." Generic over genKernel/net.slug (MNIST-CNN, CIFAR-CNN).

Spectral-norm-constrained training of the verified MNIST CNN.

Spectral-norm-constrained training of the verified CIFAR-10 CNN (7-layer product).

PGD adversarial attack on the verified linear classifier. Trains via the proof-rendered train step, then runs PGD: each PGD step's input gradient is computed on the GPU by genLinearPgdStep, a hand-typed StableHLO kernel that follows the formula dx = (softmax−onehot)·Wᵀ (no theorem ties the kernel's text). Reports clean vs L∞-PGD adversarial accuracy over an eps sweep.