Error of a whole axis-by-axis pass (base Lemma 2.11 + tensorMap_liftL): if every Aa i approximates the…

Error of a whole axis-by-axis pass (base Lemma 2.11 + tensorMap_liftL): if every Aa i approximates the lifted line map liftL (L i) within ε i and the lifts are 1-Lipschitz, then tensorMapZ Aa keeps the disc and approximates 2^p · tens (kerL L) within ∑ ε i at every address.

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

theorem NLogN.KFM.tensor_fp (p : ℕ) {a b : Fin d → ℕ} [∀ i, NeZero (a i)] [∀ i, NeZero (b i)]
    (Aa : Fin d → (ℕ → ℤ × ℤ) → (ℕ → ℤ × ℤ))
    (L : (i : Fin d) → (ZMod (a i) → ℂ) →L[ℂ] (ZMod (b i) → ℂ)) (ε : Fin d → ℝ)
    (hA : ∀ i, FPApprox p (Aa i) (NLogN.KFM.liftL (L i)) (ε i)) (hL : ∀ i, SupLip (NLogN.KFM.liftL (L i)))
    (U : (Fin d → ℕ) → ℤ × ℤ) (hU : InDisc p U) :
    InDisc p (tensorMapZ Aa U) ∧ ∀ j : Fin d → ℕ,
      ‖gC (tensorMapZ Aa U j) - 2 ^ p * IntMul.OpenAI.RT.tens (kerL L)
          (fun k => gC (U (fun i => (k i).val)) / 2 ^ p) (fun i => ((j i : ℕ) : ZMod (b i)))‖
        ≤ ∑ i, ε 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.