⭐⭐ r34InputGradB IS the certified whole-net ResNet-34 gradient AT BATCH BATCH-NORM #
The per-example net's tie (retired 2026-09-19 with ResNet34RenderPC.lean; ResNet34BackCertifiedTie.lean
keeps its leaf ties) closed this for the forward the retired ResNet34Render.lean emitted. This file closes it
for the net the shipped trainers run: resnet34ForwardB_full, the [3,4,6,3] ladder at
bnBatchLA, at a variable batch N. It is tier T6 of
planning/archive/proofs_tier_to_paper_nets.md §4.2, the last real statement in that section's port
(T4/T5 there are float budgets, and planning/archive/float_budget_numbers.md closed that thread).
Nothing here is new mathematics. Two endpoint stage ties (stem and head) and one pool tie, then
the sixteen basic blocks stay opaque — they enter as the _at VJP witnesses 4.1d's apex
already takes, and the reverse chain's block slots are pinned to their .backward — so the
composition is checked between variables. ⚠ It still costs ~60 s, an order more than the
other four nets' ties: the rfl is against a seventeen-deep let chain of vjp_comp_diff_ats
whose PProd projections do not share.
The four pieces #
cbReluStridedBBack_eq_vjp_backward/r34HeadBBack_eq_vjp_backward— the concrete endpoints; the stem is the first and the pool needs no lemma. ⭐ The pool endpoint isrfl, and that is the payoff of two earlier decisions: 4.1c builtbatchMap_has_vjp_atfield by field rather than transporting it with▸, andmaxPool3s2Flat_has_vjp_at_vecdid the same one tier down, sobatchMapAuxof the leaf and the lift's.backwardare the same term. It also closes the one seam §4.2a left open — that file could thread the pool backward only as the emittedden.r34B_full_has_vjp_at— the generic eighteen-stage apexhead ∘ b16 ∘ … ∘ b1 ∘ stem, seventeenvjp_comp_diff_ats and nothing else, overopaqueA0 … A16, one prefixdefper running activation.r34InputGradB_eq_r34B_full_vjpandr34InputGradB_correct— the tie, and its reading as∑ pdiv … * dy: the chain IS the Jacobian-transpose of the eighteen-stage composition.resnet34ForwardB_full_eq_slots— the shape check: those eighteen stages AREresnet34ForwardB_full, the forwardresnet34FwdGraphB_full_faithful(4.1b) says the typed graph denotes. Without it the tie would be a statement about variables.
⛔ Two walls, both measured, both worth not re-paying #
A rfl straight at 4.1d's resnet34ForwardB_full_has_vjp_at does not terminate — five
minutes to (deterministic) timeout at isDefEq at four million heartbeats. That is §5's
elaboration trap and the reason the generic apex exists.
⛔ And so does instantiating the generic tie at the sixteen concrete blocks — a kernel
deterministic timeout at six minutes, with HasVJPAt.backward_unique or without it. So this
file stops where MobileNetV2's per-example T6 stops (opaque blocks plus a shape check) rather
than where B0's goes (concrete blocks, then backward_unique). ⭐ The difference is not depth
and not the net: it is the KINK. B0's generic tie takes GLOBAL HasVJP witnesses, which carry
no point, so instantiating them is free. r34's are HasVJPAt at opaqueA{k-1} … x, and the
witnesses a caller has are at r34Pre{k-1} N w x — sixteen defeq checks between two
sixteen-deep nested applications spelled through different definition chains.
⚠ It stays a SMOOTH-POINT statement, and r34 carries the heaviest hypothesis budget of the five nets: two relu clauses per block (the body's mid-relu and the post-residual OUTER relu), the stem's relu, and the stem pool's per-example no-tie condition. That is 4.1d's bundle list, reused verbatim — this file adds no hypothesis of its own.
⛔ What this does NOT reach. One device: the data-parallel step, collectives included, is
ResNet34SyncStepTieB.lean's. And it is about the INPUT gradient; the parameter gradients are
ResNet34StepTieB.lean's tie (§4.2a).
The conv-BN-relu STAGE tie. The hand-written
batchMap (flatConvStride2Back) ∘ bnBack ∘ reluMaskBack IS cbReluStridedB's certified
backward at a smooth point. One rw of the odd-kernel strided leaf tie, then rfl — the
stage's VJP is vjp_comp_at-built so its backward is already the composition, and the conv
leaf's backward is input-independent (a convolution is linear), so the row-wise batchMap
lift matches at every saved input.
⚠ SYMMETRIC padding (flatConvStride2Back), not the XLA-SAME phase B0's and MobileNetV2's
stems take. Identical types, different certificates.
The HEAD CONV tie. batchMap (convFlatBack) ∘ bnBack ∘ reluMaskBack IS cbReluB's
certified backward at a smooth point — the stride-1, plain-convolution peer of the stem's.
⭐ The kernel extent is a binder, so a 1×1 conv-BN-relu is one instance of this stage and not
a new one: MobileNetV4's two head convs (%h1W 256 → 960, %hW 960 → 1280) tie by applying
this twice, and its head is therefore not hypothesis-free the way ResNet-34's is.
The HEAD tie. batchMap (gapBack) ∘ batchMap (dense Wᵀ 0) IS r34HeadB's certified
backward. ⭐ The head takes no hypothesis at all: GAP and dense are smooth and each is
batchMap of a per-example op, so r34HeadB_has_vjp is GLOBAL — the one place in this net
where the certified backward comes with nothing attached. gapBack needs no rewrite; it is
definitionally the global-average-pool VJP's backward.
Whole-network batched ResNet-34 VJP, every stage opaque. head ∘ b16 ∘ … ∘ b1 ∘ stem,
seventeen vjp_comp_diff_ats and nothing else. ⭐ ResNet-34's [3,4,6,3] ladder needs no
ChainData list and no separate downsample slot: a downsample block is just a block of a
different type, and the stem's pool lives INSIDE stem. Dimension-generic and parametric in
every component, so the tie below is checked between variables.
⚠ Pointwise (HasVJPAt), as every ResNet-34 statement is: relu is kinked, and this net has
two relu sites per block.
Equations
- One or more equations did not get rendered due to their size.
Instances For
⭐⭐ r34InputGradB IS the certified whole-net batch-BN ResNet-34 gradient. The committed
backward chain, with its stem BatchNorm and relu-mask slots filled by the certified per-op
backwards, its saved pool activation the stem's own, and its sixteen basic blocks left OPAQUE,
equals the backward of r34B_full_has_vjp_at at those eighteen stages. unfold, two rws,
rfl — the blocks are variables on both sides, so the kernel never looks inside one.
⭐⭐ The batched chain IS the pdiv-contracted Jacobian of the eighteen-stage net — at
every batch size, every input, every loss cotangent and every input pixel. The tie above read
through the apex's own .correct. resnet34ForwardB_full_eq_slots below is what says those
eighteen stages are the committed forward, so the two together are the T6 statement.
⭐⭐ THE SHAPE CHECK — the eighteen slots the tie is about ARE the committed forward.
resnet34ForwardB_full, regrouped into exactly the eighteen arguments r34B_full_has_vjp_at
takes: the stem (7×7/s2 conv-BN-relu and He et al.'s 3×3/s2 pool), the [3,4,6,3] ladder as
sixteen basic blocks, and the GAP+dense head.
⛔ This is the theorem that would have caught ResNet-34's wrong pool. The tie keeps its blocks OPAQUE — they enter as the VJP witnesses, so its subject is a chain of VARIABLES and nothing in it says which net they are. §3.10's drift (the 2×2 pool's backward against a forward that pools 3×3/s2) lived a month for exactly that reason: "the same net as the tie" was prose in a docstring. Here the pool appears on both sides of one statement the kernel checks.
It goes through resnet34ForwardB_full_eq_chain (4.1d) for the depth-16 half and then unfolds
the named prefixes; the MobileNetV2 peer is mobilenetv2ForwardPaper_eq_slots.