Multi-head sdpa backward w.r.t. V — per head, the certified sdpaBackV on the head slabs; concatenated by the finProdFinEquiv column layout.

Multi-head sdpa backward w.r.t. Q.

Multi-head sdpa backward w.r.t. K.

Flattened multi-head sdpa backward w.r.t. V (saved projections Q K V fixed).

Flattened multi-head sdpa backward w.r.t. Q.

Flattened multi-head sdpa backward w.r.t. K.

The full multi-head self-attention input-gradient backward (cotangent dY ↦ dX): output-projection backward (dense Woᵀ 0, per token) → the three sdpa cores → Q/K/V projection backwards (dense Wᵀ 0, per token), fanning in at X (the three paths add). The certified MHSA backward at the input (mhsaLayer, Attention.lean) is dconcat = dY·Woᵀ, (dQ, dK, dV) = sdpaBack{Q,K,V}(dconcat) per head, dX = dQ·Wqᵀ + dK·Wkᵀ + dV·Wvᵀ; mhsaBackFlat_eq_mhsa_vjp says this chain is that.

The vector-LayerNorm ViT encoder-block input-gradient backward. rowLNVecFlatBack in both LN slots at the site's flat saved input, per-token GELU slopes in the MLP sublayer's per-row fold (perRowFlatPR), and each sublayer's residual outside its fold.

Reading right to left, this is the reverse of transformerBlockV: the MLP sublayer's dense W₂ ∘ gelu ∘ dense W₁ ∘ LN₂ backward under a residual, then the attention sublayer's mhsa ∘ LN₁ backward under a residual. The shipped depth-12 net is vitForwardKV, whose blocks are transformerBlockV at γ β : Vec D; this is the spelling the whole-net tie is stated at.

vitBlockBackV with every saved slot pinned to the real forward at the block's own input. The Q/K/V projections at LN₁(A), the LN₁ backward at A and the LN₂ backward at the attention sublayer's output, the GELU derivative at dense₁(LN₂(attn A)) — one function of the block's flat input v, so the tower recursion can be written down. cnxBlockChBackAt's shape.

The depth-k encoder-tower backward at a saved tower input v.

Head-first, like the forward it reverses. vitBodyKVFlat (k+1) ps = vitBodyKVFlat k (ps ∘ succ) ∘ blockVFlat (ps 0) runs block 0 FIRST, so the backward applies block 0's reverse LAST, and the tail's saved input is block 0's forward OUTPUT. cnxStageChKBack's recursion verbatim, one architecture over. Writing the fold as its own recursion (rather than a list fold) is what makes the saved-activation thread visible, and the thread is the content.

The CLS-slice backward — the adjoint of clsTokenFlat (gather row 0 of the (N+1)×D sequence): scatter the head cotangent dy back to row 0 (the CLS token), zero on the patch rows. The certified clsTokenFlatHasVJP.backward.

The patch-embed output — the encoder tower's saved input. Named as a FUNCTION of the image so that the same constant is both the activation the tower's slots are saved at and the f argument of the chain's first vjpComp (cnxSavedA0 … cnxSavedA10's reason).

The encoder tower's output — the final LayerNorm's saved input.

THE WHOLE-NET ViT-TINY INPUT GRADIENT, at the depth, head count and LayerNorm spelling the net runs. The reverse of vitForwardKV = classifierFlat ∘ LNᵥ ∘ vitBodyKVFlat ∘ patchEmbed:

patchEmbedBack ∘ towerBack ∘ finalLNBack ∘ clsScatter ∘ dense Wclsᵀ

with every slot concrete — the patch-embed backward is patchEmbedInputGradFormula (which IS patchEmbedFlatHasVJP's backward, definitionally), the head is the free dense Wᵀ 0 followed by the CLS scatter, the final LN is rowLNVecFlatBack at the tower's output, and the tower is vitTowerBackK. vitInputGradK_eq_vitForwardKV_vjp is the apex that says this is the certified whole-net gradient.

The batched patch embedding: StableHLO.batchMap B of vitSavedPE, the tower's saved input at every example.

The batched tower output: StableHLO.batchMap B of the tower at the batched patch embedding — saved stage by stage, not batchMap B of the composed per-example prefix (the two agree only up to batchMap_comp, ViTWholeBackCertifiedTieB.lean).

The batched whole-net ViT input gradient — vitInputGradK at each of B examples, stage by stage, as the batched render computes it. The head backward and the CLS scatter are StableHLO.batchMap B of their per-example leaves (both input-independent); the final-LN and tower backwards are StableHLO.batchMapAux B of their per-example maps, each at the batched saved activation (vitSavedBodyB, vitSavedPEB); the patch-embed backward is batchMap B of the linear formula. Every slot is a lift because no ViT op couples examples, as in the batched step tie ViTStepTieGB. B is a variable: this chain carries no batch numeral. vitInputGradKB_eq_batchMap_vitForwardKV_vjp (ViTWholeBackCertifiedTieB.lean) says it is the certified gradient of batchMap B vitForwardKV.