A phase step on the node roles

A phase step on the node roles.

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

theorem NLogN.KFW.stepQ_phase (hN : NodeR σ K t S0 r H k e B Bn) (hQ : ∀ s, Q s → Agree σ s)
    (hr : 1 ≤ r) (hS : 1 ≤ S0) (hBn : 1 ≤ Bn) (hK : 1 ≤ K)
    (hKe : K * (mC ^ (k + 1) - 1) ≤ e) (het : e - e % K + K ≤ t) (Z : ℕ)
    (hZ : zsz ((16 * (P8Lift.Wc * (nN Bn t S0 * r)) : ℕ) : ℤ) ≤ Z)
    (hZe : zsz ((e + t + K + mC * mC ^ k + mC ^ k : ℕ) : ℤ) ≤ Z)
    (hZu : zsz ((6 * mC ^ k + 6 : ℕ) : ℤ) ≤ Z)
    (w : Fin P8Lift.Wc) (k0 k1 : ℕ) (a : Fin mC → ℕ) :
    RImplQ Isym tbl Q lo hi r (nN Bn t S0) (stN K e k S0)
      ((P8Lift.RStep.phase w k0 k1 a : P8Lift.RStep (Fin P8Lift.Wc) mC).den
        (Butterfly.tens Cm : Butterfly.Op (Fin (mC ^ k))))
      (phC' w k0 k1 a) 0 (0 + (0 + 2) * P8Lift.Wc)
      (cWrapQ P8Lift.Wc (nN Bn t S0 * r) Z 0 0
        (cPhStep Z (((k0 + k1 * mC ^ k) % 4 : ℕ) : ℤ) (εTab NLogN.KFW.vE vK vF NLogN.KFW.wF (List.ofFn a)) Bn t S0 r))

Context. The lemma belongs to the part KFW: expressions over a register assignment, and the uniform phase step.

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.