The exact counterpart of an axis-by-axis pass: the base tensorMap of the lifted line maps is the kernel…

The exact counterpart of an axis-by-axis pass: the base tensorMap of the lifted line maps is the kernel tensor tens (kerL L), read on [0, a)-addresses and at ĵ = j mod b.

The following holds (Lean statement, in the scope of module Solutions.KFMLines):

theorem NLogN.KFM.tensorMap_liftL {a b : Fin d → ℕ} [∀ i, NeZero (a i)] [∀ i, NeZero (b i)]
    (L : (i : Fin d) → (ZMod (a i) → ℂ) →L[ℂ] (ZMod (b i) → ℂ))
    (x : (Fin d → ℕ) → ℂ) (j : Fin d → ℕ) :
    tensorMap (fun i => NLogN.KFM.liftL (L i)) x j =
      IntMul.OpenAI.RT.tens (kerL L) (fun k => x (fun i => (k i).val)) (fun i => ((j i : ℕ) : ZMod (b i)))

Context. The lemma belongs to the part Item 12 (math side, part 2): line maps applied axis by axis: The machine applies the per-axis fixed-point maps (Sapprox, B0P) slice by slice. That is the base tensorMapZ (via tensorGo_eq, KFMBaseTGo). This file identifies the exact counterpart, the base tensorMap of the lifted line maps liftL (L i), with the explicit tensor witness tensCLM (kerL L) of KFMR19. Then base fp_tensor gives the error of the whole pass.

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs18.