P18IL's bound in box form

P18IL's bound in box form. A coefficientwise bound against mrL on the row-major lists of f, g gives the sup-norm bound against mrX (the hMrt of chain_concrete).

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

theorem NLogN.KFM.mrt_err_of_list (t : Fin (D + 1) → ℕ) [∀ i, NeZero (t i)]
    (f g : ((i : Fin (D + 1)) → ZMod (t i)) → ℂ) {xh : List (Fin (t (Fin.last D)) → ℂ)} {E : ℝ}
    (hE : 0 ≤ E) (hl : xh.length = (tsOf t).prod)
    (h : ∀ j < (tsOf t).prod, ∀ k : Fin (t (Fin.last D)),
      ‖xh.getD j 0 k - (mrL (t (Fin.last D)) (tsOf t) (recL t f) (recL t g)).getD j 0 k‖ ≤ E) :
    ‖boxOf t xh - mrX t f g‖ ≤ E

Context. The lemma belongs to the part KFM 14: P18IL's row-major lists vs. the box of the error chain: P18IL speaks about row-major lists of records (mrL, rmSub); chain_concrete about functions on the box ∏_{i ≤ D} ℤ/t_i (mrX, last axis = record coefficient).

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_Defs22.