Round-six lemma `phaseK`

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.ATab.Rn.phaseK {W p s t α pkA pkC bA bC : ℕ} {v8 : Vr} {c1 : Cs}
    (hv : V2 p s t α (pkA * p + pkC) (bA * p + bC) v8) (hBv : BV W v8)
    (hB : PBnd W p t α pkA pkC bA bC)
    (hrW : 2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) < 2 ^ W) (hc : c1 cLC = []) :
    Rn J6Seg.ATab.phaseK v8 c1
      (fun v' => LV p s t α (pkA * p + pkC) (bA * p + bC) v' ∧ v' 10 = ncA p t α ∧ BV W v') c1
      (cPhaseK W (4 * J6A.WA p α (HAx p α) + 4 * HAx p α))

Context. A lines, table set-up, part 8: the parameter phase (run)

Rn.phase: from the registers of parA the phase pushes the kerRegs values onto 45 and |T| onto 42 and leaves the loop registers LV with 10 = nc.

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*).