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 consume the same node" was written in three fold headers and is false.

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 — congr 1 peels the outer rounding, Finset.sum_congr the batch, and the inner equality is the per-example certificate at rounded slices.

⚠ 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.lean's constructor says why), so only the two leaf reads round.

⚠ 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.

⛔ 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.