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 301 to 320 of 1,644 declarations.
theorem
Chebyshev.psi_diff_le_weighted
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:296
theorem
Chebyshev.U_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:381
theorem
Chebyshev.psi_num
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:466
theorem
Chebyshev.psi_upper
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:500
theorem
Chebyshev.psi_upper_clean
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:617
theorem
Dusart.proposition_5_4a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Dusart · PrimeNumberTheoremAnd/IEANTN/Dusart.lean:337
theorem
Dusart.proposition_5_4b
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Dusart · PrimeNumberTheoremAnd/IEANTN/Dusart.lean:422
theorem
Erdos392.Factorization.zero_total_imbalance
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:73
theorem
Erdos392.Factorization.waste_eq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:98
lemma
Erdos392.exists_submultiset_prod_between
Given a multiset of numbers ≤ L with product > n, there exists a sub-multiset
whose product m satisfies n / L < m ≤ n.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:357
lemma
Erdos392.factorization_prod_eq_count
The factorization of a product of primes at p equals the count of p in the multiset.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:376
lemma
Erdos392.Factorization.addFactor_deficit_balance_eq_zero
Adding the full deficit multiset product to a factorization with no surplus primes and all
deficit primes at most L results in zero balance for all primes.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:408
lemma
Erdos392.Factorization.lower_score_3_case1
Case 1 of lower_score_3: if the product of deficit primes is ≤ n, adding the full
deficit multiset yields a factorization with zero imbalance and lower score.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:432
lemma
Erdos392.Factorization.addFactor_submultiset_total_imbalance
Adding a submultiset M of deficit primes to a factorization reduces the total imbalance
by M.card.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:479
lemma
Erdos392.Factorization.score_sum_change
The change in the score sum when one deficit prime p (with p ≤ L) has its balance
increased by 1 (still ≤ 0).
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:529
lemma
Erdos392.Factorization.score_sum_change_multiset
The change in the score sum when a submultiset of deficit primes M is added.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:550
lemma
Erdos392.Factorization.score_le_of_add_submultiset
Adding a submultiset M of deficit primes reduces the score if n < M.prod * L.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:598
theorem
Erdos392.Factorization.lower_score_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:649
theorem
Erdos392.Factorization.lower_score_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:668
lemma
Erdos392.Factorization.lower_score_3_case2a
Case 2a of lower_score_3: If L > n and there is a deficit prime, we can add it to reduce
the score.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:752
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.