The output-scaling loop (round six, `loopC`)

Proved

J6Seg.ATab.Rn.loopC

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

complexity-theoryinteger-multiplicationkappa-improvement

The output-scaling loop.

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

theorem J6Seg.ATab.Rn.loopC {W p s t α : ℕ} {v0 : Vr} {c0 : Cs} (hv0 : BV W v0) (hc0 : c0 cI = [])
    (h1 : v0 1 = ((2 * p : ℕ) : ℤ)) (h2 : v0 2 = ((p / 2 : ℕ) : ℤ)) (h3 : v0 3 = s)
    (h4 : v0 4 = t) (h5 : v0 5 = 2 ^ (2 * p)) (h6 : v0 6 = betaT (2 * p) α)
    (h8 : v0 8 = HAx p α) (h10 : v0 10 = ((2 * HAx p α : ℕ) : ℤ))
    (h11 : v0 11 = ((t ^ 2 * α ^ 2 : ℕ) : ℤ))
    (hpW : 2 * p ≤ W + 1) (hpW' : 2 * p < 2 ^ W) (hN : 2 * HAx p α < 2 ^ W)
    (hK : t ^ 2 * α ^ 2 < 2 ^ W)
    (hb1 : ∀ κ < 2 * HAx p α, cNumA s t (HAx p α) κ < 2 ^ W)
    (hb2 : ∀ κ < 2 * HAx p α, |expPos (2 * p) (t ^ 2 * α ^ 2) (cNumA s t (HAx p α) κ) (p / 2) *
      betaT (2 * p) α| < 2 ^ W)
    (hb3 : ∀ κ < 2 * HAx p α, |expPos (2 * p) (t ^ 2 * α ^ 2) (cNumA s t (HAx p α) κ) (p / 2)| <
      2 ^ W) :
    Rn J6Seg.ATab.loopC v0 c0 (fun v' => (∀ j, j ∉ ([26, 28, 29] : List (Fin HS)) → v' j = v0 j) ∧ BV W v')
      (update c0 sS (PreT.rv (fC p s t α) (2 * HAx p α) ++ c0 sS))
      (cFor W (2 * HAx p α) (cBodyC 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.loopC {W p s t α : ℕ} {v0 : Vr} {c0 : Cs} (hv0 : BV W v0) (hc0 : c0 cI = [])
    (h1 : v0 1 = ((2 * p : ℕ) : ℤ)) (h2 : v0 2 = ((p / 2 : ℕ) : ℤ)) (h3 : v0 3 = s)
    (h4 : v0 4 = t) (h5 : v0 5 = 2 ^ (2 * p)) (h6 : v0 6 = betaT (2 * p) α)
    (h8 : v0 8 = HAx p α) (h10 : v0 10 = ((2 * HAx p α : ℕ) : ℤ))
    (h11 : v0 11 = ((t ^ 2 * α ^ 2 : ℕ) : ℤ))
    (hpW : 2 * p ≤ W + 1) (hpW' : 2 * p < 2 ^ W) (hN : 2 * HAx p α < 2 ^ W)
    (hK : t ^ 2 * α ^ 2 < 2 ^ W)
    (hb1 : ∀ κ < 2 * HAx p α, cNumA s t (HAx p α) κ < 2 ^ W)
    (hb2 : ∀ κ < 2 * HAx p α, |expPos (2 * p) (t ^ 2 * α ^ 2) (cNumA s t (HAx p α) κ) (p / 2) *
      betaT (2 * p) α| < 2 ^ W)
    (hb3 : ∀ κ < 2 * HAx p α, |expPos (2 * p) (t ^ 2 * α ^ 2) (cNumA s t (HAx p α) κ) (p / 2)| <
      2 ^ W) :
    Rn J6Seg.ATab.loopC v0 c0 (fun v' => (∀ j, j ∉ ([26, 28, 29] : List (Fin HS)) → v' j = v0 j) ∧ BV W v')
      (update c0 sS (PreT.rv (fC p s t α) (2 * HAx p α) ++ c0 sS))
      (cFor W (2 * HAx p α) (cBodyC 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.loopC`, Solutions/J6AILTab3.lean (lines 145–225) of the round-six development.

View graph