Updating the `n` segments of a slot `y < 2^L` (`ρ + n K ≤ L`) by `δ_s` without carries (`slot_add`)

Proved

IntMul.Kappa.R6.IL2C.slot_add

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

complexity-theoryinteger-multiplicationkappa-improvement

Updating the n segments of a slot y < 2^L (ρ + n K ≤ L) by δ_s without carries.

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

theorem IntMul.Kappa.R6.IL2C.slot_add (hK : 1 ≤ K) (hL : ρ + n * K ≤ L) {y : ℕ} (hy : y < 2 ^ L) (δ : ℕ → ℤ)
    (h : ∀ s < n, 0 ≤ (IntMul.Kappa.R6.IL2C.seg K ρ s y : ℤ) + δ s ∧ (IntMul.Kappa.R6.IL2C.seg K ρ s y : ℤ) + δ s < 2 ^ K) :
    ∃ y' : ℕ, (y' : ℤ) = y + ∑ s ∈ range n, δ s * ((2 : ℤ) ^ ρ * (2 ^ K) ^ s) ∧ y' < 2 ^ L ∧
      y' % 2 ^ ρ = y % 2 ^ ρ ∧ (∀ s < n, (IntMul.Kappa.R6.IL2C.seg K ρ s y' : ℤ) = IntMul.Kappa.R6.IL2C.seg K ρ s y + δ s) ∧
      y' / 2 ^ ρ / (2 ^ K) ^ n = y / 2 ^ ρ / (2 ^ K) ^ n

Context. Round six, compact controls (I2C): the value-level mechanism

Colkitt's compact dirty controls, uniform variant (see jain6/compact/DESIGN.md). The state of one record is (t, u, y) (the temporary T, the control U, the target slot Y); the source slot x is a parameter. Radices: W = 2^K (slot segments), R = 2^G (compact digits); n low selected positions j_s = ρ + s K.

dgt W s x = x / W^s % W; digits_add: digit-wise addition without carries; eq_of_digits: equal low digits and equal high part give equal numbers.
segSum tf ru rv rw w0 u v n = Σ_{s<n} w0 rw^s tf (u / ru^s) (v / rv^s) (the register loop).
The offsets oA (Y += Σ 2 z_s t_s 2^{j_s}), oB (Y += Σ z_s (1 - 2 t_s) 2^{j_s}), oS (packed selected bits), oC (Σ (y_s xor z_s) R^s), oT (the ideal toggle).
The pull maps rT, rU, rY, the inverse phase phInv and the whole pull composite Psi.
Psi_good: on a good state Psi is the ideal map (toggle the n low selected bits of y by those of x); Psi_bij-type facts are proved at rank level.

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_Defs20

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C
open Finset
variable {K ρ n L : ℕ}

Formal statement

theorem IntMul.Kappa.R6.IL2C.slot_add (hK : 1 ≤ K) (hL : ρ + n * K ≤ L) {y : ℕ} (hy : y < 2 ^ L) (δ : ℕ → ℤ)
    (h : ∀ s < n, 0 ≤ (IntMul.Kappa.R6.IL2C.seg K ρ s y : ℤ) + δ s ∧ (IntMul.Kappa.R6.IL2C.seg K ρ s y : ℤ) + δ s < 2 ^ K) :
    ∃ y' : ℕ, (y' : ℤ) = y + ∑ s ∈ range n, δ s * ((2 : ℤ) ^ ρ * (2 ^ K) ^ s) ∧ y' < 2 ^ L ∧
      y' % 2 ^ ρ = y % 2 ^ ρ ∧ (∀ s < n, (IntMul.Kappa.R6.IL2C.seg K ρ s y' : ℤ) = IntMul.Kappa.R6.IL2C.seg K ρ s y + δ s) ∧
      y' / 2 ^ ρ / (2 ^ K) ^ n = y / 2 ^ ρ / (2 ^ K) ^ n := 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 `IntMul.Kappa.R6.IL2C.slot_add`, Solutions/R6IL2CMath.lean (lines 249–290) of the round-six development.

View graph