Backward-graph faithfulness for the VERIFIED MobileNetV2 inverted-residual block

The MobileNetV2 peer of EfficientNetBackB0.lean: a backward StableHLO graph that denotes the proven VJP of the batched MobileNetV2 inverted-residual block — project ∘ depthwise-bn-relu6 ∘ expand-bn-relu6 with the linear-bottleneck skip.

The block is the EfficientNet MBConv body minus the squeeze-excite stage, with relu6 in place of swish and the same linear-bottleneck projB (1×1 conv → bn, no activation). The project stage and the residual fan-in are reused VERBATIM from the EfficientNet file (they are global/clean — no smoothness wrinkle).

The relu6 wrinkle

Unlike swish (smooth everywhere, GLOBAL swish_has_vjp), relu6 has a TWO-SIDED kink (at 0 and at 6), so its VJP is only the pointwise relu6_has_vjp_at, conditioned on the smoothness hypothesis ∀ k, x k ≠ 0 ∧ x k ≠ 6 at the pre-activation. Its per-op backward token is .selectMid (the mask if 0<x<6 then dy else 0), whose denotation faithfulness is the already-proven (rfl) selectMid_faithful (StableHLO.lean:794).

Because relu6's VJP is _at, the whole MobileNetV2 stage/body VJP and its backward- graph faithfulness are stated in the _at / hypothesis-threaded form (via vjp_comp_at, lifting the global bnBatchLA/batchMap/conv/depthwise VJPs through HasVJP.toHasVJPAt), NOT the EfficientNet global form. The relu6 smoothness hypothesis at the pre-relu6 activation bnBatchLA(…)(batchMap(conv)(x)) is threaded through; the bn/conv/depthwise pieces stay activation-independent (linear) or global.

Structure

• cbrB / dwbrB — batched conv/depthwise → bn → relu6 stages (cbsB/dwbsB with relu6 for swish), with _at differentiability + VJP and backward-graph faithfulness (cbrBackBatchedGraph + …_faithful).
• cbrLayer / dwbrLayer / dwbrStridedLayer / projLayer — the four stages as CertLayers. mnv2BodyLayer / mnv2DownBodyLayer compose them with CertLayer.comp, and each body VJP, differentiability lemma and graph _faithful is that layer's vjp / diff / faithful.
• mnv2BodyB_has_vjp_at — the SE-less body projB ∘ dwbrB ∘ cbrB at the relu6 smoothness families, with its backward graph mnv2BodyBackBatchedGraph + …_faithful. ⚠ This family takes ic and oc SEPARATELY (2026-09-06). It was written for the residual block and pinned them equal, which is right there but wrong one level up: the paper ladder's b11 (64 → 96) and b17 (160 → 320) are stride-1 bodies with ic ≠ oc, and MobileNetV2FullB.lean's mnv2ExpOnlyB is exactly that shape. Generalising changed no proof — mnv2DownBodyB already had this shape, and every existing call site (BackNetFolds.lean) is at ic = oc and infers it.
• mnv2ResidBlockBackBatchedGraph_faithful — the CAPSTONE: the whole batched MobileNetV2 inverted-residual block backward graph (body + identity skip) denotes the proven residual_has_vjp_at of the SE-less body. Mirrors the EfficientNet mbResidBlockBackBatchedGraph_faithful without the seB factor, threaded through the relu6 smoothness hypotheses; CertLayer.residual mnv2BodyLayer's faithful.

@[reducible]

noncomputable def Proofs.StableHLO.cbrB (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 → relu6 stage (MobileNetV2 expand), at the network layout N·(oc·h·w). Identical to EfficientNet's cbsB but with relu6 for swish.

Equations

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

@[reducible]

noncomputable def Proofs.StableHLO.dwbrB (N : ℕ) {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β : Vec c) : Vec (N * (c * h * w)) → Vec (N * (c * h * w))

Batched depthwise → bn → relu6 stage (MobileNetV2 depthwise), at the network layout. Identical to EfficientNet's dwbsB but with relu6 for swish.

Equations

• Proofs.StableHLO.dwbrB N W b ε γ β = Proofs.relu6 (N * (c * h * w)) ∘ Proofs.StableHLO.bnBatchLA N c h w ε γ β ∘ Proofs.StableHLO.batchMap N (Proofs.depthwiseFlat W b)

@[reducible]

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

Batched STRIDE-2 depthwise → bn → relu6 stage (MobileNetV2 downsample depthwise), at the network layout. The stride-2 analogue of dwbrB: maps the larger input spatial c·(2h)·(2w) to the output spatial c·h·w. Identical to EfficientNet's dwbsSB but with relu6 for swish.

Equations

• Proofs.StableHLO.dwbrBstrided N W b ε γ β = Proofs.relu6 (N * (c * h * w)) ∘ Proofs.StableHLO.bnBatchLA N c h w ε γ β ∘ Proofs.StableHLO.batchMap N (Proofs.depthwiseStride2FlatXla W b)

noncomputable def Proofs.StableHLO.bnRelu6Stage_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 ∧ bnBatchLA N oc h w ε γ β (batchMap N op x) k ≠ 6) : HasVJPAt (relu6 (N * (oc * h * w)) ∘ bnBatchLA N oc h w ε γ β ∘ batchMap N op) x

Generic relu6-on-batched-bn-stage _at VJP. The relu6 analogue of bnSwishStage_has_vjp, but _at (relu6 only has a pointwise VJP): compose the batched-op VJP, the true-BN VJP (both global, lifted via .toHasVJPAt), and relu6's pointwise VJP at the pre-relu6 activation.

Equations

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

theorem Proofs.StableHLO.bnRelu6Stage_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 ∧ bnBatchLA N oc h w ε γ β (batchMap N op x) k ≠ 6) : DifferentiableAt ℝ (relu6 (N * (oc * h * w)) ∘ bnBatchLA N oc h w ε γ β ∘ batchMap N op) x

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

noncomputable def Proofs.StableHLO.cbrB_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 ∧ bnBatchLA N oc h w ε γ β (batchMap N (flatConv W b) x) k ≠ 6) : HasVJPAt (cbrB N W b ε γ β) x

cbrB (conv-bn-relu6) _at VJP at a smooth point.

Equations

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

theorem Proofs.StableHLO.cbrB_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 ∧ bnBatchLA N oc h w ε γ β (batchMap N (flatConv W b) x) k ≠ 6) : DifferentiableAt ℝ (cbrB N W b ε γ β) x

noncomputable def Proofs.StableHLO.dwbrB_has_vjp_at (N : ℕ) {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * h * w))) (h_smooth : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε γ β (batchMap N (depthwiseFlat W b) x) k ≠ 0 ∧ bnBatchLA N c h w ε γ β (batchMap N (depthwiseFlat W b) x) k ≠ 6) : HasVJPAt (dwbrB N W b ε γ β) x

dwbrB (depthwise-bn-relu6) _at VJP at a smooth point.

Equations

• Proofs.StableHLO.dwbrB_has_vjp_at N W b ε hε γ β x h_smooth = Proofs.StableHLO.bnRelu6Stage_has_vjp_at N (Proofs.depthwiseFlat W b) ⋯ (Proofs.depthwiseFlat_has_vjp W b) ε hε γ β x h_smooth

theorem Proofs.StableHLO.dwbrB_differentiableAt (N : ℕ) {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (hε : 0 < ε) (γ β : Vec c) (x : Vec (N * (c * h * w))) (h_smooth : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε γ β (batchMap N (depthwiseFlat W b) x) k ≠ 0 ∧ bnBatchLA N c h w ε γ β (batchMap N (depthwiseFlat W b) x) k ≠ 6) : DifferentiableAt ℝ (dwbrB N W b ε γ β) x

noncomputable def Proofs.StableHLO.dwbrBstrided_has_vjp_at (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)))) (h_smooth : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε γ β (batchMap N (depthwiseStride2FlatXla W b) x) k ≠ 0 ∧ bnBatchLA N c h w ε γ β (batchMap N (depthwiseStride2FlatXla W b) x) k ≠ 6) : HasVJPAt (dwbrBstrided N W b ε γ β) x

dwbrBstrided (STRIDE-2 depthwise-bn-relu6) _at VJP at a smooth point. The stride-2 analogue of dwbrB_has_vjp_at: lifts depthwiseStride2FlatXla_has_vjp (the strided per-channel conv input-VJP) through the generic relu6-bn stage.

Equations

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

theorem Proofs.StableHLO.dwbrBstrided_differentiableAt (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)))) (h_smooth : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε γ β (batchMap N (depthwiseStride2FlatXla W b) x) k ≠ 0 ∧ bnBatchLA N c h w ε γ β (batchMap N (depthwiseStride2FlatXla W b) x) k ≠ 6) : DifferentiableAt ℝ (dwbrBstrided N W b ε γ β) x

noncomputable def Proofs.StableHLO.cbrBackBatchedGraph {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 → relu6 stage backward graph (MobileNetV2 expand): convBackBatched ∘ bnBatchLABack ∘ selectMid, each at its cumulative forward activation. The relu6 analogue of cbsBackBatchedGraph — .selectMid (the relu6 two-sided-kink mask) replaces .swishBack.

Equations

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

theorem Proofs.StableHLO.cbrBackBatchedGraph_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 ∧ bnBatchLA N oc h w ε γ β (batchMap N (flatConv W b) x) k ≠ 6) : den (cbrBackBatchedGraph W b ε γ β x e) = (cbrB_has_vjp_at N W b ε hε γ β x h_smooth).backward (den e)

noncomputable def Proofs.StableHLO.dwbrBackBatchedGraph {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 → relu6 stage backward graph (MobileNetV2 depthwise).

Equations

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

theorem Proofs.StableHLO.dwbrBackBatchedGraph_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))) (h_smooth : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε γ β (batchMap N (depthwiseFlat W b) x) k ≠ 0 ∧ bnBatchLA N c h w ε γ β (batchMap N (depthwiseFlat W b) x) k ≠ 6) : den (dwbrBackBatchedGraph W b ε γ β x e) = (dwbrB_has_vjp_at N W b ε hε γ β x h_smooth).backward (den e)

noncomputable def Proofs.StableHLO.dwbrBstridedBackBatchedGraph {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 → relu6 stage backward graph (MobileNetV2 downsample depthwise). The stride-2 analogue of dwbrBackBatchedGraph: the bn/relu6 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). The relu6 back is .selectMid as before.

Equations

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

theorem Proofs.StableHLO.dwbrBstridedBackBatchedGraph_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))) (h_smooth : ∀ (k : Fin (N * (c * h * w))), bnBatchLA N c h w ε γ β (batchMap N (depthwiseStride2FlatXla W b) x) k ≠ 0 ∧ bnBatchLA N c h w ε γ β (batchMap N (depthwiseStride2FlatXla W b) x) k ≠ 6) : den (dwbrBstridedBackBatchedGraph W b ε γ β x e) = (dwbrBstrided_has_vjp_at N W b ε hε γ β x h_smooth).backward (den e)

noncomputable def Proofs.StableHLO.cbrLayer (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 → relu6 stage as a CertLayer, certified where its pre-relu6 activation misses both kinks. 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.

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

The depthwise → bn → relu6 stage as a CertLayer.

Equations

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

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

The stride-2 depthwise → bn → relu6 stage as a CertLayer: 2h × 2w in, h × w out.

Equations

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

noncomputable def Proofs.StableHLO.projLayer (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 stage (projB, no activation) as a CertLayer. Globally certified (ok = True): with no activation there is no kink.

Equations

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

noncomputable def Proofs.StableHLO.mnv2BodyLayer (N : ℕ) {ic mid oc h w kHd kWd : ℕ} (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) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) : CertLayer (N * (ic * h * w)) (N * (oc * h * w))

The SE-less body as a CertLayer: cbrLayer ; dwbrLayer ; projLayer, left-nested so its fwd is projB ∘ (dwbrB ∘ cbrB), the association the stated types use. Its ok is the expand and depthwise relu6 clauses; projLayer contributes True.

Equations

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

noncomputable def Proofs.StableHLO.mnv2BodyB_has_vjp_at (N : ℕ) {ic mid oc h w kHd kWd : ℕ} (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) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) (x : Vec (N * (ic * h * w))) (h_se : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 0 ∧ bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 6) (h_sd : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 0 ∧ bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 6) : HasVJPAt (projB N Wp bp εp γp βp ∘ dwbrB N Wd bd εd γd βd ∘ cbrB N We be εe γe βe) x

The batched MobileNetV2 inverted-residual body's VJP at a smooth point — projB ∘ dwbrB ∘ cbrB (the EfficientNet MBConv body MINUS seB, with relu6 for swish), mnv2BodyLayer's VJP.

h_se is the expand relu6 smoothness (at the cbrB pre-relu6 activation); h_sd is the depthwise relu6 smoothness (at the dwbrB pre-relu6 activation, fed the cbrB output).

Equations

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

theorem Proofs.StableHLO.mnv2BodyB_differentiableAt (N : ℕ) {ic mid oc h w kHd kWd : ℕ} (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) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) (x : Vec (N * (ic * h * w))) (h_se : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 0 ∧ bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 6) (h_sd : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 0 ∧ bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 6) : DifferentiableAt ℝ (projB N Wp bp εp γp βp ∘ dwbrB N Wd bd εd γd βd ∘ cbrB N We be εe γe βe) x

noncomputable def Proofs.StableHLO.mnv2BodyBackBatchedGraph {N ic mid oc h w kHd kWd : ℕ} (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) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (x : Vec (N * (ic * h * w))) (e : SHlo (N * (oc * h * w))) : SHlo (N * (ic * h * w))

The batched MobileNetV2 body backward graph: the three stage graphs chained at their cumulative forward activations (cbrB⁻¹ ∘ dwbrB⁻¹ ∘ projB⁻¹).

Equations

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

theorem Proofs.StableHLO.mnv2BodyBackBatchedGraph_faithful {N ic mid oc h w kHd kWd : ℕ} (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) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) (x : Vec (N * (ic * h * w))) (e : SHlo (N * (oc * h * w))) (h_se : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 0 ∧ bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 6) (h_sd : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 0 ∧ bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 6) : den (mnv2BodyBackBatchedGraph We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp x e) = (mnv2BodyB_has_vjp_at N We be εe hεe γe βe Wd bd εd hεd γd βd Wp bp εp hεp γp βp x h_se h_sd).backward (den e)

noncomputable def Proofs.StableHLO.mnv2DownBodyLayer (N : ℕ) {ic mid oc h w kHd kWd : ℕ} (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) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) : CertLayer (N * (ic * (2 * h) * (2 * w))) (N * (oc * h * w))

The downsample body as a CertLayer: cbrLayer at 2h × 2w, then dwbrStridedLayer and projLayer at h × w.

Equations

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

noncomputable def Proofs.StableHLO.mnv2DownBodyB_has_vjp_at (N : ℕ) {ic mid oc h w kHd kWd : ℕ} (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) (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)))) (h_se : ∀ (k : Fin (N * (mid * (2 * h) * (2 * w)))), bnBatchLA N mid (2 * h) (2 * w) εe γe βe (batchMap N (flatConv We be) x) k ≠ 0 ∧ bnBatchLA N mid (2 * h) (2 * w) εe γe βe (batchMap N (flatConv We be) x) k ≠ 6) (h_sd : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseStride2FlatXla Wd bd) (cbrB N We be εe γe βe x)) k ≠ 0 ∧ bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseStride2FlatXla Wd bd) (cbrB N We be εe γe βe x)) k ≠ 6) : HasVJPAt (projB N Wp bp εp γp βp ∘ dwbrBstrided N Wd bd εd γd βd ∘ cbrB N We be εe γe βe) x

The batched MobileNetV2 DOWNSAMPLE inverted-residual body's VJP at a smooth point — projB ∘ dwbrBstrided ∘ cbrB, the stride-2 analogue of mnv2BodyB_has_vjp_at (swaps the stride-1 dwbrB depthwise stage for the STRIDED dwbrBstrided). The expand cbrB runs at the larger 2h×2w (1×1 conv keeps spatial), the strided depthwise then halves spatial to h×w; project runs at h×w. NO residual (spatial/channels change), so this is the body alone: mnv2DownBodyLayer's VJP.

h_se is the expand relu6 smoothness (at the cbrB pre-relu6 activation, at 2h×2w); h_sd is the strided-depthwise relu6 smoothness (at the dwbrBstrided pre-relu6 activation, fed the cbrB output).

Equations

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

theorem Proofs.StableHLO.mnv2DownBodyB_differentiableAt (N : ℕ) {ic mid oc h w kHd kWd : ℕ} (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) (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)))) (h_se : ∀ (k : Fin (N * (mid * (2 * h) * (2 * w)))), bnBatchLA N mid (2 * h) (2 * w) εe γe βe (batchMap N (flatConv We be) x) k ≠ 0 ∧ bnBatchLA N mid (2 * h) (2 * w) εe γe βe (batchMap N (flatConv We be) x) k ≠ 6) (h_sd : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseStride2FlatXla Wd bd) (cbrB N We be εe γe βe x)) k ≠ 0 ∧ bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseStride2FlatXla Wd bd) (cbrB N We be εe γe βe x)) k ≠ 6) : DifferentiableAt ℝ (projB N Wp bp εp γp βp ∘ dwbrBstrided N Wd bd εd γd βd ∘ cbrB N We be εe γe βe) x

noncomputable def Proofs.StableHLO.mnv2DownBodyBackBatchedGraph {N ic mid oc h w kHd kWd : ℕ} (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) (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 MobileNetV2 downsample body backward graph: the three stage graphs chained at their cumulative forward activations (cbrB⁻¹ ∘ dwbrBstrided⁻¹ ∘ projB⁻¹). Stride-2 analogue of mnv2BodyBackBatchedGraph (strided depthwise stage graph, no residual).

Equations

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

theorem Proofs.StableHLO.mnv2DownBodyBackBatchedGraph_faithful {N ic mid oc h w kHd kWd : ℕ} (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) (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))) (h_se : ∀ (k : Fin (N * (mid * (2 * h) * (2 * w)))), bnBatchLA N mid (2 * h) (2 * w) εe γe βe (batchMap N (flatConv We be) x) k ≠ 0 ∧ bnBatchLA N mid (2 * h) (2 * w) εe γe βe (batchMap N (flatConv We be) x) k ≠ 6) (h_sd : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseStride2FlatXla Wd bd) (cbrB N We be εe γe βe x)) k ≠ 0 ∧ bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseStride2FlatXla Wd bd) (cbrB N We be εe γe βe x)) k ≠ 6) : den (mnv2DownBodyBackBatchedGraph We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp x e) = (mnv2DownBodyB_has_vjp_at N We be εe hεe γe βe Wd bd εd hεd γd βd Wp bp εp hεp γp βp x h_se h_sd).backward (den e)

CAPSTONE — the batched MobileNetV2 DOWNSAMPLE inverted-residual body: backward graph ↔ the proven mnv2DownBodyB_has_vjp_at. The three batched stage backward graphs (cbrB/dwbrBstrided/projB) chained at their forward activations, proven equal to the downsample-body VJP. The stride-2 analogue of mnv2BodyBackBatchedGraph_faithful (no residual skip — the downsample block changes spatial/channels, so the body alone is the block), threaded through the two relu6 smoothness hypotheses (relu6's VJP is only _at). The MobileNetV2 relu6 peer of the EfficientNet mbDownBodyBackBatchedGraph_faithful; it is mnv2DownBodyLayer's faithful.

noncomputable def Proofs.StableHLO.mnv2ResidBlockBackBatchedGraph {N c mid h w kHd kWd : ℕ} (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) (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 MobileNetV2 inverted-residual block backward graph (body + identity skip).

Equations

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

theorem Proofs.StableHLO.mnv2ResidBlockBackBatchedGraph_faithful {N c mid h w kHd kWd : ℕ} (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) (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))) (h_se : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 0 ∧ bnBatchLA N mid h w εe γe βe (batchMap N (flatConv We be) x) k ≠ 6) (h_sd : ∀ (k : Fin (N * (mid * h * w))), bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 0 ∧ bnBatchLA N mid h w εd γd βd (batchMap N (depthwiseFlat Wd bd) (cbrB N We be εe γe βe x)) k ≠ 6) : den (mnv2ResidBlockBackBatchedGraph We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp x ecot) = (residual_has_vjp_at (projB N Wp bp εp γp βp ∘ dwbrB N Wd bd εd γd βd ∘ cbrB N We be εe γe βe) x ⋯ (mnv2BodyB_has_vjp_at N We be εe hεe γe βe Wd bd εd hεd γd βd Wp bp εp hεp γp βp x h_se h_sd)).backward (den ecot)

CAPSTONE — the whole batched MobileNetV2 inverted-residual block: backward graph ↔ the proven VJP. The three batched stage backward graphs (cbrB/dwbrB/projB) chained at their forward activations + the identity skip, proven equal to residual_has_vjp_at of the SE-less body projB ∘ dwbrB ∘ cbrB. The MobileNetV2 analogue of the EfficientNet mbResidBlockBackBatchedGraph_faithful, without the seB factor, threaded through the relu6 smoothness hypotheses (relu6's VJP is only _at).

It is CertLayer.residual mnv2BodyLayer's faithful: the residual fan-in backward (body cotangent + the identity skip's verbatim %dy).