Off-Line Strong Negative Certificate

Abstract

Every off-line zero yields an admissible shift with a quantitative strong negative certificate.

Theorem 1.1 (Off-line strong negative certificate).

$\forall r h o \in C, \forall d e lt a \in R, \forall g amma \in R, (r h o = \frac{1}{2} + d e lt a + i \cdot g amma \land 0 < d e lt a \land x i R e a d in g (r h o) = 0) \Rightarrow \exists o m e g a \in R, 0 < o m e g a \land o m e g a < d e lt a \land x i R e a d in g (r h o - 2 \cdot o m e g a) \neq = 0 \land d ia g o na l Va l u e (o m e g a, - g amma + i \cdot (d e lt a - o m e g a)) = - \frac{1}{o m e g a \cdot ( d e lt a - o m e g a )} \land d ia g o na l Va l u e (o m e g a, - g amma + i \cdot (d e lt a - o m e g a)) < 0 \land d ia g o na l Va l u e (o m e g a, - g amma + i \cdot (d e lt a - o m e g a)) \leq - \frac{4}{d e lt a ^{2}}$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaCore/OffLineStrongNegativeCertificate.off_line_strong_negative_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The entire shifted xi reading cannot vanish throughout an interval: analytic isolation and the value xiReading zero equals one half produce a positive shift below the off-line displacement where the shifted reading is nonzero.

At that shift, the frozen one-point computation gives the exact negative reciprocal value, strict negativity, and the sharp minus-four-over-delta-squared bound.

References

Truth anchor: D5/S3/Weil/ZetaCore/OffLineStrongNegativeCertificate.off_line_strong_negative_certificate
Dependency: D5/S3/Weil/ZetaCore/OffLinePickWitness

Keyboard shortcuts

trureturing Blueprint

Off-Line Strong Negative Certificate

Abstract

References