Computer-Assisted Proofs of Even-Simplicity for Three Finite Galerkin Weil Forms

We give computer-assisted proofs of finite even-simplicity for three Galerkin matrices associated with the Weil quadratic form used in the Connes–Consani–Moscovici and Connes–van Suijlekom spectral program. For cutoff–dimension pairs (c, N) = (13, 120), (29, 160), (53, 200), we certify that the smallest eigenvalue of the even sector is simple and lies strictly below the smallest eigenvalue of the odd sector. The proof does not compare two extremely small floating-point eigenvalues. Instead, it uses a bordered Schur reduction and a residual lower bound. A proposed scalar ℓ and vector x are treated only as witnesses. An independent verifier, implemented solely with Arb ball arithmetic through python-flint, reconstructs every matrix entry, certifies positive definiteness by interval LDLT factorizations, bounds the largest eigenvalue of a shifted block by Gershgorin’s theorem, and proves a strictly positive residual margin. The certified lower margins are respectively 1.048 × 10⁻⁵⁴, 4.329 × 10⁻¹³⁷, and 1.385 × 10⁻²²², while the corresponding ball radii are hundreds of orders of magnitude smaller. The result concerns exactly these three finite matrices. It does not establish even-simplicity for the continuous operator, uniformity in the cutoff, or the Riemann Hypothesis. The archival record includes the manuscript source and a complete reproducibility package containing the rigorous verifier, all three witness files, complete verifier outputs, full-range consistency logs, environment metadata, licensing information, and a SHA-256 manifest. No private repository is required to audit the certificates.