The loop body of phase 3

The loop body of phase 3.

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

theorem NLogN.KFV.body3_ok {eSw : Fin Pp} {dW : Fin HS} {Kc : ℝ} (HSw : SwOK I iprog eSw dW Kc)
    (hd0 : dW ≠ 0) (hd56 : dW.val < 56) (hKc : 0 ≤ Kc) (hdW : dW ∉ r3)
    (hK : 0 < K) (hℓ : 2 ≤ ℓ) {mk p W B : ℕ}
    (hB : (pLP D ℓ K long).n + ℓ + 5 ≤ B) (hNB : D * qq ℓ K + D + 1 ≤ B) (hWB : W ≤ B) :
    LoopBody (r := 2 ^ ℓ) I iprog (body3 eSw dW) (fun s => LRg s (pLP D ℓ K long) mk W)
      (fun t s => encK s (F2 (D * qq ℓ K) t))
      (fun t => Synth.runArr (pLP D ℓ K long).n 0 (opX D ℓ K long t)) (2 ^ (pLP D ℓ K long).n)
      p W (cBody3 D ℓ K Kc (pLP D ℓ K long).n W B) (D * qq ℓ K)

Context. The lemma belongs to the part KFV §37: phase 3 of the layout (the chunk exchanges) as a fixed IL loop: Iteration t < N = D q: the chase x ← src t; N times (x ← src x while x < t) runs in the register gV (an RS counter loop on gT2), then, unless x = t, the chunks t and x (after the prefix Lst) are exchanged by the Lemma 12 entry (xchC). ph3_ok: the loop computes runArr n 0 (ops3 …).

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.