The size loop (round six, `zloopQ`)

The size loop.

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

theorem IntMul.Kappa.R6.IL3H.zloopQ {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) {jZ : Fin Pp} {cont : IStmt HS Pp}
    (hj : tbl jZ = zloopC c jZ cont) {P K D S ρ r w Mb Bz : ℕ} (hP : 1 ≤ P)
    (hS : 1 ≤ S) (hr : 1 ≤ r) (hMb : zsz (Mb : ℤ) ≤ Bz)
    (hM : 2 * aV c P S r w D + c.Aw * (D + 1) ^ c.p + (D + 1) ^ c.p + 2 * c.m + 10 ≤ Mb)
    {f g : Fin HS → List ℤ} (hf : Clean0 f) (hg : Clean0 g) {cc : ℕ}
    (Cont : ∀ σ, DescR σ P K D S ρ r w → σ 11 = some (Nat.size (aV c P S r w D) : ℤ) →
      RunQ Isym tbl σ cont f g cc) :
    ∀ n σ, (DescR σ P K D S ρ r w ∧ ∃ j : ℕ, σ 11 = some (j : ℤ) ∧
      σ 12 = some ((2 ^ j : ℕ) : ℤ) ∧ j + n = Nat.size (aV c P S r w D)) →
      RunQ Isym tbl σ (.call jZ) f g (cc + (n + 1) * cLoopS (szZ c) 2 Bz)

Context. Round six, item language (I3): the local size loop of the uniform Proposition 14

zloopC c jZ cont: with the descriptor registers, finds j = Nat.size a on 11 (2^j on 12; zloopQ), where a = 32 W' P S r + w + EwH D. The local size bound is then Zl = j + K D, so zsz (32 W' P 2^{K D} S r) ≤ Zl and H + 1 < 2^{Zl} for H = w + EwH D (zl_spec). The field width G is computed from Zl (not from the caller's Z), so the per-row factor is ≈ log of the size of the array and of the width bound.

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