Certified-accuracy scorecard (post_audit_roadmap §1) #

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.

The one-input certificate of LipschitzCertInstance.lean, scaled to a dataset-level claim over a FIXED subset — the first 100 MNIST test images (4×4-pooled, exact pixel-sum rationals) — at a FIXED radius ε = 1/10 (pooled-feature L2; a pooled coordinate is a 16-pixel block average, so ε is a 4×4-block-averaged pixel budget of 0.1·255 ≈ 25.5 gray levels concentrated on one block, or spread L2-wise across blocks). Two nets:

• unconstrained — the committed /128 net (W1t/W2t, q-acc 0.898), Schatten-8 product L = 63.79 (mlpT_lip_gram2): 1/100 certified at ε;
• spectrally capped — same recipe + projected SGD onto ‖Wᵢ‖₂ ≤ 4 (host-side rescaling after every step, as mnist-mlp-spectral), 36 epochs, /256-rationalized (W1s/W2s, q-acc 0.870), Schatten-8 product L = 19.76: 34/100 certified at the same ε.

Same theorem, same ε — the training method decides whether the certificate bites (the roadmap's caps 1.5–2 cost too much clean accuracy at this scale: σ ≤ 2 → 66% test acc; σ ≤ 4 keeps 87.0% vs 89.8% unconstrained).

Theorem vs. measurement — read this before quoting a number. Soundness lives in the ENGINE (certified_at_eps + LipschitzCert.lean), proved once — kernel-checking the 57th image buys nothing the 56th didn't. The counts above are exact-rational MEASUREMENTS over the first 100 images, carried in full by the certMargin* data table at the aggregate below (which is what downstream measurement passes read); the first 8 certified images per net additionally carry hpre*/margin*/certified* THEOREMS, and scorecard states only those. Every img<i> of the measured set is kept regardless — the 34 image definitions are cheap and other tiers reference them.

Each of the 8 EMITTED images gets a margin lemma (exact rational, in-kernel) and a ∀ δ, ‖δ‖ < ε → argmax fixed theorem via certified_at_eps. Every OTHER certified image appears only as a -- certMargin* comment line: a measurement, carrying no lemma of any kind. The aggregate count is the honest direction only ("at least K of 100") — an upper-bound L cannot prove an image UNcertifiable. Empirical bracket (not proof): L2-PGD (100 steps, 4 restarts) leaves uncon 69/100, capped 72/100 robust at the same ε — cert ≤ TRUE ≤ PGD.

Generated by scripts/lipschitz_cert_scorecard.py; weights/images are DATA.