The paper's layout [P] × [2^u] × [G] × [2^u] × [B] and the address permutation (p, h, g, d, z) ↦ (p, d, g,…

The paper's layout [P] × [2^u] × [G] × [2^u] × [B] and the address permutation (p, h, g, d, z) ↦ (p, d, g, h, z).

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

theorem AModelL12.l12bin_correct_paper {child : Oracle α} {d : α} {W m q Kp : ℕ}
    (hspec : OracleSpec child d W m q Kp) (hm : 2 ≤ m) (hW : 1 ≤ W) (ρ : ℕ)
    (P G B : ℕ) {e u : ℕ} (he : e ≤ m ^ Kp) (hu : 2 ^ u ≤ q ^ e) (xs : List α) :
    l12bin child W m q Kp ρ e u [P] [G] [B] d xs =
      pull [P, 2 ^ u, G, 2 ^ u, B] [P, 2 ^ u, G, 2 ^ u, B] (swapPos 1 3) d xs

Context. The lemma belongs to the part Lemma 12 (arbitrary-width interchange), array model: the procedure and its denotation: Radix-q layer. The array lives on qShape Pre G Suf q e = Pre ++ [q]*e ++ G ++ [q]*e ++ Suf (prefix, chunk h, gap, chunk d, suffix; the chunks are e radix-q digits each). The procedure l12q (paper, proof of Lemma 12):

1. interchange the top ρ digits of the two chunks one pair at a time (highSwaps, ρ primitive single-digit swaps);
2. join: move h⁺ next to d⁺ (a field rotation; the result lives on joinShape);
3. reshape (free): prefix ↦ one field P = vol Pre, d⁺h⁺ ↦ one row field R = q^(2ρ);
4. pad the row field to R' = padRows W Kp R (a multiple of W ^ Kp, zero rows appended);
5. write n = e - ρ in base m and call the Prop. 11 oracle child j on each corresponding pair of pieces of width m ^ j (pieceLevels, runPieces), all with the shared row field R';
6. unpad (scan away the padded rows), reshape back, reverse the joining rotation. If ρ > e (bounded widths) the procedure does e single-digit interchanges instead.

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.