q-Newton / q-Vandermonde-type identity behind `T = Γ L Γ⁻¹ U Γ` (`qpascal_identity`)
ProvedJ6QLU.qpascal_identitycomplexity-theoryinteger-multiplicationkappa-improvement
q-Newton / q-Vandermonde-type identity behind T = Γ L Γ⁻¹ U Γ:
∑_{k ≤ u} [u k] (q^(v-k+1);q)_k q^((u-k)(v-k)) = 1 for all u v.
The following holds (Lean statement, in the scope of module Solutions.J6QLUBasic):
theorem J6QLU.qpascal_identity (q : K) : ∀ (u v : ℕ),
∑ k ∈ range (u + 1), qbin q u k * qfall q v k * q ^ ((u - k) * (v - k)) = 1
Context. q-Pochhammer symbols and Gaussian binomials (algebraic core of the segmented-inverse q-LU)
Over an arbitrary field K:
qpoch q n = (q;q)_n = ∏_{i<n} (1 - q^(i+1)),qbin q n k= Gaussian binomial[n k]_q, defined by the q-Pascal recurrence[n+1, k+1] = [n, k] + q^(k+1) [n, k+1],qbin_mul_qpoch:[n k] (q;q)_k (q;q)_{n-k} = (q;q)_n,qbin_rothe(q-binomial theorem / Rothe):∑_{j ≤ h} (-1)^j q^(j choose 2) [h j] y^j = ∏_{i<h} (1 - y q^i),qbin_alt_sum:∑_{j ≤ h} (-1)^j q^(j choose 2) [h j] = δ_{h0},qpascal_identity(q-Newton type identity behind the LU factor):∑_{k ≤ u} [u k] (q^(v-k+1);q)_k q^((u-k)(v-k)) = 1.
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_Defs1
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6QLU
open Finset
variable {K : Type*} [Field K]
Formal statement
theorem J6QLU.qpascal_identity (q : K) : ∀ (u v : ℕ),
∑ k ∈ range (u + 1), qbin q u k * qfall q v k * q ^ ((u - k) * (v - k)) = 1 := by sorrySource
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 `J6QLU.qpascal_identity`, Solutions/J6QLUBasic.lean (lines 158–210) of the round-six development.