The PAPER-SPEC MobileNetV2 — all 17 bottleneck blocks, forward graph + faithfulness

Scales MobileNetV2RenderPC.lean's reduced ch7 net (strided stem + 6 inverted-residual blocks + 1×1 head) to the real MobileNetV2 [t,c,n,s] table — 17 bottleneck blocks at 224² — closing the "honest caveat on full" in planning/archive/mobilenetv2_close.md. Pure enumeration + chaining of the per-channel stage machinery (ivExpandPC/ivDepthwisePC/ ivDepthwiseStridedPC/ivProjectPC), the EfficientNetFullB0 recipe; the only genuinely-new block shape is the t=1 first bottleneck (no expand conv — depthwise → BN → relu6 → project → BN, the torchvision/official layout).

Paper [t,c,n,s] spec (stem 3×3-s2 3→32; head 1×1 320→1280 → GAP → dense): (1, 16,1,1) (6, 24,2,2) (6, 32,3,2) (6, 64,4,2) (6, 96,3,1) (6,160,3,2) (6,320,1,1) Per-block (ic→oc, mid=t·ic, spatial, kind): b1 32→16 mid32 @112 noExp(t=1) b10 64→64 mid384 @14 resid b2 16→24 mid96 112→56 strided b11 64→96 mid384 @14 exp(no-resid, s=1) b3 24→24 mid144 @56 resid b12 96→96 mid576 @14 resid b4 24→32 mid144 56→28 strided b13 96→96 mid576 @14 resid b5 32→32 mid192 @28 resid b14 96→160 mid576 14→7 strided b6 32→32 mid192 @28 resid b15 160→160 mid960 @7 resid b7 32→64 mid192 28→14 strided b16 160→160 mid960 @7 resid b8 64→64 mid384 @14 resid b17 160→320 mid960 @7 exp(no-resid, s=1) b9 64→64 mid384 @14 resid

Like ResNet-34's full net (ResNet34RenderPC), the deliverable HERE is forward + graph + faithfulness; the param-grad close is already covered: every MobileNetV2Close/MobileNetV2ChainClose bridge is dim-polymorphic and applies at the paper shapes verbatim.

The whole-net input-VJP at all seventeen now exists, one file over: Proofs.mobilenetv2_full_has_vjp_at (MobileNetV2FullVJP.lean), folded over the IVW/IVWNoExp bundles and the four block wrappers defined below. It replaces Proofs.mobilenetv2_has_vjp_at (MobileNetV2.lean:489), which binds a stem, TWO inverted-residual blocks and a head.

⚠ That fold is POINTWISE (HasVJPAt), and that is not a limitation waiting to be lifted. relu6 is kinked, so a global HasVJP through it is false and each of the 35 activation sites carries a ≠ 0 ∧ ≠ 6 side condition at its running activation. EfficientNetFullB0.lean's efficientnetForwardB_full_has_vjp is a GLOBAL HasVJP over all 16 blocks only because EfficientNet's activation is swish, smooth everywhere (ch7's MLIR caveat: the SE fan-in carries no kink condition, and the only smooth-point hypotheses are the BatchNorms' 0 < ε). Pointwise-only is the repo standard for relu-family nets, same as full ResNet-34. The axis the fold moved was DEPTH (2 → 17), not pointwise → global.

structure Proofs.IVW (ic mid oc : ℕ) : Type

Weights of one MobileNetV2 bottleneck (expand ic→mid 1×1, depthwise 3×3, project mid→oc 1×1, per-channel BN after each).

• eW : Kernel4 mid ic 1 1
• eb : Vec mid
• eε : ℝ
• eγ : Vec mid
• eβ : Vec mid
• dW : DepthwiseKernel mid 3 3
• db : Vec mid
• dε : ℝ
• dγ : Vec mid
• dβ : Vec mid
• pW : Kernel4 oc mid 1 1
• pb : Vec oc
• pε : ℝ
• pγ : Vec oc
• pβ : Vec oc

structure Proofs.IVWNoExp (ic oc : ℕ) : Type

Weights of the t=1 first bottleneck (NO expand conv): depthwise 3×3 on ic, project ic→oc 1×1, per-channel BN after each.

• dW : DepthwiseKernel ic 3 3
• db : Vec ic
• dε : ℝ
• dγ : Vec ic
• dβ : Vec ic
• pW : Kernel4 oc ic 1 1
• pb : Vec oc
• pε : ℝ
• pγ : Vec oc
• pβ : Vec oc

structure Proofs.MNV2PaperWeights : Type

All paper-spec MobileNetV2 parameters: stem (3×3-s2 3→32) + the 17 bottlenecks of the [t,c,n,s] table + head (1×1 320→1280) + dense (1280→10).

• sW : Kernel4 32 3 3 3
• sb : Vec 32
• sε : ℝ
• sγ : Vec 32
• sβ : Vec 32
• b1 : IVWNoExp 32 16
• b2 : IVW 16 96 24
• b3 : IVW 24 144 24
• b4 : IVW 24 144 32
• b5 : IVW 32 192 32
• b6 : IVW 32 192 32
• b7 : IVW 32 192 64
• b8 : IVW 64 384 64
• b9 : IVW 64 384 64
• b10 : IVW 64 384 64
• b11 : IVW 64 384 96
• b12 : IVW 96 576 96
• b13 : IVW 96 576 96
• b14 : IVW 96 576 160
• b15 : IVW 160 960 160
• b16 : IVW 160 960 160
• b17 : IVW 160 960 320
• hW : Kernel4 1280 320 1 1
• hb : Vec 1280
• hε : ℝ
• hγ : Vec 1280
• hβ : Vec 1280
• fcW : Mat 1280 10
• fcb : Vec 10

noncomputable def Proofs.ivNoExpW (h w : ℕ) {ic oc : ℕ} (p : IVWNoExp ic oc) : Vec (ic * h * w) → Vec (oc * h * w)

t=1 bottleneck (no expand, stride-1, no skip — ic ≠ oc): project ∘ depthwise.

Equations

• Proofs.ivNoExpW h w p = Proofs.ivProjectPC p.pW p.pb p.pε p.pγ p.pβ ∘ Proofs.ivDepthwisePC p.dW p.db p.dε p.dγ p.dβ

noncomputable def Proofs.ivExpOnlyW (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) : Vec (ic * h * w) → Vec (oc * h * w)

Stride-1 bottleneck WITHOUT skip (ic ≠ oc, the stage-first blocks of the s=1 stages): plain invresBodyPC.

Equations

• Proofs.ivExpOnlyW h w p = Proofs.invresBodyPC 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β

noncomputable def Proofs.ivResidW (h w : ℕ) {c mid : ℕ} (p : IVW c mid c) : Vec (c * h * w) → Vec (c * h * w)

Stride-1 bottleneck WITH the identity skip (s = 1 ∧ ic = oc).

Equations

• Proofs.ivResidW h w p = Proofs.residual (Proofs.invresBodyPC 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β)

noncomputable def Proofs.ivStridedW (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

Stride-2 downsampling bottleneck (no skip).

Equations

• Proofs.ivStridedW h w p = Proofs.invresBodyStridedPC 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β

noncomputable def Proofs.mobilenetv2ForwardPaper (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : Vec 10

Equations

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

def Proofs.StableHLO.ivNoExpGraphW (pfx epsStr : String) (h w : ℕ) {ic oc : ℕ} (p : IVWNoExp ic oc) (e : SHlo (ic * h * w)) : SHlo (oc * h * w)

t=1 bottleneck graph: bnPC ∘ conv1×1 ∘ relu6 ∘ bnPC ∘ depthwise.

Equations

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

theorem Proofs.StableHLO.ivNoExpGraphW_faithful (pfx epsStr : String) (h w : ℕ) {ic oc : ℕ} (p : IVWNoExp ic oc) (e : SHlo (ic * h * w)) : den (ivNoExpGraphW pfx epsStr h w p e) = ivNoExpW h w p (den e)

def Proofs.StableHLO.ivExpOnlyGraphW (pfx epsStr : String) (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (e : SHlo (ic * h * w)) : SHlo (oc * h * w)

Stride-1 no-skip bottleneck graph: expand → depthwise → project (per-channel BN).

Equations

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

theorem Proofs.StableHLO.ivExpOnlyGraphW_faithful (pfx epsStr : String) (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (e : SHlo (ic * h * w)) : den (ivExpOnlyGraphW pfx epsStr h w p e) = ivExpOnlyW h w p (den e)

def Proofs.StableHLO.ivResidGraphW (pfx epsStr : String) (h w : ℕ) {c mid : ℕ} (p : IVW c mid c) (e : SHlo (c * h * w)) : SHlo (c * h * w)

Stride-1 skip bottleneck graph: the body + the addV identity skip (input subtree shared between both arms).

Equations

• Proofs.StableHLO.ivResidGraphW pfx epsStr h w p e = (Proofs.StableHLO.ivExpOnlyGraphW pfx epsStr h w p e).addV e

theorem Proofs.StableHLO.ivResidGraphW_faithful (pfx epsStr : String) (h w : ℕ) {c mid : ℕ} (p : IVW c mid c) (e : SHlo (c * h * w)) : den (ivResidGraphW pfx epsStr h w p e) = ivResidW h w p (den e)

def Proofs.StableHLO.ivStridedGraphW (pfx epsStr : String) (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (e : SHlo (ic * (2 * h) * (2 * w))) : SHlo (oc * h * w)

Stride-2 downsampling bottleneck graph: expand (at 2h×2w) → strided depthwise → project (per-channel BN).

Equations

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

theorem Proofs.StableHLO.ivStridedGraphW_faithful (pfx epsStr : String) (h w : ℕ) {ic mid oc : ℕ} (p : IVW ic mid oc) (e : SHlo (ic * (2 * h) * (2 * w))) : den (ivStridedGraphW pfx epsStr h w p e) = ivStridedW h w p (den e)

def Proofs.StableHLO.mobilenetv2FwdGraphPaper (epsStr : String) (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : SHlo 10

The full paper-spec MobileNetV2 forward graph (3×224² → 10): strided stem → the 17 bottlenecks of the [t,c,n,s] table (4 stride-2 downsamples, 10 identity skips, 2 stage-first s=1 widenings, the t=1 no-expand first block) → 1×1 conv-bn-relu6 head → GAP → dense. Per-channel BN throughout.

Equations

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

theorem Proofs.StableHLO.mobilenetv2FwdGraphPaper_faithful (epsStr : String) (w : MNV2PaperWeights) (x : Vec (3 * 224 * 224)) : den (mobilenetv2FwdGraphPaper epsStr w x) = mobilenetv2ForwardPaper w x

Full paper-spec MobileNetV2 forward faithfulness. The 17-bottleneck graph denotes mobilenetv2ForwardPaper — chained from the per-block-kind *GraphW_faithful lemmas (the EfficientNetFullB0 recipe), then a structural rfl (the forward is nested-application form, blocks opaque).