The tie predicates at either precision — ConvWTiedBAt bf16, ConvWSyncAt bf16, … #

GradNodesB states each parameter gradient node against the certified Σ_n gradient (ConvWTiedB, …), ParamGradNodes makes it a loss derivative (convW_hasGradAt, …) and SyncKit ties the all-reduced collective to the batch-R·N node (ConvWSync, …) — all at the f32 constructor. The ImageNet renders the book reports train from are bf16, and a bf16 render emits the *GradBBf16 kind at every conv weight gradient. This file states the same three things with the node chosen by the renderers' own switch (StableHLO.PrecisionSwitch: convWeightGradBAt bf16 id … is the f32 kind at false, the bf16 kind at true), and proves each for either value from the f32 lemma and Bf16Erasure (den_convWeightGradBAt_id): at the identity rounding the bf16 node denotes what the f32 node does, so a tie stated on the switch reads the bf16 artifact's text over ℝ exactly as the f32 tie reads the f32 artifact's.

The kinds here are the ones the ResNet and MobileNet / EfficientNet ties emit — conv, convStrided, convStridedXla (the TF-origin stems), depthwise, depthwiseStrided (B0's and MobileNetV4's downsampling depthwise) and depthwiseStridedXla (MobileNetV2's); the remaining kinds (stride-4, row-dense, patch-embed) follow the same pattern as ConvNeXt's and ViT's ties move onto the switch (planning/bf16_tie.md §3.3). At false each predicate is its f32 original by rfl (convWTiedBAt_false, …), except DepthwiseStridedXlaWTiedBAt, whose f32 form MobileNetV2StepTieB stated inline rather than as a GradNodesB predicate.

Nothing here is about the size of the rounding: rnd is id throughout, as in the renderers.