Backward-graph faithfulness for the VERIFIED ResNet-34 basic block

The ResNet-34 peer of EfficientNetBackB0.lean / MobileNetV2BackB0.lean: a backward StableHLO graph that denotes the proven VJP of the batched ResNet-34 basic block.

The basic block is relu ∘ residual(F) (identity block), with body F = (conv-bn) ∘ (conv-bn-relu) — a 3×3 conv → bn → relu, then a 3×3 conv → bn (no activation), and an identity skip, followed by an outer relu after the residual add. This last fact is the structural difference from the MobileNetV2/EfficientNet residual blocks (whose residual add is the block output): r34 wraps the residual add in one more relu.

The relu wrinkle (vs relu6 / swish)

r34 uses relu (one kink, at 0): its VJP is only the pointwise relu_has_vjp_at, conditioned on the smoothness hypothesis ∀ k, x k ≠ 0 at the pre-activation — simpler than relu6's two-sided x k ≠ 0 ∧ x k ≠ 6, but the same _at machinery (vjp_comp_at + HasVJP.toHasVJPAt). Its per-op backward token is .selectPos (the mask if x>0 then dy else 0), whose denotation faithfulness is the already-proven (rfl) selectPos_faithful (StableHLO.lean:782).

Because there are TWO relu kinks (the body's mid-relu AND the outer post-residual relu), the whole-block VJP and its backward-graph faithfulness are _at / hypothesis-threaded: one smoothness family at the body's mid-relu pre-activation, one at the outer relu's pre-activation residual(F)(x).

Structure

• cbReluB — batched conv → bn → relu stage (cbrB from MobileNetV2BackB0 with relu for relu6), _at VJP + backward-graph faithfulness (cbReluBackBatchedGraph + …_faithful), chaining selectPos_faithful
  • bnBatchLABack_faithful + convBackBatched_faithful.
• cbB (= projB, conv → bn, no activation) backward is reused VERBATIM from EfficientNetBackB0 (projBackBatchedGraph / projBackBatchedGraph_faithful).
• the body cbB ∘ cbReluB — its backward graph r34BodyBackBatchedGraph, the two stage graphs chained at their cumulative activations, certified through the block layer.
• r34BasicBlockBackBatchedGraph_faithful — the CAPSTONE: the whole batched ResNet-34 identity basic block backward graph (outer-relu selectPos ∘ residual-fan-in(body-back) + identity skip) denotes the proven relu ∘ residual(F) VJP (vjp_comp_at(residual_has_vjp_at(body), relu)), threaded through both relu smoothness hypotheses.
• cbReluLayer / projLayer (from MobileNetV2BackB0) / cbReluStridedLayer / projStridedLayer — the four stages as CertLayers. r34BasicBlockLayer / r34DownBlockLayer compose them with CertLayer.comp, residual / residualProj and reluOut, and each body/block VJP and capstone here is that composite's .vjp / .faithful.

The strided/downsample block (relu ∘ residualProj(proj, F_s))

The downsample-block capstone (r34DownBlockBackBatchedGraph_faithful) reuses the new strided batched-conv backward primitive convStridedBackBatched (StableHLO.lean, the stride-2 analog of convBackBatched; its _faithful lives in EfficientNetBackB0). The body F_s = projB ∘ cbReluStridedB has a stride-2 conv1 (cbReluStridedB, the strided sibling of cbReluB) and a stride-1 conv2 (projB); the projection skip projStridedB is a stride-2 conv-bn. The whole block composes vjp_comp_at(residualProj_has_vjp_at(proj, F_s), relu) exactly like the identity block, but with the projection skip (residualProj, both paths nontrivial) instead of the identity skip (residual), and the strided convs in the body+skip.

@[reducible]

noncomputable def Proofs.StableHLO.cbReluB (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) : Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

Batched conv → bn → relu stage (ResNet basic-block first stage), at the network layout N·(oc·h·w). The relu analogue of MobileNetV2's cbrB (relu for relu6).

Equations

• Proofs.StableHLO.cbReluB N W b ε γ β = Proofs.relu (N * (oc * h * w)) ∘ Proofs.StableHLO.bnBatchLA N oc h w ε γ β ∘ Proofs.StableHLO.batchMap N (Proofs.flatConv W b)

noncomputable def Proofs.StableHLO.bnReluStage_has_vjp_at (N : ℕ) {a oc h w : ℕ} (op : Vec a → Vec (oc * h * w)) (hop : Differentiable ℝ op) (hopv : HasVJP op) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * a)) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N op x) k ≠ 0) : HasVJPAt (relu (N * (oc * h * w)) ∘ bnBatchLA N oc h w ε γ β ∘ batchMap N op) x

Generic relu-on-batched-bn-stage _at VJP. The relu analogue of bnRelu6Stage_has_vjp_at (and of bnSwishStage_has_vjp, but _at — relu only has a pointwise VJP): compose the batched-op VJP, the true-BN VJP (both global, lifted via .toHasVJPAt), and relu's pointwise VJP at the pre-relu activation. The smoothness hypothesis is the one-sided ≠ 0.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.bnReluStage_differentiableAt (N : ℕ) {a oc h w : ℕ} (op : Vec a → Vec (oc * h * w)) (hop : Differentiable ℝ op) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * a)) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N op x) k ≠ 0) : DifferentiableAt ℝ (relu (N * (oc * h * w)) ∘ bnBatchLA N oc h w ε γ β ∘ batchMap N op) x

Differentiability of the generic relu-on-batched-bn-stage at a smooth point.

noncomputable def Proofs.StableHLO.cbReluB_has_vjp_at (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * (ic * h * w))) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N (flatConv W b) x) k ≠ 0) : HasVJPAt (cbReluB N W b ε γ β) x

cbReluB (conv-bn-relu) _at VJP at a smooth point.

Equations

• Proofs.StableHLO.cbReluB_has_vjp_at N W b ε hε γ β x h_smooth = Proofs.StableHLO.bnReluStage_has_vjp_at N (Proofs.flatConv W b) ⋯ (Proofs.flatConv_has_vjp W b) ε hε γ β x h_smooth

theorem Proofs.StableHLO.cbReluB_differentiableAt (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * (ic * h * w))) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N (flatConv W b) x) k ≠ 0) : DifferentiableAt ℝ (cbReluB N W b ε γ β) x

noncomputable def Proofs.StableHLO.cbReluBackBatchedGraph {N ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (x : Vec (N * (ic * h * w))) (e : SHlo (N * (oc * h * w))) : SHlo (N * (ic * h * w))

Batched conv → bn → relu stage backward graph (ResNet basic-block stage 1): convBackBatched ∘ bnBatchLABack ∘ selectPos, each at its cumulative forward activation. The relu analogue of MobileNetV2's cbrBackBatchedGraph — .selectPos (the relu one-sided-kink mask) replaces .selectMid.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.cbReluBackBatchedGraph_faithful {N ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * (ic * h * w))) (e : SHlo (N * (oc * h * w))) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N (flatConv W b) x) k ≠ 0) : den (cbReluBackBatchedGraph W b ε γ β x e) = (cbReluB_has_vjp_at N W b ε hε γ β x h_smooth).backward (den e)

noncomputable def Proofs.StableHLO.cbReluLayer (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) : CertLayer (N * (ic * h * w)) (N * (oc * h * w))

The conv → bn → relu stage as a CertLayer, certified where its pre-relu activation misses 0. The kernel extent is a binder, so the same layer is a 1×1 or a 3×3.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.cbReluLayer_fwd_apply (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (v : Vec (N * (ic * h * w))) : (cbReluLayer N W b ε hε γ β).fwd v = cbReluB N W b ε γ β v

cbReluLayer's forward is cbReluB.

noncomputable def Proofs.StableHLO.r34BodyBackBatchedGraph {N c h w kH₁ kW₁ kH₂ kW₂ : ℕ} (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (ε₁ : ℝ) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (ε₂ : ℝ) (γ₂ β₂ : Vec c) (x : Vec (N * (c * h * w))) (e : SHlo (N * (c * h * w))) : SHlo (N * (c * h * w))

The batched ResNet-34 body backward graph: the two stage graphs chained at their cumulative forward activations (cbReluB⁻¹ ∘ projB⁻¹).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.StableHLO.r34BasicBlockLayer (N : ℕ) {c h w kH₁ kW₁ kH₂ kW₂ : ℕ} (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (ε₁ : ℝ) (hε₁ : 0 < ε₁) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (ε₂ : ℝ) (hε₂ : 0 < ε₂) (γ₂ β₂ : Vec c) : CertLayer (N * (c * h * w)) (N * (c * h * w))

The batched R34 identity basic block as a CertLayer: residual (cbReluLayer ; projLayer), then reluOut. Its ok is the body's mid-relu and the OUTER post-residual relu — the extra factor R34 has over the MBConv/inverted-residual blocks (projLayer contributes True). An endomorphism, so chain iterates it into a stage tail.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.StableHLO.r34BasicBlockB_has_vjp_at (N : ℕ) {c h w kH₁ kW₁ kH₂ kW₂ : ℕ} (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (ε₁ : ℝ) (hε₁ : 0 < ε₁) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (ε₂ : ℝ) (hε₂ : 0 < ε₂) (γ₂ β₂ : Vec c) (x : Vec (N * (c * h * w))) (h_s1 : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε₁ γ₁ β₁ (batchMap N (flatConv W₁ b₁) x) k ≠ 0) (h_out : ∀ (k : Fin (N * (c * h * w))), residual (projB N W₂ b₂ ε₂ γ₂ β₂ ∘ cbReluB N W₁ b₁ ε₁ γ₁ β₁) x k ≠ 0) : HasVJPAt (relu (N * (c * h * w)) ∘ residual (projB N W₂ b₂ ε₂ γ₂ β₂ ∘ cbReluB N W₁ b₁ ε₁ γ₁ β₁)) x

The batched ResNet-34 identity basic block's VJP at a smooth point — relu ∘ residual(F) with body F = projB ∘ cbReluB: the residual fan-in VJP of the body, then the OUTER relu's pointwise VJP at the pre-relu activation residual(F)(x) (r34BasicBlockLayer's VJP).

h_s1 is the body's mid-relu smoothness; h_out is the outer-relu smoothness (at residual(F)(x)).

Equations

• Proofs.StableHLO.r34BasicBlockB_has_vjp_at N W₁ b₁ ε₁ hε₁ γ₁ β₁ W₂ b₂ ε₂ hε₂ γ₂ β₂ x h_s1 h_out = (Proofs.StableHLO.r34BasicBlockLayer N W₁ b₁ ε₁ hε₁ γ₁ β₁ W₂ b₂ ε₂ hε₂ γ₂ β₂).vjp x ⋯

noncomputable def Proofs.StableHLO.r34BasicBlockBackBatchedGraph {N c h w kH₁ kW₁ kH₂ kW₂ : ℕ} (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (ε₁ : ℝ) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (ε₂ : ℝ) (γ₂ β₂ : Vec c) (x : Vec (N * (c * h * w))) (ecot : SHlo (N * (c * h * w))) : SHlo (N * (c * h * w))

The whole batched ResNet-34 identity basic block backward graph: selectPos (outer relu) ∘ residual fan-in (body backward + identity skip). The outer relu is the LAST forward op, so its .selectPos backward is the OUTERMOST backward op; inside, the residual addV sums the body's input-cotangent (r34BodyBackBatchedGraph fed the relu-masked cotangent) and the identity skip's verbatim cotangent (%dy).

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.r34BasicBlockBackBatchedGraph_faithful {N c h w kH₁ kW₁ kH₂ kW₂ : ℕ} (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (ε₁ : ℝ) (hε₁ : 0 < ε₁) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (ε₂ : ℝ) (hε₂ : 0 < ε₂) (γ₂ β₂ : Vec c) (x : Vec (N * (c * h * w))) (ecot : SHlo (N * (c * h * w))) (h_s1 : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε₁ γ₁ β₁ (batchMap N (flatConv W₁ b₁) x) k ≠ 0) (h_out : ∀ (k : Fin (N * (c * h * w))), residual (projB N W₂ b₂ ε₂ γ₂ β₂ ∘ cbReluB N W₁ b₁ ε₁ γ₁ β₁) x k ≠ 0) : den (r34BasicBlockBackBatchedGraph W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ x ecot) = (r34BasicBlockB_has_vjp_at N W₁ b₁ ε₁ hε₁ γ₁ β₁ W₂ b₂ ε₂ hε₂ γ₂ β₂ x h_s1 h_out).backward (den ecot)

CAPSTONE — the whole batched ResNet-34 identity basic block: backward graph ↔ the proven VJP. The two batched stage backward graphs (cbReluB/projB) chained at their forward activations, wrapped in the residual additive fan-in (body cotangent + identity skip) and the OUTER post-residual relu, proven equal to r34BasicBlockB_has_vjp_at (= vjp_comp_at(residual_has_vjp_at(F), relu)). The ResNet-34 analogue of mbResidBlockBackBatchedGraph_faithful / mnv2ResidBlockBackBatchedGraph_faithful, with the extra outer-relu factor, threaded through both relu smoothness hypotheses. It is r34BasicBlockLayer's faithful.

Key fact: the outer relu's .selectPos mask is applied ONCE to the incoming dy (giving masked = relu_has_vjp_at.backward (den ecot)), and that masked cotangent is what the residual fan-in (r34BodyBackBatchedGraph + identity skip) sees — exactly matching vjp_comp_at(residual, relu)'s structure: first apply relu's backward, then residual's backward to the result.

@[reducible]

noncomputable def Proofs.StableHLO.cbReluStridedB (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) : Vec (N * (ic * (2 * h) * (2 * w))) → Vec (N * (oc * h * w))

Batched STRIDE-2 conv → bn → relu stage (downsample basic-block first stage), at the network layout N·(oc·h·w) ← N·(ic·(2h)·(2w)). The strided sibling of cbReluB (flatConvStride2 for flatConv); halves spatial.

Equations

• Proofs.StableHLO.cbReluStridedB N W b ε γ β = Proofs.relu (N * (oc * h * w)) ∘ Proofs.StableHLO.bnBatchLA N oc h w ε γ β ∘ Proofs.StableHLO.batchMap N (Proofs.flatConvStride2 W b)

noncomputable def Proofs.StableHLO.cbReluStridedB_has_vjp_at (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N (flatConvStride2 W b) x) k ≠ 0) : HasVJPAt (cbReluStridedB N W b ε γ β) x

cbReluStridedB (strided conv-bn-relu) _at VJP at a smooth point. The strided sibling of cbReluB_has_vjp_at (flatConvStride2 for flatConv).

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.cbReluStridedB_differentiableAt (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N (flatConvStride2 W b) x) k ≠ 0) : DifferentiableAt ℝ (cbReluStridedB N W b ε γ β) x

noncomputable def Proofs.StableHLO.cbReluStridedBackBatchedGraph {N ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (e : SHlo (N * (oc * h * w))) : SHlo (N * (ic * (2 * h) * (2 * w)))

Batched strided conv → bn → relu stage backward graph: convStridedBackBatched ∘ bnBatchLABack ∘ selectPos, each at its cumulative forward activation. The strided sibling of cbReluBackBatchedGraph — convStridedBackBatched (the new stride-2 batched-conv VJP) replaces convBackBatched.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.cbReluStridedBackBatchedGraph_faithful {N ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (e : SHlo (N * (oc * h * w))) (h_smooth : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε γ β (batchMap N (flatConvStride2 W b) x) k ≠ 0) : den (cbReluStridedBackBatchedGraph W b ε γ β x e) = (cbReluStridedB_has_vjp_at N W b ε hε γ β x h_smooth).backward (den e)

noncomputable def Proofs.StableHLO.cbReluStridedLayer (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) : CertLayer (N * (ic * (2 * h) * (2 * w))) (N * (oc * h * w))

The strided conv → bn → relu stage as a CertLayer — cbReluLayer with flatConvStride2.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

noncomputable def Proofs.StableHLO.projStridedB (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) : Vec (N * (ic * (2 * h) * (2 * w))) → Vec (N * (oc * h * w))

Batched strided conv → bn projection skip (downsample basic-block skip): bnBatchLA ∘ batchMap (flatConvStride2) — the 3×3 stride-2 projection that matches the body's downsampled oc·h·w output. The strided sibling of projB (flatConvStride2 for flatConv); no activation (linear bottleneck).

Equations

• Proofs.StableHLO.projStridedB N W b ε γ β = Proofs.StableHLO.bnBatchLA N oc h w ε γ β ∘ Proofs.StableHLO.batchMap N (Proofs.flatConvStride2 W b)

theorem Proofs.StableHLO.projStridedB_differentiable (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) : Differentiable ℝ (projStridedB N W b ε γ β)

noncomputable def Proofs.StableHLO.projStridedB_has_vjp (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) : HasVJP (projStridedB N W b ε γ β)

Equations

• Proofs.StableHLO.projStridedB_has_vjp N W b ε hε γ β = Proofs.bnStage_has_vjp N (Proofs.flatConvStride2 W b) ⋯ (Proofs.flatConvStride2_has_vjp W b) ε hε γ β

noncomputable def Proofs.StableHLO.projStridedBackBatchedGraph {N ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ _β : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (e : SHlo (N * (oc * h * w))) : SHlo (N * (ic * (2 * h) * (2 * w)))

Batched strided conv → bn projection-skip backward graph: convStridedBackBatched ∘ bnBatchLABack, at the skip's forward activation. The strided sibling of projBackBatchedGraph.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.projStridedBackBatchedGraph_faithful {N ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (e : SHlo (N * (oc * h * w))) : den (projStridedBackBatchedGraph W b ε γ β x e) = (projStridedB_has_vjp N W b ε hε γ β).backward x (den e)

noncomputable def Proofs.StableHLO.projStridedLayer (N : ℕ) {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (hε : 0 < ε) (γ β : Vec oc) : CertLayer (N * (ic * (2 * h) * (2 * w))) (N * (oc * h * w))

The strided conv → bn projection skip as a CertLayer — projLayer with flatConvStride2, globally certified.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.StableHLO.r34DownBodyBackBatchedGraph {N ic oc h w kH₁ kW₁ kH₂ kW₂ : ℕ} (W₁ : Kernel4 oc ic kH₁ kW₁) (b₁ : Vec oc) (ε₁ : ℝ) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc kH₂ kW₂) (b₂ : Vec oc) (ε₂ : ℝ) (γ₂ β₂ : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (e : SHlo (N * (oc * h * w))) : SHlo (N * (ic * (2 * h) * (2 * w)))

The batched ResNet-34 downsample body backward graph: the two stage graphs chained at their cumulative forward activations (cbReluStridedB⁻¹ ∘ projB⁻¹). The strided sibling of r34BodyBackBatchedGraph.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.StableHLO.r34DownBlockLayer (N : ℕ) {ic oc h w kH₁ kW₁ kH₂ kW₂ kHp kWp : ℕ} (W₁ : Kernel4 oc ic kH₁ kW₁) (b₁ : Vec oc) (ε₁ : ℝ) (hε₁ : 0 < ε₁) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc kH₂ kW₂) (b₂ : Vec oc) (ε₂ : ℝ) (hε₂ : 0 < ε₂) (γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) : CertLayer (N * (ic * (2 * h) * (2 * w))) (N * (oc * h * w))

The batched R34 downsample basic block as a CertLayer: residualProj (projStridedLayer) (cbReluStridedLayer ; projLayer), then reluOut. Halves resolution (hence the 2*h in the input type), with a strided conv1 and a strided projection skip.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.StableHLO.r34DownBlockB_has_vjp_at (N : ℕ) {ic oc h w kH₁ kW₁ kH₂ kW₂ kHp kWp : ℕ} (W₁ : Kernel4 oc ic kH₁ kW₁) (b₁ : Vec oc) (ε₁ : ℝ) (hε₁ : 0 < ε₁) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc kH₂ kW₂) (b₂ : Vec oc) (ε₂ : ℝ) (hε₂ : 0 < ε₂) (γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (h_s1 : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε₁ γ₁ β₁ (batchMap N (flatConvStride2 W₁ b₁) x) k ≠ 0) (h_out : ∀ (k : Fin (N * (oc * h * w))), residualProj (projStridedB N Wp bp εp γp βp) (projB N W₂ b₂ ε₂ γ₂ β₂ ∘ cbReluStridedB N W₁ b₁ ε₁ γ₁ β₁) x k ≠ 0) : HasVJPAt (relu (N * (oc * h * w)) ∘ residualProj (projStridedB N Wp bp εp γp βp) (projB N W₂ b₂ ε₂ γ₂ β₂ ∘ cbReluStridedB N W₁ b₁ ε₁ γ₁ β₁)) x

The batched ResNet-34 downsample basic block's VJP at a smooth point — relu ∘ residualProj(proj, F_s) with body F_s = projB ∘ cbReluStridedB and projection skip proj = projStridedB: the projected residual fan-in VJP (skip + body), then the OUTER relu's pointwise VJP at the pre-relu activation residualProj(proj, F_s)(x) (r34DownBlockLayer's VJP).

The strided sibling of r34BasicBlockB_has_vjp_at: residualProj (BOTH paths nontrivial) for residual (identity skip), strided convs in body+skip.

h_s1 is the body's mid-relu smoothness; h_out is the outer-relu smoothness.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.StableHLO.r34DownBlockBackBatchedGraph {N ic oc h w kH₁ kW₁ kH₂ kW₂ kHp kWp : ℕ} (W₁ : Kernel4 oc ic kH₁ kW₁) (b₁ : Vec oc) (ε₁ : ℝ) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc kH₂ kW₂) (b₂ : Vec oc) (ε₂ : ℝ) (γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (ecot : SHlo (N * (oc * h * w))) : SHlo (N * (ic * (2 * h) * (2 * w)))

The whole batched ResNet-34 downsample basic block backward graph: selectPos (outer relu) ∘ projected-residual fan-in (body backward + PROJECTION skip backward). The outer relu is the LAST forward op, so its .selectPos backward is the OUTERMOST backward op; inside, the residualProj addV sums the projection skip's input-cotangent (projStridedBackBatchedGraph fed the relu-masked cotangent) and the body's input-cotangent (r34DownBodyBackBatchedGraph, same masked cotangent). Unlike the identity block, BOTH operands are nontrivial backward subgraphs (the skip is a strided conv-bn, not a verbatim %dy passthrough).

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.r34DownBlockBackBatchedGraph_faithful {N ic oc h w kH₁ kW₁ kH₂ kW₂ kHp kWp : ℕ} (W₁ : Kernel4 oc ic kH₁ kW₁) (b₁ : Vec oc) (ε₁ : ℝ) (hε₁ : 0 < ε₁) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc kH₂ kW₂) (b₂ : Vec oc) (ε₂ : ℝ) (hε₂ : 0 < ε₂) (γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (ecot : SHlo (N * (oc * h * w))) (h_s1 : ∀ (k : Fin (N * (oc * h * w))), bnBatchLA N oc h w ε₁ γ₁ β₁ (batchMap N (flatConvStride2 W₁ b₁) x) k ≠ 0) (h_out : ∀ (k : Fin (N * (oc * h * w))), residualProj (projStridedB N Wp bp εp γp βp) (projB N W₂ b₂ ε₂ γ₂ β₂ ∘ cbReluStridedB N W₁ b₁ ε₁ γ₁ β₁) x k ≠ 0) : den (r34DownBlockBackBatchedGraph W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ Wp bp εp γp βp x ecot) = (r34DownBlockB_has_vjp_at N W₁ b₁ ε₁ hε₁ γ₁ β₁ W₂ b₂ ε₂ hε₂ γ₂ β₂ Wp bp εp hεp γp βp x h_s1 h_out).backward (den ecot)

CAPSTONE — the whole batched ResNet-34 DOWNSAMPLE basic block: backward graph ↔ the proven VJP. The two batched stage backward graphs of the body (cbReluStridedB/projB) chained at their forward activations, wrapped in the PROJECTED-residual additive fan-in (body cotangent + STRIDED projection-skip cotangent) and the OUTER post-residual relu, proven equal to r34DownBlockB_has_vjp_at (= vjp_comp_at(residualProj_has_vjp_at(proj, F_s), relu)). The strided sibling of r34BasicBlockBackBatchedGraph_faithful: residualProj (both backward paths nontrivial) for residual (identity skip), convStridedBackBatched in the body's conv1 and the whole projection skip. It is r34DownBlockLayer's faithful.

Key fact: the outer relu's .selectPos mask is applied ONCE to the incoming dy (giving masked = relu_has_vjp_at.backward (den ecot)), and that masked cotangent is what BOTH residualProj fan-in operands see — matching vjp_comp_at(residualProj, relu)'s structure: first relu's backward, then residualProj's backward (= proj.backward + body.backward at the masked cotangent).