Off-Line One-Point Witness

Abstract

The shifted finite-difference observer has a quantitative negative one-point witness at an off-line zero.

Theorem 1.1 (Off-line one-point witness).

$\forall r h o \in C, \forall d e lt a \in R, \forall g amma \in R, \forall o m e g a \in R, (r h o = \frac{1}{2} + d e lt a + i \cdot g amma \land 0 < d e lt a \land 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) = 0 \land x i R e a d in g (r h o - 2 \cdot o m e g a) \neq = 0) \Rightarrow 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/OffLinePickWitness.off_line_one_point_pick_witness (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a zero represented as one half plus a positive real displacement and an imaginary ordinate, and for a positive shift smaller than that displacement, the finite-difference observer evaluates to a negative diagonal value. The value is exactly minus the reciprocal product of the shift and the remaining displacement, and is bounded above by minus four over the squared displacement. The nonvanishing shifted evaluation is the source condition that keeps the observer defined.

References

Truth anchor: D5/S3/Weil/ZetaCore/OffLinePickWitness.off_line_one_point_pick_witness
Dependency: D5/S3/Zeros/CompletedZeta

Keyboard shortcuts

trureturing Blueprint

Off-Line One-Point Witness

Abstract

References