Separable Rank of Radial Kernels: Machine-Checked Characterization in Lean 4 and Applications

Abstract

Filtering an image or three-dimensional wave field directly with a radially symmetric (round) kernel K(x) = phi(||x||^2) of width W costs W^d multiply-adds per output sample. When a 2-D kernel is a product h(x_0)v(x_1) of a horizontal and a vertical 1-D filter, it can instead be applied as two cheap 1-D passes; the separable rank R is the smallest number of such coordinate-product terms needed to sum to K. On a d-dimensional grid, rank R reduces W^d taps to d R W one-dimensional taps per sample (for example, a 9-tap-wide 3-D stencil drops from 9^3 = 729 taps to 3 x 4 x 9 = 108 taps when R = 4). Single bell-shaped Gaussians exp(-alpha ||x||^2) have rank 1, but cannot form flat-top camera defocus disks or ringed wave stencils, motivating sums of damped radial oscillations exp(-alpha ||x||^2) cos(omega ||x||^2 + theta) (complex-rate Gaussians) and polynomials in ||x||^2 times exponentials (exponential polynomials). We determine which continuous radial kernels on R^d (d >= 2) have finite separable rank and find the exact minimum number of product terms each requires. First, K(x) = phi(||x||^2) has finite rank if and only if phi(s) (s >= 0) is a finite sum of exponential polynomials, whereas decaying complex-rate Gaussians with one shared width and equally spaced frequencies can approximate any continuous radial kernel vanishing at infinity. Second, an alternating angle-sampling identity evaluates each complex-rate Gaussian in d real products (rather than two to the power d - 1 under naive real/imaginary expansion), yielding a constant d - 2 real-over-complex overhead across all polynomial degrees. Third, allowing uniform limits on compact sets (border rank) never lowers rank in 2-D, whereas in 3-D on ||x||^2 cos(||x||^2) over R, general limits, radial multi-Gaussian limits, and exact decompositions strictly separate as 5 < 6 < 7. All 32 mathematical theorems are formally verified in the Lean 4 proof assistant. Analytical operator constructions and illustrative 2-D bokeh and 3-D acoustic wave case studies examine steerable pass bounds, 16-bit channel orthogonalization, GPU crossovers against cuFFT and compact FDTD, and spatially varying media c(x) in Section 6, alongside explicit floating-point stability limits for high polynomial degree, high dimension, and border-rank approximations in Section 7. Code, proofs, and data are public domain (CC0 1.0) at https://github.com/OlliNiemitalo/kernel-rank-lean.

Keywords