Proposition 11 with Lemma 10 discharged (paper's Lemma 10 proof)

Proposition 11 with Lemma 10 discharged (paper's Lemma 10 proof). Given the circuit hypotheses (gates OK, routing ρ, Mout (ρ w) − Min w = 1) and s / W < m ^ τ where s = Σ_e rank_ℚ A_e over all frame changes, there is q₀ such that for every prime q > q₀ and every level bound K, the program whose frame changes use the integer lifts mod q ^ m ^ K of the (once chosen) rational Lemma 9 factorizations satisfies: 1. at every level k ≤ K, it interchanges the two chunks of m ^ k radix-q digits; 2. its cost is ≤ K₀ V (m ^ k) ^ τ with K₀ independent of K.

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

theorem AModelFac.prop11_rat (C : Circuit R m W) (hm : 2 ≤ m)
    (gatesOK : ∀ g ∈ C.gates, g.OK)
    (route : ∀ (v : Fin W → R) w, scalarRun C.gates v (C.ρ w) = v w)
    (unit : ∀ w, C.Mout (C.ρ w) - C.Min w = 1) {τ : ℝ} (hτ : 0 < τ ∧ τ < 1)
    (hs : ((frameSum (fun A => (ratM A).rank) C.gates C.Min C.Mout : ℕ) : ℝ) / W <
      (m : ℝ) ^ τ) :
    ∃ q₀ : ℕ, ∀ q, q.Prime → q₀ < q →
      (∀ K k, k ≤ 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 (withFac C (facZ (q ^ m ^ K))) 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 k V, 0 ≤ V →
        progCost (withFac C (facZ (q ^ m ^ K))) q k V ≤ K₀ * V * ((m : ℝ) ^ k) ^ τ

Context. The lemma belongs to the part Discharging the factorization hypothesis of Proposition 11 (Lemma 10 data).

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.