EfficientNet — MBConv with Squeeze-Excite, end-to-end VJP

The hardest of the three flagship CNN VJPs in this stack (alongside the ResNet cnn_has_vjp_at and the MobileNet depthwise chain), because the squeeze-excite gate is a genuine fan-out sub-network multiplied back into the main path. We reuse seBlock_has_vjp (SE.lean), which already carries the product-rule fan-in for x ⊙ gate(x); here we supply the concrete gate (seGate) — a real Vec → Vec differentiable map with its own composed VJP — plus its differentiability.

What this file provides

• sigmoid / sigmoid_has_vjp — smooth logistic activation (chosen over the kinked h-sigmoid so the gate is differentiable everywhere; same diagonal-Jacobian proof template as swish/gelu in LayerNorm.lean).
• broadcastFlat / broadcastFlat_has_vjp — per-channel scalar broadcast to spatial layout (the adjoint reindex of globalAvgPoolFlat).
• seGate / seGate_has_vjp — the concrete squeeze-excite gate broadcast ∘ sigmoid ∘ dense ∘ swish ∘ dense ∘ GAP, assembled with the chain rule; fed into seBlock_has_vjp to give seBlockFull_has_vjp (the full x ⊙ gate(x)).
• mbconvBody / mbconvBody_has_vjp — one MBConv block body project(1×1 conv-bn) ∘ SE ∘ depthwise(bn-swish) ∘ expand(1×1 conv-bn-swish), smooth everywhere (global HasVJP).
• mbconvResidual_has_vjp_at — the stride-1, cin = cout block wrapped in the identity residual skip.
• efficientnet_has_vjp_at / _correct — a representative end-to-end EfficientNet (stem → MBConv-with-SE-and-residual → MBConv-with-SE → globalAvgPool → dense head), built by vjp_comp_at, exposing the pdiv-contracted Jacobian. Spatial dims held constant (stride-1; the separable striding/pooling plumbing is already in CNN.lean). Only the 0 < ε batch-norm hypotheses are required — swish and sigmoid are smooth, so there are no relu-style kink hypotheses anywhere in the block.

noncomputable def Proofs.sigmoidScalar (x : ℝ) : ℝ

Equations

• Proofs.sigmoidScalar x = 1 / (1 + Real.exp (-x))

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

Equations

• Proofs.sigmoid n x i = Proofs.sigmoidScalar (x i)

noncomputable def Proofs.sigmoidScalarDeriv (x : ℝ) : ℝ

Equations

• Proofs.sigmoidScalarDeriv x = deriv Proofs.sigmoidScalar x

theorem Proofs.sigmoidScalar_diff : Differentiable ℝ sigmoidScalar

theorem Proofs.sigmoid_diff (D : ℕ) : Differentiable ℝ (sigmoid D)

theorem Proofs.pdiv_sigmoid (n : ℕ) (x : Vec n) (i j : Fin n) : pdiv (sigmoid n) x i j = if i = j then sigmoidScalarDeriv (x i) else 0

noncomputable def Proofs.sigmoid_has_vjp (n : ℕ) : HasVJP (sigmoid n)

Equations

• Proofs.sigmoid_has_vjp n = { backward := fun (x dy : Proofs.Vec n) (i : Fin n) => dy i * Proofs.sigmoidScalarDeriv (x i), correct := ⋯ }

theorem Proofs.sigmoid_has_vjp_correct (n : ℕ) (x dy : Vec n) (i : Fin n) : (sigmoid_has_vjp n).backward x dy i = ∑ j : Fin n, pdiv (sigmoid n) x i j * dy j

noncomputable def Proofs.broadcastFlat (c h w : ℕ) : Vec c → Vec (c * h * w)

Broadcast a per-channel vector back to spatial layout. broadcastFlat c h w v idx = v (flatChannel c h w idx) — every spatial cell of channel k receives v k. This is the reindex map along flatChannel, i.e. the adjoint of globalAvgPoolFlat (up to the 1/(h·w) scale). Vec c → Vec (c*h*w).

Equations

• Proofs.broadcastFlat c h w v idx = v (Proofs.flatChannel c h w idx)

theorem Proofs.broadcastFlat_differentiable (c h w : ℕ) : Differentiable ℝ (broadcastFlat c h w)

noncomputable def Proofs.broadcastFlat_has_vjp (c h w : ℕ) : HasVJP (broadcastFlat c h w)

Broadcast VJP — linear reindex; backward sums each channel's spatial cotangents (the adjoint of broadcast = sum-over-spatial).

Equations

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

noncomputable def Proofs.seGate {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) : Vec (c * h * w) → Vec (c * h * w)

The squeeze-excite gate. Maps Vec (c*h*w) → Vec (c*h*w): broadcast ∘ sigmoid ∘ dense(W₂,b₂) ∘ swish ∘ dense(W₁,b₁) ∘ GAP Squeeze (GAP c·h·w → c), reduce (dense c → r), swish, expand (dense r → c), sigmoid gate, broadcast back to spatial. Every stage is smooth everywhere (swish/sigmoid smooth, dense/GAP/broadcast linear-affine), so the gate is differentiable everywhere and has a global HasVJP.

Equations

• Proofs.seGate W₁ b₁ W₂ b₂ = Proofs.broadcastFlat c h w ∘ Proofs.sigmoid c ∘ Proofs.dense W₂ b₂ ∘ Proofs.swish r ∘ Proofs.dense W₁ b₁ ∘ Proofs.globalAvgPoolFlat c h w

theorem Proofs.seGate_differentiable {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) : Differentiable ℝ (seGate W₁ b₁ W₂ b₂)

noncomputable def Proofs.seGate_has_vjp {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) : HasVJP (seGate W₁ b₁ W₂ b₂)

Equations

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

noncomputable def Proofs.seBlockFull {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) : Vec (c * h * w) → Vec (c * h * w)

The full SE block with the concrete gate: x ⊙ seGate(x).

Equations

• Proofs.seBlockFull W₁ b₁ W₂ b₂ = Proofs.seBlock (Proofs.seGate W₁ b₁ W₂ b₂)

noncomputable def Proofs.seBlockFull_has_vjp {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) : HasVJP (seBlockFull W₁ b₁ W₂ b₂)

Equations

• Proofs.seBlockFull_has_vjp W₁ b₁ W₂ b₂ = Proofs.seBlock_has_vjp (Proofs.seGate W₁ b₁ W₂ b₂) ⋯ (Proofs.seGate_has_vjp W₁ b₁ W₂ b₂)

theorem Proofs.seBlockFull_differentiable {c h w r : ℕ} (W₁ : Mat c r) (b₁ : Vec r) (W₂ : Mat r c) (b₂ : Vec c) : Differentiable ℝ (seBlockFull W₁ b₁ W₂ b₂)

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

conv → bn → swish block — everywhere VJP. Like convBnRelu but with swish (smooth) instead of relu, so no smoothness hypothesis is needed; this is a global HasVJP. Vec (ic*h*w) → Vec (oc*h*w).

Equations

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

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

noncomputable def Proofs.dwBnSwish_has_vjp {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε γ β : ℝ) (hε : 0 < ε) : HasVJP (swish (c * h * w) ∘ bnForward (c * h * w) ε γ β ∘ depthwiseFlat W b)

depthwise → bn → swish block — everywhere VJP. Depthwise conv keeps channel count c; bn over c*h*w; swish smooth. Global HasVJP. Vec (c*h*w) → Vec (c*h*w).

Equations

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

theorem Proofs.dwBnSwish_differentiable {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (b : Vec c) (ε γ β : ℝ) (hε : 0 < ε) : Differentiable ℝ (swish (c * h * w) ∘ bnForward (c * h * w) ε γ β ∘ depthwiseFlat W b)

noncomputable def Proofs.mbconvBody {cin cmid cout h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid cin kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 cout cmid kHp kWp) (bp : Vec cout) (εp γp βp : ℝ) : Vec (cin * h * w) → Vec (cout * h * w)

MBConv block body (EfficientNet MBConv with squeeze-excite), in flattened Vec space:

project(1×1 conv-bn) ∘ seBlockFull ∘ depthwise(bn-swish) ∘ expand(1×1 conv-bn-swish)

Channels: cin → cmid (expand 1×1), depthwise keeps cmid, SE keeps cmid, project cmid → cout (1×1). Spatial h, w constant (stride 1). Every stage is smooth everywhere (swish/sigmoid smooth; convs/bn/depthwise/SE differentiable), so the body has a global HasVJP. Vec (cin*h*w) → Vec (cout*h*w).

Equations

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

noncomputable def Proofs.mbconvBody_has_vjp {cin cmid cout h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid cin kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (hεd : 0 < εd) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 cout cmid kHp kWp) (bp : Vec cout) (εp γp βp : ℝ) (hεp : 0 < εp) : HasVJP (mbconvBody We be εe γe βe Wd bd εd γd βd Ws₁ bs₁ Ws₂ bs₂ Wp bp εp γp βp)

Equations

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

theorem Proofs.mbconvBody_differentiable {cin cmid cout h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid cin kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (hεd : 0 < εd) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 cout cmid kHp kWp) (bp : Vec cout) (εp γp βp : ℝ) (hεp : 0 < εp) : Differentiable ℝ (mbconvBody We be εe γe βe Wd bd εd γd βd Ws₁ bs₁ Ws₂ bs₂ Wp bp εp γp βp)

noncomputable def Proofs.mbconvResidual_has_vjp {c cmid h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid c kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (hεd : 0 < εd) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 c cmid kHp kWp) (bp : Vec c) (εp γp βp : ℝ) (hεp : 0 < εp) : HasVJP (residual (mbconvBody We be εe γe βe Wd bd εd γd βd Ws₁ bs₁ Ws₂ bs₂ Wp bp εp γp βp))

Residual MBConv VJP (global). When stride is 1 and cin = cout = c, the MBConv body's input and output shapes match, so the identity skip applies: residual (mbconvBody …). The body is differentiable everywhere (global HasVJP), so the residual VJP is global too.

Equations

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

noncomputable def Proofs.mbconvResidual_has_vjp_at {c cmid h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid c kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (hεd : 0 < εd) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 c cmid kHp kWp) (bp : Vec c) (εp γp βp : ℝ) (hεp : 0 < εp) (x : Vec (c * h * w)) : HasVJPAt (residual (mbconvBody We be εe γe βe Wd bd εd γd βd Ws₁ bs₁ Ws₂ bs₂ Wp bp εp γp βp)) x

Residual MBConv VJP at a point — the global witness restricted to a point. Kept for downstream _at consumers.

Equations

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

theorem Proofs.mbconvResidual_differentiable {c cmid h w kHe kWe kHd kWd kHp kWp r : ℕ} (We : Kernel4 cmid c kHe kWe) (be : Vec cmid) (εe γe βe : ℝ) (hεe : 0 < εe) (Wd : DepthwiseKernel cmid kHd kWd) (bd : Vec cmid) (εd γd βd : ℝ) (hεd : 0 < εd) (Ws₁ : Mat cmid r) (bs₁ : Vec r) (Ws₂ : Mat r cmid) (bs₂ : Vec cmid) (Wp : Kernel4 c cmid kHp kWp) (bp : Vec c) (εp γp βp : ℝ) (hεp : 0 < εp) : Differentiable ℝ (residual (mbconvBody We be εe γe βe Wd bd εd γd βd Ws₁ bs₁ Ws₂ bs₂ Wp bp εp γp βp))

Architectural choices (documented).

We assemble a representative EfficientNet, all in flattened Vec space, spatial dims held constant (stride-1 throughout — pooling/striding is a separable concern already covered by maxPoolFlat/strided conv in CNN.lean; the VJP plumbing is identical):

stem (3×3 conv-bn-swish, ic → c) → MBConv₁ with SE, residual (stride-1, c → c identity skip) → MBConv₂ with SE, no skip (channel change c → cout) → globalAvgPool (cout·h·w → cout) → dense head (cout → nClasses)

MBConv₁ is the headline block: a genuine squeeze-excite gate (seBlockFull) inside an identity residual. MBConv₂ exercises the channel-changing path (no skip). Both blocks are smooth everywhere (swish + sigmoid + convs + bn + SE), so only the 0 < ε batch-norm hypotheses are needed — no relu-style kink hypotheses.

noncomputable def Proofs.efficientnetForward {ic c cmid₁ cout cmid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ r₁ r₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (We₁ : Kernel4 cmid₁ c kHe₁ kWe₁) (be₁ : Vec cmid₁) (εe₁ γe₁ βe₁ : ℝ) (Wd₁ : DepthwiseKernel cmid₁ kHd₁ kWd₁) (bd₁ : Vec cmid₁) (εd₁ γd₁ βd₁ : ℝ) (Ws₁₁ : Mat cmid₁ r₁) (bs₁₁ : Vec r₁) (Ws₁₂ : Mat r₁ cmid₁) (bs₁₂ : Vec cmid₁) (Wp₁ : Kernel4 c cmid₁ kHp₁ kWp₁) (bp₁ : Vec c) (εp₁ γp₁ βp₁ : ℝ) (We₂ : Kernel4 cmid₂ c kHe₂ kWe₂) (be₂ : Vec cmid₂) (εe₂ γe₂ βe₂ : ℝ) (Wd₂ : DepthwiseKernel cmid₂ kHd₂ kWd₂) (bd₂ : Vec cmid₂) (εd₂ γd₂ βd₂ : ℝ) (Ws₂₁ : Mat cmid₂ r₂) (bs₂₁ : Vec r₂) (Ws₂₂ : Mat r₂ cmid₂) (bs₂₂ : Vec cmid₂) (Wp₂ : Kernel4 cout cmid₂ kHp₂ kWp₂) (bp₂ : Vec cout) (εp₂ γp₂ βp₂ : ℝ) (Wh : Mat cout nClasses) (bh : Vec nClasses) : Vec (ic * h * w) → Vec nClasses

Equations

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

noncomputable def Proofs.efficientnet_has_vjp {ic c cmid₁ cout cmid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ r₁ r₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (hεs : 0 < εs) (We₁ : Kernel4 cmid₁ c kHe₁ kWe₁) (be₁ : Vec cmid₁) (εe₁ γe₁ βe₁ : ℝ) (hεe₁ : 0 < εe₁) (Wd₁ : DepthwiseKernel cmid₁ kHd₁ kWd₁) (bd₁ : Vec cmid₁) (εd₁ γd₁ βd₁ : ℝ) (hεd₁ : 0 < εd₁) (Ws₁₁ : Mat cmid₁ r₁) (bs₁₁ : Vec r₁) (Ws₁₂ : Mat r₁ cmid₁) (bs₁₂ : Vec cmid₁) (Wp₁ : Kernel4 c cmid₁ kHp₁ kWp₁) (bp₁ : Vec c) (εp₁ γp₁ βp₁ : ℝ) (hεp₁ : 0 < εp₁) (We₂ : Kernel4 cmid₂ c kHe₂ kWe₂) (be₂ : Vec cmid₂) (εe₂ γe₂ βe₂ : ℝ) (hεe₂ : 0 < εe₂) (Wd₂ : DepthwiseKernel cmid₂ kHd₂ kWd₂) (bd₂ : Vec cmid₂) (εd₂ γd₂ βd₂ : ℝ) (hεd₂ : 0 < εd₂) (Ws₂₁ : Mat cmid₂ r₂) (bs₂₁ : Vec r₂) (Ws₂₂ : Mat r₂ cmid₂) (bs₂₂ : Vec cmid₂) (Wp₂ : Kernel4 cout cmid₂ kHp₂ kWp₂) (bp₂ : Vec cout) (εp₂ γp₂ βp₂ : ℝ) (hεp₂ : 0 < εp₂) (Wh : Mat cout nClasses) (bh : Vec nClasses) : HasVJP (efficientnetForward Ws bs εs γs βs We₁ be₁ εe₁ γe₁ βe₁ Wd₁ bd₁ εd₁ γd₁ βd₁ Ws₁₁ bs₁₁ Ws₁₂ bs₁₂ Wp₁ bp₁ εp₁ γp₁ βp₁ We₂ be₂ εe₂ γe₂ βe₂ Wd₂ bd₂ εd₂ γd₂ βd₂ Ws₂₁ bs₂₁ Ws₂₂ bs₂₂ Wp₂ bp₂ εp₂ γp₂ βp₂ Wh bh)

End-to-end EfficientNet VJP (global). Every block is smooth everywhere (swish + sigmoid SE gate + convs + BN, no ReLU/maxpool), so the only hypotheses are the 0 < ε batch-norm conditions and the VJP holds at every input — putting EfficientNet alongside vit_full_has_vjp and convnext_has_vjp as an unconditional whole-network VJP. Chained through the global vjp_comp.

Equations

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

noncomputable def Proofs.efficientnet_has_vjp_at {ic c cmid₁ cout cmid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ r₁ r₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (hεs : 0 < εs) (We₁ : Kernel4 cmid₁ c kHe₁ kWe₁) (be₁ : Vec cmid₁) (εe₁ γe₁ βe₁ : ℝ) (hεe₁ : 0 < εe₁) (Wd₁ : DepthwiseKernel cmid₁ kHd₁ kWd₁) (bd₁ : Vec cmid₁) (εd₁ γd₁ βd₁ : ℝ) (hεd₁ : 0 < εd₁) (Ws₁₁ : Mat cmid₁ r₁) (bs₁₁ : Vec r₁) (Ws₁₂ : Mat r₁ cmid₁) (bs₁₂ : Vec cmid₁) (Wp₁ : Kernel4 c cmid₁ kHp₁ kWp₁) (bp₁ : Vec c) (εp₁ γp₁ βp₁ : ℝ) (hεp₁ : 0 < εp₁) (We₂ : Kernel4 cmid₂ c kHe₂ kWe₂) (be₂ : Vec cmid₂) (εe₂ γe₂ βe₂ : ℝ) (hεe₂ : 0 < εe₂) (Wd₂ : DepthwiseKernel cmid₂ kHd₂ kWd₂) (bd₂ : Vec cmid₂) (εd₂ γd₂ βd₂ : ℝ) (hεd₂ : 0 < εd₂) (Ws₂₁ : Mat cmid₂ r₂) (bs₂₁ : Vec r₂) (Ws₂₂ : Mat r₂ cmid₂) (bs₂₂ : Vec cmid₂) (Wp₂ : Kernel4 cout cmid₂ kHp₂ kWp₂) (bp₂ : Vec cout) (εp₂ γp₂ βp₂ : ℝ) (hεp₂ : 0 < εp₂) (Wh : Mat cout nClasses) (bh : Vec nClasses) (x : Vec (ic * h * w)) : HasVJPAt (efficientnetForward Ws bs εs γs βs We₁ be₁ εe₁ γe₁ βe₁ Wd₁ bd₁ εd₁ γd₁ βd₁ Ws₁₁ bs₁₁ Ws₁₂ bs₁₂ Wp₁ bp₁ εp₁ γp₁ βp₁ We₂ be₂ εe₂ γe₂ βe₂ Wd₂ bd₂ εd₂ γd₂ βd₂ Ws₂₁ bs₂₁ Ws₂₂ bs₂₂ Wp₂ bp₂ εp₂ γp₂ βp₂ Wh bh) x

End-to-end EfficientNet VJP at a point — the global witness restricted to a point. Kept for downstream _at consumers and the comparator.

Equations

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

theorem Proofs.efficientnet_has_vjp_correct {ic c cmid₁ cout cmid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ r₁ r₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (hεs : 0 < εs) (We₁ : Kernel4 cmid₁ c kHe₁ kWe₁) (be₁ : Vec cmid₁) (εe₁ γe₁ βe₁ : ℝ) (hεe₁ : 0 < εe₁) (Wd₁ : DepthwiseKernel cmid₁ kHd₁ kWd₁) (bd₁ : Vec cmid₁) (εd₁ γd₁ βd₁ : ℝ) (hεd₁ : 0 < εd₁) (Ws₁₁ : Mat cmid₁ r₁) (bs₁₁ : Vec r₁) (Ws₁₂ : Mat r₁ cmid₁) (bs₁₂ : Vec cmid₁) (Wp₁ : Kernel4 c cmid₁ kHp₁ kWp₁) (bp₁ : Vec c) (εp₁ γp₁ βp₁ : ℝ) (hεp₁ : 0 < εp₁) (We₂ : Kernel4 cmid₂ c kHe₂ kWe₂) (be₂ : Vec cmid₂) (εe₂ γe₂ βe₂ : ℝ) (hεe₂ : 0 < εe₂) (Wd₂ : DepthwiseKernel cmid₂ kHd₂ kWd₂) (bd₂ : Vec cmid₂) (εd₂ γd₂ βd₂ : ℝ) (hεd₂ : 0 < εd₂) (Ws₂₁ : Mat cmid₂ r₂) (bs₂₁ : Vec r₂) (Ws₂₂ : Mat r₂ cmid₂) (bs₂₂ : Vec cmid₂) (Wp₂ : Kernel4 cout cmid₂ kHp₂ kWp₂) (bp₂ : Vec cout) (εp₂ γp₂ βp₂ : ℝ) (hεp₂ : 0 < εp₂) (Wh : Mat cout nClasses) (bh : Vec nClasses) (x : Vec (ic * h * w)) (dy : Vec nClasses) (i : Fin (ic * h * w)) : (efficientnet_has_vjp Ws bs εs γs βs hεs We₁ be₁ εe₁ γe₁ βe₁ hεe₁ Wd₁ bd₁ εd₁ γd₁ βd₁ hεd₁ Ws₁₁ bs₁₁ Ws₁₂ bs₁₂ Wp₁ bp₁ εp₁ γp₁ βp₁ hεp₁ We₂ be₂ εe₂ γe₂ βe₂ hεe₂ Wd₂ bd₂ εd₂ γd₂ βd₂ hεd₂ Ws₂₁ bs₂₁ Ws₂₂ bs₂₂ Wp₂ bp₂ εp₂ γp₂ βp₂ hεp₂ Wh bh).backward x dy i = ∑ j : Fin nClasses, pdiv (efficientnetForward Ws bs εs γs βs We₁ be₁ εe₁ γe₁ βe₁ Wd₁ bd₁ εd₁ γd₁ βd₁ Ws₁₁ bs₁₁ Ws₁₂ bs₁₂ Wp₁ bp₁ εp₁ γp₁ βp₁ We₂ be₂ εe₂ γe₂ βe₂ Wd₂ bd₂ εd₂ γd₂ βd₂ Ws₂₁ bs₂₁ Ws₂₂ bs₂₂ Wp₂ bp₂ εp₂ γp₂ βp₂ Wh bh) x i j * dy j

Public correctness theorem for efficientnet_has_vjp (global) — the full EfficientNet's backward equals the pdiv-contracted Jacobian (Jacobian-transpose on the cotangent), at every input x. The unconditional EfficientNet analogue of vit_full_has_vjp_correct.

theorem Proofs.efficientnet_has_vjp_at_correct {ic c cmid₁ cout cmid₂ h w kHs kWs kHe₁ kWe₁ kHd₁ kWd₁ kHp₁ kWp₁ kHe₂ kWe₂ kHd₂ kWd₂ kHp₂ kWp₂ r₁ r₂ nClasses : ℕ} (Ws : Kernel4 c ic kHs kWs) (bs : Vec c) (εs γs βs : ℝ) (hεs : 0 < εs) (We₁ : Kernel4 cmid₁ c kHe₁ kWe₁) (be₁ : Vec cmid₁) (εe₁ γe₁ βe₁ : ℝ) (hεe₁ : 0 < εe₁) (Wd₁ : DepthwiseKernel cmid₁ kHd₁ kWd₁) (bd₁ : Vec cmid₁) (εd₁ γd₁ βd₁ : ℝ) (hεd₁ : 0 < εd₁) (Ws₁₁ : Mat cmid₁ r₁) (bs₁₁ : Vec r₁) (Ws₁₂ : Mat r₁ cmid₁) (bs₁₂ : Vec cmid₁) (Wp₁ : Kernel4 c cmid₁ kHp₁ kWp₁) (bp₁ : Vec c) (εp₁ γp₁ βp₁ : ℝ) (hεp₁ : 0 < εp₁) (We₂ : Kernel4 cmid₂ c kHe₂ kWe₂) (be₂ : Vec cmid₂) (εe₂ γe₂ βe₂ : ℝ) (hεe₂ : 0 < εe₂) (Wd₂ : DepthwiseKernel cmid₂ kHd₂ kWd₂) (bd₂ : Vec cmid₂) (εd₂ γd₂ βd₂ : ℝ) (hεd₂ : 0 < εd₂) (Ws₂₁ : Mat cmid₂ r₂) (bs₂₁ : Vec r₂) (Ws₂₂ : Mat r₂ cmid₂) (bs₂₂ : Vec cmid₂) (Wp₂ : Kernel4 cout cmid₂ kHp₂ kWp₂) (bp₂ : Vec cout) (εp₂ γp₂ βp₂ : ℝ) (hεp₂ : 0 < εp₂) (Wh : Mat cout nClasses) (bh : Vec nClasses) (x : Vec (ic * h * w)) (dy : Vec nClasses) (i : Fin (ic * h * w)) : (efficientnet_has_vjp_at Ws bs εs γs βs hεs We₁ be₁ εe₁ γe₁ βe₁ hεe₁ Wd₁ bd₁ εd₁ γd₁ βd₁ hεd₁ Ws₁₁ bs₁₁ Ws₁₂ bs₁₂ Wp₁ bp₁ εp₁ γp₁ βp₁ hεp₁ We₂ be₂ εe₂ γe₂ βe₂ hεe₂ Wd₂ bd₂ εd₂ γd₂ βd₂ hεd₂ Ws₂₁ bs₂₁ Ws₂₂ bs₂₂ Wp₂ bp₂ εp₂ γp₂ βp₂ hεp₂ Wh bh x).backward dy i = ∑ j : Fin nClasses, pdiv (efficientnetForward Ws bs εs γs βs We₁ be₁ εe₁ γe₁ βe₁ Wd₁ bd₁ εd₁ γd₁ βd₁ Ws₁₁ bs₁₁ Ws₁₂ bs₁₂ Wp₁ bp₁ εp₁ γp₁ βp₁ We₂ be₂ εe₂ γe₂ βe₂ Wd₂ bd₂ εd₂ γd₂ βd₂ Ws₂₁ bs₂₁ Ws₂₂ bs₂₂ Wp₂ bp₂ εp₂ γp₂ βp₂ Wh bh) x i j * dy j

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