Round-six lemma `take`

Proved

NLogN.Runs.take

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 NLogN.Take):

theorem NLogN.Runs.take {q a b d e : Fin S} (hqa : q ≠ a) (hqb : q ≠ b) (hqd : q ≠ d) (hqe : q ≠ e)
    (hab : a ≠ b) (had : a ≠ d) (hae : a ≠ e) (hbd : b ≠ d) (hbe : b ≠ e) (hde : d ≠ e)
    (σ : St S) (A Bw : List Bool) (ra rb : List Sym)
    (hA : σ.stk a = A.map codeBit ++ ra) (hB : σ.stk b = Bw.map codeBit ++ rb)
    (hra : bitOf ra.head? = none) (hrb : bitOf rb.head? = none) :
    Runs I prog (NLogN.take q a b d e : Stmt S P) σ
      ((((σ.set a ((A.drop Bw.length).map codeBit ++ ra)).set b rb).set d
        (((A.take Bw.length).map codeBit).reverse ++ σ.stk d)).set e
        ((Bw.map codeBit).reverse ++ σ.stk e)) (takeCost Bw.length)

Context. Lockstep transfer: take

While the top of b is a bit, pop it and push it on e; at the same time, if the top of a is a bit, move it to d. So |Bw| bits are taken from a, where Bw is the bit word on 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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN
variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

Formal statement

theorem NLogN.Runs.take {q a b d e : Fin S} (hqa : q ≠ a) (hqb : q ≠ b) (hqd : q ≠ d) (hqe : q ≠ e)
    (hab : a ≠ b) (had : a ≠ d) (hae : a ≠ e) (hbd : b ≠ d) (hbe : b ≠ e) (hde : d ≠ e)
    (σ : St S) (A Bw : List Bool) (ra rb : List Sym)
    (hA : σ.stk a = A.map codeBit ++ ra) (hB : σ.stk b = Bw.map codeBit ++ rb)
    (hra : bitOf ra.head? = none) (hrb : bitOf rb.head? = none) :
    Runs I prog (NLogN.take q a b d e : Stmt S P) σ
      ((((σ.set a ((A.drop Bw.length).map codeBit ++ ra)).set b rb).set d
        (((A.take Bw.length).map codeBit).reverse ++ σ.stk d)).set e
        ((Bw.map codeBit).reverse ++ σ.stk e)) (takeCost Bw.length) := 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 `NLogN.Runs.take`, Solutions/Take.lean (lines 42–150) of the round-six development.

View graph