Kronecker unpacking inverts packing for balanced digits

Proved

IntMul.HvdH.kunpack_kpack

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

integer-multiplication

Let $B>0$ be even and let $c=(c_0,\dots,c_{n-1})$ be integers with $2|c_i|<B$ . Then reading $n$ balanced base- $B$ digits from $\sum_ic_iB^i$ recovers $c$ :

\mathrm{kunpack}_B\bigl(n,\textstyle\sum_i c_iB^i\bigr)=c.

This is the unpacking step (3) of Lemma 2.5 of Harvey–van der Hoeven (see IntMul_HvdH_KronMul).

Preamble

import Definitions.Def_IntMul_HvdH_KronMul

Formal statement

namespace IntMul.HvdH
theorem kunpack_kpack (B : ℤ) (hB : 0 < B) (hBe : Even B) (c : List ℤ)
    (hc : ∀ x ∈ c, 2 * |x| < B) : kunpack B c.length (kpack B c) = c := by sorry
end IntMul.HvdH

Source

Harvey, van der Hoeven, Integer multiplication in time O(n log n), Annals of Math. 193 (2021), https://hal.science/hal-02070778, Lemma 2.5 (Kronecker substitution)

View graph