VonMangoldtCount analytic source: Integral
Abstract
VonMangoldtCount analytic source: Integral
Faithful source transplant from google-deepmind/cryptids at immutable revision e5f59ed70d1549a61ef8873a6fbae9268fdbd557, Cryptids/Semantics/Riemann/VonMangoldtCount.lean. Copyright 2026 Google LLC, Apache-2.0; the full license is docs/reports/licenses/cryptids-LICENSE.txt. Only routing and current-pin API adaptations are local. The original declaration namespace and proof ownership are preserved. This is reuse of the upstream proof, not a claim of new mathematical content. Retire this transplant when an equivalent RH-only real-variable psi estimate above 5000 is present at this repository own Mathlib revision in lake-manifest.json; directly reference that supplier and remove its unused transplanted closure.
Theorem 1.1 (nontrivialZetaZerosUpTo subset biUnion fourWindows).
Lean statement: D5/S3/Weil/Mertens/Cryptids/VonMangoldtCount/Integral.nontrivialZetaZerosUpTo_subset_biUnion_fourWindows
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/Cryptids/VonMangoldtCount/Integral.nontrivialZetaZerosUpTo_subset_biUnion_fourWindows (✓ std3). ∎
Citation. Google LLC (Google DeepMind) (2026). Cryptids — formal RH Chebyshev psi estimate and analytic source closure. URL: https://github.com/google-deepmind/cryptids/blob/e5f59ed70d1549a61ef8873a6fbae9268fdbd557/Cryptids/Semantics/Riemann/Analytic.lean.
Commentary.
The exact statement and hypotheses are those of the original declaration, checked on the current project pins.