Round-six lemma `LRep_rgp`

Proved

J6A.LRep_rgp

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

theorem J6A.LRep_rgp {K M w post pre : ℕ} (hK : 0 < K) (hM : 0 < M) (hw : 0 < w) (hp : 0 < post)
    {L : List α} {φ : ℕ → ℕ → List α} (hL : LRep pre (K * (M * w)) post L φ) :
    LRep (pre * (M * K)) w post (rgp K M w post pre L)
      (fun b' c => (((φ (b' / (M * K)) c).drop ((b' % K * M + b' % (M * K) / K) * w)).take w))

Context. A lines, IL side 2: copies and regrouping of line representations

dupL K L: K copies of L concatenated (what the IL duplication leaves on stack 0);
LRep_cpy: K = 2^f copies of a (pre, n, post) array, followed by the two fine exposures (1, K, N) → (1, N, K) and (pre, n·post, K) → (pre, K, n·post), are the (pre, K·n, post) array whose lines are K copies of the old lines;
LRep_rgp: a (pre, K·M·w, post) array (K = 2^f classes of M windows of length w), after the exposures (pre, K, M·w·post) → (pre, M·w·post, K) and (pre·M, w·post, K) → (pre·M, K, w·post), is the (pre·(M·K), w, post) array whose row b·(M K) + j K + r is window j of class r of line b.

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_Defs62

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6A
open IntMul.HvdH IntMul.HvdH.Ref
open J6Seg
variable {α : Type*} [Inhabited α]

Formal statement

theorem J6A.LRep_rgp {K M w post pre : ℕ} (hK : 0 < K) (hM : 0 < M) (hw : 0 < w) (hp : 0 < post)
    {L : List α} {φ : ℕ → ℕ → List α} (hL : LRep pre (K * (M * w)) post L φ) :
    LRep (pre * (M * K)) w post (rgp K M w post pre L)
      (fun b' c => (((φ (b' / (M * K)) c).drop ((b' % K * M + b' % (M * K) / K) * w)).take w)) := 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 `J6A.LRep_rgp`, Solutions/J6AIL2.lean (lines 82–142) of the round-six development.

View graph