Round-six lemma `jreal`

Proved

J6Seg.Side.jreal

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem J6Seg.Side.jreal {T u w1 mS K3 Bc2 B2 d p l Nc Ln C1 W2 W3 bc : ℝ}
    (hu : u = mS + 2 * 10 ^ 5 * K3 + 10 ^ 8 * Bc2 ^ 2) (hT : 0 ≤ T) (hw1 : 0 ≤ w1)
    (hmS : 0 ≤ mS) (r1 : w1 ≤ 15 * d) (r2 : w1 * Bc2 ^ 2 ≤ 30 * (10 + bc) ^ 2 * (p * l))
    (r3 : w1 * K3 ≤ 15 * (3 * W2 + 12) * (d * p)) (r4 : B2 * w1 ≤ 15 * W3 * (d * p))
    (r5 : mS ≤ 32500 * C1 * p * Ln ^ 2) (hdN : d ≤ Nc) (hlN : l ≤ Nc) (hL2 : 1 ≤ Ln ^ 2)
    (hp : 0 ≤ p) (hd : 0 ≤ d) (hC1 : 0 ≤ C1) (hW2 : 0 ≤ W2) (hW3 : 0 ≤ W3) (hbc : 0 ≤ bc)
    (hl : 0 ≤ l) :
    T * (400000 * w1 * u + 40000000000 * B2 * w1) ≤
      (4 * 10 ^ 5 * (487500 * C1 + 3 * 10 ^ 6 * (3 * W2 + 12) + 3 * 10 ^ 9 * (10 + bc) ^ 2) +
        6 * 10 ^ 11 * W3) * (T * p * Nc * Ln ^ 2)

Context. J cost 6: jBudget6_all

With W2 = 3 kA + kC, W3 = W + W2 + bcC + 16, C1 = Cfm (W2+10)(W2+x+14)², the J pass costs ≤ KJ · cU6 P n 2 / (D+1), KJ = 4·10^5 (487500 C1 + 3·10^6 (3 W2 + 12) + 3·10^9 (10+bcC)²) + 6·10^11 W3.

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel
import Definitions.Def_IntMul_HvdH_Numeric
import Definitions.Def_IntMul_HvdH_ExpApprox
import Definitions.Def_IntMul_HvdH_RealExp
import Definitions.Def_IntMul_HvdH_MachineRef
import Definitions.Def_IntMul_HvdH_Twiddle
import Definitions.Def_IntMul_HvdH_SApprox
import Definitions.Def_IntMul_HvdH_DiagApprox
import Definitions.Def_IntMul_HvdH_EApprox
import Definitions.Def_IntMul_HvdH_JApprox
import Definitions.Def_IntMul_HvdH_BApprox
import Definitions.Def_IntMul_HvdH_FPApprox
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_KappaJainData

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open Finset
open IntMul NLogN NLogN.KIL IntMul.Kappa.R6

Formal statement

theorem J6Seg.Side.jreal {T u w1 mS K3 Bc2 B2 d p l Nc Ln C1 W2 W3 bc : ℝ}
    (hu : u = mS + 2 * 10 ^ 5 * K3 + 10 ^ 8 * Bc2 ^ 2) (hT : 0 ≤ T) (hw1 : 0 ≤ w1)
    (hmS : 0 ≤ mS) (r1 : w1 ≤ 15 * d) (r2 : w1 * Bc2 ^ 2 ≤ 30 * (10 + bc) ^ 2 * (p * l))
    (r3 : w1 * K3 ≤ 15 * (3 * W2 + 12) * (d * p)) (r4 : B2 * w1 ≤ 15 * W3 * (d * p))
    (r5 : mS ≤ 32500 * C1 * p * Ln ^ 2) (hdN : d ≤ Nc) (hlN : l ≤ Nc) (hL2 : 1 ≤ Ln ^ 2)
    (hp : 0 ≤ p) (hd : 0 ≤ d) (hC1 : 0 ≤ C1) (hW2 : 0 ≤ W2) (hW3 : 0 ≤ W3) (hbc : 0 ≤ bc)
    (hl : 0 ≤ l) :
    T * (400000 * w1 * u + 40000000000 * B2 * w1) ≤
      (4 * 10 ^ 5 * (487500 * C1 + 3 * 10 ^ 6 * (3 * W2 + 12) + 3 * 10 ^ 9 * (10 + bc) ^ 2) +
        6 * 10 ^ 11 * W3) * (T * p * Nc * Ln ^ 2) := 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.Side.jreal`, Solutions/J6SegJCost6.lean (lines 42–83) of the round-six development.

View graph