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 321 to 340 of 1,644 declarations.
lemma
Erdos392.Factorization.lower_score_3_case2b
Case 2b of lower_score_3: If L ≤ n and the product of deficit primes is > n,
we can find a submultiset to add that reduces the score.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:798
lemma
Erdos392.Factorization.lower_score_3_clean
The clean case of lower_score_3, combining the three subcases.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:822
theorem
Erdos392.Factorization.lower_score_3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:834
theorem
Erdos392.Factorization.lowest_score
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:866
theorem
Erdos392.Params.initial.card
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:945
lemma
Erdos392.Params.initial.div_le
For elements m in the initial factorization, n/m ≤ (1 - 1/M)⁻¹.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:968
theorem
Erdos392.Params.initial.waste
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:985
theorem
Erdos392.Params.initial.balance_large_prime_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1013
lemma
Erdos392.Params.initial.factorial_factorization_eq_div
For primes p > √n, the p-adic valuation of n! equals ⌊n/p⌋. This follows from
Legendre's formula since p² > n implies all higher power terms vanish.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1034
theorem
Erdos392.Params.initial.balance_large_prime_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1053
lemma
Erdos392.Params.initial.count_multiples_le
The number of multiples of p in [A, B) is at most ⌈(B - A)/p⌉, computed as
(B - A + p - 1) / p.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1089
lemma
Erdos392.Params.initial.sum_valuation_le_M_mul_interval_count
For primes p > √n, the sum of p-adic valuations in the initial factorization is bounded by
M times the count of multiples of p in [n - n/M, n).
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1123
theorem
Erdos392.Params.initial.balance_medium_prime_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1154
lemma
Erdos392.Params.initial.smooth_of_multiple
If √n < p < n/L and p ∣ m with 0 < m < n, then m is (n/L)-smooth.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1177
lemma
Erdos392.Params.initial.valuation_eq_one
For √n < p prime and p ∣ m with 0 < m < n,
we have ν_p(m) = 1 since p² > n ≥ m.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1193
lemma
Erdos392.Params.initial.count_multiples_lower_bound
The interval [n - n/M, n) contains at least ⌊n/M⌋/p multiples of p.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1204
lemma
Erdos392.Params.initial.sum_valuation_eq
For √n < p < n/L, ∑_{a ∈ initial.a} ν_p(a) = M · #{m ∈ [n-n/M, n) : p ∣ m}.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1250
theorem
Erdos392.Params.initial.balance_medium_prime_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1274
lemma
Erdos392.sum_factorization_eq_sum_multiples
The sum of p-adic valuations of numbers in an interval equals the sum over k of the count of
multiples of p^k in that interval.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1295
lemma
Erdos392.Params.initial.term_bound
The contribution of the k-th power of p to the balance is bounded by M.
Specifically, M * count(p^k) ≤ floor(n/p^k) + M.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1317
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.