ResNet-50's non-degeneracy seal, on the full-width batched net (levels 2 and 3) #
ResNet50FullBVJP.lean proves
resnet50ForwardBFullHasVJPAt under 48 relu clauses — three per bottleneck — plus the stem's
and the stem pool's. This file exhibits the clause bundle's joint satisfiability, and a nonzero
Jacobian with it, on resnet50ForwardBFull itself.
What is inherited and what is new #
Almost everything is Training/BatchSealKit.lean's or ResNet-34's. The carrier (EDiff and its
per-op steps), the ray, the centre-tap kernel and the 7×7/s2 stem's no-tie are the kit's; the
strided projection (BatchSeal.sealProj), the zeroed-body collapse (projB_zero_const), the
relu-removal (cbReluStridedB_eq) and the stem's own collapse (r34StemB_eq) are ResNet-34's,
stated at variable shapes and instantiated here — the same reuse ResNet50FullB.lean already makes
of r34StemB and r34HeadB themselves.
Three things are genuinely new:
- three convolutions per block, so three relu clauses. The bottleneck's
hm2sits after the 3×3 — but withW₂zeroed it sees a constant channel, so it isβ₂ = 1 ≠ 0and, likehm1, needs nothing of the activation. Onlyhoutdoes, through0 ≤ activation; - a stride-1 projection. Stage 1 block 0 changes channels (64 → 256) at unchanged resolution,
so its skip is
projB, notprojStridedB, and the carrier crosses it through the kit's stride-1eDiff_conv. That also makes the carrier's BN count five, not the four of ResNet-34: stem,s1b0,s2b0,s3b0,s4b0; qstays a binder. ResNet-50 ships at two resolutions and the VJP is stated at both, so the seal is too:0 < qandq ≤ 7are all the witness needs, andq = 7(224 px) andq = 5(160 px) are instances of one theorem. The bound is theβ = 160margin against the widest BN, the stem's2·(16q)² = 512q²; a largerqwants a largerβ, not a different argument.
The structural identity bottleneck: all three convs zeroed, every BN (ε, γ, β) = (1, 1, 1).
The body is then the constant 1 and the block is a ↦ a + 1 on a nonnegative activation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The structural projection bottleneck — one record for both projection forms, as R50ProjW is.
Zeroed body, centre-tap 1×1 skip, β_p = 160 (the margin that keeps the post-residual relu off
its kink at every input).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The witness weights, generic in the class count.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bottleneck body is the constant 1 at every input — the third conv is zeroed, so
projB_zero_const collapses it whatever the two stages beneath it do.
The strided projection block's body is the constant 1. v1.5: its middle stage is the
STRIDED conv-bn-relu, so this is not seal_pr_body at other shapes.
The structural STRIDE-1 projection: a 1×1 centre-tap conv-BN.
Equations
- Proofs.R50FullBSeal.sealProj1 N h w ic oc = Proofs.projB N (Proofs.BatchSeal.ctK oc ic 1 1 1) (Proofs.BatchSeal.kv oc 0) 1 (Proofs.BatchSeal.kv oc 1) (Proofs.BatchSeal.kv oc 160)
Instances For
The bottleneck's three relu clauses. Both interior ones see a constant channel (their
convs are zeroed), so they are β = 1 ≠ 0 and weight-only; only the post-residual one needs
the activation, and only through 0 ≤ ·.
The strided projection block's three relu clauses — all weight-only. v1.5: hm1 is at the
INPUT resolution and only hm2 is at the halved one.
The witness input: the shared ray at 32q × 32q (224 px at q = 7, 160 at q = 5).
Equations
Instances For
Its direction — all of example 0's channel 0.
Equations
Instances For
The stem's centre-tap conv output — the carrier's first stop.
Equations
- Proofs.R50FullBSeal.Zs q t = Proofs.BatchSeal.ctConv 64 7 7 (2 * (2 * (2 * q))) (2 * (2 * (2 * q))) t
Instances For
The stem BN is strictly positive at every point of the ray.
The stem's relu is off at the witness, so the pool's no-tie can be read on the BN output.
The stem, collapsed: its relu is off, so it is pool ∘ bn ∘ centre-tap conv.
Every BN ε of the witness is 1.
The whole-net VJP at the witness — all 48 relu clauses, the stem clause and the
pool's no-tie discharged at (sealW nCls, sealX q t), on resnet50ForwardBFull itself
(transported through resnet50ForwardBFull_eq_chain), at BOTH shipped resolutions.
Equations
- Proofs.R50FullBSeal.sealVJP q hq0 hq nCls t = Proofs.HasVJPAt.congr ⋯ (Proofs.resnet50ForwardBFullHasVJPAt 2 q (Proofs.R50FullBSeal.sealW nCls) ⋯ (Proofs.R50FullBSeal.sealX q t) ⋯)
Instances For
The net is differentiable at the witness — fderiv_ne_zero_of_ray's first hypothesis.
The carrier after it.
Equations
- Proofs.R50FullBSeal.dP4 q nCls t ci = Proofs.R50FullBSeal.dP3 q nCls t 0 * Proofs.bnIstd (2 * (q * q)) (Proofs.BatchSeal.bnRowLA 2 2048 q q (Proofs.R50FullBSeal.Zp4 q nCls t) ci) 1
Instances For
The positive, continuous nonlinear factor: one istd per BN on the carrier's path —
the stem's and the FOUR projections'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
R is continuous: every bottleneck is, and fun_prop composes the thirteen-block prefix once
the chain is unfolded to its atoms. Every BN on the witness has ε = 1.
Level 2 — the witness is non-degenerate: the full-width batch-BN ResNet-50 at the structural weights is NOT constant in its input, at either shipped resolution.
The seal: the proven whole-network backward of the full-width, batch-BatchNorm,
[3,4,6,3]-bottleneck ResNet-50 — resnet50ForwardBFull, at BOTH shipped resolutions —
is not the zero map at the witness.