The copy `0 → rZ` (round six, `copyAx_ok`)

Proved

J6Seg.AxC.copyAx_ok

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

complexity-theoryinteger-multiplicationkappa-improvement

The copy 0 → rZ as a two-array step (g A _ = (A, A)).

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

theorem J6Seg.AxC.copyAx_ok {dA : Fin HS} (hA : DAok dA) (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k B w : ℕ)
    (hk : k ≤ D) (hB : DescB P n src D k B) (hw : w ≤ B) :
    Ax.Pass2OK Isym tbl (copyRS dA).code dA (descAx6 P n src D k)
      (fun A Bl => Bl = [] ∧ A.length = (List.ofFn (tD6 P n D)).prod ∧ GB w A)
      (fun A _ => (A, A)) (cCopy (2 * (List.ofFn (tD6 P n D)).prod) B)

Context. The axis program: the copy 0 → rZ (after pass 2) and the swap 0 ↔ rZ (before pass 7)

Both read the count 2·pre·t·post (the number of integers of an axis array) off the axis descriptor descAx6 = [k, pre, post, s, t, …] on dA (restored), on the scratch stacks 1 … 7.

cntRS dA: pushes 2·(pre·(t·post)) on CN = 5 (sp_cnt);
copyAx dA: gflat L ++ l on 0 and l₂ on rZ ↦ gflat L ++ l₂ on rZ, stack 0 unchanged (copyAx_runs);
swapAx dA: gflat A ++ l on 0, gflat B ++ l₂ on rZ ↦ gflat B ++ l on 0, gflat A ++ l₂ on rZ (swapAx_runs).

Convention (FineBody6): every stack other than 0, dA, rZ empty; dA ∉ {0, …, 7, 53}, dA < 56.

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_Defs67

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.AxC
open IntMul NLogN NLogN.KIL NLogN.KFB IntMul.Kappa.R6 Function
open J6Seg.Slab (rZ)
variable {Pp : ℕ} {Isym : List Sym} {tbl : Fin Pp → IStmt HS Pp}

Formal statement

theorem J6Seg.AxC.copyAx_ok {dA : Fin HS} (hA : DAok dA) (P : Prm) (n : ℕ) (src : ℕ → ℕ) (D k B w : ℕ)
    (hk : k ≤ D) (hB : DescB P n src D k B) (hw : w ≤ B) :
    Ax.Pass2OK Isym tbl (copyRS dA).code dA (descAx6 P n src D k)
      (fun A Bl => Bl = [] ∧ A.length = (List.ofFn (tD6 P n D)).prod ∧ GB w A)
      (fun A _ => (A, A)) (cCopy (2 * (List.ofFn (tD6 P n D)).prod) B) := 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.AxC.copyAx_ok`, Solutions/J6SegAxCopy.lean (lines 267–319) of the round-six development.

View graph