Toward real ResNet-34 — the deep-block chain (Chapter 5 Milestone B4) #
A real ResNet-34 stacks 16 basic blocks in four stages (3+4+6+3). Within a
stage every block is a self-map Vec n → Vec n (same channel count) but with its
own weights — so it is a composition of a list of distinct same-type maps,
not an iterate of one map.
This file proves the generic enabler: if every map in a list is differentiable
and has a VJP, their composition (chainComp) does too — by induction chaining
vjp_comp. That turns "16 blocks deep" into a List.length, no per-block
boilerplate. The full ResNet-34 forward (strided proj blocks via flatConvStride2
- chained identity blocks + per-channel BN) is assembled on top of this.
Closes under [propext, Classical.choice, Quot.sound].
Compose a list of self-maps left-to-right as data flows: chainComp [f₁,…,fₖ] = f₁ ∘ … ∘ fₖ (the last list element runs first, i.e. is the deepest). A
ResNet stage is chainComp of its blocks.
Equations
- Proofs.chainComp fs = List.foldr (fun (x1 x2 : Proofs.Vec n → Proofs.Vec n) => x1 ∘ x2) id fs
Instances For
A chain of differentiable maps is differentiable.
Deep-chain VJP. A composition of a list of differentiable maps that each
have a VJP has a VJP — the backward runs each block's backward in reverse
order. By induction chaining vjp_comp; the structural heart of a deep
ResNet stage (k distinct-weight basic blocks).
Equations
- One or more equations did not get rendered due to their size.
- Proofs.vjp_chain [] hdiff_2 hvjp_2 = Proofs.identity_has_vjp n
Instances For
Deep-chain VJP correctness (ℝ-headline): the chained backward equals the
pdiv-contracted Jacobian of the whole composition.
Recursive hypothesis bundle for a chain of HasVJPAt blocks: each block is
DifferentiableAt and HasVJPAt at its running activation — the point
chainComp rest x feeding it (the deeper blocks run first). Residual identity
blocks are only HasVJPAt at smooth points, so the chain must thread the
point, not assume global differentiability.
Equations
- Proofs.ChainData x [] = PUnit.{1}
- Proofs.ChainData x (f :: rest) = (DifferentiableAt ℝ f (Proofs.chainComp rest x) ×' Proofs.HasVJPAt f (Proofs.chainComp rest x) ×' Proofs.ChainData x rest)
Instances For
The chain at a point both has a VJP and is differentiable there, from the
per-block ChainData. The companion DifferentiableAt is carried alongside
so the recursion can feed the inner-composition differentiability into each
vjp_comp_at / DifferentiableAt.comp.
Equations
- Proofs.chain_vjp_diff_at x [] x_3 = ⟨(Proofs.identity_has_vjp n).toHasVJPAt x, ⋯⟩
- Proofs.chain_vjp_diff_at x (f :: rest) d = ⟨Proofs.vjp_comp_at (Proofs.chainComp rest) f x ⋯ ⋯ (Proofs.chain_vjp_diff_at x rest d.snd.snd).fst d.snd.fst, ⋯⟩
Instances For
Deep-block chain VJP at a smooth point. A composition of conditional
(HasVJPAt) blocks — e.g. the k identity residual blocks of a ResNet stage —
has a VJP at x, given each block is differentiable + has a VJP at its
running activation (ChainData). The _at peer of vjp_chain.
Equations
- Proofs.vjp_chain_at x fs hdata = (Proofs.chain_vjp_diff_at x fs hdata).fst
Instances For
A full ResNet stage has a VJP at a point. A stage is a downsample block
down : Vec m → Vec n (channel/spatial change — rblkPStrided, or for the
first stage the identity / stem-fed input) followed by a chain of k identity
residual blocks chainComp ids : Vec n → Vec n. VJPAt by one vjp_comp_at
gluing the downsample to the (deep-chained) identity blocks. The reusable
composition pattern for assembling ResNet-34's four stages.
Equations
- Proofs.resStage_has_vjp_at down ids x hdown_diff hdown hids = Proofs.vjp_comp_at down (Proofs.chainComp ids) x hdown_diff ⋯ hdown (Proofs.vjp_chain_at (down x) ids hids)
Instances For
ResNet-stage VJP correctness (ℝ-headline): the stage's backward equals the
pdiv-Jacobian of (identity-block chain) ∘ downsample at x.
Compose two HasVJPAt-with-DifferentiableAt pairs (carried as PProd so the
DifferentiableAt Prop is allowed). The fold step for the whole net.
Equations
- Proofs.vjp_comp_diff_at f g x hf hg = ⟨Proofs.vjp_comp_at f g x ⋯ ⋯ hf.fst hg.fst, ⋯⟩
Instances For
Whole-network ResNet-34 VJP. The conditional VJP of a real ResNet-34-shaped
network at an input x:
dense ∘ GAP ∘ stage₄ ∘ stage₃ ∘ stage₂ ∘ stage₁ ∘ maxpool ∘ stem
with stageᵢ = (identity-block chain) ∘ downsampleᵢ for the three downsampling
stages (the 3+4+6+3 = 16 basic blocks live in the idsᵢ lists + the three
downᵢ blocks; instantiate down/ids/stem/gap/dense with the verified
convBnReluStrided/rblkPStrided/rblk/globalAvgPoolFlat/dense and
maxPoolFlat). Parametric over the component functions and their per-component
VJP+differentiability witnesses at the running activations — so depth is a
List.length, not 100 explicit weight arguments. Folded from the verified
vjp_comp_at / vjp_chain_at (ChainData threads each block's smooth point).
This is the structural analogue of cnn_has_vjp_at scaled to 34 layers; the
discharge of the smoothness/no-tie hypotheses for a concrete instance (à la
CnnConcrete) plus per-channel BN and the GPU render remain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
conv(stride-2) → bn block VJP (no ReLU), everywhere. The strided peer of
convBn_has_vjp: flatConvStride2 then bnForward, both differentiable
everywhere, so a global HasVJP. The downsampling body of a stage-start
block and its strided 1×1 projection skip.
Equations
- One or more equations did not get rendered due to their size.
Instances For
conv(stride-2) → bn is differentiable everywhere.
conv(stride-2) → bn → relu block VJP at a smooth point. The strided peer
of convBnRelu_has_vjp_at (the workhorse opening each downsampling stage):
two vjp_comp_at, with flatConvStride2_has_vjp for the conv and the ReLU
smoothness hypothesis h_smooth (no post-BN activation hits the kink).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strided block VJP correctness (ℝ-headline): the strided downsampling
block's backward equals the pdiv-Jacobian of relu ∘ bn ∘ conv_stride2.
Strided basic-block body VJP F = convBn₂(stride 1) ∘ convBnRelu₁(stride 2)
(channels ic → oc, spatial 2h×2w → h×w). The strided peer of
resblock_body_has_vjp_at: inner downsampling conv→bn→relu (needs h_smooth₁),
outer stride-1 conv→bn (everywhere); two vjp_comp_at.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strided basic-block body is DifferentiableAt at a smooth point.
Full strided residual-projection block VJP — the block that opens each
ResNet-34 downsampling stage: relu( proj(x) + F(x) ) where both the body's
first conv W₁ and the 1×1 projection skip Wp are stride-2 (so ic→oc,
2h×2w → h×w), and the body's second conv W₂ is stride-1. Built via
residualProj_has_vjp_at (fan-in of the strided proj convBnStrided and the
strided body) then a final vjp_comp_at with the post-add ReLU. The strided
peer of resblockProj_has_vjp_at.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Strided residual-projection block VJP correctness (ℝ-headline): the
downsampling block's backward equals the pdiv-Jacobian of
relu ∘ residualProj (strided proj) (strided body).
BN of an injective vector is injective when γ ≠ 0: bn is the strictly
monotone affine map γ·istd·(· − μ) + β (istd > 0), so it preserves the
distinctness needed for the stem's maxpool to have no ties.
The strided decimation index is injective (distinct output cells map to
distinct even input cells) — so decimateFlat of an injective vector is
injective, the keystone of the strided stem's maxpool no-tie discharge.
decimateFlat of an injective vector is injective.
A conv with everywhere-zero kernel/bias maps anything to 0 (local copy of
MobileNetV2's flatConv_eq_zero).
A stride-2 conv with zero kernel/bias maps anything to 0 (decimate of 0).
A single-channel identity residual block with zero weights and BN (ε,γ,β)=(1,0,1):
relu( x + bn₂(conv₂(relu(bn₁(conv₁ x)))) ). The body collapses to the constant
β₂ = 1, so the block is relu(1 + x).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity block has a VJP at any nonnegative activation: bn₁-input is constant
(β₁=1≠0) and the post-add ReLU input is 1 + aₖ > 0 since aₖ ≥ 0.
Equations
- Proofs.idBlk_hasVJPAt h w hhw a ha = Proofs.resblock_has_vjp_at Proofs.Zk Proofs.Zb Proofs.Zk Proofs.Zb 1 0 1 1 0 1 Proofs.idBlk_hasVJPAt._proof_1 Proofs.idBlk_hasVJPAt._proof_1 a ⋯ ⋯
Instances For
ChainData for j stacked identity blocks at a nonnegative base — every running
activation is a ReLU output (or the base), so each block's smooth-point hypotheses hold.
Equations
- One or more equations did not get rendered due to their size.
- Proofs.idChainData h w hhw base hbase 0 = PUnit.unit
Instances For
A single-channel strided projection block with zero weights and BN (1,0,1):
relu( proj(x) + bn₂(conv₂(relu(bn₁(conv₁ x)))) ), both conv₁ and proj stride-2.
Body and projection both collapse to the constant 1, so the post-add ReLU input is
1 + 1 = 2 everywhere — unconditional (no activation-sign assumption).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The strided block has a VJP at every point (smoothness is unconditional: both paths are
constant 1, so the post-add ReLU input is 2 ≠ 0).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Stem: a 1×1 identity conv (so flatConvStride2 collapses to decimation),
BN (ε,γ,β) = (1,1,20), ReLU. β = 20 > √256 forces bn > 0 (bnForward_lb),
so ReLU is the identity and the stem output stays injective — the maxpool no-tie.
Equations
- Proofs.ResNet34Concrete.Ws x✝³ x✝² x✝¹ x✝ = 1
Instances For
Equations
Instances For
Equations
- Proofs.ResNet34Concrete.Wd x✝¹ x✝ = 0
Instances For
Equations
Instances For
The stem relu ∘ bn ∘ conv_stride2 at 1ch, 16×16 output.
Equations
- Proofs.ResNet34Concrete.stem = Proofs.relu (1 * 16 * 16) ∘ Proofs.bnForward (1 * 16 * 16) 1 1 20 ∘ Proofs.flatConvStride2 Proofs.ResNet34Concrete.Ws Proofs.ResNet34Concrete.bs
Instances For
Stride-2 identity conv = decimation.
The stem output is injective: bn of the injective decimated input is injective
(bnForward_injective, γ = 1 ≠ 0) and the ReLU is the identity (stem_pos).
The maxpool output is strictly positive (max of positive stem outputs).
The maxpool point bridge: flatten ∘ unflatten = id at the stem output.
Maxpool VJP at the stem output (no ties via stem_maxpool_smooth).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Maxpool differentiability at the stem output.
ResNet-34's four stages: 3 + 4 + 6 + 3 = 16 identity blocks.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
The concrete whole-network forward map: dense ∘ gap ∘ (stage₄…₁) ∘ maxpool ∘ stem,
a real 34-layer ResNet (strided stem + 3 strided downsamplers + 16 identity blocks +
GAP + dense) at 1 channel / 32×32.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Whole-network VJP for a concrete ResNet-34 — every smoothness/no-tie hypothesis of
resnet34_has_vjp_at discharged. The strided identity stem yields distinct positive BN
outputs (so the maxpool has no ties via stem_maxpool_smooth); every residual block uses
zero weights, so its body is the constant 1 (bnForward_const_eq) and the post-add ReLU
input is 1 + activation > 0 (identity blocks, activation ≥ 0) or 2 (downsamplers).
Equations
- One or more equations did not get rendered due to their size.