The correlation loop (round six, `loopR`)

Proved

J6Seg.ATab.Rn.loopR

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

The correlation loop.

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

theorem J6Seg.ATab.Rn.loopR {W p s t α H q : ℕ} {v0 : Vr} {c0 : Cs} (hv0 : BV W v0) (hc0 : c0 cI = [])
    (h1 : v0 1 = ((2 * p : ℕ) : ℤ)) (h3 : v0 3 = s) (h4 : v0 4 = t)
    (h7 : v0 7 = ((t ^ 3 * α ^ 2 : ℕ) : ℤ)) (h8 : v0 8 = H) (h9 : v0 9 = J6A.WA p α H)
    (h10 : v0 10 = ((2 * J6A.WA p α H + 2 * H : ℕ) : ℤ))
    (h12 : v0 12 = 2 ^ J6A.QA p)
    (h25 : v0 25 = (t : ℤ) * (J6A.jcB s t H (J6A.kkA H q) - J6A.WA p α H) -
      s * J6A.kcB H (J6A.kkA H q))
    (hpW : 2 * p ≤ W + 1) (hN : 2 * J6A.WA p α H + 2 * H < 2 ^ W)
    (hb1 : ∀ e < 2 * J6A.WA p α H + 2 * H, (rNum p s t α H q e : ℤ) ≤ 2 ^ W)
    (hb2 : ∀ e < 2 * J6A.WA p α H + 2 * H, |fR p s t α H q e| ≤ 2 ^ W) :
    Rn J6Seg.ATab.loopR v0 c0 (fun v' => (∀ j, j ∉ ([26, 28, 29] : List (Fin HS)) → v' j = v0 j) ∧ BV W v')
      (update c0 sS (PreT.rv (fR p s t α H q) (2 * J6A.WA p α H + 2 * H) ++ c0 sS))
      (cFor W (2 * J6A.WA p α H + 2 * H) (cBodyR W))

Context. A lines, table set-up, part 3: the correlation and output-scaling table loops

loopR: for e < 2W + 2H: 28 := s (A0 + t(2W+H) - t e)²; 29 := expNeg 2p (t³α²) 28; push 2^Q · 29, i.e. it pushes rTabA … q (Rn.loopR);
loopC: for κ < 2H: 28 := s (t-s)⁺ (κ - H)²; 29 := expPos 2p (t²α²) 28 (p/2); 29 := 29 · β; push tdiv 29 2^(2p), i.e. it pushes cTabA … q (Rn.loopC).

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

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs69

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.ATab
open IntMul NLogN NLogN.KIL NLogN.RS J6Seg.PJ IntMul.HvdH Function

Formal statement

theorem J6Seg.ATab.Rn.loopR {W p s t α H q : ℕ} {v0 : Vr} {c0 : Cs} (hv0 : BV W v0) (hc0 : c0 cI = [])
    (h1 : v0 1 = ((2 * p : ℕ) : ℤ)) (h3 : v0 3 = s) (h4 : v0 4 = t)
    (h7 : v0 7 = ((t ^ 3 * α ^ 2 : ℕ) : ℤ)) (h8 : v0 8 = H) (h9 : v0 9 = J6A.WA p α H)
    (h10 : v0 10 = ((2 * J6A.WA p α H + 2 * H : ℕ) : ℤ))
    (h12 : v0 12 = 2 ^ J6A.QA p)
    (h25 : v0 25 = (t : ℤ) * (J6A.jcB s t H (J6A.kkA H q) - J6A.WA p α H) -
      s * J6A.kcB H (J6A.kkA H q))
    (hpW : 2 * p ≤ W + 1) (hN : 2 * J6A.WA p α H + 2 * H < 2 ^ W)
    (hb1 : ∀ e < 2 * J6A.WA p α H + 2 * H, (rNum p s t α H q e : ℤ) ≤ 2 ^ W)
    (hb2 : ∀ e < 2 * J6A.WA p α H + 2 * H, |fR p s t α H q e| ≤ 2 ^ W) :
    Rn J6Seg.ATab.loopR v0 c0 (fun v' => (∀ j, j ∉ ([26, 28, 29] : List (Fin HS)) → v' j = v0 j) ∧ BV W v')
      (update c0 sS (PreT.rv (fR p s t α H q) (2 * J6A.WA p α H + 2 * H) ++ c0 sS))
      (cFor W (2 * J6A.WA p α H + 2 * H) (cBodyR W)) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `J6Seg.ATab.Rn.loopR`, Solutions/J6AILTab3.lean (lines 44–108) of the round-six development.

View graph