Round-six lemma `xorBody_fsp`

Proved

NLogN.KFL.xorBody_fsp

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

theorem NLogN.KFL.xorBody_fsp {d Q j : ℕ} (hd : 0 < d) (hQ : 0 < Q) {Bb : ℕ} (hB2 : 2 ≤ Bb)
    (zd : zsz (d : ℤ) ≤ Bb) (zQ : zsz (Q : ℤ) ≤ Bb) (zr : zsz ((2 : ℤ) ^ j) ≤ Bb)
    (s : IState HS) (G : Fin HS → List ℤ) (N : ℕ) (hN : 1 ≤ N) (zN : zsz (N : ℤ) ≤ Bb)
    {LP : List ℤ} (hGq : G rP = (N : ℤ) :: LP) :
    FSp (xorBody d Q j) (encK s G)
      (encK s (Function.update (Function.update G 14 ((xorA d Q j (N - 1) : ℤ) :: G 14)) rP
        (((N : ℤ) - 1) :: LP))) (20 * 10 ^ 7 * (Bb + 2) ^ 2)

Context. KFL §8: the last selected bit (two-bit XOR)

xorStep: table b(c₀) = bit j of c₀ (j = ρ + (f-1)K, xorGen), then rotF on the view [N0·Q·N1·E, 2, D·S1] (D = 2^j, Q = 2 D E): the bit j of the y chunk is flipped iff bit j of x is set. xorStep_geo: the result is rixT g (XLc K ρ f).

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
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFL
open IntMul NLogN.RS NLogN.KIL NLogN.KFD Butterfly AModel

Formal statement

theorem NLogN.KFL.xorBody_fsp {d Q j : ℕ} (hd : 0 < d) (hQ : 0 < Q) {Bb : ℕ} (hB2 : 2 ≤ Bb)
    (zd : zsz (d : ℤ) ≤ Bb) (zQ : zsz (Q : ℤ) ≤ Bb) (zr : zsz ((2 : ℤ) ^ j) ≤ Bb)
    (s : IState HS) (G : Fin HS → List ℤ) (N : ℕ) (hN : 1 ≤ N) (zN : zsz (N : ℤ) ≤ Bb)
    {LP : List ℤ} (hGq : G rP = (N : ℤ) :: LP) :
    FSp (xorBody d Q j) (encK s G)
      (encK s (Function.update (Function.update G 14 ((xorA d Q j (N - 1) : ℤ) :: G 14)) rP
        (((N : ℤ) - 1) :: LP))) (20 * 10 ^ 7 * (Bb + 2) ^ 2) := 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.KFL.xorBody_fsp`, Solutions/KFLXor.lean (lines 38–82) of the round-six development.

View graph