ConvNeXt-T's whole-net backward tie — the stage fold, and ⛔ what the tie FOUND #

⭐ Read EvenKernelConvBack.lean first; the finding is the deliverable. This file was started as the ConvNeXt peer of ResNet-34's whole-net tie (today r34InputGradB_eq_r34B_full_vjp) — planning/archive/float_budget_numbers_log.md §3.18, done BEFORE the number rather than after it, because §3.10's tie found r34 reversing the wrong pool and moved a committed number 4×. It paid out the same way at the first leaf it touched.

⛔⛔ WHAT THE TIE FOUND: convFlatBack IS NOT THE ADJOINT AT AN EVEN KERNEL, and ConvNeXt is the only net in the repo that has one. conv2d pads by pH = (kH-1)/2, so the reversed-kernel forward conv is the adjoint only when kH - 1 - pH = pH, i.e. only for odd kH. ConvNeXt's 4×4/s4 patchify stem and its three 2×2/s2 downsamples are the four sites where that fails; at kH = 4 the hand-written backward is the adjoint of a conv shifted one pixel. Every other net is all-odd (R34 7×7/3×3/1×1, MobileNetV2 and EfficientNet-B0 1×1/3×3/5×5), and ViT's 16×16 patch embed never routes through conv2d at all.

⚠ Nothing trained is affected, and the codegen tier already knew. StableHLO.lean's .convStridedBack pads ASYMMETRICALLY, [[kH-1-pH, pH]], in both the per-example (:6120) and the batched (:8248) arms, and its den is the certified VJP; the batched comment names the same quantity — "the symmetric [[p,p],[p,p]] … AGREES at every odd kernel and is WRONG at even ones (kH=2 ⇒ [[0,0]] where the VJP needs [[1,0]])". The fix landed on TWO tiers and never reached the third: BackwardMaps.lean's flatConvStride2Back / flatConvStride4Back, which are convFlatBack ∘ scatter at the SYMMETRIC pad. ⭐ That is imagenet_specs_drift_from_twins in its "a fix landed on one tier and its twin kept the old spelling" form, for the third time (§3.10's pool and §3.16's head LayerNorm were the first two).

What is here. The repair is padOdd (EvenKernelConvBack.lean): an even-kernel conv is an odd-kernel conv on the kernel zero-extended at (+1,+1), which is the emitter's asymmetric pad written in the vocabulary BackwardMaps.lean already has, so the existing odd-kernel leaf tie does all the work and no new conv machinery is needed. On top of it:

1. cnxDownChBack_eq_vjp — the stage-boundary downsample tie, lnB ∘ flatConvStride2Back (padOdd W) against (cnxDownChW_has_vjp …).backward. ⛔ padOdd is load-bearing: p.W is 2×2. Two existing ties composed.
2. cnxStageChKBack_eq_vjp — ⭐ the depth-k stage fold, §3.18's "one real proof". HasVJP for convNextStageChK is built head-first (block 0 runs first), so its backward composes the block backwards in the OPPOSITE order, each at its own saved activation, and the tail's saved input is block 0's forward OUTPUT. The induction step is one rewrite of the block tie (cnxBlockChBack_eq_vjp) and one of the inductive hypothesis.
3. cnxSavedA0 … cnxSavedA10 — convNextForwardTCh's eleven stage inputs, named as FUNCTIONS, so that the same twelve constants are both the activations the backward's slots are saved at and the f argument of each vjp_comp.
4. ⭐⭐ convnextInputGrad_eq_convNextForwardTCh_vjp — THE APEX. convnextInputGrad, with every slot pinned to the certified per-op backward at its own saved activation, IS (convNextForwardTCh_has_vjp …).backward x. The ConvNeXt peer of r34InputGradB_eq_r34B_full_vjp, and stronger: convNextForwardTCh_has_vjp is HasVJP — everywhere — not the smooth-point HasVJPAt that one is, because GELU, LayerNorm, convolution and the layer scale are all smooth and ConvNeXt has no kink anywhere. Its only hypotheses are the 23 LayerNorm positivities, so unlike every other whole-net backward tie in this repo it carries no smoothness side-condition. ⭐⭐ And ConvNeXt has its shape check too (planning/archive/float_budget_numbers_log.md §3.14): convNextForwardTCh_eq_chain, the rfl saying the chain the apex instantiates IS the committed forward, written before anyone needed it.

⭐⭐ WHAT THE ASSEMBLY COST, AND IT IS ONE RULE: never hand the unifier two spellings of the same thing in an APPLIED position. Every expensive step in this file was an instance, and each is free once the spelling is normalised at a definition:

• cnxDownChW h w p is declared over Vec (cin * (2 * h) * (2 * w)) where the chain spells Vec (96 * 56 * 56). Both are closed terms and equal, and the unifier still descends into the semantics of both sides rather than reducing 2 * 28 — the diagnostics reach conv2d_input_grad_formula, Finset.sum, Mat.unflatten, cnxBlockChW. Measured one link at a time, the three downsamples cost 3 s, 15 s and then do not finish, while every stage, LayerNorm, GAP and dense link is free. cnxDn1/cnxDn2/cnxDn3 below are the whole fix: a one-line def with the type ascribed in the chain's spelling, plus Differentiable/HasVJP peers ascribed the same way. Same for cnxLNh at Vec 768 against rowLNVecFlat 1 768's Vec (1 * 768).
• A leaf tie goes the OTHER way — state it in the LEMMA's spelling, not the chain's (cnxLNhBack_eq_vjp takes v : Vec (1 * 768)); at Vec 768 the same statement does not finish.
• The saved activations are functions, so each cnxTk is a one-step iota with syntactically identical sides. Stated the other way — the chain's own f x against an applied cnxSavedA k w x — identifying the two costs 2 s at depth one and does not finish at depth two.
• The closing step is rw [cnxV0] and rw [Function.comp_apply], not rfl: after the eleven peels the two sides differ only by Function.comp and cnxV0, and rfl will not take that route. ⛔ Nor simp only [Function.comp_apply, cnxV0], which elaborates just as fast: both lemmas are definitional, so simp records no step and the KERNEL re-derives the whole chain by unfolding — 17 s and 6 GB for this module on Lean 4.32.2, 6 min and 48 GB on 4.34.0. The rws hand it syntactic rewrites instead: 3 s and 3 GB on 4.34.0.

⚠ planning/archive/float_budget_numbers_log.md §3.7(d) records this trap in its other guise, where the computed dimension meets a metavariable (2 * ?h = 112) and the unification is higher-order; there the fix is to pin the implicit. Here h is given explicitly and it still costs — two CLOSED spellings of one numeral are enough. ⛔ And it is invisible in an unapplied position: convNextForwardTCh_vjp_chain's ascription compares the whole twelve-factor composition against the committed one and is free, because no x is in sight to evaluate.

⛔ The other half of the shape is the term-mode chain, and it is not a preference. convNextForwardTCh_has_vjp is a tactic proof, so its eleven haves are letFun and its .backward does not reduce; the whole-net rfl against it returned no result at maxHeartbeats 8000000, twice, ~8 min each. HasVJP.backward_unique transfers through .correct instead, which costs nothing, and the term-mode peer must be top-level defs rather than a let chain — a let used twice per level zeta-expands to 2^11 copies of the prefix.

⚠ ResNet-34's shape check is resnet34ForwardB_full_eq_slots (ResNet34BackCertifiedTieB.lean), and it is the net the hole first bit.

⭐⭐ Every stage whose declared type carries a COMPUTED dimension gets a wrapper here, and that is the whole reason this section closes in seconds. cnxDownChW h w p is declared over Vec (cin * (2 * h) * (2 * w)); the chain spells the same type Vec (96 * 56 * 56). Both are closed terms and they are equal, but in an APPLIED position the unifier does not reduce 2 * 28 to 56 — it descends into the semantics of both sides instead, and the diagnostics name what it reaches: conv2d_input_grad_formula, Finset.sum, Mat.unflatten, cnxBlockChW. Measured, one tie at a time: the three downsample links cost 3 s, 15 s and then do not finish, while every stage, LayerNorm, GAP and dense link is free. With the wrappers below — a one-line def per offending stage, its type ascribed in the chain's spelling, and its Differentiable/HasVJP peers ascribed the same way — the twelve chain defs and all eleven links together cost 2.9 s, of which the links are ~0.3 s.

⚠ planning/archive/float_budget_numbers_log.md §3.7(d) records this trap in its other guise, where the computed dimension meets a metavariable (2 * ?h = 112) and the unification is higher-order. There the fix is to pin the implicit. Here h is already given explicitly and it still costs: two CLOSED spellings of one numeral are enough. ⛔ And it is invisible in an unapplied position — convNextForwardTCh_vjp_chain's ascription below compares the whole twelve-factor composition against the committed one and is free, because no x is in sight to evaluate.

⭐ The wrappers, their Differentiable/HasVJP peers, the stem's cnxD0/cnxV0 and the four normalised leaf ties below are PUBLIC: ConvNeXtWholeBackCertifiedTieB.lean lifts the same twelve stages over a batch and needs them at exactly these spellings.

⭐ convNextForwardTCh's eleven stage inputs, named — and named as FUNCTIONS, so that the same twelve constants are both the saved activations the backward's slots are indexed by and the f argument of each vjp_comp. That is what makes every link below a one-step iota with syntactically identical sides: the alternative — an applied cnxSavedA k w x on one side and the chain's own f x on the other — is defeq, and identifying the two costs 2 s at depth one and does not finish at depth two.