The batched f32 gradient nodes — one *GradB_den per op kind, shared by every conv net #
Every batched train step the suite renders emits the RAW gradient (*GradB) and hands it to an
optimizer tail (SGD, heavy-ball, Adam/AdamW, RMSProp, EMA, the data-parallel all-reduce), so one
lemma per op kind — "this node denotes the certified Σ_n gradient" — certifies every optimizer
variant of every net at once. Each proof is Finset.sum_congr rfl over the batch and then the
per-example VJP at batchSlice n. The bf16 kinds (*GradBBf16) are a different real number and
are folded in Bf16GradNodes; the fused *SgdB ops are these through
StableHLO.lean's *SgdB_eq_grad family (rfl).
Namespaces are the net that first needed the op (kept so that every citation keeps its name):
| op kinds | namespace | emitted by |
|---|---|---|
conv / strided-conv (symmetric) W and b, BN γ/β, dense W/b, the *TiedB clause Props | ResNet34PoCB | every conv net |
XLA-SAME strided conv W, depthwise W, symmetric strided depthwise W, rectangular dense b | EnetPoCG | EfficientNet-B0, MobileNetV2/V4, ConvNeXt |
XLA-SAME strided conv b, depthwise b, XLA-SAME strided depthwise W and b | Mnv2PaperPoCG | MobileNetV2, ConvNeXt |
| stride-4 patchify conv W | CnxPoCGB | ConvNeXt |
The per-token dense and vector-LayerNorm nodes (ViTPoCGB) live in ViTFoldGB, beside
the per-example bridges they fold; ConvNeXt's channel-LN and layer-scale nodes in
ConvNeXtFoldGB.
⚠ Padding is invisible in the types: the symmetric and XLA-SAME strided kinds have identical
types and identical emitted shapes, and only the certificate tells them apart.
Every lemma is ∀ cot; pinning each cotangent to the emitted backward subgraph is each net's
*StepTie* file.
Batched stride-1 conv weight GRADIENT denotes the certified Σ_n weight gradient. The
un-fused peer of EnetPoC.convWB_den: same Σ_n of conv_weight_grad_bridge, with no
θ − lr· wrapper because the batched r34 render hands this node to an optimizer tail.
Batched stride-1 conv bias GRADIENT denotes the certified Σ_n bias gradient.
Batched strided conv weight GRADIENT denotes the certified Σ_n weight gradient. Generic
in the kernel size, so the one lemma certifies the 7x7 stem AND every 3x3 downsample W1 AND
every 1x1 projection Wp.
Batched strided conv bias GRADIENT denotes the certified Σ_n bias gradient.
Batched BN γ GRADIENT denotes the certified per-channel γ gradient over the merged
batch+spatial axis m = N·(h·w). γ enters affinely, so there is no batch coupling in the
PARAM gradient and this is bnPerChannel_grad_gamma_correct at that width, through the
network→oc-major reindex bnchwFwd. Generic in the free β.
Batched BN β GRADIENT denotes the certified per-channel β gradient Σ_{batch,spatial} cot
at m = N·(h·w). Carries a free v/γ — β's gradient is the channel sum and depends on
neither.
One batched BN layer's γ and β gradient nodes, tied — the pair every step tie states per
BatchNorm: the emitted bnGammaGradB / bnBetaGradB denote the certified per-channel γ and β
gradients over the merged batch+spatial axis, at the layer's pre-BN activation v and its
output cotangent cot (both in the network layout).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Batched dense weight GRADIENT denotes the certified Σ_n outer product.
Batched dense bias GRADIENT denotes the certified Σ_n cotangent sum.
A stride-1 conv weight gradient node, tied (convWGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-1 conv bias gradient node, tied (convBGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-2 (symmetric-pad) conv weight gradient node, tied (convStridedWGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-2 (symmetric-pad) conv bias gradient node, tied (convStridedBGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-2 XLA-SAME conv weight gradient node, tied (EnetPoCG.convStridedXlaWGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-1 depthwise weight gradient node, tied (EnetPoCG.depthwiseWGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-1 depthwise bias gradient node, tied (Mnv2PaperPoCG.depthwiseBGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A stride-2 depthwise weight gradient node, tied (EnetPoCG.depthwiseStridedWGradB_den).
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Batched XLA-SAME strided conv bias GRADIENT denotes the certified Σ_n bias gradient.
The stem's bias slot, at convBias := true. Same reduce text as the stride-1 bias grad; the
den is the odd-phase bias VJP.
Batched stride-1 depthwise bias GRADIENT denotes the certified Σ_n bias gradient. The
depthwise bias slots at convBias := true. EfficientNet has no instance of this op — its
depthwise convs are followed by BatchNorm, so their bias is always folded.
Batched XLA-SAME strided depthwise weight GRADIENT denotes the certified Σ_n weight
gradient. The four stride-2 depthwises (b2/b4/b7/b14). ⚠ This is the Xla op — its
weight-grad correlation keeps the [p−1, p+1] pad, the opposite asymmetry from the input-grad,
and that asymmetry is the whole content of the variant. B0's strided depthwise is the
SYMMETRIC op, so the two nets do not share this certificate.
Batched XLA-SAME strided depthwise bias GRADIENT denotes the certified Σ_n bias
gradient. At convBias := true.
Batched patchify-stem weight GRADIENT denotes the certified Σ_n weight gradient.
⚠ The emitted convolution contracts the batch axis itself (the transpose trick), so the outer
sum is inside one op rather than across N of them — same as the strided ops.
Each tie clause holds #
One lemma per clause above, every argument implicit: a step tie's conjunction of clauses is then an anonymous constructor of these, its arguments read off the goal.