MobileNetV2 — end-to-end inverted-residual VJP (flattened Vec space)

Builds a representative MobileNetV2 forward and proves its end-to-end vector–Jacobian product correct, analogous to cnn_has_vjp_at for the ResNet basic block. Everything lives in flattened Vec space and reuses the foundation rules from CNN.lean, Depthwise.lean, BatchNorm.lean, MLP.lean, and Residual.lean through vjp_comp_at chaining.

What's new here

• relu6 — the clamped activation min (max x 0) 6. Unlike relu, the saturated branch is the constant 6 (not linear-through-origin), so the local-linearization trick matches relu6 against an affine surrogate g (proj on the active region, constant 0 below, constant 6 above) whose fderiv is the diagonal indicator 1_{0<x<6}. Smoothness is the two-sided x k ≠ 0 ∧ x k ≠ 6.

• Inverted-residual body — project ∘ depthwise ∘ expand:

  • expand : 1×1 conv → bn → relu6 (ic → mid, mid = t·ic)
  • depthwise: depthwise conv → bn → relu6 (mid → mid)
  • project : 1×1 conv → bn (linear bottleneck, no activation; mid → oc) With a stride-1 / ic = oc skip it becomes residual body (no final activation — MobileNetV2's linear-bottleneck design).

• End-to-end — stem (3×3 conv-bn-relu6) → skip inverted-residual → no-skip inverted-residual (channel change) → global average pool → dense head. Fixed block counts; generic channel/kernel dims; spatial h w preserved throughout (SAME convs).

Padding convention

The strided sites — the 6-block mobilenetv2Forward_full's stem and its four downsample depthwises — read flatConvStride2Xla / depthwiseStride2FlatXla, the XLA-SAME (odd) phase every MobileNetV2 artifact emits, re-spelled 2026-09-05 with the rest of the Proofs tier. This net is the scalar-BN stepping stone mobilenetv2Forward_full_pc replaced: no artifact and no float number rests on it, and it moved so the whole MobileNetV2 cone reads one phase. The 2-block generic mobilenetv2Forward below has a stride-1 stem and is not affected either way.

All new defs/theorems certify to exactly [propext, Classical.choice, Quot.sound].

noncomputable def Proofs.relu6 (n : ℕ) (x : Vec n) : Vec n

Equations

• Proofs.relu6 n x i = min (max (x i) 0) 6

noncomputable def Proofs.relu6LinearPart (n : ℕ) (x : Vec n) : Vec n →L[ℝ] Vec n

ReLU6's local linear part at a smooth point: projects to y k when 0 < x k < 6, otherwise zero.

Equations

• Proofs.relu6LinearPart n x = ContinuousLinearMap.pi fun (k : Fin n) => if 0 < x k ∧ x k < 6 then ContinuousLinearMap.proj k else 0

@[simp]

theorem Proofs.relu6LinearPart_apply (n : ℕ) (x y : Vec n) (k : Fin n) : (relu6LinearPart n x) y k = if 0 < x k ∧ x k < 6 then y k else 0

theorem Proofs.relu6_hasFDerivAt (n : ℕ) (x : Vec n) (h_smooth : ∀ (k : Fin n), x k ≠ 0 ∧ x k ≠ 6) : HasFDerivAt (relu6 n) (relu6LinearPart n x) x

theorem Proofs.relu6_differentiableAt_of_smooth (n : ℕ) (x : Vec n) (h_smooth : ∀ (k : Fin n), x k ≠ 0 ∧ x k ≠ 6) : DifferentiableAt ℝ (relu6 n) x

theorem Proofs.pdiv_relu6 (n : ℕ) (x : Vec n) (h_smooth : ∀ (k : Fin n), x k ≠ 0 ∧ x k ≠ 6) (i j : Fin n) : pdiv (relu6 n) x i j = if i = j then if 0 < x i ∧ x i < 6 then 1 else 0 else 0

noncomputable def Proofs.relu6_has_vjp_at (n : ℕ) (x : Vec n) (h_smooth : ∀ (k : Fin n), x k ≠ 0 ∧ x k ≠ 6) : HasVJPAt (relu6 n) x

Equations

• Proofs.relu6_has_vjp_at n x h_smooth = { backward := fun (dy : Proofs.Vec n) (i : Fin n) => if 0 < x i ∧ x i < 6 then dy i else 0, correct := ⋯ }

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

1×1 conv → bn → relu6 (expand stage / stem). Mirror of convBnRelu_has_vjp_at with relu6 in place of relu.

Equations

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

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

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

Depthwise → bn → relu6 (depthwise stage of an inverted residual). Channels & spatial dims preserved: Vec (c*h*w) → Vec (c*h*w).

Equations

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

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

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

conv → bn (no activation) — the project (linear bottleneck) stage. Everywhere differentiable, global HasVJP.

Equations

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

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

@[reducible]

noncomputable def Proofs.ivExpand {ic mid h w kHe kWe : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe γe βe : ℝ) : Vec (ic * h * w) → Vec (mid * h * w)

The expand stage as a flat map.

Equations

• Proofs.ivExpand We be εe γe βe = Proofs.relu6 (mid * h * w) ∘ Proofs.bnForward (mid * h * w) εe γe βe ∘ Proofs.flatConv We be

@[reducible]

noncomputable def Proofs.ivDepthwise {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) : Vec (mid * h * w) → Vec (mid * h * w)

The depthwise stage as a flat map.

Equations

• Proofs.ivDepthwise Wd bd εd γd βd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnForward (mid * h * w) εd γd βd ∘ Proofs.depthwiseFlat Wd bd

@[reducible]

noncomputable def Proofs.ivProject {mid oc h w kHp kWp : ℕ} (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp γp βp : ℝ) : Vec (mid * h * w) → Vec (oc * h * w)

The project (linear bottleneck) stage as a flat map.

Equations

• Proofs.ivProject Wp bp εp γp βp = Proofs.bnForward (oc * h * w) εp γp βp ∘ Proofs.flatConv Wp bp

@[reducible]

noncomputable def Proofs.invresBody {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe γe βe : ℝ) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp γp βp : ℝ) : Vec (ic * h * w) → Vec (oc * h * w)

Inverted-residual body = project ∘ depthwise ∘ expand. Flat Vec (ic*h*w) → Vec (oc*h*w).

Equations

• Proofs.invresBody We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp = Proofs.ivProject Wp bp εp γp βp ∘ Proofs.ivDepthwise Wd bd εd γd βd ∘ Proofs.ivExpand We be εe γe βe

noncomputable def Proofs.invresBody_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 : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp γp βp : ℝ) (hεp : 0 < εp) (v : Vec (ic * h * w)) (h_se : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εe γe βe (flatConv We be v) k ≠ 0 ∧ bnForward (mid * h * w) εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εd γd βd (depthwiseFlat Wd bd (ivExpand We be εe γe βe v)) k ≠ 0 ∧ bnForward (mid * h * w) εd γd βd (depthwiseFlat Wd bd (ivExpand We be εe γe βe v)) k ≠ 6) : HasVJPAt (invresBody We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

Inverted-residual body VJP at a smooth point. Two vjp_comp_at chains: (1) depthwise ∘ expand over the two relu6 smoothness families, (2) project (everywhere) on top.

Equations

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

theorem Proofs.invresBody_differentiableAt {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp γp βp : ℝ) (hεp : 0 < εp) (v : Vec (ic * h * w)) (h_se : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εe γe βe (flatConv We be v) k ≠ 0 ∧ bnForward (mid * h * w) εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εd γd βd (depthwiseFlat Wd bd (ivExpand We be εe γe βe v)) k ≠ 0 ∧ bnForward (mid * h * w) εd γd βd (depthwiseFlat Wd bd (ivExpand We be εe γe βe v)) k ≠ 6) : DifferentiableAt ℝ (invresBody We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

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

Inverted-residual block WITH skip (stride 1, ic = oc = c): residual (invresBody) — body(x) + x. No final activation (MobileNetV2 uses linear bottleneck; the project stage has no relu6, and the residual add is the block output).

Equations

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

theorem Proofs.invresSkip_differentiableAt {c mid h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid c kHe kWe) (be : Vec mid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) (hεd : 0 < εd) (Wp : Kernel4 c mid kHp kWp) (bp : Vec c) (εp γp βp : ℝ) (hεp : 0 < εp) (v : Vec (c * h * w)) (h_se : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εe γe βe (flatConv We be v) k ≠ 0 ∧ bnForward (mid * h * w) εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εd γd βd (depthwiseFlat Wd bd (ivExpand We be εe γe βe v)) k ≠ 0 ∧ bnForward (mid * h * w) εd γd βd (depthwiseFlat Wd bd (ivExpand We be εe γe βe v)) k ≠ 6) : DifferentiableAt ℝ (residual (invresBody We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp)) v

noncomputable def Proofs.mobilenetv2Forward {ic c mid₁ oc mid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (We₁ : Kernel4 mid₁ c kHe₁ kWe₁) (be₁ : Vec mid₁) (e₁ ge₁ be1 : ℝ) (Wd₁ : DepthwiseKernel mid₁ kHd₁ kWd₁) (bd₁ : Vec mid₁) (d₁ gd₁ bd1 : ℝ) (Wp₁ : Kernel4 c mid₁ kHp₁ kWp₁) (bp₁ : Vec c) (p₁ gp₁ bp1 : ℝ) (We₂ : Kernel4 mid₂ c kHe₂ kWe₂) (be₂ : Vec mid₂) (e₂ ge₂ be2 : ℝ) (Wd₂ : DepthwiseKernel mid₂ kHd₂ kWd₂) (bd₂ : Vec mid₂) (d₂ gd₂ bd2 : ℝ) (Wp₂ : Kernel4 oc mid₂ kHp₂ kWp₂) (bp₂ : Vec oc) (p₂ gp₂ bp2 : ℝ) (Wh : Mat oc nClasses) (bh : Vec nClasses) : Vec (ic * h * w) → Vec nClasses

The forward MobileNetV2.

Equations

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

noncomputable def Proofs.mobilenetv2_has_vjp_at {ic c mid₁ oc mid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (hεs : 0 < εs) (We₁ : Kernel4 mid₁ c kHe₁ kWe₁) (be₁ : Vec mid₁) (e₁ ge₁ be1 : ℝ) (he₁ : 0 < e₁) (Wd₁ : DepthwiseKernel mid₁ kHd₁ kWd₁) (bd₁ : Vec mid₁) (d₁ gd₁ bd1 : ℝ) (hd₁ : 0 < d₁) (Wp₁ : Kernel4 c mid₁ kHp₁ kWp₁) (bp₁ : Vec c) (p₁ gp₁ bp1 : ℝ) (hp₁ : 0 < p₁) (We₂ : Kernel4 mid₂ c kHe₂ kWe₂) (be₂ : Vec mid₂) (e₂ ge₂ be2 : ℝ) (he₂ : 0 < e₂) (Wd₂ : DepthwiseKernel mid₂ kHd₂ kWd₂) (bd₂ : Vec mid₂) (d₂ gd₂ bd2 : ℝ) (hd₂ : 0 < d₂) (Wp₂ : Kernel4 oc mid₂ kHp₂ kWp₂) (bp₂ : Vec oc) (p₂ gp₂ bp2 : ℝ) (hp₂ : 0 < p₂) (Wh : Mat oc nClasses) (bh : Vec nClasses) (x : Vec (ic * h * w)) (h_stem : ∀ (k : Fin (c * h * w)), bnForward (c * h * w) εs γs βs (flatConv Ws bs x) k ≠ 0 ∧ bnForward (c * h * w) εs γs βs (flatConv Ws bs x) k ≠ 6) (h_b1e : ∀ (k : Fin (mid₁ * h * w)), bnForward (mid₁ * h * w) e₁ ge₁ be1 (flatConv We₁ be₁ ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)) k ≠ 0 ∧ bnForward (mid₁ * h * w) e₁ ge₁ be1 (flatConv We₁ be₁ ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)) k ≠ 6) (h_b1d : ∀ (k : Fin (mid₁ * h * w)), bnForward (mid₁ * h * w) d₁ gd₁ bd1 (depthwiseFlat Wd₁ bd₁ (ivExpand We₁ be₁ e₁ ge₁ be1 ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 0 ∧ bnForward (mid₁ * h * w) d₁ gd₁ bd1 (depthwiseFlat Wd₁ bd₁ (ivExpand We₁ be₁ e₁ ge₁ be1 ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 6) (h_b2e : ∀ (k : Fin (mid₂ * h * w)), bnForward (mid₂ * h * w) e₂ ge₂ be2 (flatConv We₂ be₂ (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 0 ∧ bnForward (mid₂ * h * w) e₂ ge₂ be2 (flatConv We₂ be₂ (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 6) (h_b2d : ∀ (k : Fin (mid₂ * h * w)), bnForward (mid₂ * h * w) d₂ gd₂ bd2 (depthwiseFlat Wd₂ bd₂ (ivExpand We₂ be₂ e₂ ge₂ be2 (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)))) k ≠ 0 ∧ bnForward (mid₂ * h * w) d₂ gd₂ bd2 (depthwiseFlat Wd₂ bd₂ (ivExpand We₂ be₂ e₂ ge₂ be2 (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)))) k ≠ 6) : HasVJPAt (mobilenetv2Forward Ws bs εs γs βs We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1 We₂ be₂ e₂ ge₂ be2 Wd₂ bd₂ d₂ gd₂ bd2 Wp₂ bp₂ p₂ gp₂ bp2 Wh bh) x

MobileNetV2 end-to-end VJP at a smooth point. Chains the stem, a skip inverted-residual, a no-skip inverted-residual, global avg pool, and dense head with vjp_comp_at under one bundled smoothness family (one ≠0∧≠6 hypothesis per relu6 site, evaluated at the running activation).

Equations

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

theorem Proofs.mobilenetv2_has_vjp_at_correct {ic c mid₁ oc mid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (hεs : 0 < εs) (We₁ : Kernel4 mid₁ c kHe₁ kWe₁) (be₁ : Vec mid₁) (e₁ ge₁ be1 : ℝ) (he₁ : 0 < e₁) (Wd₁ : DepthwiseKernel mid₁ kHd₁ kWd₁) (bd₁ : Vec mid₁) (d₁ gd₁ bd1 : ℝ) (hd₁ : 0 < d₁) (Wp₁ : Kernel4 c mid₁ kHp₁ kWp₁) (bp₁ : Vec c) (p₁ gp₁ bp1 : ℝ) (hp₁ : 0 < p₁) (We₂ : Kernel4 mid₂ c kHe₂ kWe₂) (be₂ : Vec mid₂) (e₂ ge₂ be2 : ℝ) (he₂ : 0 < e₂) (Wd₂ : DepthwiseKernel mid₂ kHd₂ kWd₂) (bd₂ : Vec mid₂) (d₂ gd₂ bd2 : ℝ) (hd₂ : 0 < d₂) (Wp₂ : Kernel4 oc mid₂ kHp₂ kWp₂) (bp₂ : Vec oc) (p₂ gp₂ bp2 : ℝ) (hp₂ : 0 < p₂) (Wh : Mat oc nClasses) (bh : Vec nClasses) (x : Vec (ic * h * w)) (h_stem : ∀ (k : Fin (c * h * w)), bnForward (c * h * w) εs γs βs (flatConv Ws bs x) k ≠ 0 ∧ bnForward (c * h * w) εs γs βs (flatConv Ws bs x) k ≠ 6) (h_b1e : ∀ (k : Fin (mid₁ * h * w)), bnForward (mid₁ * h * w) e₁ ge₁ be1 (flatConv We₁ be₁ ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)) k ≠ 0 ∧ bnForward (mid₁ * h * w) e₁ ge₁ be1 (flatConv We₁ be₁ ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)) k ≠ 6) (h_b1d : ∀ (k : Fin (mid₁ * h * w)), bnForward (mid₁ * h * w) d₁ gd₁ bd1 (depthwiseFlat Wd₁ bd₁ (ivExpand We₁ be₁ e₁ ge₁ be1 ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 0 ∧ bnForward (mid₁ * h * w) d₁ gd₁ bd1 (depthwiseFlat Wd₁ bd₁ (ivExpand We₁ be₁ e₁ ge₁ be1 ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 6) (h_b2e : ∀ (k : Fin (mid₂ * h * w)), bnForward (mid₂ * h * w) e₂ ge₂ be2 (flatConv We₂ be₂ (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 0 ∧ bnForward (mid₂ * h * w) e₂ ge₂ be2 (flatConv We₂ be₂ (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x))) k ≠ 6) (h_b2d : ∀ (k : Fin (mid₂ * h * w)), bnForward (mid₂ * h * w) d₂ gd₂ bd2 (depthwiseFlat Wd₂ bd₂ (ivExpand We₂ be₂ e₂ ge₂ be2 (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)))) k ≠ 0 ∧ bnForward (mid₂ * h * w) d₂ gd₂ bd2 (depthwiseFlat Wd₂ bd₂ (ivExpand We₂ be₂ e₂ ge₂ be2 (residual (invresBody We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1) ((relu6 (c * h * w) ∘ bnForward (c * h * w) εs γs βs ∘ flatConv Ws bs) x)))) k ≠ 6) (dy : Vec nClasses) (i : Fin (ic * h * w)) : (mobilenetv2_has_vjp_at Ws bs εs γs βs hεs We₁ be₁ e₁ ge₁ be1 he₁ Wd₁ bd₁ d₁ gd₁ bd1 hd₁ Wp₁ bp₁ p₁ gp₁ bp1 hp₁ We₂ be₂ e₂ ge₂ be2 he₂ Wd₂ bd₂ d₂ gd₂ bd2 hd₂ Wp₂ bp₂ p₂ gp₂ bp2 hp₂ Wh bh x h_stem h_b1e h_b1d h_b2e h_b2d).backward dy i = ∑ j : Fin nClasses, pdiv (mobilenetv2Forward Ws bs εs γs βs We₁ be₁ e₁ ge₁ be1 Wd₁ bd₁ d₁ gd₁ bd1 Wp₁ bp₁ p₁ gp₁ bp1 We₂ be₂ e₂ ge₂ be2 Wd₂ bd₂ d₂ gd₂ bd2 Wp₂ bp₂ p₂ gp₂ bp2 Wh bh) x i j * dy j

Public correctness theorem for mobilenetv2_has_vjp_at — exposes the witness's .correct field: the full MobileNetV2 backward equals the pdiv-contracted Jacobian (Jacobian-transpose applied to the cotangent). MobileNetV2 analogue of cnn_has_vjp_at_correct.

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

Stride-2 conv → bn → relu6 (the strided stem). Strided mirror of convBnRelu6_has_vjp_at with flatConvStride2Xla; input spatial halves (2h×2w → h×w).

Equations

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

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

@[reducible]

noncomputable def Proofs.ivDepthwiseStrided {mid h w kHd kWd : ℕ} (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) : Vec (mid * (2 * h) * (2 * w)) → Vec (mid * h * w)

The strided depthwise stage as a flat map (Vec (mid*(2h)*(2w)) → Vec (mid*h*w)).

Equations

• Proofs.ivDepthwiseStrided Wd bd εd γd βd = Proofs.relu6 (mid * h * w) ∘ Proofs.bnForward (mid * h * w) εd γd βd ∘ Proofs.depthwiseStride2FlatXla Wd bd

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

Stride-2 depthwise → bn → relu6 (downsampling depthwise stage). Strided mirror of dwBnRelu6_has_vjp_at with depthwiseStride2FlatXla.

Equations

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

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

@[reducible]

noncomputable def Proofs.invresBodyStrided {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe γe βe : ℝ) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp γp βp : ℝ) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

Strided inverted-residual body = project ∘ depthwiseStrided ∘ expand. Expand is SAME at the input resolution (2h×2w); the stride-2 depthwise halves spatial (2h×2w → h×w); project is SAME at the output resolution. Flat Vec (ic*(2h)*(2w)) → Vec (oc*h*w). (No skip: strided blocks change spatial / channels, so MobileNetV2 never wraps them in a residual.)

Equations

• Proofs.invresBodyStrided We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp = Proofs.ivProject Wp bp εp γp βp ∘ Proofs.ivDepthwiseStrided Wd bd εd γd βd ∘ Proofs.ivExpand We be εe γe βe

noncomputable def Proofs.invresBodyStrided_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 : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp γp βp : ℝ) (hεp : 0 < εp) (v : Vec (ic * (2 * h) * (2 * w))) (h_se : ∀ (k : Fin (mid * (2 * h) * (2 * w))), bnForward (mid * (2 * h) * (2 * w)) εe γe βe (flatConv We be v) k ≠ 0 ∧ bnForward (mid * (2 * h) * (2 * w)) εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpand We be εe γe βe v)) k ≠ 0 ∧ bnForward (mid * h * w) εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpand We be εe γe βe v)) k ≠ 6) : HasVJPAt (invresBodyStrided We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

Strided inverted-residual body VJP at a smooth point. Strided mirror of invresBody_has_vjp_at: expand SAME (at 2h×2w) → depthwise-strided → project.

Equations

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

theorem Proofs.invresBodyStrided_differentiableAt {ic mid oc h w kHe kWe kHd kWd kHp kWp : ℕ} (We : Kernel4 mid ic kHe kWe) (be : Vec mid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd γd βd : ℝ) (hεd : 0 < εd) (Wp : Kernel4 oc mid kHp kWp) (bp : Vec oc) (εp γp βp : ℝ) (hεp : 0 < εp) (v : Vec (ic * (2 * h) * (2 * w))) (h_se : ∀ (k : Fin (mid * (2 * h) * (2 * w))), bnForward (mid * (2 * h) * (2 * w)) εe γe βe (flatConv We be v) k ≠ 0 ∧ bnForward (mid * (2 * h) * (2 * w)) εe γe βe (flatConv We be v) k ≠ 6) (h_sd : ∀ (k : Fin (mid * h * w)), bnForward (mid * h * w) εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpand We be εe γe βe v)) k ≠ 0 ∧ bnForward (mid * h * w) εd γd βd (depthwiseStride2FlatXla Wd bd (ivExpand We be εe γe βe v)) k ≠ 6) : DifferentiableAt ℝ (invresBodyStrided We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

noncomputable def Proofs.mobilenetv2Forward_full (Ws : Kernel4 16 3 3 3) (bs : Vec 16) (εs γs βs : ℝ) (We1 : Kernel4 64 16 1 1) (be1 : Vec 64) (εe1 γe1 βe1 : ℝ) (Wd1 : DepthwiseKernel 64 3 3) (bd1 : Vec 64) (εd1 γd1 βd1 : ℝ) (Wp1 : Kernel4 24 64 1 1) (bp1 : Vec 24) (εp1 γp1 βp1 : ℝ) (We2 : Kernel4 96 24 1 1) (be2 : Vec 96) (εe2 γe2 βe2 : ℝ) (Wd2 : DepthwiseKernel 96 3 3) (bd2 : Vec 96) (εd2 γd2 βd2 : ℝ) (Wp2 : Kernel4 24 96 1 1) (bp2 : Vec 24) (εp2 γp2 βp2 : ℝ) (We3 : Kernel4 96 24 1 1) (be3 : Vec 96) (εe3 γe3 βe3 : ℝ) (Wd3 : DepthwiseKernel 96 3 3) (bd3 : Vec 96) (εd3 γd3 βd3 : ℝ) (Wp3 : Kernel4 32 96 1 1) (bp3 : Vec 32) (εp3 γp3 βp3 : ℝ) (We4 : Kernel4 128 32 1 1) (be4 : Vec 128) (εe4 γe4 βe4 : ℝ) (Wd4 : DepthwiseKernel 128 3 3) (bd4 : Vec 128) (εd4 γd4 βd4 : ℝ) (Wp4 : Kernel4 32 128 1 1) (bp4 : Vec 32) (εp4 γp4 βp4 : ℝ) (We5 : Kernel4 128 32 1 1) (be5 : Vec 128) (εe5 γe5 βe5 : ℝ) (Wd5 : DepthwiseKernel 128 3 3) (bd5 : Vec 128) (εd5 γd5 βd5 : ℝ) (Wp5 : Kernel4 64 128 1 1) (bp5 : Vec 64) (εp5 γp5 βp5 : ℝ) (We6 : Kernel4 256 64 1 1) (be6 : Vec 256) (εe6 γe6 βe6 : ℝ) (Wd6 : DepthwiseKernel 256 3 3) (bd6 : Vec 256) (εd6 γd6 βd6 : ℝ) (Wp6 : Kernel4 64 256 1 1) (bp6 : Vec 64) (εp6 γp6 βp6 : ℝ) (Wh : Kernel4 128 64 1 1) (bh : Vec 128) (εh γh βh : ℝ) (Wfc : Mat 128 10) (bfc : Vec 10) : Vec (3 * 224 * 224) → Vec 10

The full MobileNetV2 forward (ch7 render): stem-s2 → 6 inverted-residual blocks (b1/b3/b5/b6 stride-2 downsample, b2/b4 stride-1 skip) → 1×1 conv-bn-relu6 head → global-avg-pool → dense. Scalar BN; faithful topology.

Equations

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

theorem Proofs.bnForward_const {n : ℕ} (hn : 0 < n) (ε γ β c : ℝ) : (bnForward n ε γ β fun (x : Fin n) => c) = fun (x : Fin n) => β

BN of a constant vector is the (constant) shift β — centering zeroes the normalized term, killing the √. Keystone for discharging ReLU6 smoothness on a constant-activation net.

theorem Proofs.flatConv_eq_zero {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (hW : ∀ (o : Fin oc) (c : Fin ic) (kh : Fin kH) (kw : Fin kW), W o c kh kw = 0) (hb : ∀ (o : Fin oc), b o = 0) (v : Vec (ic * h * w)) : flatConv W b v = fun (x : Fin (oc * h * w)) => 0

A conv with everywhere-zero kernel and bias maps anything to 0.

theorem Proofs.depthwiseFlat_eq_zero {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (hW : ∀ (ch : Fin c) (kh : Fin kH) (kw : Fin kW), W ch kh kw = 0) (hb : ∀ (ch : Fin c), b ch = 0) (v : Vec (c * h * w)) : depthwiseFlat W b v = fun (x : Fin (c * h * w)) => 0

A depthwise conv with everywhere-zero kernel and bias maps anything to 0.

noncomputable def Proofs.MobileNetV2Concrete.Ws : Kernel4 2 1 1 1

Equations

• Proofs.MobileNetV2Concrete.Ws x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bs : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bs x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.We₁ : Kernel4 2 2 1 1

Equations

• Proofs.MobileNetV2Concrete.We₁ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bE₁ : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bE₁ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.Wd₁ : DepthwiseKernel 2 1 1

Equations

• Proofs.MobileNetV2Concrete.Wd₁ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bD₁ : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bD₁ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.Wp₁ : Kernel4 2 2 1 1

Equations

• Proofs.MobileNetV2Concrete.Wp₁ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bP₁ : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bP₁ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.We₂ : Kernel4 2 2 1 1

Equations

• Proofs.MobileNetV2Concrete.We₂ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bE₂ : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bE₂ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.Wd₂ : DepthwiseKernel 2 1 1

Equations

• Proofs.MobileNetV2Concrete.Wd₂ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bD₂ : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bD₂ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.Wp₂ : Kernel4 2 2 1 1

Equations

• Proofs.MobileNetV2Concrete.Wp₂ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bP₂ : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bP₂ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.Wh : Mat 2 2

Equations

• Proofs.MobileNetV2Concrete.Wh x✝¹ x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.bh : Vec 2

Equations

• Proofs.MobileNetV2Concrete.bh x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.X : Vec (1 * 2 * 2)

Equations

• Proofs.MobileNetV2Concrete.X x✝ = 0

noncomputable def Proofs.MobileNetV2Concrete.mnv2Concrete_has_vjp_at : HasVJPAt (mobilenetv2Forward Ws bs 1 1 1 We₁ bE₁ 1 1 1 Wd₁ bD₁ 1 1 1 Wp₁ bP₁ 1 1 1 We₂ bE₂ 1 1 1 Wd₂ bD₂ 1 1 1 Wp₂ bP₂ 1 1 1 Wh bh) X

Whole-network VJP for a concrete MobileNetV2 — every ReLU6 smoothness hypothesis (bn ≠ 0 ∧ bn ≠ 6 at the five relu6 sites) discharged: every BN input is the zero vector (zero kernels), so each BN output is its shift β = 1 ∈ (0,6) via bnForward_const.

Equations

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

theorem Proofs.MobileNetV2Concrete.mnv2Concrete_has_vjp_correct (dy : Vec 2) (i : Fin (1 * 2 * 2)) : mnv2Concrete_has_vjp_at.backward dy i = ∑ j : Fin 2, pdiv (mobilenetv2Forward Ws bs 1 1 1 We₁ bE₁ 1 1 1 Wd₁ bD₁ 1 1 1 Wp₁ bP₁ 1 1 1 We₂ bE₂ 1 1 1 Wd₂ bD₂ 1 1 1 Wp₂ bP₂ 1 1 1 Wh bh) X i j * dy j

Public unconditional correctness theorem — the concrete MobileNetV2's backward equals the pdiv-Jacobian VJP, no hypotheses.

theorem Proofs.Mnv2Live.bn13_window (n : ℕ) (hn : 0 < n) (hn8 : n ≤ 8) (ε : ℝ) (hε : 0 < ε) (z : Vec n) (k : Fin n) : 0 < bnForward n ε 1 3 z k ∧ bnForward n ε 1 3 z k < 6

With γ=1, β=3 and length n ≤ 8, every BN output is in (0,6) — for an arbitrary input z and arbitrary ε>0. No constant-collapse, no sqrt computed: the bound reduces to (zₖ−μ)² < 9(σ²+ε).

theorem Proofs.Mnv2Live.dev_sum_zero (n : ℕ) (hn : 0 < n) (z : Vec n) : ∑ k : Fin n, (z k - bnMean n z) = 0

Deviations sum to zero: Σₖ (zₖ − μ) = 0.

theorem Proofs.Mnv2Live.bnForward_mean (n : ℕ) (hn : 0 < n) (ε γ β : ℝ) (z : Vec n) : bnMean n (bnForward n ε γ β z) = β

BN forces the output mean to β (for n > 0).

theorem Proofs.Mnv2Live.bn1_devSum_scale (n : ℕ) (hn : 0 < n) (ε β : ℝ) (z : Vec n) (S : Finset (Fin n)) : ∑ k ∈ S, (bnForward n ε 1 β z k - bnMean n (bnForward n ε 1 β z)) = bnIstd n z ε * ∑ k ∈ S, (z k - bnMean n z)

BN rescales every deviation by istd (the γ=1 case). Over any index set S, the BN-output deviation-sum is the input deviation-sum scaled by the positive bnIstd. This is what carries a stem-planted cross-channel asymmetry through the four BN layers undamped.

theorem Proofs.Mnv2Live.bnIstd_pos (n : ℕ) (ε : ℝ) (hε : 0 < ε) (z : Vec n) : 0 < bnIstd n z ε

bnIstd is strictly positive (so the rescaling above never kills the sign).

noncomputable def Proofs.Mnv2Live.Ws : Kernel4 2 1 1 1

Equations

• Proofs.Mnv2Live.Ws o x✝² x✝¹ x✝ = if o = 0 then 1 else 2

noncomputable def Proofs.Mnv2Live.bs : Vec 2

Equations

• Proofs.Mnv2Live.bs x✝ = 0

noncomputable def Proofs.Mnv2Live.We₁ : Kernel4 2 2 1 1

Equations

• Proofs.Mnv2Live.We₁ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.Mnv2Live.be₁ : Vec 2

Equations

• Proofs.Mnv2Live.be₁ x✝ = 0

noncomputable def Proofs.Mnv2Live.Wd₁ : DepthwiseKernel 2 1 1

Equations

• Proofs.Mnv2Live.Wd₁ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.Mnv2Live.bd₁ : Vec 2

Equations

• Proofs.Mnv2Live.bd₁ x✝ = 0

noncomputable def Proofs.Mnv2Live.Wp₁ : Kernel4 2 2 1 1

Equations

• Proofs.Mnv2Live.Wp₁ x✝³ x✝² x✝¹ x✝ = 0

noncomputable def Proofs.Mnv2Live.bp₁ : Vec 2

Equations

• Proofs.Mnv2Live.bp₁ x✝ = 0

noncomputable def Proofs.Mnv2Live.We₂ : Kernel4 2 2 1 1

block2 expand: identity channel map.

Equations

• Proofs.Mnv2Live.We₂ o i x✝¹ x✝ = if o = i then 1 else 0

noncomputable def Proofs.Mnv2Live.be₂ : Vec 2

Equations

• Proofs.Mnv2Live.be₂ x✝ = 0

noncomputable def Proofs.Mnv2Live.Wd₂ : DepthwiseKernel 2 1 1

block2 depthwise: identity (single 1×1 tap).

Equations

• Proofs.Mnv2Live.Wd₂ x✝² x✝¹ x✝ = 1

noncomputable def Proofs.Mnv2Live.bd₂ : Vec 2

Equations

• Proofs.Mnv2Live.bd₂ x✝ = 0

noncomputable def Proofs.Mnv2Live.Wp₂ : Kernel4 2 2 1 1

block2 project: identity channel map.

Equations

• Proofs.Mnv2Live.Wp₂ o i x✝¹ x✝ = if o = i then 1 else 0

noncomputable def Proofs.Mnv2Live.bp₂ : Vec 2

Equations

• Proofs.Mnv2Live.bp₂ x✝ = 0

noncomputable def Proofs.Mnv2Live.Wh : Mat 2 2

identity dense head ⇒ output = per-channel GAP.

Equations

• Proofs.Mnv2Live.Wh i j = if i = j then 1 else 0

noncomputable def Proofs.Mnv2Live.bh : Vec 2

Equations

• Proofs.Mnv2Live.bh x✝ = 0

noncomputable def Proofs.Mnv2Live.X : Vec (1 * 2 * 2)

Non-constant input.

Equations

• Proofs.Mnv2Live.X i = ↑↑i

noncomputable def Proofs.Mnv2Live.mnv2Live_has_vjp_at : HasVJPAt (mobilenetv2Forward Ws bs 1 1 3 We₁ be₁ 1 1 3 Wd₁ bd₁ 1 1 3 Wp₁ bp₁ 1 1 3 We₂ be₂ 1 1 3 Wd₂ bd₂ 1 1 3 Wp₂ bp₂ 1 1 3 Wh bh) X

Unconditional whole-network VJP on a nonzero, non-collapsed MobileNetV2. Every ReLU6 smoothness hypothesis of mobilenetv2_has_vjp_at is discharged by win (the window lemma) — not by a constant collapse. No side conditions; three-axiom closure.

Equations

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

theorem Proofs.Mnv2Live.mnv2Live_has_vjp_correct (dy : Vec 2) (i : Fin (1 * 2 * 2)) : mnv2Live_has_vjp_at.backward dy i = ∑ j : Fin 2, pdiv (mobilenetv2Forward Ws bs 1 1 3 We₁ be₁ 1 1 3 Wd₁ bd₁ 1 1 3 Wp₁ bp₁ 1 1 3 We₂ be₂ 1 1 3 Wd₂ bd₂ 1 1 3 Wp₂ bp₂ 1 1 3 Wh bh) X i j * dy j

Public unconditional correctness theorem — the nonzero-weight MobileNetV2's backward equals the pdiv-Jacobian VJP, no hypotheses.

theorem Proofs.Mnv2Live.conv2d_1x1' {ic oc h w : ℕ} (W : Kernel4 oc ic 1 1) (b : Vec oc) (t : Tensor3 ic h w) (o : Fin oc) (hi : Fin h) (wi : Fin w) : conv2d W b t o hi wi = b o + ∑ c : Fin ic, W o c 0 0 * t c hi wi

theorem Proofs.Mnv2Live.relu6_id_window (n : ℕ) (y : Vec n) (hy : ∀ (k : Fin n), 0 < y k ∧ y k < 6) : relu6 n y = y

ReLU6 is the identity wherever every coordinate is strictly inside (0,6).

theorem Proofs.Mnv2Live.flatConv_id2 (W : Kernel4 2 2 1 1) (b : Vec 2) (hW : ∀ (o i : Fin 2), W o i 0 0 = if o = i then 1 else 0) (hb : ∀ (o : Fin 2), b o = 0) (v : Vec (2 * 2 * 2)) : flatConv W b v = v

A 1×1 channel-identity conv (W o i = δ_oi, b = 0) is the identity.

theorem Proofs.Mnv2Live.depthwiseFlat_id1 (W : DepthwiseKernel 2 1 1) (b : Vec 2) (hW : ∀ (ch : Fin 2), W ch 0 0 = 1) (hb : ∀ (ch : Fin 2), b ch = 0) (v : Vec (2 * 2 * 2)) : depthwiseFlat W b v = v

The 1×1 unit depthwise conv (W = 1, b = 0) is the identity.

theorem Proofs.Mnv2Live.relu6_const3 (n : ℕ) : (relu6 n fun (x : Fin n) => 3) = fun (x : Fin n) => 3

ReLU6 fixes the constant-3 vector.

theorem Proofs.Mnv2Live.bn8_const (c : ℝ) : (bnForward (2 * 2 * 2) 1 1 3 fun (x : Fin (2 * 2 * 2)) => c) = fun (x : Fin (2 * 2 * 2)) => 3

BN (γ=1,β=3) sends the constant-c vector to constant 3.

theorem Proofs.Mnv2Live.relu6_bn8 (z : Vec (2 * 2 * 2)) : relu6 (2 * 2 * 2) (bnForward (2 * 2 * 2) 1 1 3 z) = bnForward (2 * 2 * 2) 1 1 3 z

ReLU6 fixes every BN output (the window lands in (0,6)).

theorem Proofs.Mnv2Live.invresBody₁_const (y : Vec (2 * 2 * 2)) : invresBody We₁ be₁ 1 1 3 Wd₁ bd₁ 1 1 3 Wp₁ bp₁ 1 1 3 y = fun (x : Fin (2 * 2 * 2)) => 3

The zeroed skip-block body is constantly 3, for any input.

theorem Proofs.Mnv2Live.invresBody₂_eq (y : Vec (2 * 2 * 2)) : invresBody We₂ be₂ 1 1 3 Wd₂ bd₂ 1 1 3 Wp₂ bp₂ 1 1 3 y = bnForward (2 * 2 * 2) 1 1 3 (bnForward (2 * 2 * 2) 1 1 3 (bnForward (2 * 2 * 2) 1 1 3 y))

Block-2 (identity convs) reduces to three genuine BN layers.

theorem Proofs.Mnv2Live.gap_const (c : ℝ) : (globalAvgPoolFlat 2 2 2 fun (x : Fin (2 * 2 * 2)) => c) = fun (x : Fin 2) => c

GAP of a constant vector is that constant.

theorem Proofs.Mnv2Live.dense_id3 (c : ℝ) : (dense Wh bh fun (x : Fin 2) => c) = fun (x : Fin 2) => c

The identity dense head fixes a constant vector.

theorem Proofs.Mnv2Live.flatConv_Ws_zero : (flatConv Ws bs fun (x : Fin (1 * 2 * 2)) => 0) = fun (x : Fin (2 * 2 * 2)) => 0

The stem conv sends the zero input to zero (bias 0).

theorem Proofs.Mnv2Live.forward_zero : (mobilenetv2Forward Ws bs 1 1 3 We₁ be₁ 1 1 3 Wd₁ bd₁ 1 1 3 Wp₁ bp₁ 1 1 3 We₂ be₂ 1 1 3 Wd₂ bd₂ 1 1 3 Wp₂ bp₂ 1 1 3 Wh bh fun (x : Fin (1 * 2 * 2)) => 0) = fun (x : Fin 2) => 3

forward 0 = 3 (constant) — the zero input collapses through every layer.

def Proofs.Mnv2Live.ι (p : Fin 2 × Fin 2) : Fin (2 * 2 * 2)

Flat index of channel-0 spatial position p (matches globalAvgPoolFlat_as_sum).

Equations

• Proofs.Mnv2Live.ι p = finProdFinEquiv (finProdFinEquiv (0, p.1), p.2)

noncomputable def Proofs.Mnv2Live.chSum (z : Vec (2 * 2 * 2)) : ℝ

Sum of channel-0 deviations from the (full-vector) mean.

Equations

• Proofs.Mnv2Live.chSum z = ∑ p : Fin 2 × Fin 2, (z (Proofs.Mnv2Live.ι p) - Proofs.bnMean (2 * 2 * 2) z)

theorem Proofs.Mnv2Live.bn8_sub3 (z : Vec (2 * 2 * 2)) (k : Fin (2 * 2 * 2)) : bnForward (2 * 2 * 2) 1 1 3 z k - 3 = (z k - bnMean (2 * 2 * 2) z) * bnIstd (2 * 2 * 2) z 1

Per-coordinate BN identity (γ=1, β=3): BN z k − 3 = (z k − μ)·istd.

theorem Proofs.Mnv2Live.chSum_bn (z : Vec (2 * 2 * 2)) : chSum (bnForward (2 * 2 * 2) 1 1 3 z) = bnIstd (2 * 2 * 2) z 1 * chSum z

BN rescales the channel-0 deviation sum by istd (no sqrt value needed).

theorem Proofs.Mnv2Live.chSum_const_add (c : ℝ) (z : Vec (2 * 2 * 2)) : (chSum fun (k : Fin (2 * 2 * 2)) => c + z k) = chSum z

Adding a constant leaves the channel-0 deviation sum unchanged.

theorem Proofs.Mnv2Live.gap0_eq (z : Vec (2 * 2 * 2)) : globalAvgPoolFlat 2 2 2 z 0 = 1 / 4 * chSum z + bnMean (2 * 2 * 2) z

GAP of channel 0 in terms of the deviation sum and the mean.

theorem Proofs.Mnv2Live.convX_chan (c hi wi : Fin 2) : conv2d Ws bs (Tensor3.unflatten X) c hi wi = (if c = 0 then 1 else 2) * Tensor3.unflatten X 0 hi wi

The stem conv at output channel c: (if c=0 then 1 else 2)·input.

theorem Proofs.Mnv2Live.convX_ι (p : Fin 2 × Fin 2) : flatConv Ws bs X (ι p) = Tensor3.unflatten X 0 p.1 p.2

convX at a channel-0 index is just the (channel-0) input there.

theorem Proofs.Mnv2Live.sumX0 : ∑ p : Fin 2 × Fin 2, Tensor3.unflatten X 0 p.1 p.2 = 6

Σ over the four channel-0 positions of the input is 6 (= 0+1+2+3).

theorem Proofs.Mnv2Live.sum_flatten8 (T : Tensor3 2 2 2) : ∑ k : Fin (2 * 2 * 2), T.flatten k = ∑ c : Fin 2, ∑ hi : Fin 2, ∑ wi : Fin 2, T c hi wi

Sum over a flattened tensor equals the tensor's triple sum (index reindex).

theorem Proofs.Mnv2Live.sumConvX : ∑ k : Fin (2 * 2 * 2), flatConv Ws bs X k = 18

The total of convX over all eight cells is 18 (= 6 + 12).

theorem Proofs.Mnv2Live.chSum_convX : chSum (flatConv Ws bs X) = -3

chSum convX = −3 — the stem plants a nonzero channel-0 asymmetry.

theorem Proofs.Mnv2Live.dense_Wh_apply (u : Vec 2) (j : Fin 2) : dense Wh bh u j = u j

The identity dense head reads off channel j.

theorem Proofs.Mnv2Live.forward_X_eq : mobilenetv2Forward Ws bs 1 1 3 We₁ be₁ 1 1 3 Wd₁ bd₁ 1 1 3 Wp₁ bp₁ 1 1 3 We₂ be₂ 1 1 3 Wd₂ bd₂ 1 1 3 Wp₂ bp₂ 1 1 3 Wh bh X = dense Wh bh (globalAvgPoolFlat 2 2 2 (bnForward (2 * 2 * 2) 1 1 3 (bnForward (2 * 2 * 2) 1 1 3 (bnForward (2 * 2 * 2) 1 1 3 fun (k : Fin (2 * 2 * 2)) => 3 + bnForward (2 * 2 * 2) 1 1 3 (flatConv Ws bs X) k))))

The X-forward reduces to four BN layers on a constant-shifted stem output.

theorem Proofs.Mnv2Live.mnv2Live_forward_nonconstant : mobilenetv2Forward Ws bs 1 1 3 We₁ be₁ 1 1 3 Wd₁ bd₁ 1 1 3 Wp₁ bp₁ 1 1 3 We₂ be₂ 1 1 3 Wd₂ bd₂ 1 1 3 Wp₂ bp₂ 1 1 3 Wh bh X ≠ mobilenetv2Forward Ws bs 1 1 3 We₁ be₁ 1 1 3 Wd₁ bd₁ 1 1 3 Wp₁ bp₁ 1 1 3 We₂ be₂ 1 1 3 Wd₂ bd₂ 1 1 3 Wp₂ bp₂ 1 1 3 Wh bh fun (x : Fin (1 * 2 * 2)) => 0

The live witness is non-degenerate: its forward computes a non-trivial function of the input — forward X ≠ forward 0. So the Jacobian is not identically zero, unlike MobileNetV2Concrete.