The FULL EfficientNet-B0 — all 16 MBConv blocks, batched forward graph + faithfulness

Scales EfficientNetRenderPC.lean's representative (stem + 3 MBConv + head) to the real B0 [t,c,n,s,k] spec — 16 MBConv layers — at the batched index N·(c·h·w). Pure enumeration + chaining of the generic per-block machinery; the only genuinely-new piece is the 4th block shape (mbExp: expand + stride-1 + no residual, used by stage-5/stage-7 first blocks where ic ≠ oc).

B0 stage spec [t,c,n,s,k]: s1 (1,16,1,1,3) s2 (6,24,2,2,3) s3 (6,40,2,2,5) s4 (6,80,3,2,3) s5 (6,112,3,1,5) s6 (6,192,4,2,5) s7 (6,320,1,1,3); stem 3×3-s2 (3→32), head 1×1 (320→1280)→GAP→dense. Per-block (ic, mid=t·ic, oc, r=⌈ic/4⌉, k, spatial, kind): b1 32→16 mid32 r8 k3 @112 noExp b9 80→112 mid480 r20 k5 @14 exp(no-resid) b2 16→24 mid96 r4 k3 112→56 strided b10 112→112 mid672 r28 k5 @14 resid b3 24→24 mid144 r6 k3 @56 resid b11 112→112 mid672 r28 k5 @14 resid b4 24→40 mid144 r6 k5 56→28 strided b12 112→192 mid672 r28 k5 14→7 strided b5 40→40 mid240 r10 k5 @28 resid b13 192→192 mid1152 r48 k5 @7 resid b6 40→80 mid240 r10 k3 28→14 strided b14 192→192 mid1152 r48 k5 @7 resid b7 80→80 mid480 r20 k3 @14 resid b15 192→192 mid1152 r48 k5 @7 resid b8 80→80 mid480 r20 k3 @14 resid b16 192→320 mid1152 r48 k3 @7 exp(no-resid)

structure Proofs.MBW (ic mid oc r kh kw : ℕ) : Type

Weights of one MBConv6 block (expand ic→mid, depthwise k×k, SE mid→r→mid, project mid→oc).

• eW : Kernel4 mid ic 1 1
• eb : Vec mid
• eε : ℝ
• eγ : Vec mid
• eβ : Vec mid
• dW : DepthwiseKernel mid kh kw
• db : Vec mid
• dε : ℝ
• dγ : Vec mid
• dβ : Vec mid
• z1 : Mat mid r
• zb1 : Vec r
• z2 : Mat r mid
• zb2 : Vec mid
• pW : Kernel4 oc mid 1 1
• pb : Vec oc
• pε : ℝ
• pγ : Vec oc
• pβ : Vec oc

structure Proofs.MBWNoExp (ic oc r kh kw : ℕ) : Type

Weights of the MBConv1 block (t=1, no expand; depthwise on ic, SE ic→r→ic, project ic→oc).

• dW : DepthwiseKernel ic kh kw
• db : Vec ic
• dε : ℝ
• dγ : Vec ic
• dβ : Vec ic
• z1 : Mat ic r
• zb1 : Vec r
• z2 : Mat r ic
• zb2 : Vec ic
• pW : Kernel4 oc ic 1 1
• pb : Vec oc
• pε : ℝ
• pγ : Vec oc
• pβ : Vec oc

structure Proofs.B0Weights : Type

All 262 EfficientNet-B0 parameters: stem (3×3-s2 3→32) + 16 MBConv blocks (the real [t,c,n,s,k] spec) + 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 : MBWNoExp 32 16 8 3 3
• b2 : MBW 16 96 24 4 3 3
• b3 : MBW 24 144 24 6 3 3
• b4 : MBW 24 144 40 6 5 5
• b5 : MBW 40 240 40 10 5 5
• b6 : MBW 40 240 80 10 3 3
• b7 : MBW 80 480 80 20 3 3
• b8 : MBW 80 480 80 20 3 3
• b9 : MBW 80 480 112 20 5 5
• b10 : MBW 112 672 112 28 5 5
• b11 : MBW 112 672 112 28 5 5
• b12 : MBW 112 672 192 28 5 5
• b13 : MBW 192 1152 192 48 5 5
• b14 : MBW 192 1152 192 48 5 5
• b15 : MBW 192 1152 192 48 5 5
• b16 : MBW 192 1152 320 48 3 3
• 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.mbExpFwdB (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) : Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

MBConv6 expand, stride-1, NO residual: project-bn ∘ SE ∘ dw-bn-swish ∘ expand-bn-swish (the mbResidFwdB body without the identity skip).

Equations

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

theorem Proofs.mbExpFwdB_differentiable (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) : Differentiable ℝ (mbExpFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

noncomputable def Proofs.mbExpFwdB_has_vjp (N : ℕ) {ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (hεe : 0 < εe) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (hεd : 0 < εd) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (hεp : 0 < εp) (γp βp : Vec oc) : HasVJP (mbExpFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp)

Equations

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

def Proofs.StableHLO.mbExpGraphB (p epsStr : String) {N ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (e : SHlo (N * (ic * h * w))) : SHlo (N * (oc * h * w))

MBConv6 expand + stride-1 + no-residual graph (the mbResidGraphB body without the addV skip).

Equations

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

theorem Proofs.StableHLO.mbExpGraphB_faithful (p epsStr : String) {N ic mid oc h w kHd kWd r : ℕ} (We : Kernel4 mid ic 1 1) (be : Vec mid) (εe : ℝ) (γe βe : Vec mid) (Wd : DepthwiseKernel mid kHd kWd) (bd : Vec mid) (εd : ℝ) (γd βd : Vec mid) (Wz₁ : Mat mid r) (bz₁ : Vec r) (Wz₂ : Mat r mid) (bz₂ : Vec mid) (Wp : Kernel4 oc mid 1 1) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (e : SHlo (N * (ic * h * w))) : den (mbExpGraphB p epsStr We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp e) = mbExpFwdB N We be εe γe βe Wd bd εd γd βd Wz₁ bz₁ Wz₂ bz₂ Wp bp εp γp βp (den e)

noncomputable def Proofs.mbNoExpW (N h w : ℕ) {ic oc kh kw r : ℕ} (p : MBWNoExp ic oc r kh kw) : Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

Equations

• Proofs.mbNoExpW N h w p = Proofs.mbNoExpFwdB N p.dW p.db p.dε p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε p.pγ p.pβ

noncomputable def Proofs.mbStridedW (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) : Vec (N * (ic * (2 * h) * (2 * w))) → Vec (N * (oc * h * w))

Equations

• Proofs.mbStridedW N h w p = Proofs.mbStridedFwdB N p.eW p.eb p.eε p.eγ p.eβ p.dW p.db p.dε p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε p.pγ p.pβ

noncomputable def Proofs.mbResidW (N h w : ℕ) {c mid kh kw r : ℕ} (p : MBW c mid c r kh kw) : Vec (N * (c * h * w)) → Vec (N * (c * h * w))

Equations

• Proofs.mbResidW N h w p = Proofs.mbResidFwdB N p.eW p.eb p.eε p.eγ p.eβ p.dW p.db p.dε p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε p.pγ p.pβ

noncomputable def Proofs.mbExpW (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) : Vec (N * (ic * h * w)) → Vec (N * (oc * h * w))

Equations

• Proofs.mbExpW N h w p = Proofs.mbExpFwdB N p.eW p.eb p.eε p.eγ p.eβ p.dW p.db p.dε p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε p.pγ p.pβ

theorem Proofs.mbNoExpW_differentiable (N h w : ℕ) {ic oc kh kw r : ℕ} (p : MBWNoExp ic oc r kh kw) (hd : 0 < p.dε) (hp : 0 < p.pε) : Differentiable ℝ (mbNoExpW N h w p)

noncomputable def Proofs.mbNoExpW_has_vjp (N h w : ℕ) {ic oc kh kw r : ℕ} (p : MBWNoExp ic oc r kh kw) (hd : 0 < p.dε) (hp : 0 < p.pε) : HasVJP (mbNoExpW N h w p)

Equations

• Proofs.mbNoExpW_has_vjp N h w p hd hp = id (Proofs.mbNoExpFwdB_has_vjp N p.dW p.db p.dε hd p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε hp p.pγ p.pβ)

theorem Proofs.mbStridedW_differentiable (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (he : 0 < p.eε) (hd : 0 < p.dε) (hp : 0 < p.pε) : Differentiable ℝ (mbStridedW N h w p)

noncomputable def Proofs.mbStridedW_has_vjp (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (he : 0 < p.eε) (hd : 0 < p.dε) (hp : 0 < p.pε) : HasVJP (mbStridedW N h w p)

Equations

• Proofs.mbStridedW_has_vjp N h w p he hd hp = id (Proofs.mbStridedFwdB_has_vjp N p.eW p.eb p.eε he p.eγ p.eβ p.dW p.db p.dε hd p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε hp p.pγ p.pβ)

theorem Proofs.mbResidW_differentiable (N h w : ℕ) {c mid kh kw r : ℕ} (p : MBW c mid c r kh kw) (he : 0 < p.eε) (hd : 0 < p.dε) (hp : 0 < p.pε) : Differentiable ℝ (mbResidW N h w p)

noncomputable def Proofs.mbResidW_has_vjp (N h w : ℕ) {c mid kh kw r : ℕ} (p : MBW c mid c r kh kw) (he : 0 < p.eε) (hd : 0 < p.dε) (hp : 0 < p.pε) : HasVJP (mbResidW N h w p)

Equations

• Proofs.mbResidW_has_vjp N h w p he hd hp = id (Proofs.mbResidFwdB_has_vjp N p.eW p.eb p.eε he p.eγ p.eβ p.dW p.db p.dε hd p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε hp p.pγ p.pβ)

theorem Proofs.mbExpW_differentiable (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (he : 0 < p.eε) (hd : 0 < p.dε) (hp : 0 < p.pε) : Differentiable ℝ (mbExpW N h w p)

noncomputable def Proofs.mbExpW_has_vjp (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (he : 0 < p.eε) (hd : 0 < p.dε) (hp : 0 < p.pε) : HasVJP (mbExpW N h w p)

Equations

• Proofs.mbExpW_has_vjp N h w p he hd hp = id (Proofs.mbExpFwdB_has_vjp N p.eW p.eb p.eε he p.eγ p.eβ p.dW p.db p.dε hd p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε hp p.pγ p.pβ)

noncomputable def Proofs.efficientnetForwardB_full (N : ℕ) (w : B0Weights) (x : Vec (N * (3 * 224 * 224))) : Vec (N * 10)

Equations

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

def Proofs.StableHLO.mbNoExpGraphW (pfx epsStr : String) (N h w : ℕ) {ic oc kh kw r : ℕ} (p : MBWNoExp ic oc r kh kw) (e : SHlo (N * (ic * h * w))) : SHlo (N * (oc * h * w))

Equations

• Proofs.StableHLO.mbNoExpGraphW pfx epsStr N h w p e = Proofs.StableHLO.mbNoExpGraphB pfx epsStr p.dW p.db p.dε p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε p.pγ p.pβ e

theorem Proofs.StableHLO.mbNoExpGraphW_faithful (pfx epsStr : String) (N h w : ℕ) {ic oc kh kw r : ℕ} (p : MBWNoExp ic oc r kh kw) (e : SHlo (N * (ic * h * w))) : den (mbNoExpGraphW pfx epsStr N h w p e) = mbNoExpW N h w p (den e)

def Proofs.StableHLO.mbStridedGraphW (pfx epsStr : String) (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) : SHlo (N * (oc * h * w))

Equations

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

theorem Proofs.StableHLO.mbStridedGraphW_faithful (pfx epsStr : String) (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) : den (mbStridedGraphW pfx epsStr N h w p e) = mbStridedW N h w p (den e)

def Proofs.StableHLO.mbResidGraphW (pfx epsStr : String) (N h w : ℕ) {c mid kh kw r : ℕ} (p : MBW c mid c r kh kw) (e : SHlo (N * (c * h * w))) : SHlo (N * (c * h * w))

Equations

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

theorem Proofs.StableHLO.mbResidGraphW_faithful (pfx epsStr : String) (N h w : ℕ) {c mid kh kw r : ℕ} (p : MBW c mid c r kh kw) (e : SHlo (N * (c * h * w))) : den (mbResidGraphW pfx epsStr N h w p e) = mbResidW N h w p (den e)

def Proofs.StableHLO.mbExpGraphW (pfx epsStr : String) (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (e : SHlo (N * (ic * h * w))) : SHlo (N * (oc * h * w))

Equations

• Proofs.StableHLO.mbExpGraphW pfx epsStr N h w p e = Proofs.StableHLO.mbExpGraphB pfx epsStr p.eW p.eb p.eε p.eγ p.eβ p.dW p.db p.dε p.dγ p.dβ p.z1 p.zb1 p.z2 p.zb2 p.pW p.pb p.pε p.pγ p.pβ e

theorem Proofs.StableHLO.mbExpGraphW_faithful (pfx epsStr : String) (N h w : ℕ) {ic mid oc kh kw r : ℕ} (p : MBW ic mid oc r kh kw) (e : SHlo (N * (ic * h * w))) : den (mbExpGraphW pfx epsStr N h w p e) = mbExpW N h w p (den e)

def Proofs.StableHLO.efficientnetFwdGraphB_full (N : ℕ) (epsStr : String) (w : B0Weights) (x : Vec (N * (3 * 224 * 224))) : SHlo (N * 10)

The full batched EfficientNet-B0 forward graph at the batched index N·(c·h·w): stem → 16 MBConv blocks (the real [t,c,n,s,k] spec, 3×3 and 5×5 depthwise, true batch-norm, squeeze-excite, 4 stride-2 downsamples, identity residuals where s=1 ∧ ic=oc) → head → GAP → dense.

Equations

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

theorem Proofs.StableHLO.efficientnetFwdGraphB_full_faithful (N : ℕ) (epsStr : String) (w : B0Weights) (x : Vec (N * (3 * 224 * 224))) : den (efficientnetFwdGraphB_full N epsStr w x) = efficientnetForwardB_full N w x

Full batched EfficientNet-B0 forward faithfulness. The full 16-MBConv batched graph (true batch-norm + SE) denotes efficientnetForwardB_full. Chained from the per-block *GraphW_faithful lemmas (one rw per block, outermost→innermost), then a structural rfl (the forward is nested-application form, blocks opaque) — the ResNet34RenderPC recipe at full depth.

noncomputable def Proofs.efficientnetForwardB_full_has_vjp (N : ℕ) (w : B0Weights) (hsε : 0 < w.sε) (hb1d : 0 < w.b1.dε) (hb1p : 0 < w.b1.pε) (hb2e : 0 < w.b2.eε) (hb2d : 0 < w.b2.dε) (hb2p : 0 < w.b2.pε) (hb3e : 0 < w.b3.eε) (hb3d : 0 < w.b3.dε) (hb3p : 0 < w.b3.pε) (hb4e : 0 < w.b4.eε) (hb4d : 0 < w.b4.dε) (hb4p : 0 < w.b4.pε) (hb5e : 0 < w.b5.eε) (hb5d : 0 < w.b5.dε) (hb5p : 0 < w.b5.pε) (hb6e : 0 < w.b6.eε) (hb6d : 0 < w.b6.dε) (hb6p : 0 < w.b6.pε) (hb7e : 0 < w.b7.eε) (hb7d : 0 < w.b7.dε) (hb7p : 0 < w.b7.pε) (hb8e : 0 < w.b8.eε) (hb8d : 0 < w.b8.dε) (hb8p : 0 < w.b8.pε) (hb9e : 0 < w.b9.eε) (hb9d : 0 < w.b9.dε) (hb9p : 0 < w.b9.pε) (hb10e : 0 < w.b10.eε) (hb10d : 0 < w.b10.dε) (hb10p : 0 < w.b10.pε) (hb11e : 0 < w.b11.eε) (hb11d : 0 < w.b11.dε) (hb11p : 0 < w.b11.pε) (hb12e : 0 < w.b12.eε) (hb12d : 0 < w.b12.dε) (hb12p : 0 < w.b12.pε) (hb13e : 0 < w.b13.eε) (hb13d : 0 < w.b13.dε) (hb13p : 0 < w.b13.pε) (hb14e : 0 < w.b14.eε) (hb14d : 0 < w.b14.dε) (hb14p : 0 < w.b14.pε) (hb15e : 0 < w.b15.eε) (hb15d : 0 < w.b15.dε) (hb15p : 0 < w.b15.pε) (hb16e : 0 < w.b16.eε) (hb16d : 0 < w.b16.dε) (hb16p : 0 < w.b16.pε) (hhε : 0 < w.hε) : HasVJP (headFwdB N w.hW w.hb w.hε w.hγ w.hβ w.fcW w.fcb ∘ mbExpW N 7 7 w.b16 ∘ mbResidW N 7 7 w.b15 ∘ mbResidW N 7 7 w.b14 ∘ mbResidW N 7 7 w.b13 ∘ mbStridedW N 7 7 w.b12 ∘ mbResidW N 14 14 w.b11 ∘ mbResidW N 14 14 w.b10 ∘ mbExpW N 14 14 w.b9 ∘ mbResidW N 14 14 w.b8 ∘ mbResidW N 14 14 w.b7 ∘ mbStridedW N 14 14 w.b6 ∘ mbResidW N 28 28 w.b5 ∘ mbStridedW N 28 28 w.b4 ∘ mbResidW N 56 56 w.b3 ∘ mbStridedW N 56 56 w.b2 ∘ mbNoExpW N 112 112 w.b1 ∘ stemB N w.sW w.sb w.sε w.sγ w.sβ)

The full EfficientNet-B0 has a (correct) VJP. Chained from the per-block gradients (stem → 16 MBConv blocks → head) via vjp_comp. Stated on the ∘-composition of the blocks (= the full forward by construction; keeps the blocks opaque so the chain closes structurally). The full-depth, batched, true-batch-norm + SE analogue of efficientnet_has_vjp.

Equations

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

theorem Proofs.efficientnetForwardB_full_eq_chain (N : ℕ) (w : B0Weights) (x : Vec (N * (3 * 224 * 224))) : efficientnetForwardB_full N w x = (headFwdB N w.hW w.hb w.hε w.hγ w.hβ w.fcW w.fcb ∘ mbExpW N 7 7 w.b16 ∘ mbResidW N 7 7 w.b15 ∘ mbResidW N 7 7 w.b14 ∘ mbResidW N 7 7 w.b13 ∘ mbStridedW N 7 7 w.b12 ∘ mbResidW N 14 14 w.b11 ∘ mbResidW N 14 14 w.b10 ∘ mbExpW N 14 14 w.b9 ∘ mbResidW N 14 14 w.b8 ∘ mbResidW N 14 14 w.b7 ∘ mbStridedW N 14 14 w.b6 ∘ mbResidW N 28 28 w.b5 ∘ mbStridedW N 28 28 w.b4 ∘ mbResidW N 56 56 w.b3 ∘ mbStridedW N 56 56 w.b2 ∘ mbNoExpW N 112 112 w.b1 ∘ stemB N w.sW w.sb w.sε w.sγ w.sβ) x

efficientnetForwardB_full = the ∘-chain of the VJP's statement — the kernel-checked bridge between the nested-application and composition forms, closing the form-gap this file shipped with. PROOF-SHAPE MATTERS (the ConvNeXt-T convNextForwardTCh_eq_chain lesson): equation-lemma rw + 17 comp_apply rewrites close syntactically; a simp/rfl proof of the same statement makes the kernel reduce the block bodies (no reducibility, no defeq cache) and deterministically time out.

theorem Proofs.efficientnetForwardB_full_has_vjp_correct (N : ℕ) (w : B0Weights) (hsε : 0 < w.sε) (hb1d : 0 < w.b1.dε) (hb1p : 0 < w.b1.pε) (hb2e : 0 < w.b2.eε) (hb2d : 0 < w.b2.dε) (hb2p : 0 < w.b2.pε) (hb3e : 0 < w.b3.eε) (hb3d : 0 < w.b3.dε) (hb3p : 0 < w.b3.pε) (hb4e : 0 < w.b4.eε) (hb4d : 0 < w.b4.dε) (hb4p : 0 < w.b4.pε) (hb5e : 0 < w.b5.eε) (hb5d : 0 < w.b5.dε) (hb5p : 0 < w.b5.pε) (hb6e : 0 < w.b6.eε) (hb6d : 0 < w.b6.dε) (hb6p : 0 < w.b6.pε) (hb7e : 0 < w.b7.eε) (hb7d : 0 < w.b7.dε) (hb7p : 0 < w.b7.pε) (hb8e : 0 < w.b8.eε) (hb8d : 0 < w.b8.dε) (hb8p : 0 < w.b8.pε) (hb9e : 0 < w.b9.eε) (hb9d : 0 < w.b9.dε) (hb9p : 0 < w.b9.pε) (hb10e : 0 < w.b10.eε) (hb10d : 0 < w.b10.dε) (hb10p : 0 < w.b10.pε) (hb11e : 0 < w.b11.eε) (hb11d : 0 < w.b11.dε) (hb11p : 0 < w.b11.pε) (hb12e : 0 < w.b12.eε) (hb12d : 0 < w.b12.dε) (hb12p : 0 < w.b12.pε) (hb13e : 0 < w.b13.eε) (hb13d : 0 < w.b13.dε) (hb13p : 0 < w.b13.pε) (hb14e : 0 < w.b14.eε) (hb14d : 0 < w.b14.dε) (hb14p : 0 < w.b14.pε) (hb15e : 0 < w.b15.eε) (hb15d : 0 < w.b15.dε) (hb15p : 0 < w.b15.pε) (hb16e : 0 < w.b16.eε) (hb16d : 0 < w.b16.dε) (hb16p : 0 < w.b16.pε) (hhε : 0 < w.hε) (x : Vec (N * (3 * 224 * 224))) (dy : Vec (N * 10)) (i : Fin (N * (3 * 224 * 224))) : (efficientnetForwardB_full_has_vjp N w hsε hb1d hb1p hb2e hb2d hb2p hb3e hb3d hb3p hb4e hb4d hb4p hb5e hb5d hb5p hb6e hb6d hb6p hb7e hb7d hb7p hb8e hb8d hb8p hb9e hb9d hb9p hb10e hb10d hb10p hb11e hb11d hb11p hb12e hb12d hb12p hb13e hb13d hb13p hb14e hb14d hb14p hb15e hb15d hb15p hb16e hb16d hb16p hhε).backward x dy i = ∑ j : Fin (N * 10), pdiv (efficientnetForwardB_full N w) x i j * dy j

Public correctness theorem for efficientnetForwardB_full_has_vjp — the full B0's backward equals the pdiv-contracted Jacobian of efficientnetForwardB_full itself at every input, tying the chain-stated VJP back to the nested forward via efficientnetForwardB_full_eq_chain.