HorizontalBounds analytic source: Foundation
Abstract
HorizontalBounds analytic source: Foundation
Faithful source transplant from google-deepmind/cryptids at immutable revision e5f59ed70d1549a61ef8873a6fbae9268fdbd557, Cryptids/Semantics/Riemann/HorizontalBounds.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 (norm logDeriv riemannZeta le on Icc of gap).
Lean statement: D5/S3/Weil/Mertens/Cryptids/HorizontalBounds/Foundation.norm_logDeriv_riemannZeta_le_on_Icc_of_gap
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/Cryptids/HorizontalBounds/Foundation.norm_logDeriv_riemannZeta_le_on_Icc_of_gap (✓ 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.