tensorGo_eq (Base `ref`: `tensorGo` computes `tensorMapZ` (copies))

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

theorem IntMul.HvdH.RefPf.tensorGo_eq (K : ℕ) (ns ns' : List ℕ) (hns : ns.length = K) (hns' : ns'.length = K)
    (hpos : ∀ i < K, 0 < ns.getD i 1)
    (A : ℕ → (ℕ → ℤ × ℤ) → (ℕ → ℤ × ℤ))
    (hloc : ∀ i < K, ∀ U U' : ℕ → ℤ × ℤ, (∀ j < ns.getD i 1, U j = U' j) → A i U = A i U')
    (g : (Fin K → ℕ) → ℤ × ℤ) :
    tensorGo ((List.range K).map fun i => (ns'.getD i 1, fun X : List (ℤ × ℤ) =>
        (List.range (ns'.getD i 1)).map (A i fun j => X.getD j (0, 0))))
      ns (listOf ns fun j => g fun i => j i) =
    listOf ns' fun j => tensorMapZ (fun i : Fin K => A i) g fun i => j i

Context. The lemma belongs to the part Base ref: tensorGo computes tensorMapZ (copies): Verbatim excerpts of the base thread's ref/ development (not in this workspace): Spec.ixf, all of ListBox, the lists section and the boxIdxs/ixf cons lemmas of MDif, the snoc lemmas of FermatW, and all of TGo. Main result: tensorGo_eq, the list pipeline tensorGo (nlogn's machine reference) on row-major listOf arrays equals the base fixed-point tensor tensorMapZ read on the output box.

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.