Spike: fan-in backward-graph faithfulness (EfficientNet-B0 assembly brick)

The first reusable brick toward an efficientnet*_back_faithful theorem: a backward StableHLO graph that denotes the proven whole-net VJP, the way mlpVerified_back_faithful does for the MLP.

EfficientNet-B0 has two branching ops the MLP/dense-chain nets don't: the MBConv residual skip (additive fan-in) and the squeeze-excite gate (multiplicative fan-in). The SHlo backward inductive only has unary backward constructors (convBack, swishBack, denseRowBack, …), but the fan-ins are expressible with the existing forward elementwise combinators: addV (den (.addV a b) = den a + den b) for the residual here, and layerScaleF (Hadamard by a known activation vector) + addV for SE.

This file proves the residual case in general, then closes a fully concrete instance (a dense body) end-to-end with no remaining hypothesis.

def Proofs.StableHLO.residualBackGraph {n : ℕ} (fBack ecot : SHlo n) : SHlo n

Backward graph for a residual block x ↦ x + f x, given a subgraph fBack that renders the body f's input-cotangent. The identity skip contributes the cotangent verbatim (%dy); addV sums the two paths. This is the renderable image of residual_has_vjp's biPath backward.

Equations

• Proofs.StableHLO.residualBackGraph fBack ecot = fBack.addV ecot

theorem Proofs.StableHLO.residualBackGraph_faithful {n : ℕ} (f : Vec n → Vec n) (hf_diff : Differentiable ℝ f) (hf : HasVJP f) (x : Vec n) (ecot fBack : SHlo n) (hfb : den fBack = hf.backward x (den ecot)) : den (residualBackGraph fBack ecot) = (residual_has_vjp f hf_diff hf).backward x (den ecot)

Residual additive-fan-in backward faithfulness (general). If fBack denotes the body's VJP backward (den fBack = hf.backward x dy), then the residual backward graph denotes the proven residual_has_vjp backward, which is f.backward x dy + dy. The proof is structural — the only definitional facts are den (addV a b) = den a + den b and the identity skip's backward = dy — so it composes without a whole-net terminal rfl.

def Proofs.StableHLO.seBlockBackGraph {n : ℕ} (gateBack : SHlo n) (gateVal dy : Vec n) : SHlo n

Backward graph for an SE block x ↦ x ⊙ gate x, given a subgraph gateBack rendering the gate sub-network's input-cotangent at the SE-specific cotangent x ⊙ dy. The main (identity) path contributes gate x ⊙ dy, rendered as a Hadamard (layerScaleF) of the cotangent by the gate activation; addV sums the two paths. The renderable image of seBlock_has_vjp's elemwiseProduct (bi-cotangent) backward.

Equations

• Proofs.StableHLO.seBlockBackGraph gateBack gateVal dy = (Proofs.StableHLO.SHlo.layerScaleF "%segate" gateVal (Proofs.StableHLO.SHlo.operand "%dy" dy)).addV gateBack

theorem Proofs.StableHLO.seBlockBackGraph_faithful {n : ℕ} (gate : Vec n → Vec n) (hg_diff : Differentiable ℝ gate) (hg : HasVJP gate) (x dy : Vec n) (gateBack : SHlo n) (hgb : den gateBack = hg.backward x fun (j : Fin n) => x j * dy j) : den (seBlockBackGraph gateBack (gate x) dy) = (seBlock_has_vjp gate hg_diff hg).backward x dy

SE multiplicative fan-in backward faithfulness (general). If gateBack denotes the gate path's VJP backward at the cotangent x ⊙ dy (den gateBack = hg.backward x (x ⊙ dy)), then the SE backward graph denotes the proven seBlock_has_vjp backward, which is gate x ⊙ dy + gate.backward x (x ⊙ dy). Like the residual brick the proof is structural — the composition is delegated to gateBack, so the only definitional facts are layerScaleF/addV denotation and the identity main-path backward.

noncomputable def Proofs.StableHLO.seGateBackGraph {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (x u : Vec (c * h * w)) : SHlo (c * h * w)

The SE gate's backward graph. The gate is broadcastFlat ∘ sigmoid ∘ dense W₂ ∘ swish ∘ dense W₁ ∘ GAP, so its VJP backward (reverse order) is gapBack ∘ denseᵀW₁ ∘ swishBack ∘ denseᵀW₂ ∘ sigmoidBack ∘ broadcastBack, each per-op back applied at the matching forward activation.

Equations

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

theorem Proofs.StableHLO.seGate_backGraph_faithful {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (x dy : Vec (c * h * w)) : den (seGateBackGraph W₁ b₁ W₂ b₂ x fun (j : Fin (c * h * w)) => x j * dy j) = (seGate_has_vjp W₁ b₁ W₂ b₂).backward x fun (j : Fin (c * h * w)) => x j * dy j

The concrete SE gate's backward graph is faithful to seGate_has_vjp. Assembles gapBack/swishBack/sigmoidBack/broadcastBack + the two dense dotOut backs into the gate's whole VJP. Closes the gateBack hypothesis of seBlockBackGraph_faithful for the real EfficientNet gate.

theorem Proofs.StableHLO.bnBack_faithful_fn {n : ℕ} (gN xN es : String) (ε γ β : ℝ) (hε : 0 < ε) (x : Vec n) (e : SHlo n) : den (SHlo.bnBack gN xN es ε γ x e) = (bn_has_vjp n ε γ β hε).backward x (den e)

Function-level BatchNorm backward bridge. bnBack denotes bn_grad_input, which is NOT rfl-equal to (bn_has_vjp …).backward (the witness is built via a rw [bnForward_eq_compose] cast). They agree through the canonical VJP sum: bnBack_faithful gives the ∑ pdiv form and bn_has_vjp.correct matches it. This lemma is the one non-rfl bridge the bn-containing stages need.

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

conv → bn → swish backward graph (the MBConv expand stage), at input x, cotangent subgraph e: convBack ∘ bnBack ∘ swishBack.

Equations

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

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

noncomputable def Proofs.StableHLO.dwBnSwishBackGraph {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε γ β : ℝ) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : SHlo (c * h * w)

depthwise → bn → swish backward graph (the MBConv depthwise stage).

Equations

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

theorem Proofs.StableHLO.dwBnSwishBackGraph_faithful {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε γ β : ℝ) (hε : 0 < ε) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : den (dwBnSwishBackGraph W b ε γ β x e) = (dwBnSwish_has_vjp W b ε γ β hε).backward x (den e)

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

conv → bn backward graph (the MBConv project stage, no swish).

Equations

• Proofs.StableHLO.convBnBackGraph W b ε γ _β x e = Proofs.StableHLO.SHlo.convBack "%pW" W b x (Proofs.StableHLO.SHlo.bnBack "%pG" "%pX" "pE" ε γ (Proofs.flatConv W b x) e)

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

noncomputable def Proofs.StableHLO.seGateBackGraphE {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : SHlo (c * h * w)

SE gate backward graph taking a cotangent subgraph e (not a %dy operand), so it can sit mid-chain inside the MBConv body.

Equations

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

theorem Proofs.StableHLO.seGateBackGraphE_faithful {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : den (seGateBackGraphE W₁ b₁ W₂ b₂ x e) = (seGate_has_vjp W₁ b₁ W₂ b₂).backward x (den e)

noncomputable def Proofs.StableHLO.seBlockFullBackGraphE {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : SHlo (c * h * w)

SE block backward graph, subgraph-cotangent form: main path gate(x) ⊙ (den e) via layerScaleF, gate path fed x ⊙ (den e).

Equations

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

theorem Proofs.StableHLO.seBlockFullBackGraphE_faithful {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : den (seBlockFullBackGraphE W₁ b₁ W₂ b₂ x e) = (seBlockFull_has_vjp W₁ b₁ W₂ b₂).backward x (den e)

noncomputable def Proofs.StableHLO.mbconvBodyBackGraph {c cmid h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid c kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 c cmid kHp kWp) (bp : Vec c) (εp γp βp : ℝ) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : SHlo (c * h * w)

The MBConv body backward graph E⁻¹ ∘ D⁻¹ ∘ S⁻¹ ∘ P⁻¹, each stage at its cumulative forward activation. cin = cout = c (stride-1 residual block).

Equations

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

theorem Proofs.StableHLO.mbconvBodyBackGraph_faithful {c cmid h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid c kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (hεd : 0 < εd) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 c cmid kHp kWp) (bp : Vec c) (εp γp βp : ℝ) (hεp : 0 < εp) (x : Vec (c * h * w)) (e : SHlo (c * h * w)) : den (mbconvBodyBackGraph We be εe γe βe Wd bd εd γd βd Ws₁ bs₁ Ws₂ bs₂ Wp bp εp γp βp x e) = (mbconvBody_has_vjp We be εe γe βe hεe Wd bd εd γd βd hεd Ws₁ bs₁ Ws₂ bs₂ Wp bp εp γp βp hεp).backward x (den e)

theorem Proofs.StableHLO.bnBatchBack_faithful {N oc h w : ℕ} (gN xN es : String) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) (x : Vec (N * (oc * (h * w)))) (e : SHlo (N * (oc * (h * w)))) : den (SHlo.bnBatchBack gN xN es ε γ x e) = (bnBatchTensor4_has_vjp N oc h w ε hε γ β).backward x (den e)

bnBatchBack (true batch-norm backward) faithfulness. The first batched-backward primitive: bnBatchBack denotes the proven bnBatchTensor4 VJP backward (batch-COUPLED batch-norm on [N,C,H,W], reduce over [0,2,3] per channel) via the renderable three-term bnBatchTensor4_grad_input. This is the genuinely-new op the batched MBConv stages need (their bn is bnBatchLA, not a per-example batchMap); the other batched stages (conv/depthwise/SE) are batchMap of the per-example backwards already proven above. The bnBatchLA layout-reindex wrapper to the network's N·(oc·h·w) index is a thin remaining layer.

theorem Proofs.StableHLO.convBackBatched_faithful {N ic oc h w kH kW : ℕ} (wN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (v : Vec (N * (ic * h * w))) (e : SHlo (N * (oc * h * w))) : den (SHlo.convBackBatched wN W b e) = (batchMap_has_vjp (flatConv W b) (flatConv_has_vjp W b) ⋯).backward v (den e)

Batched conv input-VJP faithfulness. convBackBatched denotes the proven VJP of the batched conv batchMap N (flatConv W b) — i.e. the per-example conv input-grad applied independently across the batch. Conv is linear, so its backward ignores the forward activation; the batched backward is a plain batchMap of the per-example backward, matching batchMap_has_vjp. The second batch-separable stage brick (after seB); together with bnBatchBack these are the batched MBConv's per-stage backward pieces.

theorem Proofs.StableHLO.convStridedBackBatched_faithful {N ic oc h w kH kW : ℕ} (wN : String) (W : Kernel4 oc ic kH kW) (b : Vec oc) (v : Vec (N * (ic * (2 * h) * (2 * w)))) (e : SHlo (N * (oc * h * w))) : den (SHlo.convStridedBackBatched wN W b e) = (batchMap_has_vjp (flatConvStride2 W b) (flatConvStride2_has_vjp W b) ⋯).backward v (den e)

Batched STRIDE-2 conv input-VJP faithfulness. The stride-2 analogue of convBackBatched_faithful: convStridedBackBatched denotes the proven VJP of the batched strided conv batchMap N (flatConvStride2 W b) — i.e. the per-example strided-conv input-grad (flatConvStride2_has_vjp = zero-upsample the cotangent then the reversed-kernel conv) applied independently across the batch. Strided conv (decimate ∘ conv) is linear, so its backward ignores the forward activation; the batched backward is a plain batchMap of the per-example backward, matching batchMap_has_vjp. The downsample basic-block's stride-2 conv1 backward brick.

theorem Proofs.StableHLO.depthwiseStridedBackBatched_faithful {N c h w kH kW : ℕ} (wN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (v : Vec (N * (c * (2 * h) * (2 * w)))) (e : SHlo (N * (c * h * w))) : den (SHlo.depthwiseStridedBackBatched wN W b e) = (batchMap_has_vjp (depthwiseStride2Flat W b) (depthwiseStride2Flat_has_vjp W b) ⋯).backward v (den e)

Batched STRIDE-2 depthwise input-VJP faithfulness. The stride-2 analogue of depthwiseBackBatched_faithful (and the depthwise analogue of convStridedBackBatched_faithful): depthwiseStridedBackBatched denotes the proven VJP of the batched strided depthwise batchMap N (depthwiseStride2Flat W b) — i.e. the per-example strided-depthwise input-grad (depthwiseStride2Flat_has_vjp = zero-upsample the cotangent then the reversed-kernel per-channel depthwise) applied independently across the batch. Strided depthwise (decimate ∘ depthwise) is linear, so its backward ignores the forward activation; the batched backward is a plain batchMap of the per-example backward, matching batchMap_has_vjp. The EfficientNet downsample MBConv's stride-2 depthwise backward brick.

theorem Proofs.StableHLO.depthwiseStridedXlaBackBatched_faithful {N c h w kH kW : ℕ} (wN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (v : Vec (N * (c * (2 * h) * (2 * w)))) (e : SHlo (N * (c * h * w))) : den (SHlo.depthwiseStridedXlaBackBatched wN W b e) = (batchMap_has_vjp (depthwiseStride2FlatXla W b) (depthwiseStride2FlatXla_has_vjp W b) ⋯).backward v (den e)

Batched XLA-SAME STRIDE-2 depthwise input-VJP faithfulness. The odd-phase peer of depthwiseStridedBackBatched_faithful: depthwiseStridedXlaBackBatched (pad [p+1, p-1], the token MobileNetV2's Adam render emits at its four strided depthwises) denotes the proven VJP of batchMap N (depthwiseStride2FlatXla W b). Same proof: a scatter onto the odd positions is as linear as one onto the even ones.

theorem Proofs.StableHLO.depthwiseBackBatched_faithful {N c h w kH kW : ℕ} (wN : String) (W : DepthwiseKernel c kH kW) (b : Vec c) (v : Vec (N * (c * h * w))) (e : SHlo (N * (c * h * w))) : den (SHlo.depthwiseBackBatched wN W b e) = (batchMap_has_vjp (depthwiseFlat W b) (depthwiseFlat_has_vjp W b) ⋯).backward v (den e)

Batched depthwise input-VJP faithfulness. The depthwise analogue of convBackBatched_faithful: depthwiseBackBatched denotes the proven VJP of the batched depthwise batchMap N (depthwiseFlat W b). Depthwise conv is linear, so its backward is activation-independent and the batched backward is a plain batchMap of the per-example backward. The MBConv depthwise stage's batch-separable backward brick.

theorem Proofs.StableHLO.bnBatchLA_back_conj {N oc h w : ℕ} (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) (x dy : Vec (N * (oc * h * w))) : (reindex_has_vjp (Fin.cast ⋯)).backward x (bnBatchTensor4_grad_input N oc h w ε γ ((reindexCLM (Fin.cast ⋯)) x) ((reindex_has_vjp (Fin.cast ⋯)).backward ((reindexCLM (Fin.cast ⋯)) x) dy)) = (bnBatchLA_has_vjp N oc h w ε hε γ β).backward x dy

bnBatchLA backward = reindex-conjugated bnBatchTensor4 backward. The network indexes at N·(oc·h·w) (left-assoc) but the proven true-BN bnBatchTensor4 lives at N·(oc·(h·w)); bnBatchLA bridges by conjugating with the associativity-cast reindexes (bnBatchLA_eq_comp). Its VJP backward is therefore: scatter the cotangent into [N,C,(H·W)], run the renderable three-term bnBatchTensor4_grad_input at the reindexed activation, scatter back. This is what a network-layout bnBatchLABack op denotes.

theorem Proofs.StableHLO.bnBatchLABack_faithful {N oc h w : ℕ} (gN xN es : String) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) (x : Vec (N * (oc * h * w))) (e : SHlo (N * (oc * h * w))) : den (SHlo.bnBatchLABack gN xN es ε γ x e) = (bnBatchLA_has_vjp N oc h w ε hε γ β).backward x (den e)

bnBatchLABack (network-layout true batch-norm backward) faithfulness. The den (inline scatter-conjugated bnBatchTensor4_grad_input) equals the proven bnBatchLA_has_vjp backward — the bn backward at the network's N·(oc·h·w) index. This is the layout wrapper that lets bnBatchBack compose with convBackBatched / depthwiseBackBatched (all on the left-assoc index) into batched stages.

theorem Proofs.StableHLO.seBackBatched_faithful {N c h w r : ℕ} (w1N b1N w2N b2N vN : String) (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) (v : Vec (N * (c * h * w))) (e : SHlo (N * (c * h * w))) : den (SHlo.seBackBatched w1N b1N w2N b2N vN W₁ b₁ W₂ b₂ v e) = (seB_has_vjp N W₁ b₁ W₂ b₂).backward v (den e)

seBackBatched (batched squeeze-excite backward) faithfulness. The den (rowwise application of the proven per-example seBlockFull VJP) equals the proven batched seB_has_vjp backward. SE is non-linear, so — unlike the linear convBackBatched/depthwiseBackBatched — the backward threads each example's forward activation v; the rowwise batchMap_has_vjp structure handles that. The fourth (and last) MBConv stage's batch-separable backward.

noncomputable def Proofs.StableHLO.cbsBackBatchedGraph {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 → swish stage backward graph (MBConv expand), at the network layout: convBackBatched ∘ bnBatchLABack ∘ swishBack, each at its cumulative forward activation.

Equations

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

theorem Proofs.StableHLO.cbsBackBatchedGraph_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))) : den (cbsBackBatchedGraph W b ε γ β x e) = (cbsB_has_vjp N W b ε hε γ β).backward x (den e)

noncomputable def Proofs.StableHLO.dwbsBackBatchedGraph {N c h w kH kW : ℕ} (W : DepthwiseKernel 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))

Batched depthwise → bn → swish stage backward graph (MBConv depthwise).

Equations

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

theorem Proofs.StableHLO.dwbsBackBatchedGraph_faithful {N c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * h * w))) (e : SHlo (N * (c * h * w))) : den (dwbsBackBatchedGraph W b ε γ β x e) = (dwbsB_has_vjp N W b ε hε γ β).backward x (den e)

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

Batched STRIDE-2 depthwise → bn → swish stage backward graph (the EfficientNet downsample MBConv's depthwise). The stride-2 analogue of dwbsBackBatchedGraph: the bn/swish run at the OUTPUT spatial h×w, then depthwiseStridedBackBatched maps the bn-cotangent back to the larger input c·(2h)·(2w) (zero-upsample + reversed-kernel per-channel depthwise).

Equations

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

theorem Proofs.StableHLO.dwbsSBackBatchedGraph_faithful {N c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * (2 * h) * (2 * w)))) (e : SHlo (N * (c * h * w))) : den (dwbsSBackBatchedGraph W b ε γ β x e) = (dwbsSB_has_vjp N W b ε hε γ β).backward x (den e)

noncomputable def Proofs.StableHLO.projBackBatchedGraph {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 stage backward graph (MBConv project, no swish).

Equations

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

theorem Proofs.StableHLO.projBackBatchedGraph_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))) : den (projBackBatchedGraph W b ε γ β x e) = (projB_has_vjp N W b ε hε γ β).backward x (den e)

noncomputable def Proofs.StableHLO.mbBodyB_has_vjp (N : ℕ) {c mid h w kHd kWd r : ℕ} (We : Kernel4 mid c 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp : Vec c) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec c) : HasVJP (projB N Wp bp εp γp βp ∘ seB N Wz₁ bz₁ Wz₂ bz₂ ∘ dwbsB N Wd bd εd γd βd ∘ cbsB N We be εe γe βe)

The batched MBConv body's VJP — projB ∘ seB ∘ dwbsB ∘ cbsB, reconstructed as the exact vjp_comp chain mbResidFwdB_has_vjp builds inline (vBody).

Equations

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

noncomputable def Proofs.StableHLO.mbBodyBackBatchedGraph {N c mid h w kHd kWd r : ℕ} (We : Kernel4 mid c 1 1) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp : Vec c) (εp : ℝ) (γp βp : Vec c) (x : Vec (N * (c * h * w))) (e : SHlo (N * (c * h * w))) : SHlo (N * (c * h * w))

The batched MBConv body backward graph: the four stage graphs chained at their cumulative forward activations (cbsB⁻¹ ∘ dwbsB⁻¹ ∘ seB⁻¹ ∘ projB⁻¹).

Equations

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

theorem Proofs.StableHLO.mbBodyBackBatchedGraph_faithful {N c mid h w kHd kWd r : ℕ} (We : Kernel4 mid c 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp : Vec c) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec c) (x : Vec (N * (c * h * w))) (e : SHlo (N * (c * h * w))) : den (mbBodyBackBatchedGraph We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp x e) = (mbBodyB_has_vjp N We be εe hεe γe βe Wd bd εd hεd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp hεp γp βp).backward x (den e)

noncomputable def Proofs.StableHLO.mbDownBodyB_has_vjp (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) : HasVJP (projB N Wp bp εp γp βp ∘ seB N Wz₁ bz₁ Wz₂ bz₂ ∘ dwbsSB N Wd bd εd γd βd ∘ cbsB N We be εe γe βe)

The batched downsample MBConv body's VJP — projB ∘ seB ∘ dwbsSB ∘ cbsB, the stride-2 analogue of mbBodyB_has_vjp (swaps the stride-1 dwbsB depthwise stage for the STRIDED dwbsSB). The expand cbsB runs at the larger 2h×2w, the strided depthwise then halves spatial to h×w; the rest at h×w. No residual (spatial/channels change), so this is the body alone — reconstructed as the exact vjp_comp chain mbStridedFwdB_has_vjp builds inline.

Equations

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

noncomputable def Proofs.StableHLO.mbDownBodyBackBatchedGraph {N ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (γp βp : 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 downsample MBConv body backward graph: the four stage graphs chained at their cumulative forward activations (cbsB⁻¹ ∘ dwbsSB⁻¹ ∘ seB⁻¹ ∘ projB⁻¹). Stride-2 analogue of mbBodyBackBatchedGraph (strided depthwise stage graph).

Equations

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

theorem Proofs.StableHLO.mbDownBodyBackBatchedGraph_faithful {N ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) (x : Vec (N * (ic * (2 * h) * (2 * w)))) (e : SHlo (N * (oc * h * w))) : den (mbDownBodyBackBatchedGraph We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp x e) = (mbDownBodyB_has_vjp N We be εe hεe γe βe Wd bd εd hεd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp hεp γp βp).backward x (den e)

CAPSTONE — the batched EfficientNet DOWNSAMPLE MBConv body: backward graph ↔ the proven mbDownBodyB_has_vjp. The four batched stage backward graphs (cbsB/dwbsSB/seB/projB) chained at their forward activations, proven equal to the downsample-body VJP. The stride-2 analogue of mbBodyBackBatchedGraph_faithful (no residual skip — the downsample block changes spatial/channels, so the body alone is the block). EfficientNet uses swish (a global VJP), so this stays in the clean global HasVJP/vjp_comp form (no _at recompute, unlike r34/mnv2's relu blocks).

noncomputable def Proofs.StableHLO.mbResidBlockBackBatchedGraph {N c mid h w kHd kWd r : ℕ} (We : Kernel4 mid c 1 1) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp : Vec c) (εp : ℝ) (γp βp : Vec c) (x : Vec (N * (c * h * w))) (ecot : SHlo (N * (c * h * w))) : SHlo (N * (c * h * w))

The whole batched MBConv residual block backward graph (body + identity skip).

Equations

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

theorem Proofs.StableHLO.mbResidBlockBackBatchedGraph_faithful {N c mid h w kHd kWd r : ℕ} (We : Kernel4 mid c 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 c mid 1 1) (bp : Vec c) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec c) (x : Vec (N * (c * h * w))) (ecot : SHlo (N * (c * h * w))) : den (mbResidBlockBackBatchedGraph We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp x ecot) = (mbResidFwdB_has_vjp N We be εe hεe γe βe Wd bd εd hεd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp hεp γp βp).backward x (den ecot)

CAPSTONE — the whole batched EfficientNet MBConv residual block: backward graph ↔ the proven mbResidFwdB_has_vjp. The four batched stage backward graphs (cbsB/dwbsB/seB/projB) chained at their forward activations + the identity skip, proven equal to the repo's batched MBConv block VJP.