T3 §1 fold for EfficientNet-B0 at the UN-FUSED gradient — the Adam artifact's op set #
EfficientNetFold.lean makes every parameter output of the SGD-inline
efficientnet_train_step.mlir den-faithful: each *SgdB op denotes θ − lr·(certified Jacobian · cotangent). Every OTHER train step this net renders — efficientnet_adam_train_step, the
_rms_/_emarms_/_do_/_drop_/_dp_/bf16 families, and the ImageNet
efficientnetin_emarmsdp64dropdo_train_step whose accuracy the book quotes — takes
EfficientNetRender's adam := true branch, which emits the RAW gradient (*GradB) and hands it to
an optimizer tail. This file is the fold at those nodes. ⚠ The bf16 family's conv and depthwise
weight nodes are *GradBBf16, their own kind, folded in Foundation/Bf16GradNodes.lean.
⭐ One lemma per op kind certifies every optimizer variant at once, because RMSProp, AdamW,
plain SGD, EMA and the data-parallel peers all consume the same gradient node. The fusion itself is
rfl (StableHLO.lean's *SgdB_eq_grad family), so nothing here is new mathematics, and
EfficientNetFold.lean's fused lemmas are these (and ResNet34FoldB.lean's) through that family.
⭐ Five of the eight op kinds were ALREADY proven, in r34's file #
ResNet34FoldB.lean states its eight folds at op kinds, not at r34 — and five of them are
the same constructors this net emits, at the same generality: convWeightGradB (every 1×1 expand /
project / head conv), bnGammaGradB / bnBetaGradB (all 49 BatchNorm sites, and every conv bias,
which the render folds onto the following BN's β), and denseWeightGradB (the SE squeeze/excite
denses and the classifier). So B0's package is three genuinely new lemmas, not eight; the five
below are one-line delegations that say so out loud, so this file is still the complete op table for
the artifact. (denseBiasGradB is restated rather than delegated only to widen r34's square
Mat c c witness to the SE's rectangular Mat a c — the gradient is W-free either way.)
The three that are new, and why #
convStridedXlaWeightGradB— the 3×3/s2 stem. ⚠ This is the XLA-SAMEop (flatConvStride2Xla), where r34's peer is the symmetricconvStridedWeightGradB(flatConvStride2). The two have identical types and emit identical shapes; only the certificate tells them apart, and B0 is the TF-origin net.depthwiseWeightGradB/depthwiseStridedWeightGradB— the MBConv depthwise kernels, 3×3 and 5×5, which ResNet-34 has no instance of. ⚠ The strided one is the symmetric op, which is whatEfficientNetRenderemits on the forward side too (.depthwiseStrided, not.depthwiseStridedXla); the XLA phase is B0's stem only.
Honest residual #
- Every lemma is
∀ cot, so it holds at the actual backward-chain cotangent without naming it. Pinning each to the emitted backward subgraph is the §1a tie (EfficientNetStepTie.lean), and re-pointing that capstone at these nodes needs the smoothed-target loss cotangent, which is scoped with r34's batched tie. - The all-reduce in the
*dp*artifacts is emitted text outside the AST, so these lemmas are about the per-replica gradient node.
Batched 1×1-conv weight GRADIENT denotes the certified Σ_n weight gradient. Every expand,
project and head conv. Identical to r34's block convs as an op: ResNet34PoCB.convWGradB_den.
Batched BN β GRADIENT denotes the certified per-channel β gradient Σ_{batch,spatial} cot.
Used at all 49 BN βs AND at every conv bias, which the render folds onto the following BN.
ResNet34PoCB.bnBetaGradB_den.
Batched dense weight GRADIENT denotes the certified Σ_n outer product. The SE
squeeze (c → r) and excite (r → c) denses and the classifier head.
ResNet34PoCB.denseWGradB_den.
Batched dense bias GRADIENT denotes the certified Σ_n cotangent sum. r34's peer at a
RECTANGULAR witness Mat a c, which the SE's c → r squeeze needs; the gradient is the
channel sum and depends on neither W nor x, so the widening is free.
Batched XLA-SAME strided conv weight GRADIENT denotes the certified Σ_n weight
gradient. B0's 3×3/s2 stem, the net's one XLA-phase site. Σ_n of
flatConvStride2Xla_weight_grad_has_vjp.correct — the odd-phase weight VJP, so the certified
gradient is the gradient of the net that ships.
Batched stride-1 depthwise weight GRADIENT denotes the certified Σ_n weight gradient.
Σ_n of the flattened depthwise_weight_grad_has_vjp3.correct. Generic in the kernel size, so
the one lemma covers every 3×3 and every 5×5 depthwise.
Batched strided depthwise weight GRADIENT denotes the certified Σ_n weight gradient. The
strided VJP is already flat, so this is Σ_n of
depthwiseStride2_weight_grad_has_vjp.correct.