A phase step (round six, `stepH_phase`)

A phase step on the node roles.

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

theorem IntMul.Kappa.R6.IL3H.stepH_phase (hN : NodeRH c σ K t S0 r H E e B) (hQ : ∀ s, Q s → Agree σ s)
    (hm : 1 ≤ c.m) (hF : 1 ≤ E / c.m) (hW : 1 ≤ c.Wr)
    (hr : 1 ≤ r) (hS : 1 ≤ S0) (hBn : 1 ≤ B / c.W) (hK : 1 ≤ K)
    (hKe : K * (c.m * (E / c.m) - 1) ≤ e) (het : e - e % K + K ≤ t) (Z : ℕ)
    (hZ : zsz ((16 * (c.Wr * (nN (B / c.W) t S0 * r)) : ℕ) : ℤ) ≤ Z)
    (hZe : zsz ((e + t + K + c.m * (E / c.m) + E / c.m : ℕ) : ℤ) ≤ Z)
    (hZu : zsz ((6 * (E / c.m) + 6 : ℕ) : ℤ) ≤ Z)
    (w : Fin c.Wr) (k0 k1 : ℕ) (a : Fin c.m → ℕ) :
    RImplQ Isym tbl Q lo hi r (nN (B / c.W) t S0) (stH c.m K e (E / c.m) S0)
      ((RStep.phase w k0 k1 a : RStep (Fin c.Wr) c.m).den (1 : Op (Fin (E / c.m))))
      (phH c.Wr w.val k0 k1 (List.ofFn a)) 0 (0 + (0 + 2) * c.Wr)
      (cWrapQ c.Wr (nN (B / c.W) t S0 * r) Z 0 0
        (cPhStep Z (((k0 + k1 * (E / c.m)) % 4 : ℕ) : ℤ) (εTab vE vK vF wF (List.ofFn a))
          (B / c.W) t S0 r))

Context. Round six, item language (I3): the local steps of a node

A node on E bits (F = E / m) acts on W + T role streams of nN (B/W) t S₀ records, bits Fin m × Fin F at the positions IL3F.posR m K e F, strides stH. Parametric copies of the frozen KFWStep1/2/3/5 step lemmas (P8Lift.Wc → W + T, mC → m, mC^k → F):

• stepH_gate (atoms), stepH_perm (role permutation), stepH_phase (with epsOK_tabM, the m-generic epsOK_tab), stepH_fixG (a ±1 role diagonal as phase steps), stepH_row (from RowUCG, a row interface with a general coefficient aK K).

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).