Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Even Fourier Observation Tail

Abstract

The full even Fourier tail admits an absolutely convergent complex-frequency response with cubic squared cutoff decay. The estimate controls the observable needed by the Weil-to-Xi route.

The actual window is [-L/2,L/2]. For n>0 use the existing phase-adjusted cosine basis (-1)^nsqrt(2/L)cos(2pinx/L), zero extended outside that interval, with Fourier kernel exp(iz*x). The coefficient sequence v_j refers to n=N+j+1. The Fourier identification is a paper bridge in the existing RH source analysis.

Definition 1.1 (The complete exterior response).

Formalization. D5/S3/Weil/ZetaBridge/WeilEvenFourierObservationTail.evenExteriorResponse (✓ std3).

Source. Repository-derived.

Commentary.

Write w=zL/(2pi) and n_j=N+j+1. The response is [-Lsqrt(2L)/(2pi^2)]zsin(Lz/2) sum_j v_j/(n_j^2-w^2). This is an infinite coefficient series, not an upper-truncated matrix. The theorem uses only L>0, N>0 and Lnorm(z)<=pi*N, which exclude every denominator zero. No identity at a totalized removable pole is claimed.

Theorem 1.2 (Absolute convergence and cubic squared tail bound).

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

Source. Repository-derived.

Commentary.

The norm restriction gives norm(n_j^2-w^2)>=3n_j^2/4. A positive telescoping identity proves sum_{n>N} n^(-4)<=1/(3N^3), including convergence. Young’s inequality gives absolute summability of the coefficient products. Finite Cauchy-Schwarz followed by the sum limit gives the full infinite-series estimate. The physical Fourier factor is retained exactly.

For norm(z)<=R and abs(Im(z))<=b the paper consequence is norm(response)<=sqrt(8/(27*pi^4))L^(3/2)Rexp(bL/2) *N^(-3/2)norm(v). This applies to an arbitrary even L2 tail after the same-source Fourier/Parseval identification. If its arithmetic energy dominates betanorm(v)^2, the squared observation budget is divided by beta.

The existing source analysis applies this estimate to the explicit, suitably normalized prolate model of Connes-Consani-Moscovici. It constructs an evenized, finite dyadic candidate family with the same Xi limit. That model-limit proof, the factor-four Mellin normalization calculation, and the observable Schur energy certificate are paper results. None is silently asserted by this Lean theorem. The fixed 129-entry numerical candidate has not been identified with that new family. No unbounded-scale ground approximation or RH conclusion is claimed. Lean and Scribe compilation were not run in this session.

Theorem 1.3 (The consumed exact inverse-fourth partial tail).

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

Source. Repository-derived.

Commentary.

SOURCE_ONLY_UNCOMPILED. For every natural N>0 and every natural k, including k=0, sum_{j<k} 1/(N+j+1)^4<=1/(3N^3)-1/(3(N+k)^3). This minimally exposes the already present private fourth_partial proof, leaving all original definitions and proof bodies intact. It is reuse, not a novelty claim. Its live consumer is ActualColumnRemainder.paired_first_jet_remainder_tail and thereby the full paired actual column. All compiler, axiom, Reg source reconstruction/enrollment, Scribe and CI checks remain pending.

References