The bf16 gradient nodes — every *GradBBf16 kind the suite emits, folded once #

A bf16 render does NOT consume the f32 gradient node. It emits its own *GradBBf16 constructor, whose den rounds the operands going in and — for every kind but one — rounds the result ONCE, outside the batch sum: the emitted convolution contracts the batch inside a single op and stores its bf16 result once, so a rounding per summand would claim a coarser computation than the hardware performs. That is a different real number from the f32 node's, and it needs its own certificate: the bf16 twins do not consume the f32 node.

This file is the whole bf16 op table, stated per op kind: each lemma says the node denotes the certified Σ_n gradient at the ROUNDED operands, rounded. The proofs are the f32 fold's — congrArg rnd peels the outer rounding, Finset.sum_congr the batch, and the inner equality is the per-example certificate at rounded slices.

Note: rowDenseWeightGradBBf16 has NO outer rounding, and that is the measurement rather than an omission: its dot_general contracts batch and token in one op and keeps its f32-typed result deliberately (StableHLO.Basic's constructor says why), so only the two leaf reads round.

Note: Padding rides along invisibly, as in the f32 folds: the symmetric and XLA-SAME strided kinds have identical types and identical emitted shapes, and only the certificate tells them apart.

Note: BatchNorm, LayerNorm and the dense head have no bf16 twin here or anywhere: every bf16 net in the suite keeps them in f32, so their γ/β and weight nodes are the f32 folds' in both worlds.