B On Verification

The proofs in this book compile with zero sorrys. Every VJP correctness theorem is machine-checked by Lean’s type system, and that covers dense layers, convolution, batch normalization, residual connections, depthwise convolution, squeeze-and-excitation, layer normalization, and self-attention. If it builds, the gradients are right. What the proofs do not say is that training converges, or how well: an optimizer handed the exact gradient can still diverge, plateau or overfit, and that is a theorem in no framework. Every accuracy in this book is a measurement, and the measurement is sharper for the proof: when a verified run matches its JAX reference, or misses it, a wrong gradient is not among the explanations.

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 printed text and the proven formula start from one term rather than from a comment. Cross-checked (empirical): what cannot be proven is watched by independent oracles that must agree before the hardware is believed, and that means the lowerer’s translation of the proven text into machine code, the GPU transcendentals, and finite-precision rounding beyond its theorem layer (§B.5). 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 1-1 follows each chapter network’s whole-network certificate back through everything it cites, chapter by chapter; Figure B-1 is the citation graph between the chapters themselves.

B.1 What each chapter proves

Table B-1 is the size of what each chapter proves about gradients, chapter by chapter. Its three columns are these. Each chapter proves a handful of VJP contracts, which are machine-checked theorems that a layer’s backward function computes the right gradient. Formally that means \(\texttt{backward}\, x\, dy\, i = \sum _j \operatorname {pdiv}f\, x\, i\, j \cdot dy_j\), so the backward equals that layer’s \(\operatorname {pdiv}\)-Jacobian contracted against the incoming cotangent, which the Foundations chapter builds up from scratch. A contract is that theorem with the weights of \(f\) left as variables, so it holds at every weight setting; there is one per function, where a function is a layer, an operator, a block, or a whole network at a stated depth (a network at two depths, or per example and at batch statistics, is two functions). A witness is the same theorem at one fixed set of weights: a hand-built tiny instance, a live-shaped one at \(224 \times 224\), or the weights a training run produced. It shows the contract’s hypotheses can be met, and is kept in its own column rather than counted as a contract. A step certificate is a theorem about the program rather than the math alone: that the train step the book emits denotes the certified gradient step (a fold for the small nets, a step tie at full width), that a hand-written backward chain is the VJP it was written to be, that a data-parallel render’s step is one device’s step on the global batch, that a gradient node is the loss’s derivative in its parameter, that an emitted optimizer update is its update law, or that one SGD step decreases the loss. A theorem that only restates a counted one at fixed dimensions or over the committed spec is not counted again. Across Chapters 1–9 there are 44 contracts, 9 witnesses and 45 step certificates. Even Chapter 1’s toolkit is used straight away by a proven model, so no chapter is pure scaffolding.

Every chapter’s theorems section opens with its own dependency graph, every box a Lean theorem and a link, and each chapter names its contracts as it proves them. The rest of this appendix is how those claims get checked: the audits, the bridge theorems, and the hardware oracles.

B.2 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.

B.2.1 The axiom audit

The Verified VJP Proofs suite proves the 44 VJP contracts and 9 witnesses of Table B-1, each asserting backward \(= \sum _j \operatorname {pdiv}f\, x\, i\, j \cdot dy_j\), with their restatements at fixed dimensions and over the committed specs; the 45 step certificates that tie the emitted programs to them, the optimizer updates among them; on top of the foundation \(\operatorname {pdiv}\) calculus and the differentiability/forward/witness machinery they rest on — and zero project axioms anywhere in it. (The bestiary’s 46 architecture families are NetSpec values the proofs do not touch; nothing there is a theorem.) That last figure is the one that matters, because it is the only one that cannot quietly grow. The axiom audit (tests/AuditAxioms.lean) prints the axiom closure of every headline declaration in the suite — the VJP contracts plus the forward-graph faithfulness, render, cotangent-chain, backward-tie, and finite-precision results (§B.5) — and every one closes under the same three core axioms: \(\texttt{\# print axioms vitFullHasVJP}\) shows only Lean core (propext, Classical.choice, Quot.sound), nothing project-level beneath those. That file is the live count. Nothing is axiomatized to get past an operator with a corner: ReLU, ReLU6 and max-pool are noncomputable defs over the canonical \(\operatorname {fderiv}\)-derived witness, and the smooth-point caveats in the chapters are the price.

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.

B.2.2 Independent kernel re-check (comparator)

tests/comparator/ wires the project up to leanprover/comparator (lake comparator, bundled with Lean since 4.35), the Lean community’s trustworthy-judge tool for projects that claim zero project axioms. It re-runs Lean’s kernel typechecker over each theorem’s statement and proof in a bwrap sandbox, independently of the elaborator, and verifies the transitive axiom closure statically against an allowlist of exactly \(\{ \texttt{propext}, \texttt{Quot.sound}, \texttt{Classical.choice}\} \). With –paranoid, the default in run.sh, five further checkers must accept every proof: leanchecker-paranoid, lean4lean, nanoda, con-leche and con-ron. Any project axiom in the closure of any listed theorem fails the run.

The 110 theorems split across three files, and the split is the point. Challenge.lean imports Mathlib and nothing else. It carries the 13 architecture-free theorems (Chapter 1’s pdiv calculus rules and Chapter 9’s matrix-level ones), with the handful of definitions they need copied inline, and chk_pdiv_is_fderiv pinning pdiv to Mathlib’s fderiv by rfl. A reviewer can read that one file and know what is claimed without reading a line of this project. Copying the definitions is safe here in a way copying an architecture would not be: comparator compares the challenge and solution statements bit-identically, so a copy that drifted would fail the run rather than quietly prove something weaker.

Thirty-nine more live in ChallengeArch.lean and do import the project, because each is a statement about a specific network, and “ResNet-34’s rendered backward equals its Fréchet derivative” cannot be phrased without ResNet-34 in scope: every chapter’s headline Jacobian, the public *HasVJP_correct wrappers, and three smooth-point pointwise variants (reluHasVJPAt_correct, mlpHasVJPAt_correct, maxPool2HasVJPAt3_correct) whose underlying .correct field is a real proof rather than rfl. Once the fderiv pin and the structural rules are checked over Mathlib alone, the architecture theorems are applications of them, and what you must additionally trust is the forward functions and nothing else.

The last 58 are ChallengeTier.lean, the layer this book’s second half rests on: the step ties, the codegen faithfulness results, the whole-net back-chains, the data-parallel results, the float bridge and the four certificate theorems. Their statements run to hundreds of lines apiece, so the file is printed from each declaration’s own type (scripts/gates/gen_comparator_tier.py) rather than transcribed, and the solution proves each one with the project theorem itself. With the four that ChallengeArch.lean already holds, these are exactly the declarations formalization.yaml puts forward, so the coverage is checkable by diffing two lists.

The 110 are not the whole proof suite: the axiom audit covers every headline declaration under the same allowlist. What the 110 add is a second, non-elaborator opinion, on every result formalization.yaml puts forward together with the calculus floor those rest on.

B.3 By construction: the code is the math

B.3.1 Verified code generation

The proofs above answer whether the mathematics is right, meaning 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 the lowerer 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, and this section describes the machinery they share.

Two pieces. The link from a proof to the GPU is built from two components, and what they leave open is the empirical layer’s (§B.4):

• Denoted IR and a bridge theorem. The emitted backward (and forward) is not a string but a Lean datatype, a small abstract syntax tree (SHlo, with Back its per-operator ancestor), 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, and each closes under the same three axioms as the rest of the project.

• A printer over the same term. The renderers (StableHLO.Pretty) print the very SHlo term whose denotation the tie theorems are about: SSA names are annotations the denotation ignores, and skel erases the real values, so the text depends on the graph’s shape and names alone, one stablehlo operation per node. The post-order token encoding the printer works from is proved invertible (StableHLOParse.roundtrip); how each token becomes a line of text (emitTok) is trusted, and checked by parsing every committed artifact as StableHLO (scripts/gates/parse_verified_mlir.py) and by the trainers executing them.

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

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

• Re-rendered, not proved: that the committed file is the printer’s current output. CI re-elaborates each renderer and git diffs its artifact; scripts/gates/check_render_coverage.py reports the ones it cannot, baselined in scripts/gates/render_guard_baseline.txt, and of the artifacts the “MLIR” sections quote, the CIFAR BatchNorm step is the one on that list, with the other CIFAR-8 train steps.

• Trusted (validated numerically, not proven): that the StableHLO text faithfully denotes \([\! [\cdot ]\! ]\), which is the per-token text above. Beyond it, three things are trusted: a formal StableHLO semantics, which does not yet exist, that the lowerer compiles the text correctly, and that the hardware’s rounding approximates \(\mathbb {R}\) within the modelled unit roundoff. The last of those is a conditional theorem validated on a measured run (§B.5) 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}\) — at a smooth point, at one replica, in f32 or bf16 — up to one printer, one lowerer, the StableHLO semantics the denotation assumes, 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 one printer’s per-token text, tested end to end, plus the hand-written lines each render declares in its own comments (the report-only %loss, for one, and ConvNeXt’s GAP-backward block).

Why it is tractable. A deep ResNet or a transformer block comes under this scheme as an engineering build rather than a research project because the VJP library is per-operator and generic: each operator is proved once over abstract dimensions, and the whole-network VJPs compose those lemmas through the chain rule. Code generation therefore carries no new proof obligation. Every architecture’s operators are proven once, the emitter reuses them, and what it adds is the printer and the numerical check.

From operators to whole training steps. The per-operator bridge is the demonstration, and the verified trainers run the full construction. Each reads a single committed .mlir holding 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, output by output, equal to the certified per-layer step: each parameter update is \(\theta - \mathrm{lr} \cdot (\text{that layer's certified Jacobian} \cdot \text{the chain cotangent})\). A companion tie theorem per network (mlp_train_step_tied_certified, r34_net_tiedB, vit_net_tied_certified and their peers) 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, so each update is one composed equation rooted at the proven forward rather than a quantifier over a free cotangent. All thirteen chapter networks are tied this way, from the MNIST linear classifier to depth-12 ViT-Tiny, and each deep net’s chain cotangent is pinned to its block’s certified VJP (r34IdCotIn_eq_vjp, vitBlockCotInB_eq_vjp and their peers). For each of the thirteen one more theorem composes the two halves: at the tie’s own cotangent, every parameter gradient node is \(\partial L/\partial \theta \) of the whole network, for any loss \(L\) with a gradient at the logits and in particular for the cross-entropy the artifacts emit, label-smoothed on the ImageNet nets (r34_net_lossGrad and its peers; one replica, either precision). 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 the bridge holds at every input, and those are BatchNorm and LayerNorm (given \(\varepsilon {\gt} 0\)), GELU, swish, sigmoid, softmax, and attention. The convolution bridges hold at every input too, with one hypothesis on the kernel rather than the data: \(k_H\) and \(k_W\) odd, which every kernel in Part 1 satisfies except ConvNeXt’s \(4\times 4\) stem and \(2\times 2\) downsamples, and those are tied through the kernel zero-extended to odd size (padOdd). For the operators with corners, which are ReLU, ReLU6 and max-pool, it holds only at a smooth point: no pre-activation exactly on the corner (zero for ReLU, \(0\) or \(6\) for ReLU6), and every \(2 \times 2\) pooling window’s maximum attained at one cell (MaxPool2Smooth). The equality is stated only off that set, where the pdiv-derived backward is \(\operatorname {fderiv}\)’s zero map and the emitted text is the framework convention. For ReLU the set is null for generic weights; for a pool on its own it is not, because an all-zero post-ReLU window attains its maximum at every cell, and the whole-net theorems carry the pooling clause as a hypothesis at the activations. The ResNets’ \(3 \times 3\)/s2 stem pool is certified together with the ReLU before it (stemReluPoolLayer), which admits the all-zero windows too, and the windows it still excludes, a positive maximum at two cells, are the twins Chapter 5 handles beside Theorem 69. That set is the boundary the smooth-point caveats in the chapter sections refer to.

B.3.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, in its per-operator form. 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 (Back; the whole-step graphs are SHlo, the same idea with every operation a train step needs):

inductive Back (inp : Nat) : Nat -> Type where
  | cotangent  : Back inp inp            -- the input dy
  | dotGeneral {m n : Nat} (A : Mat m n) : Back inp n -> Back inp m   -- matmul
  | selectPos {n : Nat} (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, which feeds 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, saying what the graph means mathematically:

and likewise for the remaining constructors (scale, sub, sumBroadcast, scaleConst and 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 pdiv-derived backward, but only under the hypothesis \(h_{\text{smooth}}\) that no coordinate sits on the corner. That hypothesis is not a technicality. At a point with a zero coordinate ReLU has no derivative, \(\operatorname {fderiv}\) returns the zero map, and the pdiv-derived backward is the zero vector in every coordinate, while the emitted compare GT 0 still passes \(dy_i\) wherever \(x_i {\gt} 0\); the theorem is stated exactly where the two agree, 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, and conv_back_bridge shows it equals the certified input gradient at every shape by reindexing the sum, a bijection exactly when the kernel is odd.

Composing the per-operator bridges. Whole-network backwards are assembled by substitution. The function 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 vjpComp 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 four of these substitutions, closed by unfolding and rfl.

Why the datatype is the point. The graph value is the pivot between two arrows. A printer walks it with names in place of its values, one stablehlo operation per node (dotGeneral \(\mapsto \) stablehlo.dot_general, and selectPos \(\mapsto \) compare GT 0 plus select), and that arrow is the trusted one; for the whole-step graphs the printer is StableHLO.Pretty over SHlo, and the chapter listings are its committed renders at batch width. The denotation interprets the same value into the proofs’ Vec type, and the bridge proves the result equals the derivative, so 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.

B.4 Cross-checked

Neither lowerer can itself be proven, and GPU transcendentals have no IEEE specification, so 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, and the first thing to know about any of them is which Lean text it runs, because two generators produce StableHLO in this project. StableHLO.Pretty prints the committed verified_mlir/ artifacts the trainers load and the theorems are about. MlirCodegen is the reference path, which lowers a NetSpec to MLIR at run time, hand-written and unverified. Table B-2 is the roster; the verified-path oracle is the row that runs the proven text, and the two MlirCodegen rows check the reference path against autodiff.

The property that makes the middle rows work is that the two sides do not share a compiler. The Lean side of those oracles lowers through IREE, and the reference pipeline is JAX, which lowers through XLA. Different code generation, different runtime, different kernels, and different authors. Agreement between them is evidence precisely because a bug would have to occur twice, in the same direction, in two unrelated compilers; that is what the second lowerer is for (Appendix A, The second lowerer).

B.4.1 Finite-difference gradient checks

The script LeanMlir/Proofs/check_jacobians.py runs 30 finite-difference gradient checks (its 31st is the identity rule, which needs none). 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, and 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, and the softmax Jacobian. It also covers 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 checks is the formula as transcribed into NumPy: that the closed form a theorem states is in fact the derivative of the forward it is claimed for. It reads neither the prose nor the Lean statement, so a chapter that narrates a different formula than its theorem states is caught by neither tool; Lean verifies its own statement, and the transcription is by hand.

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.

B.4.2 Against JAX

The judge for the next three rows is a second trainer. A Lean \(\to \) JAX generator (jax/Jax/Codegen.lean) produces an idiomatic JAX training script from the same NetSpec the reference Lean \(\to \) StableHLO pipeline consumes; JAX differentiates it with value_and_grad and XLA compiles it. It is the reference every ImageNet pair in Chapters 5–9 trains against, and in these rows the Lean side is lowered through IREE so that the two stacks share nothing.

The verified-path oracle is the one row that runs the proven text. tests/vjp_oracle/run_verified.sh takes one SGD step of the committed linear, mlp and cnn train steps — the artifacts Theorems 23, 30 and 41 are about — through the book’s own trainers on IREE llvm-cpu, against one step of the same nets in JAX from the same initial weights on the same batch, compared parameter update by parameter update at a tolerance of \(10^{-4}\). The measured worst relative difference over every tensor is \(1.3\times 10^{-6}\) for the linear and MLP steps and \(7.4\times 10^{-6}\) for the CNN’s, float32 reduction-order noise. The deep nets are not in it, and need not be: their proofs, bridge theorems and rounding budgets are statements about the graph rather than about any compiler, and both lowerers consume the same StableHLO text.

The two reference-path rows check the hand-written backward of MlirCodegen against autodiff, not the proven text. The per-operator oracle (tests/vjp_oracle/, in CI) runs fourteen one-step cases — dense, dense+ReLU, conv, conv+BN, conv+max-pool, residual, depthwise, global average pool, attention, and the SE-gated MBConv, bottleneck, MBConv-V3, fused-MBConv and UIB blocks — and each agrees with JAX on the step-2 loss to between \(2 \times 10^{-7}\) and \(10^{-4}\), the wider ones where a max-pool’s argmax tie-breaks on MNIST’s zero pixels or a BatchNorm variance’s reduction order differs between the compilers. The cross-backend traces (historical/traces/) run the MNIST MLP and CNN on IREE over ROCm and CUDA against JAX on CPU and CUDA: step-1 losses agree to float32 ULP and IREE’s own output is bit-identical across AMD and NVIDIA; step 2, the first loss through a backward, agrees to about \(10^{-4}\), and the CNN’s \(7 \times 10^{-3}\) against JAX on CPU is the reduction order of a variance over \(\sim 100\)k elements, since JAX on CPU and JAX on CUDA disagree with each other by the same amount at that step. The traces are committed as JSON-Lines, with historical/traces/CROSS_BACKEND_RESULTS.md the summary.

One fault in the CPU target is worth keeping in view. IREE 3.11’s llvm-cpu miscompiles the select_and_scatter of the batched CIFAR-8 train steps. The CPU gradient gate for those nets runs on IREE’s vmvx backend instead (tests/TestCifar8BbnGradCheck.lean), and an llvm-cpu mismatch on a pooled net means check the lowerer before the render. The GPU runs use XLA and are unaffected.

Each kind fails differently, and overlaying them is the guarantee. A deductive proof is blind to a miscompile, an empirical diff is blind to a corner it never samples, and a faithful bridge is blind to a wrong formula it renders perfectly. Verified code generation straddles two of the kinds: its bridge is structural, its printer’s text checked empirically. The finite-precision theorem layer, next, straddles the other pair: its budgets are deductive, its interface constants (\(u\), \(e_{\exp }\), \(\delta \)) empirical.

B.5 Finite precision

Every theorem in this book is over exact reals, and the GPU computes in finite precision. The empirical layer closes that gap to float32 precision, where the oracles agree. A theorem layer closes part of it exactly, and it has two halves of different reach; keeping them apart matters, as does keeping the layer’s generality apart from its usefulness (§??). The closeness half (\(|\, \text{float op} - \text{real op}\, | \le \) budget) is per-operator: the files under LeanMlir/Proofs/Float/ budget dense, ReLU and its mask, convolution and depthwise convolution (plain and mixed-precision), max-pool, global average pool, the residual sum, BatchNorm, and the softmax cross-entropy head. GELU, LayerNorm, swish, sigmoid, squeeze-and-excitation and attention have no float budget, so the EfficientNet, ConvNeXt and ViT chapters are covered only through the operators they share with the rest. The descent half (a rounded step provably decreases the loss) closes only for the shallow nets (LeanMlir/Proofs/Training/SgdDescent/, one file each for the linear net, the MLP and its biases, the CNN over \(\mathbb {R}\) and in float, and CIFAR). The way the chain avoids new axioms is the part worth explaining.

The model is a hypothesis.

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; in the subnormal range the rounding error is absolute, not relative, and the model does not cover it. 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, and the theorems are conditional on the standard model, the same way the ReLU theorems are conditional on being off the corner, and the axiom audit is untouched. Two further design choices are forced by the hardware. The dot-product budgets are proved for the left-fold association: the classical compounded bound holds for every summation order, and only that fold is formalized, so a backend that reassociates a reduction, as IREE does when it tiles, is outside the statement as proved. The price either way is a fan-in factor \(n\cdot u\). 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 a named constant: the numeric instances below assume \(e_{\exp } \le 10^{-6}\), and nothing in the repository measures it, so the deductive and empirical layers meet at a named interface rather than a hand-wave, with that one constant still owed to a measurement.

How far the model reaches, and where it stops being useful.

Because \(u\) is a parameter, nothing in the chain is float32-specific. Binary32Instance.lean constructs the rounding operator as round-to-nearest on the grid with \(p\) fraction bits, a \((p+1)\)-bit significand, and instantiates it twice: binary32 at \(p = 23\), \(u_{32} = 2^{-24}\), and fp8E4M3 at \(p = 3\), \(u_{\mathrm{e4m3}} = 2^{-4}\). Every bridge quantifies over (M : FloatModel) — the per-operator lemmas, the residual-block chain, the MNIST descent chain — so none of them is a statement about binary32 that happens to be proved; each is a statement about any rounding model, of which binary32 is one instance.

That generality is free. Usefulness is not, and the two should not be confused. The dot-product budget carries the classical fan-in factor \((1+u)^{n+1} - 1\), which goes vacuous once \(n\, u\) approaches 1 — a wall at \(n \approx 1/u\). At \(u_{32}\) that wall sits near \(1.7 \times 10^{7}\) and no layer in this book comes close. At pure bf16 (\(u = 2^{-8}\)) it sits at \(n \approx 256\), and ResNet-34’s \(3\times 3\) convolution at 512 channels has fan-in 4608. The budget is still true there. It is also worthless there.

Which is why the low-precision result is stated mixed rather than pure. dotMixed rounds the operands through a leaf model \(L\) (bf16 \(2^{-8}\), or fp8-E4M3 \(2^{-4}\)) and accumulates through \(M\) at \(u_{\mathrm{acc}}\), which is the shape the hardware actually runs: low-precision inputs, fp32 accumulator. dot_close_mixed then splits the error in two, and the split is the whole point — the leaf precision contributes a flat \((2u_{\mathrm{leaf}} + u_{\mathrm{leaf}}^2)\sum |x_i y_i|\) term that is not fan-in amplified, while the amplification rides entirely on \(u_{\mathrm{acc}}\). The wall stays at \(1/u_{\mathrm{acc}}\) no matter how coarse the leaf is. That is exactly why bf16-mixed is non-vacuous where pure bf16 is not, and it is carried to convolution and depthwise convolution in ConvMixedFloatBridge.lean, DepthwiseMixedFloatBridge.lean and ConvMixedComposeBridge.lean. The emitted bf16 graphs are tied at their gradient nodes in Bf16GradNodes.lean, and at the identity rounding the renderers instantiate each bf16 kind denotes its f32 peer (Bf16Erasure.lean), which is how every whole-network step tie is stated at either precision; Bf16Fold.lean (bf16_render_faithful, its emittable form bf16_render_faithful_emit, and bf16_render_faithful_depth2 at two layers) and E4M3Fold.lean prove, for the linear net, that the mixed-precision graph denotes the intended algorithm. The fp8 one is proved for a graph no backend here lowers, and the one committed fp8 artifact, cifar8b_fp8_adam_train_step.mlir, is a lowering probe with no fold of its own.

In three sentences, then. The theorems are over \(\mathbb {R}\). The budgets are over an arbitrary rounding model, so binary32, bf16-mixed and fp8-E4M3 are instances rather than separate theories. And the numbers those budgets produce are worth having at fp32 accumulate, worth having at a low-precision leaf over an fp32 accumulator, and not worth having at pure low precision — which is a fact about the arithmetic, not a gap in the proofs.

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, and the emitWeightGrad quantities the render closes (§B.3.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)\), with no Hessian, because the softmax ratio sandwich that powers the float budgets turns out to be the Lipschitz engine too. With the float budget fused in, so that the step’s \(\eta \) is the proven binary32 gradient accuracy rather than an assumed parameter, this closes for the linear classifier (linear_float_sgd_descends); for each of the MLP’s three weight matrices with the rest of the net held fixed (mlp_{output,hidden,input}_float_sgd_descends; the MLP’s biases descend over \(\mathbb {R}\) only, in MlpBias.lean); and for the Chapter-3 CNN’s two convolutions, weights and biases (cnn_conv{1,2}_float_sgd_descends, cnn_conv{1,2}_bias_float_sgd_descends; its dense head has no float descent). Each statement moves one parameter group. What is rounded in those statements is the gradient and nothing else: each is one example, the update \(\theta - \alpha \, \tilde g\) is taken in \(\mathbb {R}\), the loss it decreases is the real one, and the \(\exp \) inside the softmax enters through an accuracy hypothesis that the trained-weight instance (trained_linear_sgd_descends_concrete) discharges at the exact \(\exp \). The \(\mathbb {R}\)-side argument reaches one layer further: cifar8_lastConv_sgd_descends is the first non-MNIST descent. It is 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.

The corner.

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, since 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|\), meaning the accumulated rounding error must not flip a sign (reluMask_close). A qualitative side condition became a checkable margin.

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\), and He initialization already exceeds prettier bounds in its tails). An f32/f64 twin of that run (scripts/certs/margin_probe.py: a NumPy re-implementation from the same seed, coupled per step to match the single-step theorems) measures what the theorems bound. Table B-3 is the two side by side.

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 the flip count is zero across 29.5 million measured pre-activations in each of the two hidden layers. The margin hypotheses are not a technicality the proofs hide behind. They are what training actually looks like.