Backlund Definitions

Abstract

The real-part zero set used in Backlund’s bound is fixed.

Theorem 1.1 (Backlund Definitions).

Lean statement: D5/S3/Weil/ZetaRvm/BacklundDefs.mem_reZeroSet

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

Source. Repository-derived.

Commentary.

The real-part zero set used in Backlund’s bound is fixed.