Round-six lemma `fdiv_recip`

Proved

J6Seg.JK.fdiv_recip

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.J6SegILJKer1):

theorem J6Seg.JK.fdiv_recip (P k : ℕ) (a pv : ℤ) (hpv : 0 < pv) (hN : |2 * (a * 2 ^ P) + pv| < 2 ^ k) :
    (2 * (a * 2 ^ P) + pv) * ivOf k pv / 2 ^ k +
      corr (2 * (a * 2 ^ P) + pv - (2 * (a * 2 ^ P) + pv) * ivOf k pv / 2 ^ k * (2 * pv))
        (2 * pv) = J6Seg.fdiv P a pv

Context. B-line IL, the J kernel (B4), part 1: list model and arithmetic

The J kernel jKer (J6SegSw3) of a padded G-row v is

jKer v = W ++ 0^{G-m}, W_r = dotF (cc_r) ((zext K z).drop r), z = bwdK bs (fwdK fs (v.take m) []) [] []

for the coefficient streams fs = fsOf …, bs = bsOf …, cc_r = ccL … r. This file gives

the generic kernel jKerG P K G m fs bs cc v (any streams) and the step forms of fwdK (fA_succ), bwdK (bwdS_succ) and dotF on prefixes (dotF_take_succ);
the arithmetic of the IL: ediv_of_tdiv (floor division from tdiv/tmod), rs_eq (rs P x = ⌊(2x + 2^P) / 2^{P+1}⌋) and fdiv_recip: with |2 a 2^P + pv| < 2^k and pv > 0, fdiv P a pv is q₀ + δ where q₀ = ⌊N iv / 2^k⌋ (iv = ivOf k pv = ⌊2^k / 2pv⌋) and the correction δ ∈ {-1,0,1} is read off the signs of N - q₀ D and N - q₀ D - D (N = 2 a 2^P + pv, D = 2 pv): two multiplications instead of a long division.

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_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.JK
open Finset

Formal statement

theorem J6Seg.JK.fdiv_recip (P k : ℕ) (a pv : ℤ) (hpv : 0 < pv) (hN : |2 * (a * 2 ^ P) + pv| < 2 ^ k) :
    (2 * (a * 2 ^ P) + pv) * ivOf k pv / 2 ^ k +
      corr (2 * (a * 2 ^ P) + pv - (2 * (a * 2 ^ P) + pv) * ivOf k pv / 2 ^ k * (2 * pv))
        (2 * pv) = J6Seg.fdiv P a pv := 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.JK.fdiv_recip`, Solutions/J6SegILJKer1.lean (lines 56–129) of the round-six development.

View graph