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 661 to 680 of 1,644 declarations.
theorem
Kadiri.zeroImagDyadicCumulativeCountBoundSource_of_count_by_N_with_zero_height_and_backlund_growth
The additive zero-height bucket is harmless for the dyadic growth source,
because (k+1) * 2^k ≥ 1 for all dyadic shells.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1427
theorem
Kadiri.zeroImagDyadicShellMassBoundSource_of_count_bound
A dyadic shell-count source gives the dyadic mass bound.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1519
theorem
Kadiri.zeroImagSquareTailSummable_of_dyadic_shell_source
Dyadic-shell height summability gives height-square zero-tail summability.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1567
lemma
Kadiri.zeroImagSquareTail_shifted_le_four
Away from finitely many low zeros, a shifted height-square tail is controlled by the unshifted height-square tail.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1674
theorem
Kadiri.summable_zeroImagSquareTail_shifted
The shifted height-square tail is summable once the unshifted height-square tail is.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1702
theorem
Kadiri.zeroImagSquareTailSummable_of_cumulative_count_le
Square-tail summability from any cumulative dyadic count bound whose
4^(-k)-weighted series is summable.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1748
lemma
Kadiri.zetaCountingDyadic_abs_N_le_geometric
The crude counting majorant at dyadic heights, in geometric form:
(2^(k+1))^(3/2) = (2 * sqrt 2)^(k+1) <= 3^(k+1).
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1775
theorem
Kadiri.zeroImagSquareTailSummable_of_crude_majorant
Unconditional height-square zero-tail summability, from the crude majorant.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1803
theorem
Kadiri.riemannZeta_order_conj
The zero order of ζ is conjugation-symmetric away from 1.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1902
theorem
Kadiri.weighted_cumulative_count_le
The weighted cumulative dyadic count against the multiplicity count N:
positive heights land in N's window, negative heights reindex through
conjugation, the real axis lands in the fixed bucket.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:1965
theorem
Kadiri.weighted_zeroImagSquareTail_summable
The order-weighted height-square zero tail is summable, unconditionally.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2222
theorem
Kadiri.weighted_zeroImagSquareTail_shifted_summable
The order-weighted shifted height-square tail is summable for every shift.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:2247
theorem
Lcm.Criterion.prod_p_le_prod_q
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:126
lemma
Lcm.Criterion.p_gt_two
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:141
lemma
Lcm.Criterion.val_two_L'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:184
lemma
Lcm.Criterion.val_p_L'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:216
theorem
Lcm.Criterion.ln_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:269
theorem
Lcm.Criterion.q_not_dvd_L'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:293
theorem
Lcm.Criterion.σnorm_ln_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:351
theorem
Lcm.Criterion.r_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Lcm · PrimeNumberTheoremAnd/IEANTN/Lcm.lean:405
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.