The per-example fused-SGD nodes — one *_den per op kind, shared by every per-example chain #
The per-example train steps (the MNIST / CIFAR chapter nets, and the per-example tiers of
ResNet-34, MobileNetV2, ConvNeXt and ViT) emit fused θ − lr·∂Loss/∂θ ops. Each lemma here says
one such op denotes the certified SGD step at an arbitrary cotangent, so a net's fold is these at
its layers. The per-example UN-FUSED peers (a render with a separate optimizer) are the last
section, in GradNode; the batched ones are in GradNodesB.
| op | lemma | namespace |
|---|---|---|
dense weight / bias (weightSgd, biasSgd) | denseW_den, denseB_den | SgdNode |
conv weight / bias (convWeightSgd, convBiasSgd) | convW_den, convB_den | SgdNode |
per-channel BN γ / β (bnGammaSgd, bnBetaSgd), and the pair as one clause | bnGamma_den, bnBeta_den, BnSgdPairTied | SgdNode |
| conv weight / bias as tie clauses | ConvWSgdTied, ConvBSgdTied, convWSgdTied_holds, convBSgdTied_holds | Proofs |
| dense weight / bias as tie clauses | DenseWSgdTied, DenseBSgdTied, denseWSgdTied_holds, denseBSgdTied_holds | Proofs |
stride-1 depthwise weight / bias (depthwiseWeightSgd, depthwiseBiasSgd) | depthwiseW_den, depthwiseB_den | SgdNode |
stride-2 conv weight / bias (convStridedWeightSgd, convStridedBiasSgd) | convStridedW_den, convStridedB_den | SgdNode |
vector-LN γ / β (veclnGammaSgd, rowDenseBiasSgd at the LN forward), and their clauses | veclnGammaSgd_den, rowDenseBiasSgd_den_lnbeta, VecLN{Gamma,Beta}SgdTied, vecLN{Gamma,Beta}SgdTied_holds | SgdNode |
the un-fused per-example peers (weightGrad, biasGrad, convWeightGrad, convBiasGrad, bnGammaGrad, bnBetaGrad), and their clauses | denseWGrad_den, denseBGrad_den, convWGrad_den, convBGrad_den, bnGammaGrad_den, bnBetaGrad_den, ConvWGradTied, ConvBGradTied, BnGradPairTied, DenseWGradTied, DenseBGradTied | GradNode |
Any emitted dense weight op = certified. Generic in the layer dims, the
activation a, bias b and cotangent c: den (weightSgd a W (.operand _ c)) = W − lr·(certified ∂dense/∂W · c). Every small net's dense layers are instances.
Any emitted dense bias op = certified. Generic peer of denseW_den.
Any emitted conv weight op = certified. Generic in the conv dims and the
cotangent c: the convWeightSgd op denotes flatten W − lr·(certified ∂conv/∂W · c). Instantiated at each layer's (b,x,W,c) it certifies W₁…W₄.
Any emitted conv bias op = certified. Generic peer of convW_den.
Per-channel BN γ op = certified. The emitted bnGammaSgd, fed the BN-output
cotangent c and the saved conv output v, denotes γ − lr·(certified ∂(per-channel BN)/∂γ · c) — via reassocFwd into the oc·m cert layout.
Per-channel BN β op = certified. Likewise β − lr·(certified ∂BN/∂β · c).
The emitted bnGammaSgd and bnBetaSgd ops of one per-channel BN layer, fed its BN-output
cotangent c at the saved conv output v, are the certified SGD steps on γ and β — the
statements of bnGamma_den and bnBeta_den under ∀. The per-example peer of
EnetFold.BnSgdPairTiedB.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Clause Props for the per-example conv and dense ties: each is a _den lemma's statement
(SgdNode.convW_den / convB_den / denseW_den / denseB_den) under ∀, so a tie theorem
states one line per parameter tensor and intro unfolds it back; each …_holds proves it with
every argument implicit (read off the goal by a step tie's constructor). The batched peers are GradNodeB.ConvWTiedB and
EnetFold.ConvWSgdTiedB.
The emitted convWeightSgd op, fed the cotangent c at the conv output, is the certified SGD
step on the kernel W.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The emitted convBiasSgd op, fed the cotangent c at the conv output, is the certified SGD
step on the bias b.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The emitted weightSgd op, fed the activation a and the cotangent c at the dense output, is
the certified SGD step on the weight W (SgdNode.denseW_den under ∀).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The emitted biasSgd op, fed the cotangent c at the dense output, is the certified SGD step
on the bias b (SgdNode.denseB_den under ∀).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Flat stride-1 depthwise weight render bridge. The emitted op's flat weight grad
flatten W − lr·flatten((dwconv_weight_grad₃ b x).backward W (unflatten c)) equals the flat
pdiv-Jacobian form. Via HasVJP3.toHasVJP.correct (the triple→flat reindex), modulo
unflatten (flatten W) = W. The stride-1 depthwise peer of conv_weight_sgd_certified.
Stride-1 depthwise weight op = certified. The depthwiseWeightSgd op denotes
flatten W − lr·(certified ∂(depthwiseConv2d)/∂W · c) (flat pdiv form). The stride-1 depthwise
peer of SgdNode.convW_den.
Stride-1 depthwise bias op = certified. Delegates to depthwise_bias_sgd_certified.
Any emitted STRIDED conv weight op = certified. Generic in the conv dims, the kernel size
(covers the 7×7 stem AND every 3×3 downsample/projection) and the cotangent c: the
convStridedWeightSgd op denotes flatten W − lr·(certified ∂(flatConvStride2)/∂W · c), the
emitted op's den reduced (rfl) to the LHS of the generic strided weight bridge. The strided
peer of SgdNode.convW_den.
Any emitted STRIDED conv bias op = certified. The bias peer of convStridedW_den; the
convStridedBiasSgd op (which emits the same reduce text as convBiasSgd) denotes
b − lr·(certified ∂(flatConvStride2)/∂b · c).
The vector-LN γ / β nodes (every LN of ViT, and the LN-style norms of ConvNeXt's per-example
tier). The β node is the per-token bias op rowDenseBiasSgd read against the LN forward: the LN β
gradient is the same Σ_tokens dy reduce as a dense bias.
Vector-LN γ op denotes the certified step. den(veclnGammaSgd) = γ − lr·(Σ_tokens dy·x̂),
the certified ∂(rowwise vector-LN)/∂γ contraction. Covers all 25 LN-γ sites (LN1/LN2 × 12 + final).
One-line delegation to layerNormVec_gamma_sgd_certified (the den's sum IS vecLNGradGamma).
The SAME per-token bias op, certified against the vector-LN β forward. The LN β grad is
Σ_tokens dy — identical reduce to the dense bias — so rowDenseBiasSgd ALSO denotes the certified
∂(rowwise vector-LN)/∂β contraction. Covers all 25 LN-β sites. Delegation to layerNormVec_beta_sgd_certified.
A vector-LN γ SGD node, tied (veclnGammaSgd_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The per-example UN-FUSED gradient nodes #
A renderer with a separate optimizer (cifar8BnTrainStepText at opt := some _, the packed
cifar8w{,_bn}_* arms) emits *Grad ops where the SGD renders emit *Sgd: the same arm with
θ − lr· stripped. Each lemma here says one such op, at an arbitrary cotangent, denotes the
certified per-layer Jacobian contraction; the optimizer that consumes it is outside these lemmas.
The batched peers are GradNodesB.
The emitted dense weight gradient = certified.
The emitted conv weight gradient = certified.
The emitted conv bias gradient = certified.
The emitted per-channel BN γ gradient = certified, fed the BN-output cotangent c at the
saved conv output v.
The emitted per-channel BN β gradient = certified.
The conv weight-gradient node as a tie clause (convWGrad_den under ∀).
Equations
- One or more equations did not get rendered due to their size.