ResNet-34's non-degeneracy seal, on the full-width batched net (levels 2 and 3) #

ResNet34FullBVJP.lean proves resnet34ForwardBFullHasVJPAt: the whole-net VJP at any (w, x) that satisfies 32 relu clauses, a stem clause and the stem pool's condition. A conditional theorem of that shape says nothing unless its hypotheses are jointly satisfiable at a point with a nonzero Jacobian. This file exhibits such a point on resnet34ForwardBFull itself: 64→512 channels, [3,4,6,3] blocks, the 7×7/s2 stem, the 3×3/s2 pool, batch BatchNorm, at 224×224.

The witness #

Weights are structural, not trained (a trained-weight witness would be a numeric fact about millions of floats):

• every residual body is zeroed, so it is the constant β₂ = 1 whatever γ₂ is (BatchSeal.bnBatchLA_const: a constant channel has variance 0, so batch BN returns β). On a nonnegative activation the identity block is therefore the affine shift a ↦ a + 1 (sealIdB_eq) — and the shift is batch-uniform, hence invisible to the carrier;
• every channel-changing conv (the stem, the three 1×1/s2 projections) is a centre-tap broadcast (BatchSeal.ctK): every output channel is a copy of input channel 0 read through the kernel's centre tap. Centre tap, not a general kernel, because conv2d zero-pads: a conv of a constant is not constant at the border, but the centre tap is in range at every cell. And a broadcast, not a diagonal on channel 0: a kernel feeding only output channel 0 leaves the stem's other 63 channels constant, and a constant channel ties every 3×3 window of the pool — StemPoolSmoothAt quantifies over channels, so the tap has to reach all of them;
• γ = 1, β = 160 at the stem and the projections, ε = 1 everywhere. √(N·h·w) ≤ √25088 < 160 at every one of those four BN widths, so BatchSeal.bnBatchLA_pos puts every relu strictly off its kink at every input — the net needs no eventually-argument for its relus, and the only genuine kink left is the stem pool;
• the head reads channel 0 into class 0 (Wd 0 0 = 1, bd = 0), so 0 < nCls is the only constraint on the class count.

N = 2 and the input is sealX t = sealBase + t • sealV: both examples carry the same strictly decreasing ramp in channel 0, and sealV adds t to all of example 0's channel 0.

Why the carrier is a batch difference #

bnBatchLA normalizes each channel over all N·h·w cells, so a within-example channel-difference carrier is exactly what a channel's own mean subtracts, and at N = 1 this net is constant in its input. The carrier here is EDiff: example 0's slab is example 1's plus a per-channel constant. Batch BN keeps it and scales it by γ_c · istd_c (BatchSeal.bnBatchLA_exdiff) because the two examples share one mean and one istd; the centre-tap convs copy channel 0's offset to every channel; the pool shifts with it (maxPool3s2_shift, for every t, no argmax argument); the zeroed bodies add a batch-uniform constant and so are transparent. The class-0 output difference between the two examples is therefore t · R t with R a product of the four carrier-path istds, continuous and positive, so g'(0) = R 0 ≠ 0 and no BN-variance derivative is ever taken.