ResNet-50's whole-net input-VJP at TRUE BATCH-NORM #
ResNet50FullB.lean states the batch-BN forward at the [3,4,6,3] bottleneck ladder. This file
gives that forward a certified HasVJPAt.
No new mathematics, and nothing new one tier down #
Every block VJP is already proven at bnBatchLA: r50BottleneckBHasVJPAt,
r50ProjBlockBHasVJPAt and r50DownBlockBHasVJPAt (ResNet50BackB0.lean) are exactly the
three shapes r50IdB / r50ProjB / r50DownB unfold to. The bundle lemmas below are delegations
in ResNet34FullBVJP.lean's style, and the whole net is those blocks' CertLayers composed.
No Foundation lemma of its own. ResNet-50 has ResNet-34's stem and reuses
r34StemBHasVJPAt (which lifts the stem pool with batchMapHasVJPAt) verbatim. The head is
ResNet-34's too (r34HeadBHasVJP, GLOBAL: GAP and dense are smooth and each is batchMap of a
per-example op, so no hypothesis appears).
The hypothesis budget #
Pointwise (HasVJPAt), not global, and necessarily. relu is kinked. And a BOTTLENECK
carries THREE kink clauses, where ResNet-34's basic block carries two: the two interior relus
and the post-residual OUTER relu. Sixteen blocks give 48 clauses, plus the stem's relu and the stem
pool's no-tie condition — bundled per block into R50IdSmoothAt / R50ProjSmoothAt /
R50DownSmoothAt, and those 18 bundles into one R50SmoothAtB (the positivity bundles into
R50PosB), so the apex binds two hypotheses, as MobileNetV2's does.
The pool's condition is per example (StemPoolSmoothAt, reused): a tie is a property of one
image's 3×3 window, not of the batch.
No 0 < q is needed: the stem is certified as one layer (stemReluPoolLayer), whose VJP holds on
an empty output grid too.
The running activations are named r50Pre0 … r50Pre16 so each bundle can be STATED at the
activation entering its block without a sixteen-deep nested application inline; r50Pre16 doubles
as the trunk, and resnet50ForwardBFull_eq_chain bridges it back to the committed
nested-application forward.
N and q are both variables (the widths are literals), so ONE statement covers
resnet50in_fwd (q = 7, 224 px) and resnet50in160_fwd (q = 5, 160 px) at every batch size.
All four BatchNorm epsilons of a projection bottleneck are positive (body three, skip one).
One bundle for BOTH projection forms, as R50ProjW is one record for both.
Instances For
The THREE relu sites of an identity bottleneck are away from the kink at v: the 1×1 reduce's
BN output, the 3×3's BN output, and the post-residual sum. The 1×1 expand has no activation.
Instances For
The three relu sites of the STRIDE-1 projection bottleneck at v. Identical to the identity
block's except that the outer relu sits at the PROJECTED residual — both paths nontrivial.
Instances For
The three relu sites of the STRIDED projection bottleneck at v.
v1.5: the FIRST relu is at the input resolution 2h × 2w and only the second is at
h × w, because the stride is on the 3×3. Writing hm1 at h w typechecks nowhere, which is
the one place a reader can get this shape wrong.
- hm2 (k : Fin (N * (mid * h * w))) : StableHLO.bnBatchLA N mid h w p.ε₂ p.γ₂ p.β₂ (StableHLO.batchMap N (flatConvStride2 p.W₂ p.b₂) (StableHLO.cbReluB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁ v)) k ≠ 0
Instances For
Identity bottleneck VJP — r50BottleneckBHasVJPAt at the bundle's fields.
Equations
Instances For
Stride-1 projection bottleneck VJP — r50ProjBlockBHasVJPAt at the bundle's fields.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strided projection bottleneck VJP — r50DownBlockBHasVJPAt at the bundle's fields.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- Proofs.r50Pre1 N q w = Proofs.r50ProjB N (2 * (2 * (2 * q))) (2 * (2 * (2 * q))) w.s1b0 ∘ Proofs.r50Pre0 N q w
Instances For
Equations
- Proofs.r50Pre2 N q w = Proofs.r50IdB N (2 * (2 * (2 * q))) (2 * (2 * (2 * q))) w.s1b1 ∘ Proofs.r50Pre1 N q w
Instances For
Equations
- Proofs.r50Pre3 N q w = Proofs.r50IdB N (2 * (2 * (2 * q))) (2 * (2 * (2 * q))) w.s1b2 ∘ Proofs.r50Pre2 N q w
Instances For
Equations
- Proofs.r50Pre4 N q w = Proofs.r50DownB N (2 * (2 * q)) (2 * (2 * q)) w.s2b0 ∘ Proofs.r50Pre3 N q w
Instances For
Equations
- Proofs.r50Pre5 N q w = Proofs.r50IdB N (2 * (2 * q)) (2 * (2 * q)) w.s2b1 ∘ Proofs.r50Pre4 N q w
Instances For
Equations
- Proofs.r50Pre6 N q w = Proofs.r50IdB N (2 * (2 * q)) (2 * (2 * q)) w.s2b2 ∘ Proofs.r50Pre5 N q w
Instances For
Equations
- Proofs.r50Pre7 N q w = Proofs.r50IdB N (2 * (2 * q)) (2 * (2 * q)) w.s2b3 ∘ Proofs.r50Pre6 N q w
Instances For
Equations
- Proofs.r50Pre8 N q w = Proofs.r50DownB N (2 * q) (2 * q) w.s3b0 ∘ Proofs.r50Pre7 N q w
Instances For
Equations
- Proofs.r50Pre9 N q w = Proofs.r50IdB N (2 * q) (2 * q) w.s3b1 ∘ Proofs.r50Pre8 N q w
Instances For
Equations
- Proofs.r50Pre10 N q w = Proofs.r50IdB N (2 * q) (2 * q) w.s3b2 ∘ Proofs.r50Pre9 N q w
Instances For
Equations
- Proofs.r50Pre11 N q w = Proofs.r50IdB N (2 * q) (2 * q) w.s3b3 ∘ Proofs.r50Pre10 N q w
Instances For
Equations
- Proofs.r50Pre12 N q w = Proofs.r50IdB N (2 * q) (2 * q) w.s3b4 ∘ Proofs.r50Pre11 N q w
Instances For
Equations
- Proofs.r50Pre13 N q w = Proofs.r50IdB N (2 * q) (2 * q) w.s3b5 ∘ Proofs.r50Pre12 N q w
Instances For
Every BatchNorm ε of the net is positive: the stem's and each bottleneck's bundle.
- s1b0 : R50ProjPos w.s1b0
- s2b0 : R50ProjPos w.s2b0
- s3b0 : R50ProjPos w.s3b0
- s4b0 : R50ProjPos w.s4b0
Instances For
Every relu is away from its kink and every stem-pool window is smooth or dead, each at the activation
its block actually sees: the stem's clauses at the image, block k's at r50Pre(k-1). The
head has none (GAP and dense are smooth).
- s3b0 : R50DownSmoothAt N (2 * q) (2 * q) w.s3b0 (r50Pre7 N q w x)
- s3b1 : R50IdSmoothAt N (2 * q) (2 * q) w.s3b1 (r50Pre8 N q w x)
- s3b2 : R50IdSmoothAt N (2 * q) (2 * q) w.s3b2 (r50Pre9 N q w x)
- s3b3 : R50IdSmoothAt N (2 * q) (2 * q) w.s3b3 (r50Pre10 N q w x)
- s3b4 : R50IdSmoothAt N (2 * q) (2 * q) w.s3b4 (r50Pre11 N q w x)
- s3b5 : R50IdSmoothAt N (2 * q) (2 * q) w.s3b5 (r50Pre12 N q w x)
- s4b0 : R50DownSmoothAt N q q w.s4b0 (r50Pre13 N q w x)
- s4b1 : R50IdSmoothAt N q q w.s4b1 (r50Pre14 N q w x)
- s4b2 : R50IdSmoothAt N q q w.s4b2 (r50Pre15 N q w x)
Instances For
The committed nested-application forward IS the layered chain the VJP is stated on — the
ResNet-50 peer of resnet34ForwardBFull_eq_chain, and what lets the VJP be about
resnet50ForwardBFull rather than about a re-spelling of it.
ResNet-50 as one certified layer, at every batch size and resolution. Its .faithful
is a whole-net backward graph, stem pool included, proven to denote the VJP.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The composed layer's forward IS the committed nested-application forward: peeled one comp
at a time, then each layer's forward by its rfl lemma.
ResNet-50 at TRUE BATCH-NORM has a certified input-VJP at a smooth point — all sixteen
bottlenecks. r50NetLayer's .vjp, read at the layered chain, under two hypotheses: R50PosB (every ε > 0) and R50SmoothAtB (every relu clause and the stem
pool's smooth-or-dead condition, each at its block's own input).
Pointwise, and necessarily: relu is kinked. Each block contributes THREE clauses — the two interior relus and the post-residual OUTER relu — where ResNet-34's basic block contributes two and EfficientNet's MBConv none.
The head takes no hypothesis at all, and N and q are both variables, so this covers the
224-px and 160-px artifacts at every batch size.
Equations
- Proofs.resnet50ForwardBFullHasVJPAt N q w hp x hx = Proofs.HasVJPAt.congr ⋯ ((Proofs.r50NetLayer N q w hp).vjp x ⋯)
Instances For
Public correctness theorem: the sixteen-bottleneck batch-BN backward equals the
pdiv-contracted Jacobian of resnet50ForwardBFull ITSELF — the committed
nested-application forward ResNet50FullB.lean defines — not of the layered chain the VJP is
assembled on. Tied back through resnet50ForwardBFull_eq_chain.
The committed forward is differentiable at every smooth point — the layer's .diff. What
the seal's seal_differentiableAt needs.