The chain (round six, `cChainH_le`)

Proved

IntMul.Kappa.R6.IL3H.cChainH_le

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

complexity-theoryinteger-multiplicationkappa-improvement

The chain.

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

theorem IntMul.Kappa.R6.IL3H.cChainH_le {c : IntMul.Kappa.R6.IL3H.Cfg} (CB : ℕ → ℝ) {cW P K D S r w Z Zr Bz : ℕ}
    (hS : 1 ≤ S) (hP : 1 ≤ P) (hB : Bz ≤ Zr) (hZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r)
    (hw : 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)
    (hE : Etot c D (chV c cW P K D S r w).q0 (chV c cW P K D S r w).qB ≤ (chV c cW P K D S r w).H)
    (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)
    (hnp : (chV c cW P K D S r w).Bp * 2 ^ (K * (D - (chV c cW P K D S r w).q0)) * S ≤
      2 * (P * 2 ^ (K * D) * S)) :
    cChainH c CB cW P K D S r w Z Zr Bz ≤
      ((chV c cW P K D S r w).q0 + (chV c cW P K D S r w).qB) *
        ⌊CB 1 * ((P * 2 ^ (K * D) * S * Yu r Zr (chV c cW P K D S r w).H : ℕ) : ℝ)⌋₊ +
      401 * ⌊CB (D - (chV c cW P K D S r w).q0 - (chV c cW P K D S r w).qB) *
        (((chV c cW P K D S r w).Bp * 2 ^ (K * (D - (chV c cW P K D S r w).q0)) * S *
          Yu r Zr (chV c cW P K D S r w).H : ℕ) : ℝ)⌋₊ +
      10000000000 * (((chV c cW P K D S r w).G +
        (chV c cW P K D S r w).d + (chV c cW P K D S r w).q0 + (chV c cW P K D S r w).qB) *
        ((Sc c + 1) * Yu r Zr (chV c cW P K D S r w).H)) +
      10000000000 * ((chV c cW P K D S r w).za * ((Sc c + 1) * (Zr + 3) ^ 2)) +
      1000000000000000 * ((Sc c + 1) * (P * 2 ^ (K * D) * S * Yu r Zr (chV c cW P K D S r w).H))

Context. Round six, item language (I3): the cost of the chain in units

With n = P 2^{K D} S, U = Yu r Zr H, X = (Sc c + 1) U, Y = (Sc c + 1) n U:

cChainH_le: `cChainH ≤ (q₀ + q_B) ⌊CB 1 · n U⌋ + 401 ⌊CB E · n' U⌋

10^10 (G + d + q₀ + q_B) X + 10^10 z_a (Sc+1)(Zr+3)^2 + 10^15 Y (E = D - q₀ - q_B, n' = B' 2^{K (D - q₀)} S ≤ 2 n`).

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_Defs23

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL3H
open IntMul AModel NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFG NLogN.KFH NLogN.KFN NLogN.KFW Complex P8Lift Butterfly IntMul.Kappa.R6.Cx

Formal statement

theorem IntMul.Kappa.R6.IL3H.cChainH_le {c : IntMul.Kappa.R6.IL3H.Cfg} (CB : ℕ → ℝ) {cW P K D S r w Z Zr Bz : ℕ}
    (hS : 1 ≤ S) (hP : 1 ≤ P) (hB : Bz ≤ Zr) (hZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r)
    (hw : 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)
    (hE : Etot c D (chV c cW P K D S r w).q0 (chV c cW P K D S r w).qB ≤ (chV c cW P K D S r w).H)
    (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)
    (hnp : (chV c cW P K D S r w).Bp * 2 ^ (K * (D - (chV c cW P K D S r w).q0)) * S ≤
      2 * (P * 2 ^ (K * D) * S)) :
    cChainH c CB cW P K D S r w Z Zr Bz ≤
      ((chV c cW P K D S r w).q0 + (chV c cW P K D S r w).qB) *
        ⌊CB 1 * ((P * 2 ^ (K * D) * S * Yu r Zr (chV c cW P K D S r w).H : ℕ) : ℝ)⌋₊ +
      401 * ⌊CB (D - (chV c cW P K D S r w).q0 - (chV c cW P K D S r w).qB) *
        (((chV c cW P K D S r w).Bp * 2 ^ (K * (D - (chV c cW P K D S r w).q0)) * S *
          Yu r Zr (chV c cW P K D S r w).H : ℕ) : ℝ)⌋₊ +
      10000000000 * (((chV c cW P K D S r w).G +
        (chV c cW P K D S r w).d + (chV c cW P K D S r w).q0 + (chV c cW P K D S r w).qB) *
        ((Sc c + 1) * Yu r Zr (chV c cW P K D S r w).H)) +
      10000000000 * ((chV c cW P K D S r w).za * ((Sc c + 1) * (Zr + 3) ^ 2)) +
      1000000000000000 * ((Sc c + 1) * (P * 2 ^ (K * D) * S * Yu r Zr (chV c cW P K D S r w).H)) := 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 `IntMul.Kappa.R6.IL3H.cChainH_le`, Solutions/R6IL3Top11.lean (lines 245–341) of the round-six development.

View graph