WeightedStieltjes analytic source: Integral
Abstract
WeightedStieltjes analytic source: Integral
Faithful source transplant from google-deepmind/cryptids at immutable revision e5f59ed70d1549a61ef8873a6fbae9268fdbd557, Cryptids/Semantics/Riemann/WeightedStieltjes.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 psi1 sub truncated smoothedPerron two le).
Lean statement: D5/S3/Weil/Mertens/Cryptids/WeightedStieltjes/Integral.norm_psi1_sub_truncated_smoothedPerron_two_le
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/Cryptids/WeightedStieltjes/Integral.norm_psi1_sub_truncated_smoothedPerron_two_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.