Backlund Horizontal Bound

Abstract

The horizontal argument variation and vertical line are logarithmically controlled.

Theorem 1.1 (Backlund Horizontal Bound).

Lean statement: D5/S3/Weil/ZetaRvm/Backlund.backlund_horizontal

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaRvm/Backlund.backlund_horizontal (✓ std3). ∎

Source. Repository-derived.

Commentary.

The horizontal argument variation and vertical line are logarithmically controlled.

References

• Truth anchor: D5/S3/Weil/ZetaRvm/Backlund.backlund_horizontal
• Dependency: D5/S3/Weil/ZetaRvm/BacklundDefs
• Dependency: D5/S3/Weil/ZetaRvm/ReZeroCount