Erasure — every batched bf16 kind is its f32 peer at the identity rounding #

flatConvFBf16_id (StableHLO.Basic) says of the per-example CIFAR conv that the bf16 op "adds ROUNDING and nothing else — no reassociation, no dropped bias, no moved padding". This file says it of the twenty-five batched kinds the ImageNet renders emit: for each, den (or denOp) at rnd := id is the f32 constructor's den, named against its own peer. The renderers pass zrnd = id (StableHLO.Pretty), so these are the equalities the rendered bf16 ASTs satisfy, and they are what lets a whole-net statement at the f32 nodes be restated at the bf16 artifact (planning/bf16_tie.md §3).

Each lemma names its own peer. The symmetric and XLA-SAME strided kinds have identical types and emitted shapes and differ only in denOp (Basic.lean, the convStridedXla arm), so a mismatched pairing fails to prove — which is the check.

Two bias splits the suite did not have (flatConvStride2, depthwiseStride2FlatXla) are proved here beside their siblings' pattern from ParamGradNodes.

The last section states the same thing of the renderers' switches (StableHLO.PrecisionSwitch): denOp (.convAt bf16 id …) = denOp (.conv …) for either bf16, one lemma per switch. A typed forward graph built on the switches (r34IdGraphB, …) is then faithful at either precision by the f32 proof with these rewrites in front of it — simp only […, denOp_convAt_id] before denOp, since on a symbolic bf16 the denOp equations are stuck on the if and simp would otherwise unfold it to a stuck match.

Nothing here says how large the rounding is; rnd is a binder everywhere else and id here.