A log-concavity criterion for finite nonnegative linearization
Leslie P. Polzer
math.CA
Nov 1, 2026 · v1
math.CO
TL;DR
All theorems, corollaries, propositions and key lemmas are formalized in Lean 4 with Mathlib in companion code, and exact counterexample computations are machine-verified.
Abstract
In a 2005 survey, R. Szwarc asked for criteria, stated in the recurrence coefficients, for nonnegative linearization (property (P)) of finite orthogonal polynomial systems such as the Krawtchouk polynomials. For a finite three-term recurrence normalized to have row sums one, whose diagonal and downward coefficients have a constant nonnegative ratio, we prove that property (P) holds for every product, including products beyond the terminal degree, whenever the Newton coefficients of the profile $d_i=b_i+c_i$ are log-concave without internal zeros. The criterion contains the full positive Krawtchouk range and the dual $q$-Krawtchouk arrays, and through a quadratic decomposition of symmetric finite systems it covers Szwarc's quadratic system $Q_n$ in its sharp range $0<p_0\leq1/2$. As a limit to any such criterion, property (P) fails at coefficient distance $O((1-r^2)^N)$ from the Krawtchouk array of size $N$ with fixed ratio $c_i/d_i=r<1$. All theorems, corollaries and propositions are formalized in Lean 4.
Problem
Szwarc asked for criteria, stated in the recurrence coefficients, for nonnegative linearization (property (P)) of finite orthogonal polynomial systems such as the Krawtchouk polynomials. He also asked for a criterion covering his symmetric quadratic system Q_n.
Approach
The setting is normalized finite three-term recurrences with a constant ratio between the diagonal and downward coefficients. Property (P) is proved for all products, including degree sums beyond N, whenever the Newton coefficients of the profile d_i=b_i+c_i are log-concave without internal zeros. A quadratic decomposition of symmetric finite systems reduces Szwarc's Q_n to this criterion. All results are formalized in Lean 4 with Mathlib; an axiom audit admits only the standard axioms, and some Lean proofs take routes through a companion development.
Results
The criterion covers the full positive Krawtchouk range, the dual q-Krawtchouk arrays, and Q_n in its sharp range 0<p_0≤1/2. Property (P) fails at coefficient distance O((1-r^2)^N) from the Krawtchouk arrays, and Lean-verified exact computations give counterexamples for seven parameter combinations.
