Zero-Count Window Arithmetic

Abstract

Multiplicity-weighted zero counts are additive across adjacent windows.

Theorem 1.1 (Zero-Count Window Arithmetic).

Lean statement: D5/S3/Weil/ZetaRvm/NcountWindow.Ncount_add

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

Source. Repository-derived.

Commentary.

Multiplicity-weighted zero counts are additive across adjacent windows.