The uniform phase pass implements the diagonal phase

The uniform phase pass implements the diagonal phase.

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

theorem NLogN.KFW.sImplQ_phase {Is : List Sym} {Pp : ℕ} {iprog : Fin Pp → IStmt HS Pp}
    {Q : IState HS → Prop} {lo hi : ℕ}
    {ι : Type*} [Fintype ι] [DecidableEq ι] (r S t B u : ℕ) (pos : ι → ℕ)
    (hpos : ∀ i, pos i < t) (a' : ι → ℕ) (hr : 0 < r) (hS : 0 < S) (hB : 1 ≤ B) (Z : ℕ)
    (hZ : zsz ((4 * (B * (S * r * 2 ^ t) + S * r + B + 1) : ℕ) : ℤ) ≤ Z)
    {σ : Fin HS → Option ℤ} {ρR0 ρt ρB ρu ρV : Fin HS}
    (hR : PReg σ ρR0 ρt ρB ρu ρV (S * r) t B u) (hQ : ∀ s, Q s → Agree σ s)
    (εE : Ex HS) (Bε : ℕ) (hε : ∀ s, Q s → EpsOK s εE t (aEof pos a') Bε)
    (hBε : zsz (4 : ℤ) ≤ Bε)
    (hreg : ∀ j ∈ εE.regs, j ∉ [KFG.xA, NLogN.KFG.xB, NLogN.KFG.xC, NLogN.KFG.xD, xN, NLogN.KFB.c1, NLogN.KFW.xE, NLogN.KFW.cT]) (hε0 : (0 : Fin HS) ∉ εE.regs)
    (hu : ρu ≠ NLogN.KFB.c1) :
    SImplQ Is iprog Q lo hi r (fun i => 2 ^ pos i * S) (B * 2 ^ t * S)
      (Matrix.diagonal fun x => I ^ (u + ∑ i, a' i * (x i).val))
      (fcode (phLU ρR0 ρt ρB ρu ρV εE)) 0 0
      (fun w => cPhU w (B * (S * r * 2 ^ t)) t B Z (S * r) (xPh εE Bε Z))

Context. The lemma belongs to the part KFW: the uniform phase pass as a selected-bit operator.

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.