The CANONICAL MNIST MLP — 784→512→512→10 (ReLU, biased) #

mlpVerified (LeanMlir/VerifiedNets.lean, Chapter 2) is the repo's canonical MNIST reference architecture: [.dense 784 512, .relu, .dense 512 512, .relu, .dense 512 10]. Every runnable MNIST MLP path uses it (verified/e4m3/pgd/spectral/smooth trainers, the committed verified_mlir/mlp_train_step.mlir render, the baselines, margin_probe.py).

This file makes the canonical claim a CHECKABLE LEAN SURFACE: the generic MLP proof chain (whole-net VJP, float-gradient closeness, float-SGD descent, the emitted-train-step tie) instantiated at the literal canonical dims. Each declaration below IS the corresponding generic theorem at (784, 512, 512, 10) — #check shows the specialized statement; the 3-axiom audit covers them all. Nothing else in Lean consumes them: tests/AuditAxioms.lean is this file's only importer, by design. The spec-level partner is SpecVJP.lean's mlpVerified_denote_eq / mlpVerified_has_vjp* (stated over mlpVerified.layers itself; that file lives outside the Mathlib-only seam).

The OTHER MNIST proof population — the trained-weight certificate instances (LipschitzCert{Instance,Scorecard*,Float}, TrainedMlpWitness, TrainedLinearDescent) — deliberately lives on a REDUCED model (4×4-pooled 49-dim inputs, width-8 hidden, /128–/256 rational weights): every margin, Schatten/Gram sum, and LDLᵀ SOS witness is exact rational arithmetic checked in-kernel, which is infeasible today at 512-wide fan-ins (and the unconstrained canonical net's spectral-product cert is MEASURED vacuous — L ≈ 39 ⇒ 0% certified — which is why randomized smoothing, which DOES run on the canonical net, exists). Those files carry a reduced-model banner pointing here.