The field-width loop (round six, `gloopQ`)

The field-width loop.

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

theorem IntMul.Kappa.R6.IL3H.gloopQ {cz : ℕ} (hcz : 1 ≤ cz) {jG : Fin Pp} {cont : IStmt HS Pp}
    (hj : tbl jG = gloopC cz jG cont) {P K D S ρ r w Z Mb Bz : ℕ} (hMb : zsz (Mb : ℤ) ≤ Bz)
    (hM : 2 * gBnd cz Z + Gv cz Z + 2 ≤ Mb)
    {f g : Fin HS → List ℤ} (hf : Clean0 f) (hg : Clean0 g) {cc : ℕ}
    (Cont : ∀ σ, DescR σ P K D S ρ r w → σ vG = some (Z : ℤ) → σ 11 = some (Gv cz Z : ℤ) →
      RunQ Isym tbl σ cont f g cc) :
    ∀ n σ, (DescR σ P K D S ρ r w ∧ σ vG = some (Z : ℤ) ∧ ∃ j : ℕ, σ 11 = some (j : ℤ) ∧
      σ 12 = some ((2 ^ j : ℕ) : ℤ) ∧ j + n = Gv cz Z) →
      RunQ Isym tbl σ (.call jG) f g (cc + (n + 1) * cLoopS 15 2 Bz)

Context. Round six, item language (I3): the entry loops of the uniform Proposition 14

• loopQ: a generic continuation-passing loop (testC 16 cond (push step; call j) cont) from an invariant indexed by the number of remaining iterations.
• gloopC cz: with Z on vG = 24, finds G = clog₂ (4 (Z + cz) (Z + cz + 2)) on 11 (gloopQ; the compact-controls field width).
• dloopC c: with D on 22, finds d = dep m D on 12 and W^d on 13 (dloopQ).

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