Before the chunk store (round six, `cPre`)

Proved

J6Seg.PJ.Rn.cPre

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

complexity-theoryinteger-multiplicationkappa-improvement

Before the chunk store.

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

theorem J6Seg.PJ.Rn.cPre {pkA pkC bA bC kA kC wA wC pre post s t p α d W : ℕ} {c : Cs} (hcL : c cLC = [])
    {v : Vr} (hv : BV W v) (hP : ParV kA kC wA wC pre post s t p α d v)
    (bpk : pkA * segPF p d s + pkC ≤ 2 ^ W) (bb : bA * segPF p d s + bC ≤ 2 ^ W)
    (bl : pkA + pkC + bA + bC + 2 ≤ 2 ^ W) (blam : 2 * lamP d + 2 < 2 ^ W) :
    Rn (cPreP pkA pkC bA bC) v c (fun v' =>
      v' 5 = ((2 ^ Nat.clog 2 (lamP d) : ℕ) : ℤ) ∧ v' 6 = (Nat.clog 2 (lamP d) : ℤ) ∧
      v' 26 = ((pkA * segPF p d s + pkC : ℕ) : ℤ) ∧ v' 28 = ((bA * segPF p d s + bC : ℕ) : ℤ) ∧
      v' 29 = ((t / lamP d : ℕ) : ℤ) ∧
      (∀ j : Fin HS, j ≠ 5 → j ≠ 6 → j ≠ 26 → j ≠ 28 → j ≠ 29 → v' j = v j) ∧ BV W v')
      (update c J6Seg.PJ.sSt (((2 ^ Nat.clog 2 (lamP d) : ℕ) : ℤ) :: (Nat.clog 2 (lamP d) : ℤ) ::
        ((wA * segPF p d s + wC : ℕ) : ℤ) :: (post : ℤ) :: (pre : ℤ) :: c J6Seg.PJ.sSt))
      (cCPre pkA pkC bA bC W 0 (lamP d))

Context. B5 chunk side (eC), part 2: Rn.cPre

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.PJ
open IntMul NLogN NLogN.KIL NLogN.RS Function

Formal statement

theorem J6Seg.PJ.Rn.cPre {pkA pkC bA bC kA kC wA wC pre post s t p α d W : ℕ} {c : Cs} (hcL : c cLC = [])
    {v : Vr} (hv : BV W v) (hP : ParV kA kC wA wC pre post s t p α d v)
    (bpk : pkA * segPF p d s + pkC ≤ 2 ^ W) (bb : bA * segPF p d s + bC ≤ 2 ^ W)
    (bl : pkA + pkC + bA + bC + 2 ≤ 2 ^ W) (blam : 2 * lamP d + 2 < 2 ^ W) :
    Rn (cPreP pkA pkC bA bC) v c (fun v' =>
      v' 5 = ((2 ^ Nat.clog 2 (lamP d) : ℕ) : ℤ) ∧ v' 6 = (Nat.clog 2 (lamP d) : ℤ) ∧
      v' 26 = ((pkA * segPF p d s + pkC : ℕ) : ℤ) ∧ v' 28 = ((bA * segPF p d s + bC : ℕ) : ℤ) ∧
      v' 29 = ((t / lamP d : ℕ) : ℤ) ∧
      (∀ j : Fin HS, j ≠ 5 → j ≠ 6 → j ≠ 26 → j ≠ 28 → j ≠ 29 → v' j = v j) ∧ BV W v')
      (update c J6Seg.PJ.sSt (((2 ^ Nat.clog 2 (lamP d) : ℕ) : ℤ) :: (Nat.clog 2 (lamP d) : ℤ) ::
        ((wA * segPF p d s + wC : ℕ) : ℤ) :: (post : ℤ) :: (pre : ℤ) :: c J6Seg.PJ.sSt))
      (cCPre pkA pkC bA bC W 0 (lamP d)) := 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.PJ.Rn.cPre`, Solutions/J6SegILPreJC2.lean (lines 47–104) of the round-six development.

View graph