C On Verification

The proofs in this book compile with zero sorrys. Every VJP correctness theorem — dense layers, convolution, batch normalization, residual connections, depthwise convolution, squeeze-and-excitation, layer normalization, and self-attention — is machine-checked by Lean’s type system. If it builds, it’s correct.

But “it builds” is only the first of three kinds of certainty, and they are not the same kind. Proven (deductive): in Lean, against three core axioms, each operator’s gradient is its exact reverse-mode derivative. By construction (structural): the StableHLO the GPU runs is not written but printed from the same datatype the proofs reason about, with a bridge theorem pinning it to the proven formula, so the code cannot drift from the math. Cross-checked (empirical): what cannot be proven — IREE’s lowering, GPU transcendentals, float32 rounding beyond its theorem layer (§ C.4) — is watched by independent oracles that must agree before the hardware is believed. Each kind catches what the others structurally cannot; this appendix walks the mechanisms, grouped by kind.

One property makes the whole edifice auditable: every chapter is pure composition. Every primitive either inherits from Mathlib’s \(\operatorname {fderiv}\) or composes previously-proved theorems, so each architecture’s whole-network VJP traces back to the Chapter 1 calculus. Figure C.1 draws those spines for the three longest chains in the book.

!

C.1 Proven: the math is right

Two mechanisms make the deductive layer trustworthy: the proofs themselves, and an independent re-check that the kernel — not just the elaborator — accepts them with no project axioms.

C.1.1 Trust kernel

The Verified VJP Proofs suite proves 70 VJP correctness theorems — one per layer, operator, and whole-network architecture, each asserting backward \(= \sum _j \operatorname {pdiv}f\, x\, i\, j \cdot dy_j\) — on top of the foundation \(\operatorname {pdiv}\) calculus and the differentiability/forward/witness machinery they rest on, plus 41 architecture definitions in the bestiary, across 199 Lean proof files, with zero project axioms. The axiom audit (tests/AuditAxioms.lean) re-checks 1,457 theorems in all — the VJP contracts plus the forward-graph faithfulness, render, cotangent-chain, backward-tie, and float32 results (§ C.4) — every one closing under the same three core axioms: \(\texttt{\# print axioms vit\_ full\_ has\_ vjp}\) shows only Lean core (propext, Classical.choice, Quot.sound), nothing project-level beneath those. (Earlier drafts axiomatized shortcuts for the kinked operators; every one has since been proved or become a noncomputable def over the canonical \(\operatorname {fderiv}\)-derived witness — the smooth-point caveats in the chapters are all that remains of them.)

What type-checking alone cannot catch: prose narrating a different formula than the theorem states (Lean only verifies its own statement), and anything past the elaborator — which is what the next mechanism and the empirical layer are for.

C.1.2 Independent kernel re-check (comparator)

tests/comparator/ wires the project up to leanprover/comparator, the Lean community’s trustworthy-judge tool for projects that claim zero project axioms. It runs 51 theorems — the foundation rules, every chapter’s headline Jacobian, the public *_has_vjp_correct wrappers, and three smooth-point pointwise variants (relu_has_vjp_at_correct, mlp_has_vjp_at_correct, maxPool2_has_vjp_at3_correct) whose underlying .correct field is a real proof rather than rfl — through Lean’s kernel typechecker independently of the elaborator, with an axiom-allowlist of exactly \(\{ \texttt{propext}, \texttt{Quot.sound}, \texttt{Classical.choice}\} \). Any project axiom in the transitive closure of any verified theorem would fail the run.

This is what closes the gap between “the elaborator accepted my proofs” (which lake build confirms) and “the kernel agrees, audited from a separate process” (which comparator confirms). The 51-theorem coverage is illustrative rather than exhaustive — the same recipe scales to any subset of the proof suite, and the same allowlist applies because every theorem in the project closes the same way.

How much lives below the named layer.

The dependency graph accompanying this blueprint currently shows roughly a hundred nodes — one per named theorem or definition, hand-linked by \uses annotations. The compiled environment is bigger: just over 5,000 project constants once compiler-generated names are filtered out. That gap is not padding; it is the substrate the named layer stands on. Measured mechanically (with a constant-level dependency explorer; see the repo’s atlas-integration branch), the ViT capstone vit_body_has_vjp_mat alone transitively depends on 101 project constants — and only 25 of those are named theorems in this book. The other 76 are the working parts a reader never needs by name: Mat and its flatten/unflatten round-trip lemmas, the HasVJP/HasVJPMat structures themselves, forward functions, reindexing glue. Every one of the 101 type-checks sorry-free on the same three-axiom trust kernel as the named layer — the audits above make no distinction between spine and substrate, which is the point: the blueprint’s curation is pedagogical, not epistemic.

C.2 By construction: the code is the math

C.2.1 Verified code generation

The proofs above answer whether the mathematics is right — the hand-derived VJPs, their proofs, and the elaborator that accepted them. They say nothing about a different gap. The GPU never runs the Lean functions; it runs a block of emitted stablehlo that IREE compiles once per training program. A code generator can be handed a correct proof and still emit an operation that contracts the wrong axis, transposes backwards, or silently drops a term — and the only thing traditionally linking the proof to the emitted string is a code comment. The “MLIR: operator” section in each chapter closes that gap for one operator; this section describes the machinery they share.

Three pieces. The link from a proof to the GPU is built from three components:

• Denoted IR and a bridge theorem. The emitted backward (and forward) is not a string but a Lean datatype — a small abstract syntax tree (Back, Fwd, Back3) — carrying a denotation \([\! [\cdot ]\! ]\) valued in the proofs’ own Vec and Tensor3 types. A bridge theorem then proves that this denotation equals the proven derivative: \([\! [\, \text{emitted graph}\, ]\! ] = (\text{proven VJP}).\mathrm{backward}\). Examples are conv_back_bridge, bn_back_bridge, and relu_back_bridge; each closes under the same three axioms as the rest of the project.

• A computable printer. A small printer walks that same IR and emits one stablehlo operation per node — dotGeneral \(W\) becomes stablehlo.dot_general, a selectPos node becomes compare GT 0 plus select, and so on. The emitted text is the printout of the IR, by construction.

• An execution oracle. A Python harness regenerates the .mlir from the printer, compiles it with IREE for both the llvm-cpu and rocm backends, runs it, and diffs the result against an independent NumPy reference. The CPU run is the correctness gate; the GPU run (ROCm on a Radeon RX 7900 XTX, gfx1100) confirms the proof-backed graph also executes on real hardware, matching the reference to roughly \(10^{-6}\).

Proven versus trusted. The resulting claim is exact and bounded:

• Proven (Lean, three axioms): the IR’s denotation equals the proven derivative.

• By construction: the emitted StableHLO is the rendering of exactly that IR.

• Trusted (validated numerically, not proven): that the StableHLO text faithfully denotes \([\! [\cdot ]\! ]\). Its syntactic half is now partly closed — the emitted text lexes and parses back to the proven op-graph (StableHLOLex.lean, StableHLOParse.lean) — leaving a formal StableHLO semantics, which does not yet exist; that IREE lowers the text correctly; and that float32 approximates \(\mathbb {R}\), the last now a conditional theorem validated on real silicon (§ C.4) rather than a bare assumption.

So the gradient the GPU computes is, by a machine-checked theorem, the network’s exact reverse-mode derivative over \(\mathbb {R}\) — up to one printer, IREE, and floating point. Where a conventional generator leaves thousands of lines of string-building linked to the proof by nothing at all, the unproven surface here is a single printer, tested end to end.

Why it is tractable. The reason a deep ResNet or a transformer block comes under this scheme as a focused engineering build, rather than a research project, is the order things were proved in. The VJP library is per-operator and generic — proved once, over abstract dimensions, before any code generation existed — and the whole-network VJPs compose those per-operator lemmas through the chain rule. Code generation therefore carries no new proof obligation: every architecture’s operators were proven once, and the emitter reuses them, adding only the printer and the numerical check. Build the mathematical foundation per-operator and generic, and the code generation becomes mechanical.

From operators to whole training steps. The per-operator bridge is the demonstration; the verified trainers run the full construction. Each reads a single committed .mlir — its entire training step, forward through backward through the parameter update — and that file is the printout of one graph whose denotation a faithfulness theorem proves equal to the certified loss-descent step, output by output. A companion tie theorem per network (<net>_net_tied_certified) then closes the gap a per-output bridge leaves open: the cotangent each parameter update consumes is the one the network’s own backward pass delivers at that site, threaded through the real forward activations — each update one composed equation rooted at the proven forward, not a quantifier over a free cotangent. All twelve chapter networks are tied this way, from the MNIST linear classifier to depth-12 ViT-Tiny, and each deep net’s rendered block-backward is pinned to that block’s certified VJP (vitBlockBackPR_eq_transformerBlock_vjp and its peers). The axiom audit re-derives every tie under the same three axioms, and CI prints a green cell for a network only when its tie capstone is in that closure — so the scorecard cannot claim more than the kernel checked. What stays trusted is exactly what the per-operator story already trusted, now carried across the whole step: the one printer, and that each emitted operation’s text denotes what \([\! [\cdot ]\! ]\) says it does.

The one conditional. For the smooth operators — BatchNorm and LayerNorm (given \(\varepsilon {\gt} 0\)), GELU, swish, sigmoid, softmax, and attention — the bridge is unconditional, holding at every input. For the kinked operators — ReLU, ReLU6, and max-pool — it holds only at a smooth point, where no pre-activation sits exactly on the kink (zero for ReLU, \(0\) or \(6\) for ReLU6, an argmax tie for max-pool); the equality is permitted to fail precisely on that measure-zero set, and nowhere else. That set is the one irreducible boundary the smooth-point caveats in the chapter sections refer to.

C.2.2 Inside a bridge theorem

The “denoted IR and a bridge theorem” above is worth seeing concretely, because it is the step that does the real work — the place where a string of emitted code becomes a proposition Lean can check. Take the backward pass. It is represented not as text but as a value of an inductive type, a small abstract syntax tree whose constructors are exactly the StableHLO operations a backward uses:

inductive Back (inp : Nat) : Nat -> Type where
  | cotangent  : Back inp inp            -- the input dy
  | dotGeneral (A : Mat m n) : Back inp n -> Back inp m   -- matmul
  | selectPos  (x : Vec n)   : Back inp n -> Back inp n   -- ReLU mask
  -- plus scale, sub, add, sumBroadcast, scaleConst (BN, residuals)

A Back value is a closed description of one backward graph. The dense backward, for instance, is just dotGeneral W cotangent — feed the incoming cotangent into a single matrix multiply. Two functions are defined on this type, and everything rests on the gap between them being closed by a theorem.

The denotation. The first function, Back.denote, interprets a graph into the proofs’ own Vec type — it says what the graph means mathematically:

and likewise for the remaining constructors — scale, sub, sumBroadcast, scaleConst, add — which are the pieces that assemble BatchNorm’s three-term backward and the residual fan-in. So a Back value denotes a concrete \(\texttt{Vec} \to \texttt{Vec}\) function, living in the same world as the VJP theorems.

The bridge, as an equation. A bridge theorem states that this denotation equals the proven derivative. For the dense layer:

Its proof is one word, rfl: both sides reduce to the same term, Mat.mulVec \(W\, dy\), so the denotation of the emitted graph and the proven backward are definitionally identical. That base case pins the plumbing. The ReLU bridge is the first with real content:

The proof unfolds the denotation to \(\text{if } x_i {\gt} 0 \text{ then } dy_i \text{ else } 0\) and shows it equals the canonical ReLU subgradient — but only under the hypothesis \(h_{\text{smooth}}\) that no coordinate sits on the kink. That hypothesis is not a technicality. It names exactly the measure-zero set where the emitted compare GT 0 disagrees with the true derivative, and the theorem is written to permit failure precisely there and nowhere else. The convolution bridge of Chapter 3 is the same shape with a harder proof: convBackDenote unfolds to a forward conv2d of the reversed-and-transposed kernel, discharged by expansion at the concrete tensor shape.

Composing the per-operator bridges. Whole-network backwards are assembled by substitution. Back.subst plugs one graph into another’s cotangent leaf, and a chain-rule lemma proves the denotation composes:

proved by induction over the graph — the IR-level analogue of the vjp_comp that builds whole-network VJPs from per-layer ones. So the per-operator bridges compose into a whole-network bridge the same way the VJP theorems compose into a whole-network VJP: the MLP’s mlp_whole_bridge is this one substitution, chaining its five per-operator bridges.

Why the datatype is the point. The Back value is the pivot between two arrows. The printer walks it and emits one stablehlo operation per constructor (dotGeneral \(\mapsto \) stablehlo.dot_general; selectPos \(\mapsto \) compare GT 0 plus select) — that arrow is the trusted one, producing the text in each chapter’s listing. The denotation interprets the same value into the proofs’ Vec type, and the bridge proves that equals the derivative — that arrow is machine-checked. Because both arrows start from one concrete datatype rather than from a string, “the emitted code computes the proven gradient” is a theorem about a value, not a hope about a comment.

C.3 Cross-checked: the hardware agrees

Because IREE cannot itself be proven, and GPU transcendentals have no IEEE specification, the last stretch — from proven math to executed kernel — is covered by independent oracles that must agree before the hardware is believed. Each watches a different failure mode.

C.3.1 Finite-difference gradient checks

The script LeanMlir/Proofs/check_jacobians.py runs 30 finite-difference gradient checks. For each, it perturbs the input by \(\varepsilon \), compares the claimed VJP against the centered difference \((f(x + \varepsilon ) - f(x - \varepsilon )) / 2\varepsilon \), and asserts agreement within tolerance (typical max-error \(\sim 10^{-11}\) at \(\varepsilon = 10^{-5}\) in float64).

Every FD check is a belt-and-suspenders pass over a proved Jacobian theorem. The proofs already establish that each formula equals \(\operatorname {fderiv}\) at the relevant points; the FD checks confirm the formulas-as-written agree numerically with what the function actually does. Coverage spans every closed-form Jacobian we use downstream: \(\operatorname {pdiv}\_ \texttt{dense}\) and its weight/bias companions, \(\operatorname {pdiv}\_ \texttt{relu}\) (at smooth points), softmax cross-entropy, all four BN pieces (bnNormalize, bnCentered, bnIstdBroadcast, bnAffine), the conv2d and depthwise input/weight/bias VJPs, the maxPool2 input VJP, the softmax Jacobian, the three single-head SDPA Q/K/V backwards, GELU, the bundled multi-head SDPA reduction (per-head sdpa_back stacked over the head axis), the patch-embed input VJP, the full-network MLP composition, and bestiary spot-checks (bilinear upsample, channel concat, per-pixel softmax cross-entropy, U-Net skip plumbing).

What the FD pass catches that the symbolic proof can’t: typos between the proof and the prose that uses the same Jacobian. If a chapter narrates one formula but the Lean theorem states another, the proof still type-checks (Lean only verifies its own statement), but the FD test runs against the formula the prose published and would diverge.

FD is cheap, easy to reason about, and tight enough for spot-checking formulas, but it can’t probe what the compiled code actually computes on the GPU — only what the formula says in Python — and it struggles at non-smooth points where the limit definition breaks down. For those gaps and for end-to-end pipeline verification, the next oracle takes over.

C.3.2 The JAX parallel pipeline

A separate Lean \(\to \) JAX \(\to \) XLA pipeline (jax/Jax/Codegen.lean, \(\sim 1100\) lines) produces an idiomatic JAX training script from the same NetSpec the primary Lean \(\to \) StableHLO MLIR \(\to \) IREE pipeline consumes. XLA is the compiler JAX uses to produce GPU code (the same backend that powers TensorFlow and other frameworks); IREE is its Lean-side counterpart. The two stacks are independent end to end — different codegen, different runtime, different kernels — which is why agreement between them is a meaningful cross-check. Running both from identical initial parameters on identical batches gives us a pair of trace files, one per stack, that should agree modulo float32 rounding if both pipelines compute the same math.

The agreement is very tight. For the MNIST MLP, step-1 losses agree to \(\sim 2 \times 10^{-7}\) — float32 ULP — across the JAX-CPU-vs-IREE-ROCm comparison, and phase-3 IREE output is bit-identical across AMD and NVIDIA hardware at step 1. For the MNIST CNN with batch norm, step-1 agrees to \(\sim 10^{-4}\), looser because variance reductions over \(\sim 100\)k-element tensors amplify cross-compiler reduction-tree differences — both pipelines do correct math; they just sum it in different orders. Full results are committed to the repo as reproducible JSON-Lines traces; see traces/CROSS_BACKEND_RESULTS.md.

Layered on top of the end-to-end trace diff is a per-axiom differential test in tests/vjp_oracle/, which compares each Lean-proved backward pass against JAX’s value_and_grad autodiff on a minimal one-step training run. Nine cases — dense, dense+ReLU, conv, conv+BN, conv+maxPool, residual, depthwise, SE, attention — each agree with JAX autodiff at 1–2 ULP of step-2 loss. Any future hand-derived VJP added to the Lean proof base can be validated by a one-step comparison against JAX, catching algebraic errors that FD would miss (sign flips, wrong contraction axis, swapped indices).

C.3.3 The execution oracle and the margin probe

Two further watchers close the loop. The IREE-versus-NumPy oracle (§ C.2.1) regenerates every committed .mlir from the printer, compiles it for CPU and GPU, and diffs the result against an independent NumPy reference — the one check that reaches past the proofs to IREE’s lowering itself. And the margin probe (scripts/margin_probe.py) re-runs a real training trajectory in coupled f32/f64 and checks that the run stays inside the float theorems’ hypotheses — no flipped ReLU mask, no logit drift past \(\delta \) (§ C.4). It is what keeps the conditional theorems honest about actual training rather than hypothetical nets.

Each kind fails differently — a deductive proof is blind to a miscompile, an empirical diff is blind to a measure-zero kink, a faithful bridge is blind to a wrong formula it renders perfectly — and overlaying them is the guarantee. Verified code generation straddles two of the kinds: its bridge is structural, its oracle empirical. The float32 theorem layer, next, straddles the other pair: its budgets are deductive, its interface constants (\(u\), \(e_{\exp }\), \(\delta \)) empirical.

C.4 Float32: closeness, composition, and whether it still trains

Every theorem in this book is over exact reals; the GPU computes in binary32. Until recently that gap lived entirely in the empirical layer — the oracles agree to 1–2 ULP, and you were asked to find that persuasive. It is now a theorem layer, and it has two halves of different reach — keeping them apart is the honest part. The closeness half (\(|\, \text{float op} - \text{real op}\, | \le \) budget) is architecture-complete: FloatBridge.lean and the per-net *FloatBridge files budget every operator of every network, forward and backward, from the MNIST linear classifier to ViT-Tiny — and (the composition theorem below) these per-operator budgets fold into a depth-linear whole-network certificate that stays below the logit scale on all eight committed renders. The descent half (a rounded step provably decreases the loss) closes only for the shallow nets (SgdDescent{Linear,Mlp,Cnn,Cifar}.lean). The way the chain avoids new axioms is the part worth explaining.

The model is a hypothesis, not an axiom.

A FloatModel is any rounding operator \(\mathrm{rnd}\) with relative error \(u\): \(|\mathrm{rnd}(x) - x| \le u\, |x|\). Binary32 round-to-nearest satisfies this with \(u = 2^{-24}\) on the normal range (the subnormal range is characterized separately in FloatSubnormalBridge.lean — the normalized blocks provably stay normal, and the residual underflow floor is proven negligible, \(\le 2^{-86}\)); the exact-arithmetic model (\(\mathrm{rnd} = \mathrm{id}\), \(u = 0\)) shows the interface is inhabited and collapses every budget to zero. Nothing about IEEE-754 is postulated — the theorems are conditional on the standard model, the same way the ReLU theorems are conditional on being off the kink, and the axiom audit is untouched. Two further design choices are forced by the hardware: the dot-product budgets are stated in the classical compounded form valid for every summation association, because IREE tiles and reorders reductions freely (the price is a fan-in factor \(n\cdot u\); the tree-reduction bound below recovers \(\log _2 n\cdot u\) under a named balance hypothesis); and \(\exp \) enters as a hypothesis (\(|\widehat{\exp }(t) - e^t| \le e_{\exp }\, e^t\)) because GPU transcendentals have no IEEE specification — \(e_{\exp }\) is precisely the constant the VJP oracle (§ C.3.2) measures, so the deductive and empirical layers meet at a named interface instead of a hand-wave.

The chain.

Four links, each in the three-axiom audit. Forward: mlp_float_close_uniform budgets the rounded \(784{\to }512{\to }512{\to }10\) forward against the exact one, from coordinatewise magnitude bounds alone. Backward: mlp_{w2,w1,w0,b2,b1,b0}_step_float_close budget every rounded SGD parameter entry against \(\theta - \mathrm{lr}\cdot (a_i c_j)\) — entry for entry the emitWeightGrad quantities the render closes (§ C.2.1) prove equal to the \(\operatorname {pdiv}\)-Jacobian contractions, so the float step chains to the proven gradient. The loss head: softmax_ce_cot_close budgets the rounded softmax-minus-onehot cotangent against the certified \(\partial (\mathrm{crossEntropy})/\partial (\mathrm{logits})\). Descent: sgd_descends proves an \(\eta \)-accurate gradient step still decreases the loss, and linear_sgd_descends discharges its smoothness hypothesis with the explicit constant \(2a^2/(1-2aD)\) — no Hessian: the softmax ratio sandwich that powers the float budgets turns out to be the Lipschitz engine too. With the float budget fused in — the step’s \(\eta \) is the proven binary32 gradient accuracy, not an assumed parameter — this closes end-to-end for the linear classifier (linear_float_sgd_descends), the entire MLP (mlp_{output,hidden,input}_float_sgd_descends), and the entire Chapter-3 CNN, both conv weights and biases (cnn_conv{1,2}_float_sgd_descends). The \(\mathbb {R}\)-side argument reaches one layer further: cifar8_lastConv_sgd_descends is the first non-MNIST descent — CIFAR-8’s last conv, proved as an instance of the CNN lemma at its frozen earlier features — and that framing is exactly why it stops there. The admissible \(\mathrm{lr}\) is a product of per-layer operator-norm factors, so each added layer shrinks it geometrically; full-depth CIFAR and all five deep nets stay closeness-only, by design, not for want of effort.

The kink, quantitatively.

Over \(\mathbb {R}\), ReLU forced the hypotheses \(x_k \ne 0\). In float the same op inverts its role twice. The forward mask is exact — compare-and-select rounds nothing, so the op that causes all the \(\mathbb {R}\)-side conditions is the free op here. But the backward mask reads the rounded pre-activation, so the hypotheses return with a number in them: \(\mathit{ez} {\lt} |z_i|\) — the accumulated rounding error must not flip a sign (reluMask_close). A qualitative side condition became a checkable margin.

The naive whole-network bound is vacuous.

Budgeting each operator is one thing; combining those budgets into a bound on the whole network is another. The obvious way (FloatClose.comp) assumes every layer amplifies the error it inherits by that layer’s worst possible factor, then multiplies those factors down the depth. So the bound grows like \((\text{gain})^{\text{depth}}\) and blows up — \(2.7\cdot 10^{60}\) on MobileNetV2, \(\sim \! 10^{364}\) on ViT-Tiny — while the drift the GPU actually produces stays near \(10^{-5}\). Past a handful of layers, that bound says nothing at all.

The adjoint chain: add, don’t multiply.

The real error behaves differently. Each layer’s own rounding is amplified just once — by how much the rest of the network magnifies a small change made at that point — and those contributions add instead of multiplying. chain_adjointClose (AdjointChainBridge.lean) proves exactly this: the whole-network error is at most \(\sum _i H_i\, b_i\), where \(b_i\) is layer \(i\)’s fresh rounding budget (its per-operator bound, before anything is inherited) and \(H_i\) is its tail gain — how much a perturbation at layer \(i\) is stretched by all the layers after it. The proof is a single induction, exact (nothing is linearized), and because each \(b_i\) is amplified only once, the total grows roughly linearly with depth rather than exponentially. It can never lose to the naive bound: plug in worst-case tail gains and you recover the old bound exactly, so any honest estimate of \(H_i\) only helps. And an honest estimate is cheap — one backward pass reads the \(H_i\) off the network’s own trajectory. They enter the theorem as named hypotheses carrying their measured values, on the same footing as the \(\exp \) constant (§ C.3.2), never an axiom.

A certificate below the logit scale.

Two refinements make the bound small in practice. Cut the chain at every operator — each convolution, normalization, and dense its own link, with residual connections carried alongside (chain2_adjointClose) — and no worst-case products survive anywhere. And note that a sum of \(n\) terms costs a factor \((1{+}u)^{n}\) only if the hardware adds them in the worst order; IREE adds them in a balanced tree, which costs \((1{+}u)^{\lceil \log _2 n\rceil }\) instead (tree_close, TreeReduceBridge.lean) — a factor we name and check empirically rather than assume, and the one that finally tames the widest reductions (fan-in \(6272\), or \(n = 301056\) in ConvNeXt’s LayerNorm). The result is the first whole-network float certificate that means something on networks this deep: the bound lands below the logit scale on every committed render — MNIST-CNN \(0.015\), CIFAR-8 \(2.6\), MobileNetV2 \(0.30\), ResNet-34 \(0.17\), ViT-Tiny \(0.57\), EfficientNet-B0 \(0.10\), ConvNeXt-T \(0.80\), against logits of order one to five. And it is a statement about the decision, not just the numbers: cifar8_chain_argmaxSafe proves that whenever the exact network’s margin beats twice the budget, binary32 rounding cannot change which class it predicts.

Measured against proven.

The numeric capstones are instantiated at the trained magnitudes of a real 12-epoch, 97.8% GPU run (\(|W| \le 3/5\), covering the measured \(0.52\); He initialization already exceeds prettier bounds in its tails). An f32/f64 twin of that run (scripts/margin_probe.py, per-step coupled to match the single-step theorems) measures what the theorems bound:

The worst-case bounds hold with up to \(10^{8}\) to spare because worst-case composition compounds magnitude bounds the way no real activation pattern does — and that gap is exactly what the adjoint chain closes: its measured tail gains are the a-posteriori certificate past toy depth, now a theorem (chain_adjointClose) rather than an asserted argument. The whole-net budget was re-measured at the trained weights of five real checkpoints — ResNet-34, MobileNetV2, EfficientNet-B0, ViT-Tiny, ConvNeXt-T — and it holds on every one, with the telling twist that it tightens where training removes a pathological initialization (ViT’s zero-init class token, MobileNetV2’s He-init stem gain) and only loosens slightly on clean-init nets: the certificate is demonstrably a property of the deployed network, not an artifact of the initialization. And the flip count is zero across 29.5 million measured pre-activations: the margin hypotheses are not a technicality the proofs hide behind; they are what training actually looks like.