Proposition 11 (power-width interchange with rows), array model

Proposition 11 (power-width interchange with rows), array model. Let the circuit satisfy the Prop. 11 hypotheses at every level (gates OK, scalar routing ρ, Mout (ρ w) − Min w = 1, every frame change A_e with a Lemma 10 factorization E₁ Π_e E₂ valid mod q ^ m ^ k), let s = Σ_e r_e (r_e = number of ones of Π_e) with s / W < m ^ τ. Then: 1. for every k, the level-k program interchanges the two chunks of e = m ^ k radix-q digits (blockSwap of the two digit runs) whenever the row count is divisible by W ^ k; 2. its structural cost satisfies T_k(V) ≤ K V (m ^ k) ^ τ.

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

theorem AModel.prop11 (C : Circuit R m W) {q : ℕ} (hq : 2 ≤ q) (hm : 2 ≤ m)
    (hOK : ∀ k, C.OK (q ^ m ^ k)) {τ : ℝ} (hτ : 0 < τ ∧ τ < 1)
    (hs : (rankSum C : ℝ) / W < (m : ℝ) ^ τ) :
    (∀ (k P L : ℕ) (A B Cs : Shape) (xs : List R), W ^ k ∣ L →
      xs.length = vol (P :: L :: hdShape A B Cs (m ^ k) q) →
      AModel.prog C q k P L A B Cs xs =
        pull (P :: L :: hdShape A B Cs (m ^ k) q) (P :: L :: hdShape A B Cs (m ^ k) q)
          (blockSwap (A.length + 2) (A.length + B.length + m ^ k + 2) (m ^ k)) 0 xs) ∧
    ∃ K : ℝ, 0 ≤ K ∧ ∀ k V, 0 ≤ V → progCost C q k V ≤ K * V * ((m : ℝ) ^ k) ^ τ

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