T3 §1 fold for ViT-Tiny at the BATCHED index — the op set 4c leg 4 renders #

ViTFoldG.lean folds the ten gradient nodes of the PER-EXAMPLE traversal (ViTRender.vitBackAll at adam := true). This is its batched peer, at ViTRenderB.vitBackAllB's constructors, and it exists because 4c leg 4 moves every committed ViT artifact onto that traversal.

⭐ The bytes do not move and the denotation does. Measured 2026-09-07: all nineteen drop-free ViT artifacts — vit_fwd, vitin_fwd and the seventeen AdamW/EMA train steps — re-render byte-identically off vitBackAllB, because every batched form was built to emit its per-example peer's text and tests/TestBatchedEmitTie.lean pins each one individually. So this file is not about different bytes; it is about the AST those bytes are pretty of.

⭐⭐ And on one parameter the AST is genuinely better, which is the whole point of the leg. The CLS token is ONE shared [192] vector, so its gradient is the sum of every example's CLS-row cotangent. The per-example render emits denseBiasGradB (N := 1) — "sum one thing", correct there because pretty B performed the batch lift OUTSIDE the AST — where the batched one emits denseBiasGradB (N := vbB) and the sum is inside den. ViTRenderB.lean flags that line as "THE ONE LINE WHERE N := 1 → N := vbB CHANGES THE FUNCTION", and clsGrad_denB below is the statement the per-example clsGrad_den could not make. Same emitted text either way, which is why the byte tie cannot see it and den_rowDenseBiasGradB_at_one exists to argue the point.

The op table of every committed ViT train step, after leg 4 #

⭐ No new mathematics: every proof is Finset.sum_congr rfl over the batch and then the per-example bridge at batchSlice n. That is ResNet34FoldB.denseWGradB_den's shape, and it is available because each batched den arm is literally ∑_batch of the per-example one — the constructors were written that way (StableHLO.lean's own comment on veclnGammaGradB: "TWO-LEVEL: the outer Σ_n is the batch, the inner Σ_r the rows within one example").

⭐ One lemma per op kind certifies every optimizer tail at once — AdamW, the wx/clip variants, the EMA shadow and the 4× accumulation all consume the same *GradB node, and the vitin_adamdp128x4wxclipdrop artifact whose accuracy the book quotes is one of them.

⭐ The LayerNorm form is the VECTOR one (γ β : Vec D), which is what the shipped vitForwardKV runs; the scalar-affine spelling this cone was caught on three times is nowhere here.

Honest residual #

• ⚠ biasGradB is the IDENTITY on its operand and the classifier bias's batch reduce is in the emitted text, outside the AST — the constructor says so ("the channel sum happens in the emitted reduce") and it is the per-example biasGrad carve-out carried over unchanged, not a new one. So headBGradB_den is stated PER EXAMPLE, at batchSlice n, which is the whole of what the node denotes.
• Every lemma is ∀ cot. Pinning each to the emitted backward subgraph is the §1a tie: ViTTiePoCGB.vit_net_tiedGB at these nodes (4b.7); the per-example ViTStepTie.lean stays at the SGD-inline vit_train_step.mlir.
• The *bf16 artifacts emit rowDenseWeightGradBBf16 / patchEmbedWeightGradBBf16, their own kinds; Foundation/Bf16GradNodes.lean folds them (the row-dense one keeps its f32 result).
• vitin_adamdp128x4* is four replicas: the all-reduce is emitted text outside the AST, so these lemmas are about the per-replica gradient node (4d).