The chain (round six, `chainQH`)

The chain.

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

theorem IntMul.Kappa.R6.IL3H.chainQH {c : IntMul.Kappa.R6.IL3H.Cfg} (hc : CfgOK c) (cW : ℕ) (hWc : c.W ≤ 2 ^ cW)
    (jZ jG jD jK jL : Fin Pp) (rowC : IStmt HS Pp)
    (hZt : tbl jZ = zloopC c jZ (zcontC jG)) (hGt : tbl jG = gloopC czH jG (gcontC jD))
    (hDt : tbl jD = dloopC c.m c.W jD (coreCH c cW (bodyCH c jK jL)))
    (hK : tbl jK = kerLoopC jK jL) (hL : tbl jL = levCH c jL rowC)
    {K r Z Zr P D S ρ w Bz : ℕ} {CB : ℕ → ℝ}
    (L1 : LvH c Isym tbl jL rowC K r (chV c cW P K D S r w).Zl Zr (chV c cW P K D S r w).H
      (chV c cW P K D S r w).G CB 1)
    (hρ : ρ < K) (hK1 : 1 ≤ K) (hS : 1 ≤ S) (hP : 1 ≤ P) (hr : 1 ≤ r) (hD : 1 ≤ D)
    (hKW : cW * (chV c cW P K D S r w).d + 2 * (D / c.m * (chV c cW P K D S r w).G) ≤ K * D)
    (hGm : (chV c cW P K D S r w).G + c.m ≤ P * 2 ^ (K * D) * S * r)
    (hZ32 : zsz ((32 * (P * 2 ^ (K * D) * S * r) : ℕ) : ℤ) ≤ Z)
    (hHZ : zsz ((chV c cW P K D S r w).H : ℤ) ≤ Z)
    (hV1 : zsz ((VbH c K (K * D) S r (chV c cW P K D S r w).H 1 (ρ + K * (D - 1)) P : ℕ) : ℤ) ≤ Zr)
    (hMb : zsz ((MbChain c cW P K D S r w : ℕ) : ℤ) ≤ Bz)
    (pre : (chV c cW P K D S r w).q0 + (chV c cW P K D S r w).qB < D →
      MidPre c Isym tbl jL rowC CB K S r (chV c cW P K D S r w).H P D ρ (chV c cW P K D S r w).q0
        (chV c cW P K D S r w).Bp (chV c cW P K D S r w).qB (chV c cW P K D S r w).Zl Z Zr
        (chV c cW P K D S r w).G)
    (hEZ : zsz ((Etot c D (chV c cW P K D S r w).q0 (chV c cW P K D S r w).qB : ℕ) : ℤ) ≤ Z)
    {σ : Fin HS → Option ℤ} (hd : DescR σ P K D S ρ r w)
    (f : Fin HS → List ℤ) (zs : List GI) (l : List ℤ) (xs : List (Fin r → ℂ)) (p : ℕ)
    (hC0 : Clean0 f) (h0 : f 0 = gflat zs ++ l) (hx : RecRep r p zs xs)
    (hl : xs.length = vol (Butterfly.layerShape P K D S)) (hb : GB w zs)
    (hH : w + (dwCL c D (chV c cW P K D S r w).q0 (chV c cW P K D S r w).qB + 2) ≤
      (chV c cW P K D S r w).H)
    (hdisk : ∀ j (h : j < xs.length), ‖xs[j]‖ ≤ 1)
    (hex : ∃ zs', RecRep r p zs' (Butterfly.prop14Proc (P := P) (S := S) hρ p
        (Butterfly.tens Butterfly.Cm : Butterfly.Op (Fin D)) xs)) :
    RunQ Isym tbl σ (mainCH jZ) f (Function.update f 0 (gflat (Classical.choose hex) ++ l))
      (cChainH c CB cW P K D S r w Z Zr Bz)

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

From the descriptor registers (DescR), mainCH jZ runs

• the size loop (zloopC, j = size (32 W' P S r)), then pushes Zl = j + K D on vG;
• the field-width loop (gloopC, G = clog₂ (4 (Zl + cz)(Zl + cz + 2))), then pushes G on vG;
• the depth loop (dloopC, d = dep m D, W^d);
• the core stage (coreCH) and the layer body (bodyCH).

chainQH: the run leaves gflat zs* ++ l on stack 0.

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