⛔⛔ convFlatBack is NOT the adjoint at an EVEN kernel — and the one-line repair #

convFlatBack W = flatConv (reverseSwap W) 0 is the reversed-kernel forward conv every backward in this repo runs, and convFlatBack_eq_vjp_backward (ResNet34BackCertifiedTie.lean) ties it to the certified conv input-VJP for ODD kernels only. That hypothesis is not a convenience: it is load-bearing, and the statement is FALSE without it.

conv2d pads by pH = (kH-1)/2, so convFlatBack's coefficient of dy[j] at output hi is W[hi - j + (kH-1-pH)], while the adjoint's is W[hi - j + pH]. They agree iff kH - 1 - pH = pH, i.e. iff kH is odd. At kH = 4 the reversed-kernel conv is the adjoint of a conv shifted one pixel.

⛔ ConvNeXt-T is the only net in the repo with an even kernel, and it has four: the 4×4/s4 patchify stem and the three 2×2/s2 downsamples. (ViT's 16×16 patch embed is NOT affected — patchEmbed_flat is its own definition over non-overlapping patches, with no conv2d and no padding convention.) Every other net is all-odd: R34 7×7/3×3/1×1, MobileNetV2 and EfficientNet-B0 1×1/3×3/5×5.

⚠⚠ The codegen tier already knew. StableHLO.lean's .convStridedBack emitter pads ASYMMETRICALLY, [[kH-1-pH, pH]], in both the per-example (:6120) and the batched (:8248) arms, and the batched one says so in as many words — "The symmetric [[p,p],[p,p]] this emitted AGREES at every odd kernel and is WRONG at even ones (kH=2 ⇒ [[0,0]] where the VJP needs [[1,0]]) … Found by the whole-net backward tie". Its den is (flatConvStride2_has_vjp W b).backward, the certified VJP, so the EMITTED ConvNeXt backward is correct and nothing trained is affected. What was never carried across is the third spelling of the same map — 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 (planning/archive/float_budget_numbers_log.md §3.10's pool and §3.16's head LayerNorm were the first two) — and here the fix landed on TWO tiers and missed the third.

The repair: spell the even kernel at an odd size #

An even-kernel conv IS an odd-kernel conv on the kernel zero-extended at offset (+1,+1): conv2d (padOdd W) b = conv2d W b (conv2d_padOdd_eq). The padding bookkeeping is exactly the emitter's: for even kH, a SYMMETRIC pad [[pH', pH']] at kH+1 (where pH' = kH/2 = pH+1) on a kernel whose leading tap is zero is the same program as the ASYMMETRIC [[kH-1-pH, pH]] at kH. So this is not a third convention — it is the emitter's convention, expressed in the vocabulary BackwardMaps.lean already has.

⭐ The consequence is that no new conv machinery is needed anywhere. The odd-kernel leaf tie convFlatBack_eq_vjp_backward does all the work at kH+1, and |padOdd W| ≤ w' is free (the new entries are 0), so every magnitude hypothesis transfers unchanged.