⭐⭐ convnextInputGradB IS the certified whole-net ConvNeXt-T gradient AT A BATCH #

ConvNeXtWholeBackCertifiedTie.lean closed T6 for ONE image: convnextInputGrad, the reverse of convNextForwardTCh, IS the certified gradient at that image. Every shipped ConvNeXt artifact runs a batch — convnext_adam_train_step and the convnextin_* / convnextsin_* / convnextbin_* families — and its batched T3 tie (ConvNeXtStepTieGB.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 LayerNorm is per-example and no ConvNeXt op couples examples. This file closes T6 at that index: the twelve-stage batched chain convnextInputGradB (ConvNeXtBackChains.lean), every slot the per-example slot lifted at the batched saved activation, IS the certified gradient of batchMap B convNextForwardTCh at every batch x, for every B and every class count nC. ConvNeXt was the last net without a batched whole-net tie (planning/archive/renderer_convergence.md leg 3: its ImageNet artifacts never had a batched fold); with this the *InputGradB_eq_*_vjp family covers all seven nets.

Nothing here is new mathematics, and it is ViT's batched tie (ViTWholeBackCertifiedTieB.lean) one architecture over: ConvNeXt is smooth everywhere, so every stage has a GLOBAL HasVJP and its batched witness is batchMap_has_vjp_at over HasVJP.toHasVJPAt at each row — no smooth-point hypothesis anywhere, only the 23 LayerNorm positivities the per-example tie already carries.

1. cnxSavedB0 … cnxSavedB10 — the eleven batched stage inputs, as reducible functions of the batch saved STAGE BY STAGE (batchMap B stage ∘ cnxSavedB_{k-1} B w), not as batchMap B of the composed per-example prefix: the two agree only up to batchMap_comp, not rfl, and the apex's vjp_comp_diff_at produces the former. Each is also its apex level's inner map, so the stage witness above it sits at cnxSavedB_k B w x on the nose (item 4).
2. The twelve batched stage witnesses cnx*B_at, each batchMap_has_vjp_at over the per-example HasVJP at each row — at the dimension spellings the per-example tie normalised (cnxDn1, cnxLNh, cnxSavedA0: ConvNeXtWholeBackCertifiedTie.lean's "two spellings of one numeral" rule holds one batch index over).
3. The batched leaf ties. GAP's is rfl (its per-example tie is); the others are funext to one example, one rewrite of the per-example leaf tie at that example's row, then rfl — batchMapAux's slice and the lift's .backward row are the same term. ⚠ The channel-LN and downsample leaves are proven at VARIABLE dims (cnxChanLNBackB_eq_vjp, cnxDownBackB_eq_vjp) and instantiated by term: at the literal 96 56 56 the same rfl recurses past maxRecDepth 100000 on the numerals, the batched form of the per-example tie's "two spellings of one numeral" rule.
4. convNextForwardTChB_has_vjp_at — the twelve-stage apex, eleven vjp_comp_diff_ats over the batched stage witnesses, level k's inner map named cnxSavedB_k B w — and convnextInputGradB_eq_convNextForwardTChB_vjp, the tie: twelve leaf rewrites, then the eleven levels peeled by rw [vjp_comp_diff_at_fst_backward]. ⛔ Neither may leave the kernel a definitional step across the chain. A witness point spelled as the composed chain applied to x (what _ elaborates to), or a peel by simp only (the peel lemma is rfl, so simp records no step), makes the kernel unfold saved activations against the chain underneath the witnesses' .backwards. Spelled that way this module took ~18 min on Lean 4.32.2 and does not check at all on 4.34.0 (kernel timeout; tens of GB with the budget raised). As written it checks in seconds.
5. convNextForwardTChB_eq_chain — the shape check: batchMap B of the per-example twelve-factor chain IS the twelve batched stages, by batchMap_comp eleven times — and convnextInputGradB_eq_batchMap_convNextForwardTCh_vjp, the tie carried to the committed GLOBAL witness batchMap_has_vjp _ (convNextForwardTCh_has_vjp …) through HasVJPAt.backward_unique_of_eq, plus the ∑ pdiv reading on convNextForwardTCh itself.
6. convnextImagenetInputGradB_eq_vjp — the same statement at nC = 1000, the class count of every convnextin_* artifact, B a binder.