ExplicitLarge analytic source: ExplicitLarge
Abstract
ExplicitLarge analytic source: ExplicitLarge
Faithful source transplant from google-deepmind/cryptids at immutable revision e5f59ed70d1549a61ef8873a6fbae9268fdbd557, Cryptids/Semantics/Riemann/ExplicitLarge.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 (explicit rhs le seven eighths of five thousand le).
Lean statement: D5/S3/Weil/Mertens/Cryptids/ExplicitLarge.explicit_rhs_le_seven_eighths_of_five_thousand_le
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/Cryptids/ExplicitLarge.explicit_rhs_le_seven_eighths_of_five_thousand_le (✓ 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.