Cosine-Modulated Packet

Abstract

A normalized convolution-square Weil packet has positive transform near zero, and cosine modulation gives uniform prime control and finite-side decay.

This is the packet half of the zero-infinitude argument of 增订三十. The explicit formula EF_lit holds for every ZeroConfig regardless of carrier cardinality; only the packet, its modulation, and the finite-side limits are proved here.

The prime bound needs neither Chebyshev nor the prime number theorem, because the support of the cosine-modulated packet is fixed. The test functions are this repository’s WeilTestFunction.

No statement about zeta’s zeros beyond the finite-carrier limit is made here. In particular, this document is not a proof of the Riemann hypothesis.

Definition 1.1 (The normalized packet seed).

$$\forall x\in \mathbb{R},\mathrm{packetSeed}\left(x\right)=\mathrm{standardBumpNormed}\left(volume,x\right)$$

Formalization. D5/S3/Weil/ZeroInfinitude/CosinePacket.packetSeed (✓ std3).

Source. Repository-derived.

Commentary.

The value is the repository’s canonical volume-normalized smooth bump.

Theorem 1.2 (The seed is normalized at zero).

$$\mathrm{fourierLaplace}\left(packetSeed,0\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.packetSeed_fourierLaplace_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Its Fourier-Laplace transform at the origin is exactly one.

Definition 1.3 (The convolution-square packet).

$$packetSquare=\mathrm{convolutionSquare}\left(packetSeed\right)$$

Formalization. D5/S3/Weil/ZeroInfinitude/CosinePacket.packetSquare (✓ std3).

Source. Repository-derived.

Commentary.

The positive packet is the repository convolution square of packetSeed.

Theorem 1.4 (The packet transform is real and nonnegative).

$$\forall t\in \mathbb{R},\mathrm{Im}(\mathrm{paperFT}\left(packetSquare,t\right))=0\wedge 0\le \Re (\mathrm{paperFT}\left(packetSquare,t\right))$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_real_nonneg (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the real axis, the imaginary part vanishes and the real part is nonnegative.

Theorem 1.5 (The packet transform equals one at zero).

$$\mathrm{paperFT}\left(packetSquare,0\right)=1$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Convolution-square positivity combines with seed normalization at the origin.

Theorem 1.6 (The packet transform is integrable).

$$\mathrm{Integrable}\left((t:\mathbb{R}\mapsto \mathrm{paperFT}\left(packetSquare,t\right))\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

Two derivatives and compact support give real-axis integrability.

Theorem 1.7 (The packet transform stays above one half near zero).

$$\exists delta\in \mathbb{R},0<delta\wedge \left(\forall t\in \mathbb{R},\left|t\right|\le delta\Rightarrow \frac{1}{2}\le \Re (\mathrm{paperFT}\left(packetSquare,t\right))\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_ge_half_near_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Continuity at the normalized value one supplies a positive neighborhood.

Definition 1.8 (Cosine modulation of a Weil test function).

$$\forall q\in WeilTestFunction,T\in \mathbb{R},x\in \mathbb{R},\mathrm{cosineModulation}\left(q,T,x\right)=\cos \left(T\cdot x\right)\cdot \mathrm{apply}\left(q,x\right)$$

Formalization. D5/S3/Weil/ZeroInfinitude/CosinePacket.cosineModulation (✓ std3).

Source. Repository-derived.

Commentary.

Multiplication by cos(Tx) preserves smoothness, compact support, and evenness.

Theorem 1.9 (Cosine modulation shifts the transform).

$$\forall q\in WeilTestFunction,T\in \mathbb{R},z\in \mathbb{C},\mathrm{paperFT}\left(\mathrm{cosineModulation}\left(q,T\right),z\right)=\frac{\mathrm{paperFT}\left(q,z+T\right)+\mathrm{paperFT}\left(q,z-T\right)}{2}$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two frequency shifts occur with equal coefficient one half.

Theorem 1.10 (The modulated transform decays pointwise on the unit strip).

$$\forall z\in \mathbb{C},\left|\mathrm{Im}(z)\right|\le 1\Rightarrow \mathrm{Tendsto}\left((T:\mathbb{R}\mapsto \mathrm{paperFT}\left(\mathrm{cosineModulation}\left(packetSquare,T\right),z\right)),atTop,\mathrm{nhds}\left(0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation_tendsto_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Closed-strip quadratic decay sends both translated packet transforms to zero.

Theorem 1.11 (The positive pole specialization tends to zero).

$$\mathrm{Tendsto}\left((T:\mathbb{R}\mapsto \mathrm{paperFT}\left(\mathrm{cosineModulation}\left(packetSquare,T\right),\frac{i}{2}\right)),atTop,\mathrm{nhds}\left(0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation_pole_pos_tendsto_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the pointwise strip limit specialized to positive i over two.

Theorem 1.12 (The negative pole specialization tends to zero).

$$\mathrm{Tendsto}\left((T:\mathbb{R}\mapsto \mathrm{paperFT}\left(\mathrm{cosineModulation}\left(packetSquare,T\right),-\frac{i}{2}\right)),atTop,\mathrm{nhds}\left(0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation_pole_neg_tendsto_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the pointwise strip limit specialized to negative i over two.

Theorem 1.13 (The modulated prime term has a uniform bound).

$$\exists B\in \mathbb{R},\forall T\in \mathbb{R},\Vert \sum _{n\in \mathbb{N}}\frac{\mathrm{vonMangoldt}\left(n\right)}{\mathrm{sqrt}\left(n\right)}\cdot \left(\mathrm{cosineModulation}\left(packetSquare,T,\log \left(n\right)\right)+\mathrm{cosineModulation}\left(packetSquare,T,-\log \left(n\right)\right)\right)\Vert \le B$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.primeTerm_cosineModulation_bounded (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fixed compact support reduces the prime series to one finite carrier, while the cosine factor has absolute value at most one.

Theorem 1.14 (Every finite-carrier zero side tends to zero).

$$\forall Z\in ZeroConfig,\mathrm{Finite}\left(\mathrm{carrier}\left(Z\right)\right)\Rightarrow \mathrm{Tendsto}\left((T:\mathbb{R}\mapsto \sum _{rho\in \mathrm{carrier}\left(Z\right)}\mathrm{mult}\left(Z,rho\right)\cdot \mathrm{paperFT}\left(\mathrm{cosineModulation}\left(packetSquare,T\right),\mathrm{gammaOf}\left(rho\right)\right)),atTop,\mathrm{nhds}\left(0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZeroInfinitude/CosinePacket.finiteCarrier_zeroSide_tendsto_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Pointwise strip decay passes through the finite multiplicity-weighted sum.

References

• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.cosineModulation
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.finiteCarrier_zeroSide_tendsto_zero
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.packetSeed
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.packetSeed_fourierLaplace_zero
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.packetSquare
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_ge_half_near_zero
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_integrable
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_real_nonneg
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.packetTransform_zero
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation_pole_neg_tendsto_zero
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation_pole_pos_tendsto_zero
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.paperFT_cosineModulation_tendsto_zero
• Truth anchor: D5/S3/Weil/ZeroInfinitude/CosinePacket.primeTerm_cosineModulation_bounded
• Dependency: D5/S3/Weil/TestFunctions/ConvolutionSquarePositivity
• Dependency: D5/S3/Weil/TestFunctions/FourierLaplaceClosedStripDecay