§B: the r34 identity-block backward chain IS the certified VJP #
r34IdBlockBack (ResNetBackChains.lean) is the hand-composed reverse of the r34 identity
block, written in the per-op backward maps of BackwardMaps.lean. This file closes the §B
integrity question for that block: the chain IS the certified input-gradient VJP.
The key design choice that makes this b1-free (no batched↔non-batched batchMap
reconciliation): r34IdBlockBack is the reverse of rblkPC — the
per-channel-BN, non-batched identity block (ResNet34RenderPC). So the right
certified target is a VJP of rblkPC in the same vocabulary, NOT the batched true-BN
r34BasicBlockB_has_vjp_at (ResNet34BackB0). That certified object did not exist, so we
build it here (rblkPC_has_vjp_at), then tie.
Three pieces:
convFlatBack_eq_vjp_backward— the conv leaf tie: the backward mapconvFlatBack(reversed-kernel conv) IS the certified conv input-VJP, via the general odd-kernelIR.convBackDenote_eq_input_grad_formula.rblkPC_has_vjp_at— the certified per-channel-BN identity-block VJP, assembled from the per-op VJPs (convBnReluPC_has_vjp_at+bnPerChannelTensor3_has_vjp+residual_has_vjp_at), mirroring the scalar-BNresblock_has_vjp_at.r34IdBlockBack_eq_rblkPC_vjp— the tie:r34IdBlockBackwith its abstract BN-backs pinned to the certified per-channel-BN backwards and its ReLU masks pinned to the actual pre-activation signs equals(rblkPC_has_vjp_at …).backward. Closes by rewriting the two conv leaves; everything else (residual fan-in, the∘-reversal, the relu masks, the pinned BN-backs) matches definitionally.
What the tie buys: the hand-composed chain — the spelling a reader can check against the emitted backward — IS the certified gradient, not merely a map that looks like one.
The downsample block is closed the same way (§ The DOWNSAMPLE block below): a strided-conv
leaf tie (flatConvStride2Back_eq_vjp_backward = conv leaf + the decimateBack rfl), the
certified strided block VJP rblkPStridedPC_has_vjp_at (mirrors resblockProj_has_vjp_at, with the
residualProj two-branch fan-in), and the tie r34DownBlockBack_eq_rblkPStridedPC_vjp. So both r34
block types (identity + downsample) now target the certified gradient, b1-free.
The endpoint leaf ties (§ The ENDPOINT leaf ties below) close the rest of the per-op set:
dense_transpose_eq_vjp_backward (the dense head, Wᵀ·dy = certified Mat.mulVec W),
gapBack_eq_vjp_backward (GAP broadcast-÷, rfl), maxPoolFlatBack_eq_vjp_backward (the smooth-point
arg-max scatter). With these + the conv/strided-conv leaves above, every per-op backward of the r34
whole-net r34InputGrad is now individually tied to its certified VJP.
⭐⭐ THE WHOLE-NET FOLD IS CLOSED (2026-09-03): r34InputGrad_eq_resnet34_vjp. The last
section of this file assembles the per-op ties into r34InputGrad = (resnet34_has_vjp_at … ).backward at the full 3×224² dims — so the claim is no longer "every piece of the chain is
the certified gradient" but "the chain IS the certified whole-net gradient".
⛔ The blocker recorded here previously — "resnet34_has_vjp_at is parametric / only concretely
instantiated at toy resnet34Concrete dims" — was a misreading. That theorem is dimension-
generic and parametric in its component maps, so instantiating it at ImageNet dims needs no new
apex: it needs the components' HasVJPAt/DifferentiableAt witnesses, and every one already
existed except the stem's (cbrStridedPC_has_vjp_at, added below — the strided peer of
convBnReluPC_has_vjp_at). ⭐ The blocks stay OPAQUE, entering as the ChainData/PProd bundles
resnet34_has_vjp_at already takes, so the whole-net isDefEq runs between variables.
⛔⛔ What the tie actually found was a DRIFT, and it moved the r34 backward number.
r34InputGrad pooled with maxPoolFlatBack — the 2×2 pool's backward — while the committed
forward resnet34Forward_full_pc pools with maxPool3s2Flat, He et al.'s 3×3/s2 stem pool.
MaxPool3s2.lean's header warns the two share a TYPE and are different functions; nothing forced
the two statements to unify until a theorem needed them to be about ONE net. The missing leaf is
maxPool3s2FlatBack (BackwardMaps.lean — the ACCUMULATING scatter: 3×3/s2 windows overlap, so an input
can be the argmax of up to four outputs, window 4A not A), and the whole-net number then
stated on this chain moved 4× (that budget was deleted 2026-09-08). ⚠ This is imagenet_specs_drift_from_twins for the fourth time and
ConvNeXt's stale head-LayerNorm slot for the second: "the same net as the tie" is an unchecked
claim until something forces the two statements to unify, and what forces it is needing the tie.
⚠ Still supplied, and unchanged by this: the SMOOTHNESS side. The tie takes the pool's
MaxPool3s2Smooth, the stem's post-BN no-zero, and the per-block ChainData bundles as
hypotheses — a smooth-point statement, as every HasVJPAt in this cone is.
Conv input-VJP leaf tie. The backward map convFlatBack W (= reversed-kernel forward
conv) IS the certified conv input-VJP (flatConv_has_vjp W b).backward x (conv is linear,
so the saved activation x is ignored), for odd kernels. Routes through the general
IR.convBackDenote_eq_input_grad_formula; the leaf the §B block tie reuses (×2).
Certified VJP of the per-channel-BN identity basic block rblkPC (non-batched).
relu ∘ residual(F) with F = (bnPC₂∘conv₂) ∘ (relu∘bnPC₁∘conv₁). The same-vocabulary
certified target for r34IdBlockBack — no batched/batchMap
reconciliation. Mirrors resblock_has_vjp_at (scalar BN) with bnPerChannelTensor3 for
bnForward, reusing convBnReluPC_has_vjp_at for stage 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The §B identity-block tie: hand-composed backward = certified VJP. r34IdBlockBack,
with its abstract BN-backs pinned to the certified per-channel-BN backwards
(bnPerChannelTensor3_has_vjp.backward at the respective conv outputs) and its ReLU masks
pinned to the actual pre-activation signs, equals (rblkPC_has_vjp_at …).backward.
Both sides are fun dy ↦ bodyBack(mask dy) + mask dy (residual fan-in over the outer-relu
mask). The bodies match because: the two conv leaves tie via convFlatBack_eq_vjp_backward
(3×3 is odd), the BN-backs are pinned to the exact certified terms, and the inner ReLU mask
is the mid pre-activation sign — so after rewriting the conv leaves everything is
definitional. Closes under [propext, Classical.choice, Quot.sound].
Strided conv input-VJP leaf tie. flatConvStride2Back W (= convFlatBack ∘ decimateBack)
IS the certified strided conv input-VJP (flatConvStride2_has_vjp W b).backward x, for odd
kernels. Decomposes into the conv leaf tie (convFlatBack_eq_vjp_backward) and the decimate
leaf (decimateBack_eq_vjp, rfl), matching flatConvStride2 = decimateFlat ∘ flatConv.
XLA-SAME strided conv input-VJP leaf tie. flatConvStride2XlaBack W
(= convFlatBack ∘ decimateOddBack) IS the certified (flatConvStride2Xla_has_vjp W b).backward x,
for odd kernels: the conv leaf tie and the odd-scatter leaf (decimateOddBack_eq_vjp, rfl),
matching flatConvStride2Xla = decimateOddFlat ∘ flatConv. The TF-origin stems' (B0,
MobileNetV2) leaf. ⚠ This is the theorem that fixes the odd-phase backward's DIRECTION: the
emitted transposed-conv pad [p+1, p-1] (opposite to the weight grads' [p-1, p+1]) denotes
this map through depthwiseStridedXlaBack_faithful's conv peer, so a backward derived "by
symmetry" with the weight grads cannot be tied here.
Certified VJP of the per-channel-BN downsample block rblkPStridedPC (non-batched).
relu ∘ residualProj(proj, F_s) — proj = bnPC∘convStride2(Wp) (the kHp×kWp-stride-2 skip),
F_s = (bnPC₂∘conv₂) ∘ (relu∘bnPC₁∘convStride2(W₁)) (first conv strided). The same-vocabulary
certified target for r34DownBlockBack. Mirrors the scalar-BN resblockProj_has_vjp_at with
bnPerChannelTensor3 + flatConvStride2; per-op VJPs assembled by vjp_comp_at.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The §B downsample-block tie: hand-composed backward = certified VJP. r34DownBlockBack,
with BN-backs pinned to the certified per-channel backwards and ReLU masks pinned to the pre-
activation signs, equals (rblkPStridedPC_has_vjp_at …).backward. Both sides are
fun dy ↦ projBack(mask dy) + bodyBack(mask dy) (the residualProj two-branch fan-in over the
outer-relu mask). Closes by rewriting the two strided-conv leaves
(flatConvStride2Back_eq_vjp_backward) and the one non-strided conv leaf
(convFlatBack_eq_vjp_backward); the rest is definitional. Completes the r34 block set
(identity + downsample). 3-axiom-clean.
Dense head input-VJP leaf tie. The chain's dense backward dense (Wᵀ) 0 (= Wᵀ·dy)
IS the certified dense input-VJP (dense_has_vjp W b).backward x (= Mat.mulVec W dy), conv is
linear so the activation x is ignored. One mul_comm per term.
GAP input-VJP leaf tie. The backward map gapBack c h w (broadcast dy(channel)/(h·w))
IS the certified GAP input-VJP (globalAvgPoolFlat_has_vjp c h w).backward x — definitionally
the same broadcast-÷ map (the VJP ignores its primal argument).
Maxpool input-VJP leaf tie (smooth point). The backward map maxPoolFlatBack x (scatter
dy to the arg-max cell, 0 elsewhere) IS the certified maxpool input-VJP
(maxPoolFlat_has_vjp_at x h_smooth).backward at a smooth point (unique arg-max per window).
Both denote if MaxPool2IsArgmax then dy(winRow,winCol) else 0 (IR.maxPoolBackDenote =
maxPool2_has_vjp_at3.backward).
conv(stride-2) → per-channel-BN → relu VJP at a smooth point — the strided peer of
convBnReluPC_has_vjp_at, i.e. the certified VJP of cbrStridedPC, which is r34's stem. Two
vjp_comp_ats: the strided conv, the per-channel BN (differentiable everywhere at ε > 0),
then the ReLU at its smooth point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
cbrStridedPC is differentiable at a smooth point (the companion resnet34_has_vjp_at
threads alongside every HasVJPAt).
The stem tie. r34InputGrad's stem slot — flatConvStride2Back Ws ∘ bnB ∘ reluMaskBack,
with the BN-back pinned to the certified per-channel backward and the mask to the actual
post-BN sign — IS (cbrStridedPC_has_vjp_at …).backward. Closes by rewriting the one strided
conv leaf; the BN-back and the ReLU mask are definitionally the certified terms
(relu_has_vjp_at's backward is fun dy i => if x i > 0 then dy i else 0, which is
reluMaskBack (· > 0)).
The whole-net certified tie. r34InputGrad, with every one of its slots pinned to the
certified per-op backward, IS (resnet34_has_vjp_at …).backward — the certified
input-gradient VJP of dense ∘ GAP ∘ [3,4,6,3] ∘ maxPool3s2 ∘ stem at x.
⭐ This is the statement the per-op ties above could not make: with it the chain IS the certified whole-net gradient, where before it only every piece of it was. (The whole-net float budget once stated on this chain was deleted 2026-09-08 as vacuous; the tie stays.)
⛔⛔ And closing it is what found the drift. r34InputGrad used maxPoolFlatBack — the
2×2 pool's backward — while the committed forward resnet34Forward_full_pc pools with
maxPool3s2Flat, He et al.'s 3×3/s2 stem pool. MaxPool3s2.lean warns that the two share a
TYPE and are different functions; nothing forced them to unify until this theorem needed the
two statements to be about one net. The fix is maxPool3s2FlatBack (BackwardMaps.lean, the
accumulating scatter, window 4A not A), and the r34 backward number moved
2.188·10²⁴⁵ → 8.857·10²⁴⁵.
⭐ The blocks stay OPAQUE — they enter as the ChainData/PProd witnesses
resnet34_has_vjp_at already takes, and r34InputGrad's block slots are pinned to their
backwards — so the composition is checked between variables and costs nothing (§3.7(a)'s
lesson, in the direction that works). Only the four concrete endpoints are rewritten: the
dense head, GAP, the 3×3/s2 pool and the stem.
⭐⭐ THE SHAPE CHECK — the eleven-slot chain the whole-net tie is about IS the committed
forward. resnet34Forward_full_pc, regrouped into exactly the eleven arguments
resnet34_has_vjp_at takes: the stem cbrStridedPC, He et al.'s 3×3/s2 pool, the four
chainComp stages [a2,a1,a0] / [b2,b1,b0] / [c4,c3,c2,c1,c0] / [e1,e0], the three
downFwd downsamples, GAP and the dense head.
⛔ This is the theorem that would have caught the 2×2 pool. r34InputGrad_eq_resnet34_vjp
keeps its blocks OPAQUE — they enter as the ChainData/PProd witnesses, so the apex's
subject is a chain of VARIABLES and nothing in that theorem says which net they are. The
drift it eventually found (maxPoolFlatBack, 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.
The MobileNetV2 peer is mobilenetv2Forward_full_pc_eq_chain
(MobileNetV2WholeBackCertifiedTie.lean), which had this from the day it was written; the
ConvNeXt peer is convNextForwardTCh_eq_chain (Nets/ConvNeXt/ConvNeXtFullT.lean). ⚠ Both of
those are a bare rfl and this one CANNOT be: their apexes chain their blocks one slot each,
where resnet34_has_vjp_at groups its [3,4,6,3] runs under chainComp, and a chainComp
node has to be reduced away BEFORE the defeq — see chainComp₂_comp above.