ViT-Tiny's T3 §1a TIE at the BATCHED index, the UN-FUSED gradient and the SMOOTHED loss #

ViTStepTie.lean ties all 200 parameters of the SGD-inline vit_train_step.mlir: each fused θ − lr·g op dens to the certified step at the cotangent the emitted backward chain delivers, per example, at a hard label. This file is that statement re-pointed along the THREE axes ConvNeXtStepTieGB.lean (§4b.6) moved for ConvNeXt, and it is that file's transformation applied to ViT's per-example capstone — the 4b capstone that closes the set at five of five.

⭐ Axis 1 — the OPTIMIZER FORM. Every conjunct is at the RAW gradient node (*GradB), which is what vit_adam_train_step.mlir and every vitin_* artifact emit since 4c leg 4; the fused op appears only in the SGD-inline file. One statement covers AdamW, the wx/clip variants, EMA, the 4× accumulation and the data-parallel twins, because they all consume this node. ViTFoldGB.lean (§4c-ter) is the fold each conjunct delegates to.

⭐ Axis 2 — the LOSS. g is a binder, instantiated at smoothedLossCotGraphDiv — the six-op chain expe → softmaxDiv → subB → scaleB → addVB → shiftB → divConstB this render emits at the plain width N·K, at a GENERAL target arriving as %onehot. The fused file pins it to softmax − oneHot.

⭐ Axis 3 — the INDEX. N is a binder. Every activation is batchMap N of the per-example prefix the fused file threads (patchEmbed_flat, vitBlockFwdOMHV, the final LN, clsSliceFlat) and every cotangent is batchMapAux N of the per-example chain (vitCotB2outV, vitBlockCotInAtMHV, the vitCot* family). Honest for this net because no ViT op couples examples — LayerNorm, attention, GELU and the denses are all per-example, and the *B constructors' den arms say so. nC is a binder too (10 on Imagenette, 1000 on ImageNet).

⭐⭐ The one conjunct the per-example capstone could not state is here. The CLS token is one shared [192] vector; its gradient is the sum of every example's CLS-row cotangent. The fused file's vit_cls_den is at denseBiasSgdB (N := 1) — "sum one thing", correct there because pretty B performed the batch lift outside the AST. vitEmbedTiedGB's third conjunct is ViTPoCGB.clsGrad_denB at the batched node, denseBiasGradB (N := N) on batchMap N clsSliceFlat of the embed cotangent, with the batch sum inside den.

What is NOT new #

Every save, every chain cotangent and every Jacobian witness is ViTStepTie.lean's, lifted; every conjunct's proof is one ViTPoCGB.*_den lemma. The per-example saves and internal cotangents are repackaged as functions of the block INPUT (blkSaves, cAtt … cM1) so that batchMapAux has something to lift — the let chains of vitBlockTiedAtMHV and vitBlockCotInAtMHV, verbatim. ⚠ ViT has no *BackBatchedGraph_faithful family and needs none here: the lift is the honesty argument, as it was for ConvNeXt.

⛔ Conventions carried unchanged from the fused file: the VECTOR LayerNorm (γ β : Vec D) at all 25 sites, 3 heads × d_head 64, depth 12, D 192, MLP 768, 16×16 patches, GELU (no kink — no smoothness hypothesis anywhere). Stated at ViT-Tiny's literal dims; S and B are other nets. ⛔ ONE REPLICA: in vitin_adamdp128x4* every gradient node feeds allReduceMeanF, the collective as an AST node since 4d piece 2 (2026-09-07; DataParallelNode.lean composes the per-replica statement with the replica mean), and the 4× accumulation is momVNextF at its other reading on top. ⛔ Stated at the drop-free chain.

Per-example saves and internal cotangents as functions of a block's INPUT #

vitBlockTiedMHV takes the nine saved activations as arguments; batchMapAux lifts a function of (one saved value, one input), so the batched block tie needs each save as a function of xin and each internal cotangent as a function of (xin, dyOut) — exactly the let chains of ViTTiePoC.vitBlockTiedAtMHV and vitBlockCotInAtMHV, packaged.

The multi-head block — all 16 gradient nodes, batched #

Final LN, classifier and patch embedding — batched #

The whole-net capstone — all 200 params through the REAL batched forward + composed cotangent #

The fused file's thread, lifted: ib1 is batchMap N of the patch embedding, ib_{k+1} is batchMap N of the multi-head block forward, the final LN / CLS slice / dense head are batchMap N of theirs, g is the smoothed loss cotangent at a general target, and every cotangent is batchMapAux N of the per-example chain — vitCotB2outV at the top, then twelve vitBlockCotInAtMHV attention-residual fan-ins down to the embed-output cotangent.