The body (round six, `cBodyH_le`)

Proved

IntMul.Kappa.R6.IL3H.cBodyH_le

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

complexity-theoryinteger-multiplicationkappa-improvement

The body.

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

theorem IntMul.Kappa.R6.IL3H.cBodyH_le {c : IntMul.Kappa.R6.IL3H.Cfg} (CB : ℕ → ℝ) {K S r H P D q0 qB Bp Z Zr Bz w : ℕ}
    (hS : 1 ≤ S) (hP : 1 ≤ P) (hB : Bz ≤ Zr) (hZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r)
    (hw : w + (dwCL c D q0 qB + 2) ≤ H) (hE : Etot c D q0 qB ≤ H)
    (hEZ : zsz ((Etot c D q0 qB : ℕ) : ℤ) ≤ Z)
    (hnp : Bp * 2 ^ (K * (D - q0)) * S ≤ 2 * (P * 2 ^ (K * D) * S)) :
    cBodyH c CB K S r H P D q0 qB Bp Z Zr Bz w ≤
      (q0 + qB) * ⌊CB 1 * ((P * 2 ^ (K * D) * S * Yu r Zr H : ℕ) : ℝ)⌋₊ +
      401 * ⌊CB (D - q0 - qB) * ((Bp * 2 ^ (K * (D - q0)) * S * Yu r Zr H : ℕ) : ℝ)⌋₊ +
      10000000000 * ((q0 + qB) * ((Sc c + 1) * Yu r Zr H)) +
      100000000000000 * ((Sc c + 1) * (P * 2 ^ (K * D) * S * Yu r Zr 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.cBodyH_le {c : IntMul.Kappa.R6.IL3H.Cfg} (CB : ℕ → ℝ) {K S r H P D q0 qB Bp Z Zr Bz w : ℕ}
    (hS : 1 ≤ S) (hP : 1 ≤ P) (hB : Bz ≤ Zr) (hZ : Z ≤ Zr) (hZr : Zr + 2 ≤ r)
    (hw : w + (dwCL c D q0 qB + 2) ≤ H) (hE : Etot c D q0 qB ≤ H)
    (hEZ : zsz ((Etot c D q0 qB : ℕ) : ℤ) ≤ Z)
    (hnp : Bp * 2 ^ (K * (D - q0)) * S ≤ 2 * (P * 2 ^ (K * D) * S)) :
    cBodyH c CB K S r H P D q0 qB Bp Z Zr Bz w ≤
      (q0 + qB) * ⌊CB 1 * ((P * 2 ^ (K * D) * S * Yu r Zr H : ℕ) : ℝ)⌋₊ +
      401 * ⌊CB (D - q0 - qB) * ((Bp * 2 ^ (K * (D - q0)) * S * Yu r Zr H : ℕ) : ℝ)⌋₊ +
      10000000000 * ((q0 + qB) * ((Sc c + 1) * Yu r Zr H)) +
      100000000000000 * ((Sc c + 1) * (P * 2 ^ (K * D) * S * Yu r Zr 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.cBodyH_le`, Solutions/R6IL3Top11.lean (lines 162–239) of the round-six development.

View graph