vol_replicate (Proposition 11 (power-width interchange with rows) in the array model)

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

theorem AModel.vol_replicate (m N : ℕ) : AModel.vol (List.replicate m N) = N ^ m

Context. The lemma belongs to the part Proposition 11 (power-width interchange with rows) in the array model: 1. Layout.cons2: a layout on rest lifted to P :: L :: rest; amap_cons2. 2. The concrete frame action shearπ (shear address maps on rest), its hypotheses, and shear_network: the row-split network realizes H ← H + D on every row. 3. netRunF: the network with implemented frame changes; netRunF_congr (agreement on the frame changes that actually occur, FramesOK, suffices). 4. runC: Lemma 10 steps with every field interchange delegated to a child. 5. Chunk shapes hdShape (chunks split into m fields) / swShape (chunks merged). 6. amap_swapMat_eq_blockSwap. 7. One level (levelR) with an oracle child: levelR_correct_amap, levelR_correct. 8. The recursive program prog and prog_correct (induction on the level). 9. Cost: levelCost_eq (T_{k+1}(V) = C₀ V + s T_k(V/W)), prog_cost. 10. prop11: denotation (block swap of the two m^k-digit chunks) and cost O(V (m^k)^τ).

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.