Head version
a93551347dce
a93551347dce924b1db75d40218841bf085a465f
- Toolchain
- leanprover/lean4:v4.32.0
- Revision date
- 22 Jul 2026
- Dependencies
- 13
- Versions
- 9
All packages
AlexKontorovich/PrimeNumberTheoremAnd
PrimeNumberTheoremAnd
Blueprint for the PNT+ Project
Therefore indexed 1,644 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.
External build observation
Exact head commit and toolchain
No Reservoir build observation was found for this exact commit and toolchain. This is not evidence of failure.
Pin this source in lakefile.lean
require PrimeNumberTheoremAnd from git "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git" @ "a93551347dce924b1db75d40218841bf085a465f"
Source declarations
1,644 indexed proofs
Showing 621 to 640 of 1,644 declarations.
lemma
Kadiri.riemannZeta_order_pos_nontrivialZero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:90
lemma
Kadiri.zeroes_rect_Ioo_critical_positive_height_finite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:136
lemma
Kadiri.zeroes_rect_positive_height_card_le_zeroes_sum_order
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:149
lemma
Kadiri.positive_height_nontrivial_zero_count_le_NPrime
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:173
lemma
Kadiri.riemannZeta_eventually_ne_zero_punctured_positiveHeightZero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:202
lemma
Kadiri.riemannZeta_order_pos_positiveHeightZero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:229
lemma
Kadiri.riemannZeta_one_sub_ne_zero_of_one_le_re
Shared functional-equation factorization: if 1 ≤ Re w and cos(π w / 2) ≠ 0, then the
reflected value ζ(1 - w) is non-zero. (The factors 2, (2π)^{-w}, Γ(w), ζ(w) are all
non-zero for Re w ≥ 1, so only the cosine factor can vanish.)
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:259
lemma
Kadiri.riemannZeta_ne_zero_of_real_neg
ζ does not vanish on the real segment (-1, 0]. (The non-trivial zeros lie in the
critical strip and the trivial zeros are at -2, -4, …; ζ(0) = -1/2.) Reusable for the left
edge / real point of the eq.(12) rectangle.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:285
lemma
Kadiri.riemannZeta_ne_zero_of_re_nonpos_im_ne_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:307
lemma
Kadiri.positiveHeightZero_re_mem_Ioo
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:325
lemma
Kadiri.zeroes_rect_Ioo_critical_zero_height_finite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:386
lemma
Kadiri.nontrivialZeros_norm_lt_finite
Only finitely many non-trivial zeros lie in a bounded norm ball.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:574
lemma
Kadiri.nontrivialZeros_abs_im_lt_one_finite
Only finitely many non-trivial zeros have height less than one in absolute value.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:587
lemma
Kadiri.nontrivialZeros_abs_im_lt_finite
Only finitely many non-trivial zeros have bounded absolute height.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:601
lemma
Kadiri.nontrivialZeros_dyadic_shell_finite
Every dyadic height shell contains finitely many non-trivial zeros.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:615
lemma
Kadiri.nontrivialZeros_shifted_abs_im_lt_one_finite
Only finitely many non-trivial zeros have shifted height less than one.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:630
lemma
Kadiri.zeroSquareTail_shift_le_four_zero
Away from finitely many small zeros, a shifted square tail is controlled by the zero tail.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:672
theorem
Kadiri.zeroSquareTailSummable_shift_of_zero
Shifted square zero tails follow from the unshifted square zero tail.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:706
lemma
Kadiri.zeroSquareTail_le_imagSquareTail_of_large_im
Above height one, the norm-square tail is bounded by the height-square tail.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:723
theorem
Kadiri.zeroSquareTailSummable_of_imag_tail
The unshifted norm-square zero tail follows from the height-square zero tail.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:736
Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.