Lemma 12 (arbitrary-width interchange), array model, parametric in the Prop. 11 oracle

Lemma 12 (arbitrary-width interchange), array model, parametric in the Prop. 11 oracle. For every family of oracles meeting the Prop. 11 block-swap specification at every level bound K, with cost Tc K j V ≤ K₀ V (m^j)^τ, there is K such that for every u ≥ 1 and all prefix/gap/suffix shapes the procedure interchanges the two [2^u] fields, at cost ≤ K V u^τ (V = the array's volume).

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

theorem AModelL12.lemma12 (child : ℕ → Oracle α) (Tc : ℕ → ℕ → ℝ → ℝ) (d : α) {W m q ρ₀ : ℕ}
    {τ K₀ c : ℝ} (hm : 2 ≤ m) (hW : 1 ≤ W) (hq : 2 ≤ q) (hWq : W ≤ q ^ (2 * ρ₀))
    (hτ : 0 < τ) (hK₀ : 0 ≤ K₀) (hc : 0 ≤ c)
    (hspec : ∀ K, OracleSpec (child K) d W m q K)
    (hcost : ∀ K j V, 0 ≤ V → Tc K j V ≤ K₀ * V * ((m : ℝ) ^ j) ^ τ) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ u : ℕ, 1 ≤ u → ∀ Pre G Suf : Shape,
      (∀ xs : List α, lemma12Prog child W m q ρ₀ Pre G Suf u d xs =
        pull (binShape Pre G Suf (2 ^ u)) (binShape Pre G Suf (2 ^ u))
          (swapPos Pre.length (Pre.length + 1 + G.length)) d xs) ∧
      lemma12Cost Tc c W m q ρ₀ Pre G Suf u ≤
        K * (vol (binShape Pre G Suf (2 ^ u)) : ℝ) * (u : ℝ) ^ τ

Context. The lemma belongs to the part Lemma 12 (arbitrary-width interchange), array model: final statements.

Formalization Note. This lemma belongs to the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the array model of tape data (mixed-radix arrays and pull maps), the interchange networks of §3–4 (Propositions 7, 8, 11, Lemmas 9–12), the butterfly layers of §5 (Lemma 13, Proposition 14), the synthesis of §6–7 (Lemma 16, Proposition 18), the resampling and parameter choices of §8–9, and the final glue IntMul.OpenAI.Glue.kappaBound_of_machine, which derives the platform bound KappaBound (1/2^182) (from Def_IntMul_MultitapeModel) for any correct multitape machine meeting the paper's time recurrence. All names refer to the definition bundles IntMul_Kappa_K_Defs1–IntMul_Kappa_K_Defs9.