The critical polynomial of a uniform-grid variance-deficit objective: one sign change for 3 ≤ T ≤ 300, and a closed form at x=1

Abstract

For an integer step count T ≥ 1 put b₀(x)=T, bⱼ(x)=jx+(T-j) for 1 ≤ j ≤ T, and H_T(x) = T²xΣᵢ₌₁^(T)frac(1)i bᵢ(x) bᵢ₋₁(x)²,qquad x>0. This is the finite-step variance deficit of a Schrödinger-bridge sampler on the uniform grid, in the form derived by Fallah and Yang, who prove that H_T has a unique positive critical point for 2 ≤ T ≤ 120 by exhibiting an integer polynomial with exactly one sign change in its nonzero coefficient sequence, report a numerical scan finding one local minimum for T ≤ 200 and for T ∈ {500,1000,5000}, and leave the general case open, reducing it to the conjecture that the coefficient sequence has one sign change for every T. Their polynomial is not printed, and the sign-variation count is a property of the polynomial chosen and not of the critical set, so we construct one: an explicit R_T ∈ ℤ[x], of degree 3T-3 for T ≥ 2, given by a quadratic-time integer recurrence, for which we prove — for every T ≥ 1 and every x>0, with no restriction on T — that H_T'(x)=0 if and only if R_T(x)=0. We then prove that the nonzero coefficient sequence of R_T has exactly one sign change for every 3 ≤ T ≤ 300; that R_T consequently has exactly one positive real root there; and that H_T has exactly one positive critical point for 3 ≤ T ≤ 300, which is the source's uniqueness statement on 2.5 times its proved range and 1.5 times its numerical scan. Two further results are uniform in T and involve no computation: H_T'(1)=((T+2)h_T-3T)/T² for every T ≥ 1, where h_T is the T-th harmonic number, and H_T'(1)>0 for every T ≥ 3, so that T=2 — where R₂=16X²(X-1) and the critical point is exactly x=1 — is the only step count T ≥ 2 at which x=1 is critical. The band results rest on a single exhaustive computation in exact integer arithmetic over the 298 step counts T=3,…,300, whose largest instance has degree 897 and coefficients of up to 9436 bits. Every theorem, proposition and lemma below is machine-checked in Lean 4; Section [sec:verif] records exactly what the kernel checks, and which of the remaining statements are computations outside the formal development.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-09-07 03:53 UTC

   File fingerprint

   ee18284748331c7ea111399f3cebfcaab1b8d29d7c2463b2a8b5222417db8cee