Off-Line Nonreal Zero Negative Weil Square

Abstract

An off-line nonreal zero admits a powered even separator whose full Weil-square zero sum has strictly negative real part.

Theorem 1.1 (An off-line nonreal zero yields a negative full Weil-square zero sum).

$$\forall Z\in ZeroData,n\in \mathbb{N},\left(\Re (\mathrm{zero}\left(Z,n\right))\ne criticalAbscissa\wedge \mathrm{Im}(\mathrm{zero}\left(Z,n\right))\ne 0\right)\Rightarrow \left(\exists g\in WeilTestFunction,hZero\in \mathrm{SymmetricConvergent}\left(Z,\mathrm{convolutionSquare}\left(g\right)\right),\Re (\mathrm{zeroSum}\left(Z,\mathrm{convolutionSquare}\left(g\right),hZero\right))<0\right)$$

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

Source. Repository-derived.

Commentary.

Finite even interpolation first prescribes a unit peak and an exception killer. Convolution powering preserves the target values while the frozen closed-strip decay makes the complement geometrically small.

Frozen zeta-zero absolute summability identifies every symmetric zero-sum witness with the ordinary sum. Splitting that sum into the four-point orbit and its complement leaves the prescribed negative orbit larger in magnitude than the tail.

The explicit nonzero imaginary-part hypothesis is the M3-d input. The theorem is conditional on that input and asserts no implication from O-6 to the Riemann hypothesis.

Theorem 1.2 (A unit peak and finite-exception killer exist).

$$\forall Z\in ZeroData,n\in \mathbb{N},\left(\Re (\mathrm{zero}\left(Z,n\right))\ne criticalAbscissa\wedge \mathrm{Im}(\mathrm{zero}\left(Z,n\right))\ne 0\right)\Rightarrow \left(\exists b\in WeilTestFunction,k\in WeilTestFunction,E\in \mathrm{Finset}\left(\mathbb{N}\right),\left(\left(\left(\left(\left(\left(\left(\left(\forall j\in \mathbb{N},j\in E\iff \mathrm{reflection}\left(Z,j\right)\in E\right)\wedge \left(\forall j\in \mathbb{N},j\in E\iff \mathrm{conjugation}\left(Z,j\right)\in E\right)\right)\wedge \mathrm{zeroOrbit}\left(Z,n\right)\subseteq E\right)\wedge \mathrm{fourierLaplace}\left(b,\mathrm{gamma}\left(Z,n\right)\right)=1\right)\wedge \mathrm{fourierLaplace}\left(b,\mathrm{conj}\left(\mathrm{gamma}\left(Z,n\right)\right)\right)=1\right)\wedge \mathrm{fourierLaplace}\left(k,\mathrm{gamma}\left(Z,n\right)\right)=1\right)\wedge \mathrm{fourierLaplace}\left(k,\mathrm{conj}\left(\mathrm{gamma}\left(Z,n\right)\right)\right)=-1\right)\wedge \left(\forall j\in \mathbb{N},\left(\neg j\in E\right)\Rightarrow \left(\Vert \mathrm{fourierLaplace}\left(b,\mathrm{gamma}\left(Z,j\right)\right)\Vert \le \frac{1}{2}\wedge \Vert \mathrm{fourierLaplace}\left(b,\mathrm{conj}\left(\mathrm{gamma}\left(Z,j\right)\right)\right)\Vert \le \frac{1}{2}\right)\right)\right)\wedge \left(\forall j\in \mathbb{N},\left(j\in E\wedge \left(\neg j\in \mathrm{zeroOrbit}\left(Z,n\right)\right)\right)\Rightarrow \left(\mathrm{fourierLaplace}\left(k,\mathrm{gamma}\left(Z,j\right)\right)=0\wedge \mathrm{fourierLaplace}\left(k,\mathrm{conj}\left(\mathrm{gamma}\left(Z,j\right)\right)\right)=0\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The exceptional set is a sufficiently large symmetric spectral ball. Closed-strip decay bounds the peak function outside it, while finite even interpolation makes the killer vanish at every exceptional frequency away from the target orbit and prescribes opposite values on the target conjugate pair.

Theorem 1.3 (The powered complement obeys Burnol’s geometric tail bound).

$$\forall Z\in ZeroData,n\in \mathbb{N},b\in WeilTestFunction,k\in WeilTestFunction,E\in \mathrm{Finset}\left(\mathbb{N}\right),N\in \mathbb{N},\left(\left(\forall i\in \mathbb{N},\left(\neg i\in E\right)\Rightarrow \left(\Vert \mathrm{fourierLaplace}\left(b,\mathrm{gamma}\left(Z,i\right)\right)\Vert \le \frac{1}{2}\wedge \Vert \mathrm{fourierLaplace}\left(b,\mathrm{conj}\left(\mathrm{gamma}\left(Z,i\right)\right)\right)\Vert \le \frac{1}{2}\right)\right)\wedge \left(\forall i\in \mathbb{N},\left(i\in E\wedge \left(\neg i\in \mathrm{zeroOrbit}\left(Z,n\right)\right)\right)\Rightarrow \left(\mathrm{fourierLaplace}\left(k,\mathrm{gamma}\left(Z,i\right)\right)=0\wedge \mathrm{fourierLaplace}\left(k,\mathrm{conj}\left(\mathrm{gamma}\left(Z,i\right)\right)\right)=0\right)\right)\right)\Rightarrow \left(\mathrm{Summable}\left((j:\left\{\neg j\in \mathrm{zeroOrbit}\left(Z,n\right)\mid j\in \mathbb{N}\right\}\mapsto \mathrm{zeroSummand}\left(Z,\mathrm{convolutionSquare}\left(\mathrm{convolve}\left(\mathrm{convolutionSuccPower}\left(b,N\right),k\right)\right),\mathrm{val}\left(j\right)\right))\right)\wedge \Vert \sum _{j\in \left\{\neg j\in \mathrm{zeroOrbit}\left(Z,n\right)\mid j\in \mathbb{N}\right\}}\mathrm{zeroSummand}\left(Z,\mathrm{convolutionSquare}\left(\mathrm{convolve}\left(\mathrm{convolutionSuccPower}\left(b,N\right),k\right)\right),\mathrm{val}\left(j\right)\right)\Vert \le (\frac{1}{4}{)}^{N+1}\cdot \sum _{j\in \mathbb{N}}\Vert \mathrm{zeroSummand}\left(Z,\mathrm{convolutionSquare}\left(k\right),j\right)\Vert \right)$$

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

Source. Repository-derived.

Commentary.

Outside the target orbit, exceptional indices vanish by the killer and all remaining indices acquire a factor at most one quarter at each convolution-power step. Absolute zeta-zero summability supplies the full majorant and permits summation over the subtype complement.

References

• Truth anchor: D5/S3/Weil/ZetaBridge/OffLineNonrealZeroNegativeWeilSquare.burnol_power_tail_bound
• Truth anchor: D5/S3/Weil/ZetaBridge/OffLineNonrealZeroNegativeWeilSquare.exists_peak_and_finite_exception_killer
• Truth anchor: D5/S3/Weil/ZetaBridge/OffLineNonrealZeroNegativeWeilSquare.offLineNonrealZero_yields_negative_weil_square
• Dependency: D5/S3/Fourier/ConvolutionPowerAmplification
• Dependency: D5/S3/Weil/TestFunctions/EvenTestFunctionFiniteInterpolation
• Dependency: D5/S3/Weil/TestFunctions/FourierLaplaceClosedStripDecay
• Dependency: D5/S3/Weil/ZetaBridge/PrescribedPairNegativeOrbit
• Dependency: D5/S3/Weil/ZetaBridge/SymmetricConvergentOfZetaSummable