q-LU factorization of the Gaussian Toeplitz matrix

Let $K$ be a field, $x, z \in K$ with $z \ne 0$, $q = x^2$, and $n \in \mathbb N$ with $(q;q)_i \ne 0$ for all $i < n$. Let $T =$ gaussToep x z n be the $n \times n$ Gaussian Toeplitz matrix with entries $x^{(i-j)^2} z^{i-j}$, let $\Gamma =$ Gam q n be the diagonal matrix of the q-Pochhammer weights and $L(c)$, $U(c)$ the lower/upper triangular Toeplitz matrices of a sequence $c$. With $b^{+}_h = x^{h^2} z^h/(q;q)_h$ and $b^{-}_h = x^{h^2} z^{-h}/(q;q)_h$,

This explicit LU decomposition is the algebraic core of the segmented Gaussian inverse in the round-six stack.

In Lean:

theorem J6QLU.qLU (x z : K) (n : ℕ) (hz : z ≠ 0) (hq : ∀ i < n, qpoch (x ^ 2) i ≠ 0) :
    gaussToep x z n =
      Gam (x ^ 2) n * lowT (bP x z⁻¹) * GamInv (x ^ 2) n * upT (bP x z) * Gam (x ^ 2) n

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*).