Reproducibility Package for Numerical and Formal Diagnostics of a Compactly Supported Bombieri–Weil Positivity Test

Description This repository contains the source code, numerical data, figures, interactive HTML report, analytic tail estimates, and Coq formalization accompanying the development-stage preprint Numerical and Formal Diagnostics for a Compactly Supported Bombieri–Weil Positivity Test by Oleg Glushkov. The package implements a finite-dimensional numerical diagnostic of the Bombieri–Weil positivity criterion for the Riemann zeta function. The test basis is constructed from smooth compactly supported bump functions in logarithmic coordinates, with independently evaluated Mellin transforms. The included experiments compare the arithmetic side of the explicit formula with partial sums over tabulated nontrivial zeros and investigate the effects of the zero cutoff K, the vertical cutoff T, the arithmetic cutoff X, and the internal quadrature resolution N_u. The numerical package includes two-dimensional (K,T) residual sweeps, dense resolution-scaled sweeps, elementwise matrix comparisons, block analyses of the B_00 zero contribution, analytic polynomial Fourier envelopes for the bump transform, and explicit zero-counting tail estimates. The archive also contains an autonomous interactive HTML certificate report and a Coq 8.18 proof file checking the exact rational arithmetic core of the auxiliary bound used in the analysis. The results are intended for reproducibility and methodological analysis. They do not constitute a proof of the Riemann Hypothesis. In particular, finite positivity matrices evaluated using finitely many supplied zeros do not establish positivity on the full test-function space and do not independently exclude zeros away from the critical line. The Coq artifact verifies the rational arithmetic sub-argument; it does not formalize the complete analytic explicit formula, the published zero-counting theorem, or the Bombieri–Weil equivalence.