Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Polynomial Mellin Window

Abstract

An actual finite polynomial arithmetic Mellin window has an integrable complex Fourier kernel and an exact finite endpoint transform.

This source reuses Zeta23.paperFT with kernel exp(izx). For h(t)=sum_{r<d} A_rt^(2r), the arithmetic window is 4exp(x/2)sum_{1<=m<=M, mexp(x)<=exp(a)} h(mexp(x)) on [-a,a], with zero extension. The chosen Ioc endpoints give the same Lebesgue Fourier transform. The finite polynomial is a concrete approximation of the regular prolate modes, whose independent spectral certification is explained in the source analysis.

Definition 1.1 (Fourier-shifted monomial rate).

Formalization. D5/S3/Weil/ZetaBridge/WeilPolynomialMellinWindow.mellinRate (✓ std3).

Source. Repository-derived.

Commentary.

r is natural and z complex; the exponent is 2r+1/2+iz.

Definition 1.2 (One arithmetic monomial).

Formalization. D5/S3/Weil/ZetaBridge/WeilPolynomialMellinWindow.mellinMonomial (✓ std3).

Source. Repository-derived.

Commentary.

The formula uses a real interval and a complex exponential. It is specified before any Fourier evaluation.

Definition 1.3 (Finite polynomial arithmetic synthesis).

Formalization. D5/S3/Weil/ZetaBridge/WeilPolynomialMellinWindow.polynomialMellinWindow (✓ std3).

Source. Repository-derived.

Commentary.

The sums are over m=1,…,M and r=0,…,d-1. The factor four matches the calibrated Xi Mellin normalization in the existing volume.

Theorem 1.4 (Exact polynomial identity).

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/WeilPolynomialMellinWindow.mellin_monomial_polynomial_value (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exponential form equals exp(x/2)(mexp(x))^(2*r) on the actual support. The proof uses exponential addition and natural powers; the half-power is retained.

Theorem 1.5 (Actual Fourier integrability).

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/WeilPolynomialMellinWindow.polynomial_mellin_fourier_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every real a, natural M,d, complex coefficient family A and complex z, the actual Fourier integrand is integrable. Compact interval continuity proves each summand integrable, followed by finite linearity. This excludes totalized nonintegrable Fourier values.

Theorem 1.6 (Quadrature-free Fourier evaluation).

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/WeilPolynomialMellinWindow.polynomial_mellin_window_paperFT (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume log(m)<=2*a for each included positive integer m and Im(z)<1/2. Every rate has positive real part, so no denominator is zero. The proof identifies the Fourier integrand on each arithmetic interval, uses the existing complex-exponential integral theorem, and interchanges only finite sums with proved integrable summands. No quadrature hypothesis or unknown prolate/Weil eigenvector is supplied. The numerical consumer independently certifies prolate eigenpairs and their complete Legendre tail. The all-scale arithmetic ground-model comparison remains open; this source does not prove the prolate spectral theorem, Xi convergence or RH.

References