ResNet-50's non-degeneracy seal, on the full-width batched net (levels 2 and 3) #
planning/full_width_seals.md §4.2. ResNet50FullBVJP.lean proves
resnet50ForwardB_full_has_vjp_at under 48 relu clauses — three per bottleneck — plus the stem's
and the stem pool's. ResNet-50 had no witness at all: unlike ResNet-34 and MobileNetV2 it never
had a 2-channel proxy, so the clause bundle's joint satisfiability was never exhibited. This file
exhibits it, and a nonzero Jacobian with it, on resnet50ForwardB_full 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 (R34FullBSeal.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 tier is stated at both, so the seal is too:0 < qandq ≤ 7are all the witness needs, andq = 7(224 px) andq = 5(160 px, where the 76.66% run lives) 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 stride-1 projection block's body is the constant 1.
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 sealPrBody 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.
⭐⭐ 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 resnet50ForwardB_full itself
(transported through resnet50ForwardB_full_eq_chain), at BOTH shipped resolutions.
Equations
- One or more equations did not get rendered due to their size.
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
⭐⭐ 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 — resnet50ForwardB_full, at BOTH shipped resolutions —
is not the zero map at the witness. ResNet-50's clause bundle (48 relu clauses, the stem
and the pool) had no exhibited point at all before this.