Spec → math (the verification tie), Rung 1: the linear classifier #

The shape #guard beside resnet34Verified in VerifiedNetsCore.lean only checks the parameter interface (typechecking). This file is the first rung of connecting a readable VerifiedNetSpec to the actual math — the proven VJP — on the simplest net, the Chapter-1 linear classifier (dense 784→10).

The pattern (extends to MLP → conv nets, each rigid/per-net):

1. denote maps the spec's layers to the Mathlib math function the proofs are about;
2. a rfl lemma ties the spec's denotation to that named function (mnistLinear);
3. the whole-model VJP theorem is stated about the spec's denotation and discharged by the audited op-level VJP (dense_has_vjp).

If the spec's layers drifts from [.dense 784 10], step 2/3 stop reducing and the proofs fail to typecheck — so the readable architecture is provably the verified one, at the math level, not just the shape level.

Rung 2: the MLP — the first genuine vjp_comp fold #

The linear model was the degenerate case (one layer, no fold). The MLP's denotation is a chain — dense ∘ relu ∘ dense ∘ relu ∘ dense (mlpForward) — and its VJP is built by folding vjp_comp_at down that chain (mlp_has_vjp_at). So this is where the spec→math tie first exercises the chain rule, not just a single op.

Rung 3: the CNN — the fold now runs through conv + maxpool #

The CNN's denotation is mnistCnnNoBnForward — a flat Vec 784 → Vec 10 chain flatConv → relu → flatConv → relu → maxPoolFlat → dense → relu → dense → relu → dense. The honest chain-rule fold (via vjp_comp_at through conv/maxpool/dense) is the audited mnistCnnNoBn_has_vjp_at, conditional on the four ReLU kinks + the maxpool being smooth at the input. Here we headline the unconditional canonical witness (mlp_has_vjp style); the spec is exactly the subject of that conditional fold via cnnVerified_denote_eq.

Rung E (linear): the spec ↔ the generated MLIR #

The ties above connect the spec to the math (denote = the proven forward, which has the proven VJP). This connects the spec to the StableHLO the trainer actually compiles and runs: the generated forward graph fwdGraph (→ verified_mlir/linear_fwd.mlir, the eval path) and the train-step loss-cotangent graph lossCotGraph (→ linear_train_step.mlir) denote the spec's forward and its softmax-CE gradient — via the audited faithfulness theorems (fwdGraph_faithful, lossCotGraph_isCEgrad) composed with denoteLinear = mnistLinear (rfl). So the generated code provably computes the spec's function.

What stays trusted (the codegen boundary, per Proofs/README.md): the text render linearFwdModuleV = pretty (emit fwdGraph) and that the committed .mlir equals that text — the pretty-printer + regeneration, NOT the semantics, which are proven here.

Rung E (MLP): the spec ↔ the generated MLIR — both forward and backward #

The MLP has faithfulness for the whole forward graph (mlpFwdGraph_faithful, the graph mlp_fwd.mlir prints) AND for a whole backward input-VJP graph (mlpBackGraph_faithful). Composed with denoteMLP = mlpForward and mlpVerified_has_vjp_at = mlp_has_vjp_at, both denote the spec: the rendered forward computes the spec's forward, and mlpBackGraph computes the spec's VJP backward (at a smooth input). mlpBackGraph is a spec-level graph no committed artifact prints: mlp_train_step.mlir is MlpRender.lean's mlpTrainStepFaithfulV, whose parameter ops MlpFold ties to the certified step.

Rung E (CNN): the spec ↔ the generated MLIR (forward) #

The generated CNN forward graph (flatConv→relu→flatConv→relu→maxPoolFlat→dense→relu→ dense→relu→dense) denotes the spec's forward. The backward graph faithfulness exists too (cnnBackGraph_faithful denotes mnistCnnNoBn_has_vjp_at.backward — the VJP of exactly this spec's forward), but it carries the same five ReLU/maxpool smoothness hypotheses as the conditional fold, so we headline the unconditional forward tie (matching cnnVerified_has_vjp, the canonical witness).

Rung 4 + E (CIFAR): completing the ch5 ladder #

The CIFAR-10 net (ic=3, c1=32, c2=64, h=w=8 — spatial 32→16→8) gets the spec→math denotation (= cifarCnnForward by rfl), the canonical witness VJP, and the forward spec→generated-MLIR tie (cifarFwdGraph_faithful). The conditional fold is cifarCnn_has_vjp_at (six ReLU kinks + two maxpools).

Rung B/C/E (ch7 MobileNetV2, FULL, batched): the committed spec ↔ the batch-BN net #

denoteMobilenetB maps mobilenetv2Verified.layers — the committed 21-entry full-paper [t,c,n,s] list the trainer runs (stem-s2 3→32 → 17 bottlenecks → 1×1 head 320→1280 → GAP → dense 1280→10) — to mobilenetv2ForwardB_full (MobileNetV2FullB.lean: batch BN throughout, the t=1 no-expand first block, 4 stride-2 depthwise downsamples 224→7), at every batch size. Weights ride in the MNV2BWeights bundle, so the tie stays readable. The rfl is drift-sensitive: any [t,c,n,s] edit to the spec stops the match reducing — the tripwire the 6→17-block promotion once fired while the per-example twin of this section was orphaned; certs.yml re-elaborates it on every spec push. (That per-example twin, at the forward of the retired SGD artifact, was retired on 2026-09-19.)

Rung B/C/E (FULL, unified weight bundles): r34 / enet / convnext / vit #

The mnv2 full-paper pattern applied to the remaining imagenette nets: each committed spec's ENTIRE layer list (literal dims, drift-sensitive) denotes the full proven forward, with weights riding a structure bundle so the ties stay readable. Existing bundles are reused where the Full module already has one (B0Weights, CnxTWeightsCh, R34BWeights); vit gets its bundle here (ViTTinyWeights, SpecVJP-local so no proof module's signature changes). Rung E composes each net's full graph-faithfulness apex with the tie (vit's is vitFwdGraphKMHV_faithful, ViTDepthK §3 — the depth-k multi-head vector-LN graph). Rung C is the canonical witness except vit: all-smooth, so vit's rung C is the REAL whole-net VJP vitForwardKV_has_vjp (only 0 < ε) at the committed spec.