Array version

Array version. The array permutation of amap L (the pull by its inverse amap L⁻¹) equals running the array primitives in the same order as in linear_via_bruhat (shifts for E₂, swaps, shifts for E₁); each primitive pulls by its own explicit inverse, so as pull maps the inverses compose in reverse order (invChain).

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

theorem AModel.linear_via_bruhat_array {E₁ E₂ : Matrix (Fin n) (Fin n) (ZMod Q)}
    (hE₁ : ∀ i j, i < j → E₁ i j = 0) (hE₂ : ∀ i j, i < j → E₂ i j = 0)
    (hd₁ : ∀ i, IsUnit (E₁ i i)) (hd₂ : ∀ i, IsUnit (E₂ i i))
    (σ : Equiv.Perm (Fin n)) (ts : List (Fin n × Fin n))
    (hts : (ts.map fun p => Equiv.swap p.1 p.2).prod = σ)
    {α : Type*} (d : α) (xs : List α) (hxs : xs.length = vol sh) :
    pull sh sh (amap Λ (E₁ * σ.permMatrix (ZMod Q) * E₂)⁻¹) d xs =
      AModel.runArr Λ d (bruhatSteps E₁ ts E₂) xs

Context. The lemma belongs to the part Array model: mixed-radix arrays, pull maps, and linear address maps via Bruhat factors: Arrays are lists in row-major lexicographic order over fields (first field most significant). All denotations are plain List functions.

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.