The PAPER-SPEC MobileNetV2 input-VJP — the fold at all seventeen bottlenecks

Closes MobileNetV2FullPaper.lean's standing TODO: Proofs.mobilenetv2_has_vjp_at (MobileNetV2.lean) folds a stem, TWO inverted-residual blocks and a head; this file folds the whole [t,c,n,s] table — stem + 17 bottlenecks + head — over the packaged IVW/IVWNoExp weight bundles of MobileNetV2FullPaper.lean.

⚠ The statement is the POINTWISE _at form, and that is not a limitation to be lifted. MobileNetV2's activation is relu6, which is kinked; a global HasVJP through a kink is false. EfficientNetFullB0.lean's efficientnetForwardB_full_has_vjp may be global only because EfficientNet's swish is smooth everywhere. The axis this file moves is DEPTH (2 → 17); the _at form is the repo standard for relu-family nets and stays.

What this file assembles (no new mathematics)

The per-block bodies already had certified VJPs — invresBodyPC_has_vjp_at and invresBodyStridedPC_has_vjp_at (MobileNetV2BackCertifiedTie.lean), built there as the §B tie targets. So the eight iv*W_{has_vjp_at, differentiableAt} bundle lemmas below are delegations in the EfficientNetFullB0 style, not fresh six-operation compositions. Only two per-stage pieces were genuinely missing and are supplied here: the differentiability peers of those two body VJPs, and the per-channel STRIDED stem stage convBnRelu6StridedPC_* (MobileNetV2.lean's convBnRelu6Strided_* is the global-bnForward twin, not the per-channel one the paper-spec net renders).

The hypothesis budget, and why the prefix defs exist

Seventeen blocks carry 33 relu6 sites plus the stem's and the head's, each of which must be stated AT the running activation. Spelled inline that is unreadable by block 5 and quadratic in the writing. So the running activations are named — mnv2StemW, then mnv2Pre1 … mnv2Pre17, each one ∘ deeper — and the kink conditions are bundled per block into IVSmoothAt / IVStridedSmoothAt / IVNoExpSmoothAt. The BN-epsilon positivity is bundled the same way (IVPos, IVNoExpPos). The theorem then binds 19 smoothness hypotheses and 19 positivity bundles rather than 35 and 52 loose ones.

The prefix defs double as the chain: mnv2Pre17 IS the 17-block trunk, so the VJP is stated on mnv2HeadW w ∘ mnv2Pre17 w and mobilenetv2ForwardPaper_eq_chain bridges that back to the nested-application forward, exactly as efficientnetForwardB_full_eq_chain does for B0.

noncomputable def Proofs.convBnRelu6StridedPC_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 * (2 * h) * (2 * w))) (h_smooth : ∀ (k : Fin (oc * h * w)), bnPerChannelTensor3 oc h w ε γ β (flatConvStride2Xla W b v) k ≠ 0 ∧ bnPerChannelTensor3 oc h w ε γ β (flatConvStride2Xla W b v) k ≠ 6) : HasVJPAt (relu6 (oc * h * w) ∘ bnPerChannelTensor3 oc h w ε γ β ∘ flatConvStride2Xla W b) v

Strided stem stage VJP, per-channel BN: relu6 ∘ bnPC ∘ flatConvStride2Xla. The per-channel twin of MobileNetV2.lean's convBnRelu6Strided_has_vjp_at, in the bnPerChannelTensor3 vocabulary the paper-spec net renders.

Equations

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

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

theorem Proofs.invresBodyPC_differentiableAt {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) : DifferentiableAt ℝ (invresBodyPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

Differentiability peer of invresBodyPC_has_vjp_at (which MobileNetV2BackCertifiedTie did not need, having no residual wrapper to feed).

theorem Proofs.invresBodyStridedPC_differentiableAt {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) : DifferentiableAt ℝ (invresBodyStridedPC We be εe γe βe Wd bd εd γd βd Wp bp εp γp βp) v

Differentiability peer of invresBodyStridedPC_has_vjp_at.

structure Proofs.IVPos {ic mid oc : ℕ} (q : IVW ic mid oc) : Prop

The three BN epsilons of a full bottleneck are positive.

• he : 0 < q.eε
• hd : 0 < q.dε
• hp : 0 < q.pε

structure Proofs.IVNoExpPos {ic oc : ℕ} (q : IVWNoExp ic oc) : Prop

The two BN epsilons of the t=1 (no-expand) bottleneck are positive.

• hd : 0 < q.dε
• hp : 0 < q.pε

structure Proofs.IVSmoothAt (h w : ℕ) {ic mid oc : ℕ} (q : IVW ic mid oc) (v : Vec (ic * h * w)) : Prop

Both relu6 sites of a stride-1 bottleneck are away from the kink at v: the expand-BN output and the depthwise-BN output each avoid 0 and 6 in every coordinate.

• he (k : Fin (mid * h * w)) : bnPerChannelTensor3 mid h w q.eε q.eγ q.eβ (flatConv q.eW q.eb v) k ≠ 0 ∧ bnPerChannelTensor3 mid h w q.eε q.eγ q.eβ (flatConv q.eW q.eb v) k ≠ 6
• hd (k : Fin (mid * h * w)) : bnPerChannelTensor3 mid h w q.dε q.dγ q.dβ (depthwiseFlat q.dW q.db (ivExpandPC q.eW q.eb q.eε q.eγ q.eβ v)) k ≠ 0 ∧ bnPerChannelTensor3 mid h w q.dε q.dγ q.dβ (depthwiseFlat q.dW q.db (ivExpandPC q.eW q.eb q.eε q.eγ q.eβ v)) k ≠ 6

structure Proofs.IVStridedSmoothAt (h w : ℕ) {ic mid oc : ℕ} (q : IVW ic mid oc) (v : Vec (ic * (2 * h) * (2 * w))) : Prop

Both relu6 sites of a stride-2 bottleneck are away from the kink at v (the expand runs at the pre-downsample 2h×2w grid, the depthwise at h×w).

• he (k : Fin (mid * (2 * h) * (2 * w))) : bnPerChannelTensor3 mid (2 * h) (2 * w) q.eε q.eγ q.eβ (flatConv q.eW q.eb v) k ≠ 0 ∧ bnPerChannelTensor3 mid (2 * h) (2 * w) q.eε q.eγ q.eβ (flatConv q.eW q.eb v) k ≠ 6
• hd (k : Fin (mid * h * w)) : bnPerChannelTensor3 mid h w q.dε q.dγ q.dβ (depthwiseStride2FlatXla q.dW q.db (ivExpandPC q.eW q.eb q.eε q.eγ q.eβ v)) k ≠ 0 ∧ bnPerChannelTensor3 mid h w q.dε q.dγ q.dβ (depthwiseStride2FlatXla q.dW q.db (ivExpandPC q.eW q.eb q.eε q.eγ q.eβ v)) k ≠ 6

structure Proofs.IVNoExpSmoothAt (h w : ℕ) {ic oc : ℕ} (q : IVWNoExp ic oc) (v : Vec (ic * h * w)) : Prop

The single relu6 site of the t=1 bottleneck (depthwise-BN output) is away from the kink.

• hd (k : Fin (ic * h * w)) : bnPerChannelTensor3 ic h w q.dε q.dγ q.dβ (depthwiseFlat q.dW q.db v) k ≠ 0 ∧ bnPerChannelTensor3 ic h w q.dε q.dγ q.dβ (depthwiseFlat q.dW q.db v) k ≠ 6

noncomputable def Proofs.ivNoExpW_has_vjp_at (h w : ℕ) {ic oc : ℕ} (p : IVWNoExp ic oc) (hq : IVNoExpPos p) (v : Vec (ic * h * w)) (hs : IVNoExpSmoothAt h w p v) : HasVJPAt (ivNoExpW h w p) v

t=1 bottleneck VJP: ivProjectPC ∘ ivDepthwisePC. The one block shape with no invresBody*PC body lemma to delegate to, so it composes its two stages here.

Equations

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

theorem Proofs.ivNoExpW_differentiableAt (h w : ℕ) {ic oc : ℕ} (p : IVWNoExp ic oc) (hq : IVNoExpPos p) (v : Vec (ic * h * w)) (hs : IVNoExpSmoothAt h w p v) : DifferentiableAt ℝ (ivNoExpW h w p) v

noncomputable def Proofs.ivExpOnlyW_has_vjp_at (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (hq : IVPos p) (v : Vec (ic * h * w)) (hs : IVSmoothAt h w p v) : HasVJPAt (ivExpOnlyW h w p) v

Stride-1 no-skip bottleneck VJP — invresBodyPC_has_vjp_at at the bundle's fields.

Equations

• Proofs.ivExpOnlyW_has_vjp_at h w p hq v hs = id (Proofs.invresBodyPC_has_vjp_at p.eW p.eb p.eε p.eγ p.eβ ⋯ p.dW p.db p.dε p.dγ p.dβ ⋯ p.pW p.pb p.pε p.pγ p.pβ ⋯ v ⋯ ⋯)

theorem Proofs.ivExpOnlyW_differentiableAt (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (hq : IVPos p) (v : Vec (ic * h * w)) (hs : IVSmoothAt h w p v) : DifferentiableAt ℝ (ivExpOnlyW h w p) v

noncomputable def Proofs.ivResidW_has_vjp_at (h w : ℕ) {c mid : ℕ} (p : IVW c mid c) (hq : IVPos p) (v : Vec (c * h * w)) (hs : IVSmoothAt h w p v) : HasVJPAt (ivResidW h w p) v

Stride-1 skip bottleneck VJP — the body VJP under residual_has_vjp_at. The identity arm is smooth everywhere, so it adds no hypothesis.

Equations

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

theorem Proofs.ivResidW_differentiableAt (h w : ℕ) {c mid : ℕ} (p : IVW c mid c) (hq : IVPos p) (v : Vec (c * h * w)) (hs : IVSmoothAt h w p v) : DifferentiableAt ℝ (ivResidW h w p) v

noncomputable def Proofs.ivStridedW_has_vjp_at (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (hq : IVPos p) (v : Vec (ic * (2 * h) * (2 * w))) (hs : IVStridedSmoothAt h w p v) : HasVJPAt (ivStridedW h w p) v

Stride-2 downsampling bottleneck VJP — invresBodyStridedPC_has_vjp_at at the bundle.

Equations

• Proofs.ivStridedW_has_vjp_at h w p hq v hs = id (Proofs.invresBodyStridedPC_has_vjp_at p.eW p.eb p.eε p.eγ p.eβ ⋯ p.dW p.db p.dε p.dγ p.dβ ⋯ p.pW p.pb p.pε p.pγ p.pβ ⋯ v ⋯ ⋯)

theorem Proofs.ivStridedW_differentiableAt (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (hq : IVPos p) (v : Vec (ic * (2 * h) * (2 * w))) (hs : IVStridedSmoothAt h w p v) : DifferentiableAt ℝ (ivStridedW h w p) v

noncomputable def Proofs.mnv2StemW (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (32 * 112 * 112)

The paper-spec stem: 3×3 stride-2 conv 3→32 at 224² → per-channel BN → relu6.

Equations

• Proofs.mnv2StemW w = Proofs.relu6 (32 * 112 * 112) ∘ Proofs.bnPerChannelTensor3 32 112 112 w.sε w.sγ w.sβ ∘ Proofs.flatConvStride2Xla w.sW w.sb

noncomputable def Proofs.mnv2HeadW (w : MNV2PaperWeights) : Vec (320 * 7 * 7) → Vec 10

The paper-spec head: 1×1 conv 320→1280 → per-channel BN → relu6 → GAP → dense 1280→10.

Equations

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

def Proofs.MNV2StemSmoothAt (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : Prop

Stem relu6 away from the kink at the input x.

Equations

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

def Proofs.MNV2HeadSmoothAt (w : MNV2PaperWeights) (v : Vec (320 * 7 * 7)) : Prop

Head relu6 away from the kink at the trunk output v.

Equations

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

noncomputable def Proofs.mnv2StemW_has_vjp_at (w : MNV2PaperWeights) (hs : 0 < w.sε) (x : Vec (3 * 224 * 224)) (h_stem : MNV2StemSmoothAt w x) : HasVJPAt (mnv2StemW w) x

Equations

• Proofs.mnv2StemW_has_vjp_at w hs x h_stem = Proofs.convBnRelu6StridedPC_has_vjp_at w.sW w.sb w.sε w.sγ w.sβ hs x h_stem

theorem Proofs.mnv2StemW_differentiableAt (w : MNV2PaperWeights) (hs : 0 < w.sε) (x : Vec (3 * 224 * 224)) (h_stem : MNV2StemSmoothAt w x) : DifferentiableAt ℝ (mnv2StemW w) x

noncomputable def Proofs.mnv2HeadW_has_vjp_at (w : MNV2PaperWeights) (hh : 0 < w.hε) (v : Vec (320 * 7 * 7)) (h_head : MNV2HeadSmoothAt w v) : HasVJPAt (mnv2HeadW w) v

Equations

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

theorem Proofs.mnv2HeadW_differentiableAt (w : MNV2PaperWeights) (hh : 0 < w.hε) (v : Vec (320 * 7 * 7)) (h_head : MNV2HeadSmoothAt w v) : DifferentiableAt ℝ (mnv2HeadW w) v

noncomputable def Proofs.mnv2Pre1 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (16 * 112 * 112)

Equations

• Proofs.mnv2Pre1 w = Proofs.ivNoExpW 112 112 w.b1 ∘ Proofs.mnv2StemW w

noncomputable def Proofs.mnv2Pre2 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (24 * 56 * 56)

Equations

• Proofs.mnv2Pre2 w = Proofs.ivStridedW 56 56 w.b2 ∘ Proofs.mnv2Pre1 w

noncomputable def Proofs.mnv2Pre3 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (24 * 56 * 56)

Equations

• Proofs.mnv2Pre3 w = Proofs.ivResidW 56 56 w.b3 ∘ Proofs.mnv2Pre2 w

noncomputable def Proofs.mnv2Pre4 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (32 * 28 * 28)

Equations

• Proofs.mnv2Pre4 w = Proofs.ivStridedW 28 28 w.b4 ∘ Proofs.mnv2Pre3 w

noncomputable def Proofs.mnv2Pre5 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (32 * 28 * 28)

Equations

• Proofs.mnv2Pre5 w = Proofs.ivResidW 28 28 w.b5 ∘ Proofs.mnv2Pre4 w

noncomputable def Proofs.mnv2Pre6 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (32 * 28 * 28)

Equations

• Proofs.mnv2Pre6 w = Proofs.ivResidW 28 28 w.b6 ∘ Proofs.mnv2Pre5 w

noncomputable def Proofs.mnv2Pre7 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (64 * 14 * 14)

Equations

• Proofs.mnv2Pre7 w = Proofs.ivStridedW 14 14 w.b7 ∘ Proofs.mnv2Pre6 w

noncomputable def Proofs.mnv2Pre8 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (64 * 14 * 14)

Equations

• Proofs.mnv2Pre8 w = Proofs.ivResidW 14 14 w.b8 ∘ Proofs.mnv2Pre7 w

noncomputable def Proofs.mnv2Pre9 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (64 * 14 * 14)

Equations

• Proofs.mnv2Pre9 w = Proofs.ivResidW 14 14 w.b9 ∘ Proofs.mnv2Pre8 w

noncomputable def Proofs.mnv2Pre10 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (64 * 14 * 14)

Equations

• Proofs.mnv2Pre10 w = Proofs.ivResidW 14 14 w.b10 ∘ Proofs.mnv2Pre9 w

noncomputable def Proofs.mnv2Pre11 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (96 * 14 * 14)

Equations

• Proofs.mnv2Pre11 w = Proofs.ivExpOnlyW 14 14 w.b11 ∘ Proofs.mnv2Pre10 w

noncomputable def Proofs.mnv2Pre12 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (96 * 14 * 14)

Equations

• Proofs.mnv2Pre12 w = Proofs.ivResidW 14 14 w.b12 ∘ Proofs.mnv2Pre11 w

noncomputable def Proofs.mnv2Pre13 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (96 * 14 * 14)

Equations

• Proofs.mnv2Pre13 w = Proofs.ivResidW 14 14 w.b13 ∘ Proofs.mnv2Pre12 w

noncomputable def Proofs.mnv2Pre14 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (160 * 7 * 7)

Equations

• Proofs.mnv2Pre14 w = Proofs.ivStridedW 7 7 w.b14 ∘ Proofs.mnv2Pre13 w

noncomputable def Proofs.mnv2Pre15 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (160 * 7 * 7)

Equations

• Proofs.mnv2Pre15 w = Proofs.ivResidW 7 7 w.b15 ∘ Proofs.mnv2Pre14 w

noncomputable def Proofs.mnv2Pre16 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (160 * 7 * 7)

Equations

• Proofs.mnv2Pre16 w = Proofs.ivResidW 7 7 w.b16 ∘ Proofs.mnv2Pre15 w

noncomputable def Proofs.mnv2Pre17 (w : MNV2PaperWeights) : Vec (3 * 224 * 224) → Vec (320 * 7 * 7)

Equations

• Proofs.mnv2Pre17 w = Proofs.ivExpOnlyW 7 7 w.b17 ∘ Proofs.mnv2Pre16 w

noncomputable def Proofs.mobilenetv2_full_has_vjp_at (w : MNV2PaperWeights) (hs : 0 < w.sε) (q1 : IVNoExpPos w.b1) (q2 : IVPos w.b2) (q3 : IVPos w.b3) (q4 : IVPos w.b4) (q5 : IVPos w.b5) (q6 : IVPos w.b6) (q7 : IVPos w.b7) (q8 : IVPos w.b8) (q9 : IVPos w.b9) (q10 : IVPos w.b10) (q11 : IVPos w.b11) (q12 : IVPos w.b12) (q13 : IVPos w.b13) (q14 : IVPos w.b14) (q15 : IVPos w.b15) (q16 : IVPos w.b16) (q17 : IVPos w.b17) (hh : 0 < w.hε) (x : Vec (3 * 224 * 224)) (h_stem : MNV2StemSmoothAt w x) (s1 : IVNoExpSmoothAt 112 112 w.b1 (mnv2StemW w x)) (s2 : IVStridedSmoothAt 56 56 w.b2 (mnv2Pre1 w x)) (s3 : IVSmoothAt 56 56 w.b3 (mnv2Pre2 w x)) (s4 : IVStridedSmoothAt 28 28 w.b4 (mnv2Pre3 w x)) (s5 : IVSmoothAt 28 28 w.b5 (mnv2Pre4 w x)) (s6 : IVSmoothAt 28 28 w.b6 (mnv2Pre5 w x)) (s7 : IVStridedSmoothAt 14 14 w.b7 (mnv2Pre6 w x)) (s8 : IVSmoothAt 14 14 w.b8 (mnv2Pre7 w x)) (s9 : IVSmoothAt 14 14 w.b9 (mnv2Pre8 w x)) (s10 : IVSmoothAt 14 14 w.b10 (mnv2Pre9 w x)) (s11 : IVSmoothAt 14 14 w.b11 (mnv2Pre10 w x)) (s12 : IVSmoothAt 14 14 w.b12 (mnv2Pre11 w x)) (s13 : IVSmoothAt 14 14 w.b13 (mnv2Pre12 w x)) (s14 : IVStridedSmoothAt 7 7 w.b14 (mnv2Pre13 w x)) (s15 : IVSmoothAt 7 7 w.b15 (mnv2Pre14 w x)) (s16 : IVSmoothAt 7 7 w.b16 (mnv2Pre15 w x)) (s17 : IVSmoothAt 7 7 w.b17 (mnv2Pre16 w x)) (h_head : MNV2HeadSmoothAt w (mnv2Pre17 w x)) : HasVJPAt (mnv2HeadW w ∘ mnv2Pre17 w) x

The paper-spec MobileNetV2 has a (correct) input-VJP at a smooth point — all seventeen bottlenecks. Chains stem → the 17 blocks of the [t,c,n,s] table → head with vjp_comp_at, one IVPos bundle and one *SmoothAt bundle per block. The full-depth replacement for mobilenetv2_has_vjp_at's two-block fold.

⚠ Pointwise (HasVJPAt), not global (HasVJP), and necessarily so: relu6 is kinked, so each of the 35 activation sites carries a ≠ 0 ∧ ≠ 6 side condition at its running activation. EfficientNet-B0's global fold is available to it only because swish is smooth.

Equations

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

theorem Proofs.mnv2StemW_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2StemW w x = relu6 (32 * 112 * 112) (bnPerChannelTensor3 32 112 112 w.sε w.sγ w.sβ (flatConvStride2Xla w.sW w.sb x))

theorem Proofs.mnv2HeadW_apply (w : MNV2PaperWeights) (v : Vec (320 * 7 * 7)) : mnv2HeadW w v = dense w.fcW w.fcb (globalAvgPoolFlat 1280 7 7 (relu6 (1280 * 7 * 7) (bnPerChannelTensor3 1280 7 7 w.hε w.hγ w.hβ (flatConv w.hW w.hb v))))

theorem Proofs.mnv2Pre1_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre1 w x = ivNoExpW 112 112 w.b1 (mnv2StemW w x)

theorem Proofs.mnv2Pre2_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre2 w x = ivStridedW 56 56 w.b2 (mnv2Pre1 w x)

theorem Proofs.mnv2Pre3_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre3 w x = ivResidW 56 56 w.b3 (mnv2Pre2 w x)

theorem Proofs.mnv2Pre4_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre4 w x = ivStridedW 28 28 w.b4 (mnv2Pre3 w x)

theorem Proofs.mnv2Pre5_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre5 w x = ivResidW 28 28 w.b5 (mnv2Pre4 w x)

theorem Proofs.mnv2Pre6_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre6 w x = ivResidW 28 28 w.b6 (mnv2Pre5 w x)

theorem Proofs.mnv2Pre7_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre7 w x = ivStridedW 14 14 w.b7 (mnv2Pre6 w x)

theorem Proofs.mnv2Pre8_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre8 w x = ivResidW 14 14 w.b8 (mnv2Pre7 w x)

theorem Proofs.mnv2Pre9_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre9 w x = ivResidW 14 14 w.b9 (mnv2Pre8 w x)

theorem Proofs.mnv2Pre10_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre10 w x = ivResidW 14 14 w.b10 (mnv2Pre9 w x)

theorem Proofs.mnv2Pre11_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre11 w x = ivExpOnlyW 14 14 w.b11 (mnv2Pre10 w x)

theorem Proofs.mnv2Pre12_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre12 w x = ivResidW 14 14 w.b12 (mnv2Pre11 w x)

theorem Proofs.mnv2Pre13_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre13 w x = ivResidW 14 14 w.b13 (mnv2Pre12 w x)

theorem Proofs.mnv2Pre14_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre14 w x = ivStridedW 7 7 w.b14 (mnv2Pre13 w x)

theorem Proofs.mnv2Pre15_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre15 w x = ivResidW 7 7 w.b15 (mnv2Pre14 w x)

theorem Proofs.mnv2Pre16_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre16 w x = ivResidW 7 7 w.b16 (mnv2Pre15 w x)

theorem Proofs.mnv2Pre17_apply (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mnv2Pre17 w x = ivExpOnlyW 7 7 w.b17 (mnv2Pre16 w x)

theorem Proofs.mobilenetv2ForwardPaper_eq_chain (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : mobilenetv2ForwardPaper w x = (mnv2HeadW w ∘ mnv2Pre17 w) x

mobilenetv2ForwardPaper = the ∘-chain the VJP is stated on — the kernel-checked bridge between the nested-application forward and the layered mnv2PreK form, closing the same form-gap efficientnetForwardB_full_eq_chain closes for B0. Peeled one layer at a time through the *_apply lemmas above; see their section header for why the one-step proofs do not survive (elaborator recursion depth / kernel deterministic timeout).

theorem Proofs.mobilenetv2_full_has_vjp_at_correct (w : MNV2PaperWeights) (hs : 0 < w.sε) (q1 : IVNoExpPos w.b1) (q2 : IVPos w.b2) (q3 : IVPos w.b3) (q4 : IVPos w.b4) (q5 : IVPos w.b5) (q6 : IVPos w.b6) (q7 : IVPos w.b7) (q8 : IVPos w.b8) (q9 : IVPos w.b9) (q10 : IVPos w.b10) (q11 : IVPos w.b11) (q12 : IVPos w.b12) (q13 : IVPos w.b13) (q14 : IVPos w.b14) (q15 : IVPos w.b15) (q16 : IVPos w.b16) (q17 : IVPos w.b17) (hh : 0 < w.hε) (x : Vec (3 * 224 * 224)) (h_stem : MNV2StemSmoothAt w x) (s1 : IVNoExpSmoothAt 112 112 w.b1 (mnv2StemW w x)) (s2 : IVStridedSmoothAt 56 56 w.b2 (mnv2Pre1 w x)) (s3 : IVSmoothAt 56 56 w.b3 (mnv2Pre2 w x)) (s4 : IVStridedSmoothAt 28 28 w.b4 (mnv2Pre3 w x)) (s5 : IVSmoothAt 28 28 w.b5 (mnv2Pre4 w x)) (s6 : IVSmoothAt 28 28 w.b6 (mnv2Pre5 w x)) (s7 : IVStridedSmoothAt 14 14 w.b7 (mnv2Pre6 w x)) (s8 : IVSmoothAt 14 14 w.b8 (mnv2Pre7 w x)) (s9 : IVSmoothAt 14 14 w.b9 (mnv2Pre8 w x)) (s10 : IVSmoothAt 14 14 w.b10 (mnv2Pre9 w x)) (s11 : IVSmoothAt 14 14 w.b11 (mnv2Pre10 w x)) (s12 : IVSmoothAt 14 14 w.b12 (mnv2Pre11 w x)) (s13 : IVSmoothAt 14 14 w.b13 (mnv2Pre12 w x)) (s14 : IVStridedSmoothAt 7 7 w.b14 (mnv2Pre13 w x)) (s15 : IVSmoothAt 7 7 w.b15 (mnv2Pre14 w x)) (s16 : IVSmoothAt 7 7 w.b16 (mnv2Pre15 w x)) (s17 : IVSmoothAt 7 7 w.b17 (mnv2Pre16 w x)) (h_head : MNV2HeadSmoothAt w (mnv2Pre17 w x)) (dy : Vec 10) (i : Fin (3 * 224 * 224)) : (mobilenetv2_full_has_vjp_at w hs q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 q13 q14 q15 q16 q17 hh x h_stem s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 h_head).backward dy i = ∑ j : Fin 10, pdiv (mobilenetv2ForwardPaper w) x i j * dy j

Public correctness theorem for mobilenetv2_full_has_vjp_at — the seventeen-block backward equals the pdiv-contracted Jacobian of mobilenetv2ForwardPaper ITSELF (not of the chain it is stated on), tied back through mobilenetv2ForwardPaper_eq_chain. The full-depth analogue of mobilenetv2_has_vjp_at_correct.