ViT-Tiny step tie — the SGD-inline train step, all 200 parameters at the real backward chain #

What this file is. The tie of verified_mlir/vit_train_step.mlir — the SGD-inline step ViTRender.lean writes — at the fused θ − lr·g ops: vit_net_tied_certified (the last theorem) threads all 200 ViT-Tiny parameters through the committed multi-head (3 heads, d_head 64), depth-12, vector-LayerNorm forward and the loss-driven backward cotangent chain. The statement is per example, at one image and a hard label; the artifact runs a batch of 32, and that batch and its mean lie outside this statement. Its batched peer at the un-fused gradient node, the smoothed loss and a batch binder — the chain of the drop-free f32 vitin_* artifacts — is ViTTieGB.vit_net_tiedGB, built from this file's block ties by batchMap / batchMapAux.

The file has two layers:

• vit_block_tiedMHV / vit_block_tiedAtMHV — one multi-head (3 heads, d_head 64) vector-LN block, generic in the cotangent: the two residual fan-ins (vitCotHV, vitCotXinV), the three-way fan-in at LN₁ (vitCotLn1), and the per-head SDPA backward (ViTMultiHeadChain's vitCotD{Q,K,V}mh).
• vit_net_tied_certified — the 200-parameter capstone: the 192 block parameters threaded through all 12 blocks, the final LN, the classifier and the patch embed (vit_cls_den covers the CLS token at N = 1).

Every conjunct delegates to a ViTFold.*_den fold lemma at the chain cotangent — zero new ops, zero new bridges. The vector-LN granularity that ships ([192] γ/β) is what is modelled.

Multi-head promotion (3 heads, d_head=64) — the committed-render block tie #

The committed vitTrainStepRenderV is multi-head: the SDPA-internal backward dAtt → dQ/dK/dV runs per head (vitCotD{Q,K,V}mh, ViTMultiHeadChain), so the Q/K/V dense cotangents are the multi-head …mh ones rather than the single-head vitCotD{Q,K,V}; everything else (the out-proj Wo, LN₂, the MLP) is head-agnostic. vitBlockTiedMHV states the block's 16 parameter ties with those cotangents (no separate ss/p saves — the per-head scores/weights are recomputed inside the …mh cots from the saved Q/K); every conjunct delegates to a head-agnostic fold generic ViTFold.*_den.

Multi-head forward + cot-in + input-only block wrappers (the thread template) #

The non-block param bundle + the all-200-params capstone (committed ViT-Tiny config) #

vitFinalLNTied/vitHeadTied/vitEmbedTied bundle the final vector-LN γ/β, the classifier Wcls/bcls, and the patch-embed wConv/bConv/cls/pos as den = certified at their chain cotangents — each a direct delegation to the fold generics (ViTFold.*_den), with the cls op (denseBiasSgdB N=1) folded by vit_cls_den (its row-0 batch slice IS clsTokenGrad, closed by clsToken_sgd_certified). Then vit_net_tied_certified threads the REAL forward + loss-driven backward and bundles all 200 params.

The ties' weight records #

Twelve blocks as BlockParamsV (ViTDepthK's bundle), plus the patch embed, final LN and head. The ties share ONE ε across every LN. The dot-notation wrappers are abbrevs over the constructors above: a statement over a record unfolds to the unpacked one.

Every cotangent the capstone threads is a certified VJP backward #

vit_net_tied_certified threads two per-example constructors: the head's vitCotTowerOutV and each block's vitBlockCotInAtMHV. They are the render's spelling of the backward — per-head SDPA with pad and slice, LayerNorm as rowScaleFlat then rowLNBackFlat at γ = 1, separate dense backs — so tying them to the certified VJPs is a proof, not a definitional match: the lemmas below rewrite each spelling into the one the whole-net tie (ViTWholeBackCertifiedTie) is stated at. The only hypothesis is the LayerNorm's 0 < ε.