§B: the MobileNetV2 inverted-residual body backward targets the CERTIFIED VJP

invresBodyBackPC (MobileNetBackChains.lean) is the hand-composed reverse of the inverted-residual body, written in the per-op backward maps of BackwardMaps.lean. This file closes §B for that body: the chain IS the certified input-gradient VJP, in the SAME non-batched per-channel-BN vocabulary the deployed net renders (invresBodyPC, MobileNetV2RenderPC).

The repo's invresBody_has_vjp_at (MobileNetV2.lean) is for the global-bnForward body, NOT the deployed per-channel one — so (exactly as r34 built rblkPC_has_vjp_at fresh) we build the certified per-channel body VJP invresBodyPC_has_vjp_at here (per-channel stage VJPs via bnPerChannelTensor3), then tie. b1-free: the per-example per-channel body is the non-batched object the chain reverses, no batchMap reconciliation.

The forward body is invresBodyPC = project ∘ depthwise ∘ expand, each stage (relu6) ∘ bnPC ∘ conv, so the certified VJP applies projectBack → depthwiseBack → expandBack. invresBodyBackPC is the peer chain (convFlatBack We ∘ bnBe ∘ reluMaskBack m_e) ∘ (depthwiseFlatBack Wd ∘ bnBd ∘ reluMaskBack m_d) ∘ (convFlatBack Wp ∘ bnBp). The tie pins the per-channel BN backs (bnBe/bnBd/bnBp) to bnPerChannelTensor3_has_vjp.backward at the saved activations and the relu6 masks (m_e/m_d) to the actual 0 < preact < 6 clamp-window signs (relu6's certified backward), and ties the two 1×1 convs

• the depthwise via the leaf gates (convFlatBack_eq_vjp_backward, depthwiseFlatBack_eq_vjp_backward). The conv/depthwise backwards ignore their (linear) primal, the pinned backs/masks carry the certified saved activations, so after rewriting the three convolution leaves everything matches definitionally. 3-axiom-clean.

noncomputable def Proofs.convBnRelu6PC_has_vjp_at {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) (v : Vec (ic * h * w)) (h_smooth : ∀ (k : Fin (oc * h * w)), bnPerChannelTensor3 oc h w ε γ β (flatConv W b v) k ≠ 0 ∧ bnPerChannelTensor3 oc h w ε γ β (flatConv W b v) k ≠ 6) : HasVJPAt (relu6 (oc * h * w) ∘ bnPerChannelTensor3 oc h w ε γ β ∘ flatConv W b) v

Expand / stem stage VJP, per-channel BN: relu6 ∘ bnPC ∘ conv. Mirror of convBnRelu6_has_vjp_at with bnPerChannelTensor3 for bnForward.

Equations

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

theorem Proofs.convBnRelu6PC_differentiableAt {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) (v : Vec (ic * h * w)) (h_smooth : ∀ (k : Fin (oc * h * w)), bnPerChannelTensor3 oc h w ε γ β (flatConv W b v) k ≠ 0 ∧ bnPerChannelTensor3 oc h w ε γ β (flatConv W b v) k ≠ 6) : DifferentiableAt ℝ (relu6 (oc * h * w) ∘ bnPerChannelTensor3 oc h w ε γ β ∘ flatConv W b) v

noncomputable def Proofs.dwBnRelu6PC_has_vjp_at {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β : Vec c) (hε : 0 < ε) (v : Vec (c * h * w)) (h_smooth : ∀ (k : Fin (c * h * w)), bnPerChannelTensor3 c h w ε γ β (depthwiseFlat W b v) k ≠ 0 ∧ bnPerChannelTensor3 c h w ε γ β (depthwiseFlat W b v) k ≠ 6) : HasVJPAt (relu6 (c * h * w) ∘ bnPerChannelTensor3 c h w ε γ β ∘ depthwiseFlat W b) v

Depthwise stage VJP (stride-1), per-channel BN: relu6 ∘ bnPC ∘ depthwise.

Equations

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

theorem Proofs.dwBnRelu6PC_differentiableAt {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β : Vec c) (hε : 0 < ε) (v : Vec (c * h * w)) (h_smooth : ∀ (k : Fin (c * h * w)), bnPerChannelTensor3 c h w ε γ β (depthwiseFlat W b v) k ≠ 0 ∧ bnPerChannelTensor3 c h w ε γ β (depthwiseFlat W b v) k ≠ 6) : DifferentiableAt ℝ (relu6 (c * h * w) ∘ bnPerChannelTensor3 c h w ε γ β ∘ depthwiseFlat W b) v

noncomputable def Proofs.convBnPC'_has_vjp {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) : HasVJP (bnPerChannelTensor3 oc h w ε γ β ∘ flatConv W b)

Project (linear bottleneck) stage VJP, per-channel BN: bnPC ∘ conv (no relu6, global HasVJP).

Equations

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

theorem Proofs.convBnPC'_differentiable {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) (hε : 0 < ε) : Differentiable ℝ (bnPerChannelTensor3 oc h w ε γ β ∘ flatConv W b)

noncomputable def Proofs.invresBodyPC_has_vjp_at {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (hεp : 0 < εp) (v : Vec (ic * h * w)) (h_se : ∀ (k : Fin (mid * h * w)), bnPerChannelTensor3 mid h w εe γe βe (flatConv We be v) k ≠ 0 ∧ bnPerChannelTensor3 mid h w εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnPerChannelTensor3 mid h w εd γd βd (depthwiseFlat Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 0 ∧ bnPerChannelTensor3 mid h w εd γd βd (depthwiseFlat Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 6) : HasVJPAt (invresBodyPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

Certified VJP of the per-channel-BN inverted-residual body invresBodyPC (stride-1, non-batched). project ∘ depthwise ∘ expand, mirroring the global invresBody_has_vjp_at with bnPerChannelTensor3. The same-vocabulary certified target for invresBodyBackPC — no batched/batchMap reconciliation.

Equations

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

theorem Proofs.invresBodyBackPC_eq_invresBodyPC_vjp {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (hkHe : 2 * ((kHe - 1) / 2) + 1 = kHe) (hkWe : 2 * ((kWe - 1) / 2) + 1 = kWe) (hkHd : 2 * ((kHd - 1) / 2) + 1 = kHd) (hkWd : 2 * ((kWd - 1) / 2) + 1 = kWd) (hkHp : 2 * ((kHp - 1) / 2) + 1 = kHp) (hkWp : 2 * ((kWp - 1) / 2) + 1 = kWp) (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (hεp : 0 < εp) (v : Vec (ic * h * w)) (h_se : ∀ (k : Fin (mid * h * w)), bnPerChannelTensor3 mid h w εe γe βe (flatConv We be v) k ≠ 0 ∧ bnPerChannelTensor3 mid h w εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnPerChannelTensor3 mid h w εd γd βd (depthwiseFlat Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 0 ∧ bnPerChannelTensor3 mid h w εd γd βd (depthwiseFlat Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 6) : (invresBodyBackPC We Wd Wp ((bnPerChannelTensor3_has_vjp mid h w εe hεe γe βe).backward (flatConv We be v)) ((bnPerChannelTensor3_has_vjp mid h w εd hεd γd βd).backward (depthwiseFlat Wd bd (ivExpandPC We be εe γe βe v))) ((bnPerChannelTensor3_has_vjp oc h w εp hεp γp βp).backward (flatConv Wp bp (ivDepthwisePC Wd bd εd γd βd (ivExpandPC We be εe γe βe v)))) (fun (i : Fin (mid * h * w)) => 0 < bnPerChannelTensor3 mid h w εe γe βe (flatConv We be v) i ∧ bnPerChannelTensor3 mid h w εe γe βe (flatConv We be v) i < 6) fun (i : Fin (mid * h * w)) => 0 < bnPerChannelTensor3 mid h w εd γd βd (depthwiseFlat Wd bd (ivExpandPC We be εe γe βe v)) i ∧ bnPerChannelTensor3 mid h w εd γd βd (depthwiseFlat Wd bd (ivExpandPC We be εe γe βe v)) i < 6) = (invresBodyPC_has_vjp_at We be εe γe βe hεe Wd bd εd γd βd hεd Wp bp εp γp βp hεp v h_se h_sd).backward

The §B mnv2 body tie: hand-composed backward = certified VJP. invresBodyBackPC, with its abstract per-channel BN backs pinned to bnPerChannelTensor3_has_vjp.backward at the saved activations and its relu6 masks pinned to the actual 0 < preact < 6 clamp-window signs (relu6's certified backward), equals (invresBodyPC_has_vjp_at …).backward. The two 1×1 convs tie via convFlatBack_eq_vjp_backward (1×1 odd) and the depthwise via depthwiseFlatBack_eq_vjp_backward; conv/depthwise backwards ignore their (linear) primal, so after rewriting the three leaves everything matches definitionally. Closes under [propext, Classical.choice, Quot.sound].

noncomputable def Proofs.dwStridedBnRelu6PC_has_vjp_at {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β : Vec c) (hε : 0 < ε) (v : Vec (c * (2 * h) * (2 * w))) (h_smooth : ∀ (k : Fin (c * h * w)), bnPerChannelTensor3 c h w ε γ β (depthwiseStride2FlatXla W b v) k ≠ 0 ∧ bnPerChannelTensor3 c h w ε γ β (depthwiseStride2FlatXla W b v) k ≠ 6) : HasVJPAt (relu6 (c * h * w) ∘ bnPerChannelTensor3 c h w ε γ β ∘ depthwiseStride2FlatXla W b) v

Strided depthwise stage VJP, per-channel BN: relu6 ∘ bnPC ∘ depthwiseStride2FlatXla.

Equations

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

theorem Proofs.dwStridedBnRelu6PC_differentiableAt {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε : ℝ) (γ β : Vec c) (hε : 0 < ε) (v : Vec (c * (2 * h) * (2 * w))) (h_smooth : ∀ (k : Fin (c * h * w)), bnPerChannelTensor3 c h w ε γ β (depthwiseStride2FlatXla W b v) k ≠ 0 ∧ bnPerChannelTensor3 c h w ε γ β (depthwiseStride2FlatXla W b v) k ≠ 6) : DifferentiableAt ℝ (relu6 (c * h * w) ∘ bnPerChannelTensor3 c h w ε γ β ∘ depthwiseStride2FlatXla W b) v

noncomputable def Proofs.invresBodyStridedPC_has_vjp_at {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (hεp : 0 < εp) (v : Vec (ic * (2 * h) * (2 * w))) (h_se : ∀ (k : Fin (mid * (2 * h) * (2 * w))), bnPerChannelTensor3 mid (2 * h) (2 * w) εe γe βe (flatConv We be v) k ≠ 0 ∧ bnPerChannelTensor3 mid (2 * h) (2 * w) εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnPerChannelTensor3 mid h w εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 0 ∧ bnPerChannelTensor3 mid h w εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 6) : HasVJPAt (invresBodyStridedPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

Certified VJP of the per-channel-BN strided inverted-residual body invresBodyStridedPC (downsample, non-batched). project ∘ depthwiseStrided ∘ expand(2h×2w) — the strided twin of invresBodyPC_has_vjp_at; the same-vocabulary certified target for invresBodyStridedBackPC.

Equations

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

theorem Proofs.invresBodyStridedBackPC_eq_invresBodyStridedPC_vjp {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (hkHe : 2 * ((kHe - 1) / 2) + 1 = kHe) (hkWe : 2 * ((kWe - 1) / 2) + 1 = kWe) (hkHd : 2 * ((kHd - 1) / 2) + 1 = kHd) (hkWd : 2 * ((kWd - 1) / 2) + 1 = kWd) (hkHp : 2 * ((kHp - 1) / 2) + 1 = kHp) (hkWp : 2 * ((kWp - 1) / 2) + 1 = kWp) (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (hεp : 0 < εp) (v : Vec (ic * (2 * h) * (2 * w))) (h_se : ∀ (k : Fin (mid * (2 * h) * (2 * w))), bnPerChannelTensor3 mid (2 * h) (2 * w) εe γe βe (flatConv We be v) k ≠ 0 ∧ bnPerChannelTensor3 mid (2 * h) (2 * w) εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnPerChannelTensor3 mid h w εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 0 ∧ bnPerChannelTensor3 mid h w εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpandPC We be εe γe βe v)) k ≠ 6) : (invresBodyStridedBackPC We Wd Wp ((bnPerChannelTensor3_has_vjp mid (2 * h) (2 * w) εe hεe γe βe).backward (flatConv We be v)) ((bnPerChannelTensor3_has_vjp mid h w εd hεd γd βd).backward (depthwiseStride2FlatXla Wd bd (ivExpandPC We be εe γe βe v))) ((bnPerChannelTensor3_has_vjp oc h w εp hεp γp βp).backward (flatConv Wp bp (ivDepthwiseStridedPC Wd bd εd γd βd (ivExpandPC We be εe γe βe v)))) (fun (i : Fin (mid * (2 * h) * (2 * w))) => 0 < bnPerChannelTensor3 mid (2 * h) (2 * w) εe γe βe (flatConv We be v) i ∧ bnPerChannelTensor3 mid (2 * h) (2 * w) εe γe βe (flatConv We be v) i < 6) fun (i : Fin (mid * h * w)) => 0 < bnPerChannelTensor3 mid h w εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpandPC We be εe γe βe v)) i ∧ bnPerChannelTensor3 mid h w εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpandPC We be εe γe βe v)) i < 6) = (invresBodyStridedPC_has_vjp_at We be εe γe βe hεe Wd bd εd γd βd hεd Wp bp εp γp βp hεp v h_se h_sd).backward

The §B mnv2 strided body tie: hand-composed backward = certified VJP. The downsample peer of invresBodyBackPC_eq_invresBodyPC_vjp: invresBodyStridedBackPC with its per-channel BN backs and relu6 masks pinned to the saved activations equals (invresBodyStridedPC_has_vjp_at …).backward. The strided depthwise ties via depthwiseStride2FlatXlaBack_eq_vjp_backward; the expand conv at the 2h×2w grid and the project conv via convFlatBack_eq_vjp_backward. 3-axiom-clean.