⭐⭐ vitInputGradKB IS the certified whole-net ViT-Tiny gradient AT A BATCH #

ViTWholeBackCertifiedTie.lean closed T6 for ONE image: vitInputGradK, the reverse of vitForwardKV over that image's N + 1 tokens, IS the certified gradient. Every shipped ViT artifact runs a batch — vit_adam_train_step and the vitin_* family at 128 or 512 per device — and its batched T3 tie (ViTStepTieGB.lean) states every activation as StableHLO.batchMap B of the per-example prefix and every cotangent as batchMapAux B of the per-example chain, because no ViT op couples examples. This file closes T6 at that index: the five-stage batched chain vitInputGradKB (ViTBackChains.lean) IS the certified gradient of batchMap B vitForwardKV at every batch x, for every B. ViT was the one net without a batched whole-net tie; with this the *InputGradB_eq_*_vjp family covers all seven nets.

Nothing here is new mathematics, and it is lighter than ResNet-34's batched tie because ViT is smooth everywhere: every stage has a GLOBAL HasVJP, so its batched witness is batchMap_has_vjp_at (4.1c's field-by-field lift, BatchMapVJPAt.lean) over HasVJP.toHasVJPAt at each row — no smooth-point hypothesis anywhere, only 0 < ε.

1. batchMap_comp (BatchMapVJPAt.lean, shared with ConvNeXt's batched tie) — batchMap B (g ∘ f) = batchMap B g ∘ batchMap B f, the lemma the shape check needs and the reason the chain saves its activations stage by stage: the two spellings agree only up to finProdFinEquiv.symm_apply_apply, which is not rfl.
2. The batched leaf ties. The patch-embed stage needs none (its backward is rfl); the other three are funext to one example, one rewrite of the per-example tie at that example's row (vitTowerBackK_eq_vjp, vitFinalLNBack_eq_vjp, vitHeadBack_eq_classifier_vjp), then rfl — batchMapAux's slice and the lift's .backward row are the same term, as r34's pool endpoint found.
3. vitKVB_has_vjp_at — the four-stage apex, three vjp_comp_diff_ats over the batched stage witnesses — and vitInputGradKB_eq_vitKVB_vjp, the tie: three leaf rewrites, then rfl.
4. vitForwardKVB_eq_chain — the shape check: the four batched stages compose to batchMap B vitForwardKV, by vitForwardKV_eq_chain and three batchMap_comps — and vitInputGradKB_eq_batchMap_vitForwardKV_vjp, the tie carried to the committed GLOBAL witness batchMap_has_vjp (vitForwardKV …) through HasVJPAt.backward_unique_of_eq (BatchMapVJPAt.lean; batchMap_has_vjp is ▸-transported, so its .backward does not reduce; uniqueness is the escape every whole-net tie in this repo takes), plus the ∑ pdiv reading.
5. vitTinyInputGradB_eq_vitTiny_vjp — the capstone at ViT-Tiny's literal dims, B a binder.